Fixed unification bug where gvar_fixed reversed winding

app/Tui/Interaction.hs

@@ -120,4 +120,4 @@ pImport = do
 
 pModifier :: TParser ImportModifier
 pModifier = 
-  const ImWildcard <$> (lexeme (C.char '.') *> symbol "(..)")
+  const ImWildcard <$> (lexeme (C.char '.') *> symbol "(…)")

app/Tui/Unicode.hs

@@ -106,12 +106,7 @@ unicode_input_map =
   , ("rr", 'ᛯ')
   , ("ri", 'ᛣ')
   , ("\\", '﹨')
-
-  -- arraos
-  , ("to", '→')
-  , ("fm", '←')
-  , ("up", '↑')
-  , ("dn", '↓')
+  , ("...", '…') 
 
   -- Subscripts
   , ("_0", '₀')

src/Sigil/Abstract/Names.hs

@@ -17,6 +17,7 @@ module Sigil.Abstract.Names
   , freshen
   , Gen
   , run_gen
+  , run_gen_from
   ) where
 
 
@@ -143,6 +144,9 @@ instance MonadGen m => MonadGen (ReaderT e m) where
 run_gen :: Gen a -> a
 run_gen = fst . flip runState 0 . ungen
 
+run_gen_from :: Integer -> Gen a -> a
+run_gen_from n = fst . flip runState n . ungen
+
 fresh_var :: MonadGen m => Text -> m Name
 fresh_var s = fresh_id >>= pure . Name . Right . (, s)
 

src/Sigil/Abstract/Substitution.hs

@@ -16,6 +16,7 @@ module Sigil.Abstract.Substitution
 {- 1. Regular, unnormalizing substitution.                                     -}
 {- 2. Typed, hereditary substitution.                                          -}
 {-                                                                             -}
+{- TODO: add foldrWithKey, remove Substition ctor export                       -}
 {-------------------------------------------------------------------------------}
 
 
@@ -31,6 +32,7 @@ import Prettyprinter
 
 import Sigil.Abstract.Syntax
 import Sigil.Abstract.Names
+import Sigil.Abstract.AlphaEq
 
 
 newtype Substitution n a = Substitution (Map n a)
@@ -39,6 +41,12 @@ newtype Substitution n a = Substitution (Map n a)
 instance (Pretty n, Pretty a) => Pretty (Substitution n a) where
   pretty (Substitution subst) = vsep $ fmap (\(n,a) -> pretty n <+> "↦" <+> pretty a) $ Map.toList subst
 
+instance (AlphaEq n a, Ord n) => AlphaEq n (Substitution n a) where
+  αequal rename (Substitution l) (Substitution r) =
+    (length l == length r) &&
+    Map.foldrWithKey (\k v t -> t && maybe False (αequal rename v) (Map.lookup k r)) True l
+
+
 class Subst n s a | a -> s n where
   substitute :: Set n -> Substitution n s -> a -> a
   free_vars :: a -> Set n

src/Sigil/Abstract/Syntax.hs

@@ -407,7 +407,7 @@ pretty_mod_builder pretty_entry m =
 
 instance Pretty ImportDef where
   pretty (Im (path, mod)) = pretty path <> case mod of
-    ImWildcard -> ".(..)"
+    ImWildcard -> ".(…)"
     ImSingleton -> ""
     ImAlias fm to -> "" <+> pretty fm <+> "→" <+> pretty to
     ImExcept set -> " \\" <+> (sep . fmap pretty . toList $ set)

src/Sigil/Interpret/Unify.hs

@@ -582,11 +582,15 @@ unify_eq quant_vars a b = case (a, b) of
 
     -- GVar-Fixed
     -----------------
+    -- Recall, formula has form:
+    --     … ∃x: (u₁:A₁ → … → uₙ:Aₙ → A) … ∀y₁:B₁…yₙ:Bₙ .
+    --         x yϕ(1) … yϕ(n) ≗ M
+    --
     -- While not a specific rule in itself, Gvar-fixed is useful as helper when
     -- M has the form c M₁ … Mₙ for a fixed c, (constant/universally quantified)
     -- c : (v₁:B₁) → … (vₘ:Bₘ) → B.
     -- here, we perform an imitation: let 
-    --   L = λ [u₁:A₁ … uₙ:Aₙ] (c (x₁ u₁ … uₙ) … (xₘ u₁ … uₙ))
+    --   L = λ [u₁:A₁ … uₙ:Aₙ] (c (x₁ u₁ … uₙ) … (xₘ u₁ … uₙ))   x ↦ :succ @xm  :succ :zero
     -- Then, we transition to
     --   ∃x₁: (u₁:A₁) → (uₙ:Aₙ) → B₁ ...
     --     ∃xₘ: (u₁:A₁) → (uₙ:Aₙ) → [(xₘ₋₁ u₁ … uₙ/v₁) … (x₁ u₁ … uₙ/vₘ)] Bₘ ...
@@ -603,12 +607,12 @@ unify_eq quant_vars a b = case (a, b) of
       -- the vector of bindings x₁: (∪_1:A₁) → … (uₙ:Aₙ) → B, …,
       --   xₘ (∪_1:A₁) → … (uₙ:Aₙ) → [(xₘ₋₁ u₁ … uₙ/v₁) … (x₁ u₁ … uₙ/vₘ)]B
       xₘₛ <- forM bₘₛ $ \_ -> do
-        x <- fresh_var "@xm"
+        x <- fresh_varn "@xm-"
         pure $ (x, wind (AVar x, map (Var . aname) aₙₛ))
 
       let to_l_term term = case term of
               Prd Regular bind body -> Abs Regular bind $ to_l_term body
-              _ -> foldr app (action $ fmap aname aₙₛ) $ map snd xₘₛ
+              _ -> foldl app (action $ fmap aname aₙₛ) $ map snd xₘₛ
           -- The term L, which we will substitute for x
           l = to_l_term ty
 
@@ -891,7 +895,7 @@ get_elem :: (MonadError err m, ?lift_err :: Doc ann -> err) =>
   Atom' -> Binds' -> m (Either FBind' InternalCore)
 get_elem atom qvars = case atom of
   AVar n -> Left <$> n ! qvars 
-  AUni n -> pure $ Right (Uni (n+1))  -- TODO: possibly no + 1?
+  AUni n -> pure $ Right (Uni (n+1))
   AInd _ k _ -> pure $ Right k
   ACtr label ty -> case ty of
     Ind nm _ ctors -> case List.find ((== label) . view _1) ctors of 
@@ -900,16 +904,18 @@ get_elem atom qvars = case atom of
     _ -> throw "constructor should have inductive type"
 
 unwind :: InternalCore -> Maybe (Atom', [InternalCore])        
-unwind core = case core of 
-  App l r -> (_2 %~ (r :)) <$> (unwind l)
-  Var n -> Just (AVar n, [])
-  Uni n -> Just (AUni n, [])
-  Ctr label ty -> Just (ACtr label ty, [])
-  Ind nm kind ctors -> Just (AInd nm kind ctors, [])
-  _ -> Nothing
+unwind core = fmap (_2 %~ reverse) (go core)
+  where 
+    go = \case
+      App l r -> (_2 %~ (r :)) <$> (unwind l)
+      Var n -> Just (AVar n, [])
+      Uni n -> Just (AUni n, [])
+      Ctr label ty -> Just (ACtr label ty, [])
+      Ind nm kind ctors -> Just (AInd nm kind ctors, [])
+      _ -> Nothing
 
 wind :: (Atom', [InternalCore]) -> InternalCore
-wind (a, vars) = foldr App (unatom a) vars  
+wind (a, vars) = foldl App (unatom a) vars
 
 -- telescope :: Core b n χ -> ([b n (Core b n χ)], Core b n χ)
 -- telescope term = case term of

test/Spec/Sigil/Interpret/Unify.hs

@@ -1,5 +1,6 @@
 module Spec.Sigil.Interpret.Unify (unify_spec) where
 
+import Prelude hiding (lookup)
 import Control.Monad.Except
 import Data.Text (Text)
 
@@ -8,6 +9,8 @@ import Prettyprinter.Render.Sigil
 
 import Sigil.Abstract.Unify
 import Sigil.Abstract.Names
+import Sigil.Abstract.AlphaEq
+import Sigil.Abstract.Substitution
 import Sigil.Concrete.Internal
 import Sigil.Concrete.Decorations.Implicit
 import Sigil.Interpret.Unify
@@ -20,8 +23,8 @@ unify_spec = TestGroup "unify" $ Right unify_tests
 
 type UnifyM a = ExceptT (Doc SigilStyle) Gen a
 
-runUnifyM :: UnifyM a -> Either (Doc SigilStyle) a
-runUnifyM = run_gen . runExceptT
+runUnifyM :: Integer -> UnifyM a -> Either (Doc SigilStyle) a
+runUnifyM n = run_gen_from n . runExceptT
 
 unify_tests :: [Test]     
 unify_tests = 
@@ -75,46 +78,50 @@ unify_tests =
                             Conj [idv 0 "x" :≗: ([(idn 1 "A", 𝓊 0)] ⇒ idv 1 "A")]) True
 
 
-  -- This test fails!
-  -- Trace
-  -- does it fail for 
-  -- [(n ≃ :succ :zero)]
-  -- [(:succ ≃ :succ :zero)]
+  -- ∃ x ⮜ ℕ. x ≃ one
   , let nat = Ind (idn 1 "N") (𝓊 0) [("zero", idv 1 "N"), ("succ", [(idn 2 "_", idv 1 "N")] → idv 1 "N")]
-    in can_solve_test "ex-one"
-        (Bind Exists (idn 0 "x") nat $ Conj [idv 0 "x" :≗: (Ctr "succ" nat ⋅ Ctr "zero" nat)])
-        True
-
+    in solve_test "ex-one"
+        (Bind Exists (idn 0 "x") nat $ Conj [idv 0 "x" :≗: (Ctr "succ" nat ⋅ (Ctr "succ" nat ⋅ Ctr "zero" nat))])
+        [(idn 0 "x", (Ctr "succ" nat ⋅ (Ctr "succ" nat ⋅ Ctr "zero" nat)))]
+
+  -- ∃ x ⮜ ℕ. two + x ≅ four
+  -- , let nat = Ind (idn 1 "N") (𝓊 0) [("zero", idv 1 "N"), ("succ", [(idn 2 "_", idv 1 "N")] → idv 1 "N")]
+  --   in solve_test "ex-add"
+  --       (Bind Exists (idn 0 "n") nat $ Conj [idv 0 "n" :∈: nat])
+  --       (idn 0 "n" ↦ Ctr "zero" nat)
   -- TODO: add test testing this:
-  -- ∃ x ⮜ ℕ. two + x ≃ four
+  -- ∃ x ⮜ ℕ. two + x ≅ four
 
 
   ]
 
   where 
     eq_test :: Text -> InternalCore -> InternalCore -> Bool -> Test
     eq_test name l r b = 
-      Test name $ case runUnifyM $ solve id (Conj [l :≗: r]) of 
+      Test name $ case runUnifyM 10 $ solve id (Conj [l :≗: r]) of 
         Right _ | b == True -> Nothing
                 | otherwise -> Just "unify-eq succeded when expecting fail"
         Left e  | b == False -> Nothing
                 | otherwise -> Just $ "unify failed - message:" <+> e
 
     can_solve_test :: Text -> Formula Name InternalCore -> Bool -> Test
     can_solve_test name formula b =
-      Test name $ case runUnifyM $ solve id formula of 
+      Test name $ case runUnifyM 10 $ solve id formula of 
         Right _ | b == True -> Nothing
                 | otherwise -> Just "unify-eq succeded when expecting fail"
         Left e  | b == False -> Nothing
                 | otherwise -> Just $ "unify failed - message:" <+> e
 
-    -- solve_test :: Text -> Formula (Core AnnBind Name UD) -> Substitution (Core AnnBind Name UD) -> Test
-    -- solve_test name formula sub =
-    --   Test name $ case runUnifyM $ solve formula of 
-    --     Right s
-    --       | s == sub  -> Nothing
-    --       | otherwise -> Just $ "incorrect substitution produced:" <+> pretty s <+> "expecting" <+> pretty sub
-    --     Left e -> Just $ "solve failed - message:" <+> e
+    solve_test :: Text -> Formula Name InternalCore -> [(Name, InternalCore)] -> Test
+    solve_test name formula sub =
+      Test name $ case runUnifyM 10 $ solve id formula of 
+        Right s
+          | s `has` sub -> Nothing
+          | otherwise -> Just $ vsep ["Incorrect substitution.", "Got:" <+> pretty s, "Expecting it to have:" <+> pretty sub]
+        Left e -> Just $ "solve failed - message:" <+> e
+
+    has :: Substitution Name InternalCore -> [(Name, InternalCore)] -> Bool 
+    has s sub = foldr (\(k, v) t -> t && maybe True (αeq v) (lookup k s)) True sub 
 
 
 -- var :: n -> Core b n UD