Added alpha equality to constructors

src/Sigil/Abstract/AlphaEq.hs

@@ -13,6 +13,7 @@ module Sigil.Abstract.AlphaEq
 import Control.Lens
 import qualified Data.Map as Map
 import Data.Map (Map)
+import Data.Functor.Classes (Eq1(..))
 import Data.Foldable (foldl')
 
 import Sigil.Abstract.Syntax
@@ -54,7 +55,7 @@ instance (Ord n, Binding b, AlphaEq n (Core b n χ), AlphaEq n (b n (Core b n χ
         rename' = ( maybe (fst rename) (\n -> Map.insert n (name b') (fst rename)) (name b)
                   , maybe (snd rename) (\n -> Map.insert n (name b) (snd rename)) (name b'))
 
-instance (Ord n, Binding b, Traversable (Functorχ χ), Applicative (Functorχ χ), AlphaEq n (b n (Core b n χ)), AlphaEq n (Coreχ b n χ)) => AlphaEq n (Core b n χ) where
+instance (Ord n, Binding b, Eq1 (Functorχ χ), Applicative (Functorχ χ), AlphaEq n (b n (Core b n χ)), AlphaEq n (Coreχ b n χ)) => AlphaEq n (Core b n χ) where
   αequal rename v v' = case (v, v') of 
     (Coreχ r, Coreχ r') ->
       αequal rename r r'
@@ -82,8 +83,10 @@ instance (Ord n, Binding b, Traversable (Functorχ χ), Applicative (Functorχ 
     (Dapχ _ tel val, Dapχ _ tel' val') ->
       let (tel_eq, rename') = αequal_tel rename tel tel'
       in tel_eq && αequal rename' val val'
+    (Ctrχ _ label ty, Ctrχ _ label' ty') -> label == label' && liftEq (αequal rename) ty ty'
     (Indχ _ name fsort ctors, Indχ _ name' fsort' ctors') ->
-      foldl' (&&) True ((αequal rename) <$> fsort <*> fsort') && foldl' (&&) True (zipWith (\(_, v) (_, v') -> αequal rename' v v') ctors ctors')
+      liftEq (αequal rename) fsort fsort'
+      && foldl' (&&) True (zipWith (\(_, v) (_, v') -> αequal rename' v v') ctors ctors')
       where 
         rename' = ( Map.insert name (Just name') (fst rename)
                   , Map.insert name' (Just name) (snd rename))
@@ -119,7 +122,7 @@ instance (Ord n, Binding b, AlphaEq n (Core b n χ)) => AlphaEq n (b n (Core b n
     (Nothing, Nothing) -> True
     _ -> False
 
-instance (Ord n, Binding b, Traversable (Functorχ χ), Applicative (Functorχ χ),
+instance (Ord n, Binding b, Eq1 (Functorχ χ), Applicative (Functorχ χ),
           AlphaEq n (b n (Core b n χ)), AlphaEq n (Coreχ b n χ))
     => AlphaEq n (Module b n χ) where
   αequal rename m m' = 

src/Sigil/Analysis/FormulaCheck.hs

@@ -44,7 +44,7 @@ check_scons interp@(CheckInterp {..}) env cons = case cons of
     ty_norm <- normalize (lift_err . flip NormErr mempty) env kind ty'
     val' <- check interp env val ty_norm
     val_norm <- normalize (lift_err . flip NormErr mempty) env ty_norm val'
-    pure $ (val_norm :≗: ty_norm)
+    pure $ (val_norm :∈: ty_norm)
 
 
 check_eq :: (MonadError err m, Pretty a) => Range -> (CheckInterp m err e a) -> e (Maybe a, a) -> a -> a -> a -> m ()

src/Sigil/Concrete/Internal.hs

@@ -141,7 +141,7 @@ instance Pretty InternalCore where
       , indent 2 (align (vsep (map (\(l,ty) -> pretty l <+> "⮜" <+> pretty ty) ctors)))
       ]
 
-    Ctr label _  -> ":" <> pretty label 
+    Ctr label _  -> ":" <> pretty label
 
     Rec recur val cases -> vsep
       [ "φ" <+> pretty_annbind Regular True recur <> "," <+> pretty val <> "."

src/Sigil/Interpret/Unify.hs

@@ -108,9 +108,6 @@ import Sigil.Concrete.Decorations.Implicit
 {-------------------------------------------------------------------------------}
 
 
--- type Unify ann v = ReaderT (Env v) (Except (Doc ann))
-
--- Bindings: a value is either bound within a formula (and hence quantified)
 type Binds a = [(FBind a)]
 
 type ContT a m c = ((c -> m a) -> m a)

test/Spec/Sigil/Abstract/AlphaEq.hs

@@ -32,6 +32,11 @@ alphaeq_tests =
   , eq_test "prd-renamed-eq" ([idn 0 "x"] → idv 0 "x") ([idn 1 "y"] → idv 1 "y") True
   , eq_test "prd-free-neq" ([idn 0 "x"] → idv 1 "y") ([idn 1 "y"] → idv 1 "y") False
 
+
+  , eq_test "ctr-eq" (ctr "zero" (𝓊 0)) (ctr "zero" (𝓊 0)) True
+  --, eq_test "multi-ctr-eq" ([idn 0 "x"] → idv 0 "x") ([idn 1 "y"] → idv 1 "y") True
+  --, eq_test "prd-free-neq" ([idn 0 "x"] → idv 1 "y") ([idn 1 "y"] → idv 1 "y") False
+
   , eq_test "eql-eq" (ι [] (𝓊 1) (𝓊 0) (𝓊 0)) (ι [] (𝓊 1) (𝓊 0) (𝓊 0)) True
   , eq_test "eql-neq" (ι [] (𝓊 1) (𝓊 0) (𝓊 0)) (ι [] (𝓊 1) (𝓊 0) (𝓊 1)) False
   , eq_test "eql-bnd-eq"
@@ -91,6 +96,9 @@ args → body = foldr (\var body -> Prdχ void (OptBind (Just var, Nothing)) bod
 ρ :: CoreUD -> CoreUD
 ρ = Dapχ void []
 
+ctr :: Text -> CoreUD -> CoreUD
+ctr label core = Ctrχ void label (Just core)
+
 -- (⋅) :: Core b n UD -> Core b n UD -> Core b n UD
 -- (⋅) = App void
 

test/Spec/Sigil/Abstract/CoreUD.hs

@@ -25,6 +25,9 @@ type instance Varχ UD = Void
 type instance Prdχ UD = Void
 type instance Absχ UD = Void
 type instance Appχ UD = Void
+type instance Indχ UD = Void
+type instance Ctrχ UD = Void
+type instance Recχ UD = Void
 type instance Eqlχ UD = Void
 type instance Dapχ UD = Void
 type instance Singleχ UD = Void

test/Spec/Sigil/Interpret/Unify.hs

@@ -1,5 +1,6 @@
 module Spec.Sigil.Interpret.Unify (unify_spec) where
 
+import Debug.Trace
 import Prelude hiding (lookup)
 import Control.Monad.Except
 import Data.Text (Text)
@@ -78,12 +79,20 @@ unify_tests =
                             Conj [idv 0 "x" :≗: ([(idn 1 "A", 𝓊 0)] ⇒ idv 1 "A")]) True
 
 
-  -- ∃ x ⮜ ℕ. x ≃ one
+  -- ∃ x ⮜ ℕ. x ≃ two
+  -- x ↦ two
   , let nat = Ind (idn 1 "N") (𝓊 0) [("zero", idv 1 "N"), ("succ", [(idn 2 "_", idv 1 "N")] → idv 1 "N")]
-    in solve_test "ex-one"
+    in solve_test "ex-two"
         (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 ⮜ ℕ. x ∈ ℕ
+  -- x ↦ zero
+  , let nat = Ind (idn 1 "N") (𝓊 0) [("zero", idv 1 "N"), ("succ", [(idn 2 "_", idv 1 "N")] → idv 1 "N")]
+    in solve_test "inhabit-nat"
+        (Bind Exists (idn 0 "x") nat $ Conj [idv 0 "x" :∈: nat])
+        [(idn 0 "x", 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"
@@ -121,7 +130,7 @@ unify_tests =
         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 
+    has s sub = foldr (\(k, v) t -> t && maybe False (\x -> trace (show $ "checking α=:" <+> pretty v <+> "," <+> pretty x) (αeq v x)) (lookup k s)) True sub 
 
 
 -- var :: n -> Core b n UD