caledon 0.0.0.0 → 2.0.0.0
raw patch · 32 files changed
+2394/−731 lines, 32 filesbinary-added
Files
- AST.hs +418/−127
- Choice.hs +30/−37
- Context.hs +250/−0
- HOU.hs +732/−0
- Main.hs +38/−23
- Parser.hs +272/−98
- README.md +141/−47
- Solver.hs +0/−356
- TopoSortAxioms.hs +29/−0
- caledon.cabal +9/−8
- examples/.DS_Store binary
- examples/._.DS_Store binary
- examples/circtype.ncc +5/−0
- examples/circtype_bad.ncc +5/−0
- examples/coc.ncc +15/−0
- examples/evenodd.ncc +12/−0
- examples/implicit.ncc +16/−0
- examples/infer.ncc +15/−0
- examples/linear.ncc +6/−0
- examples/prelude.ncc +211/−0
- examples/record.ncc +18/−0
- examples/substitution.ncc +2/−0
- examples/syntax.ncc +38/−0
- examples/test.ncc +12/−0
- examples/universe.ncc +30/−0
- linear.ncc +0/−6
- media/.DS_Store binary
- media/._.DS_Store binary
- media/logo.png binary
- media/logo.svg +90/−0
- prelude.ncc +0/−18
- test.ncc +0/−11
AST.hs view
@@ -1,8 +1,10 @@-{-# LANGUAGE - DeriveFunctor,+{-# LANGUAGE FlexibleInstances,- PatternGuards+ PatternGuards,+ BangPatterns,+ FlexibleContexts #-}+ module AST where import qualified Data.Foldable as F@@ -11,164 +13,453 @@ import Data.Monoid import Data.Functor import qualified Data.Map as M+import Data.Map (Map) import qualified Data.Set as S--------------------------------------------------------------------------------------------- DATA TYPES ------------------------------------------------------------------------------------------------------+import Control.Monad.RWS (RWST)+import Control.Monad.State.Class (MonadState(), get, modify)++import Choice++-----------------------------+--- abstract syntax tree ---+-----------------------------+ type Name = String- -data Variable = Var Name- | Cons Name- deriving (Ord, Eq)- -data Tm = AbsImp Name Tp Tm- | Abs Name Tp Tm- | Spine Variable [Tp] - deriving (Eq, Ord)- -var nm = Spine (Var nm) []-cons nm = Spine (Cons nm) [] -data Constraint a = a :=: a- deriving (Eq, Ord, Functor, Show)+infixr 0 ~>+infixr 0 ~~>+(~>) = forall ""+(~~>) = imp_forall "" -data Tp = Atom Tm- | Forall Name Tp Tp- | ForallImp Name Tp Tp- deriving (Eq, Ord)+data Spine = Spine Name [Type]+ | Abs Name Type Spine + deriving (Eq) -data Predicate = Predicate { predName::Name- , predType::Tp - , predConstructors::[(Name, Tp)]- } - | Query { predName :: Name, predType::Tp }- deriving (Eq)+type Type = Spine+type Term = Spine -infixl 1 :|--data Judgement = (:|-) { antecedent :: [(Name,Tp)] , succedent :: Tp }+data Predicate = Predicate { predIsSound :: !Bool, predName :: !Name, predType :: !Type, predConstructors :: ![(Name,Type)] }+ | Query { predName :: !Name, predType :: !Spine}+ | Define { predIsSound :: !Bool, predName :: !Name, predValue :: !Spine, predType :: !Type}+ deriving (Eq) +class ValueTracker c where+ putValue :: Integer -> c -> c+ takeValue :: c -> Integer -atom = Atom $ cons "atom"+instance ValueTracker Integer where+ putValue _ i = i+ takeValue i = i +getNew :: (Functor m, MonadState c m, ValueTracker c) => m String+getNew = do+ st <- takeValue <$> get+ let n = 1 + st+ modify $ putValue n+ return $ show n+ +getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String+getNewWith s = {- (++s) <$> -} getNew --------------------------------------------------------------------------------------------- PRETTY PRINT -----------------------------------------------------------------------------------------------------instance Show Variable where- show (Var n) = n- show (Cons n) = n showWithParens t = if (case t of- Forall _ _ _ -> True- Atom (Spine _ lst) -> not $ null lst- Atom (Abs _ _ _) -> True- Atom (AbsImp _ _ _) -> True+ Abs{} -> True+ Spine "#infer#" _ -> True+ Spine "#imp_abs#" _ -> True+ Spine "#forall#" _ -> True+ Spine "#exists#" _ -> True+ Spine "#imp_forall#" _ -> True+ Spine "#ascribe#" _ -> True+ Spine "#tycon#" _ -> False+ Spine _ _ -> False ) then "("++show t++")" else show t -instance Show Tm where- show (Abs nm ty tm) = "λ "++nm++" : "++showWithParens ty++" . "++show tm- show (AbsImp nm ty tm) = "?λ "++nm++" : "++showWithParens ty++" . "++show tm- show (Spine cons apps) = show cons++concatMap (\s -> " "++showWithParens s) apps-instance Show Tp where- show t = case t of- Atom t -> show t- Forall nm t t' | not (S.member nm (freeVariables t')) -> showWithParens++" → "++ show t'- where showWithParens = case t of- Forall _ _ _ -> "(" ++ show t ++ ")"- _ -> show t- Forall nm ty t -> "∀ "++nm++" : "++show ty++" . "++show t- - ForallImp nm t t' | not (S.member nm (freeVariables t')) -> showWithParens++" ⇒ "++ show t'- where showWithParens = case t of- Forall _ _ _ -> "(" ++ show t ++ ")"- _ -> show t- ForallImp nm ty t -> "?∀ "++nm++" : "++show ty++" . "++show t- -instance Show Judgement where - show (a :|- b) = removeHdTl (show a) ++" ⊢ "++ show b- where removeHdTl = reverse . tail . reverse . tail +isOperator [] = False+isOperator ('#':_) = False+isOperator (a:_) = not $ elem a ('_':['a'..'z']++['A'..'Z']++['0'..'9']) ++instance Show Spine where+ show (Spine ['\'',c,'\''] []) = show c+ show (Spine "#infer#" [_, Abs nm t t']) = "<"++nm++" : "++show t++"> "++show t'+ show (Spine "#ascribe#" (ty:v:l)) = "( "++showWithParens v++ " : " ++ show ty++" ) "++show (Spine "" l) + show (Spine "#forall#" [_,Abs nm t t']) | not (S.member nm $ freeVariables t') = showWithParens t++ " → " ++ show t'+ show (Spine "#imp_forall#" [_,Abs nm t t']) | not (S.member nm $ freeVariables t') = showWithParens t++ " ⇒ " ++ show t'+ show (Spine "#forall#" [_,Abs nm t t']) = "["++nm++" : "++show t++"] "++show t' + show (Spine "#imp_forall#" [_,Abs nm t t']) = "{"++nm++" : "++show t++"} "++show t' + show (Spine "#tycon#" [Spine nm [t]]) = "{"++nm++" = "++show t++"}"+ show (Spine "#exists#" [_,Abs nm t t']) = "∃ "++nm++" : "++show t++". "++show t' + show (Spine "#imp_abs#" [_,Abs nm ty t]) = "?λ "++nm++" : "++showWithParens ty++" . "++show t+ show (Spine nm l@[_ , Abs _ _ _]) | isOperator nm = "("++nm++") "++show (Spine "" l)+ show (Spine nm (t:t':l)) | isOperator nm = "( "++showWithParens t++" "++nm++" "++ show t'++" )"++show (Spine "" l)+ show (Spine h l) = h++concatMap showWithParens' l+ where showWithParens' t = " "++if case t of+ Abs{} -> True+ Spine "#tycon#" _ -> False+ Spine _ lst -> not $ null lst+ then "("++show t++")" else show t + show (Abs nm ty t) = "λ "++nm++" : "++showWithParens ty++" . "++show t++showT True = "defn "+showT False = "unsound "+ instance Show Predicate where- show (Predicate nm ty []) = ""++"defn "++nm++" : "++show ty++";"- show (Predicate nm ty (a:cons)) = - ""++"defn "++nm++" : "++show ty++"\n"- ++ " as "++showSingle a++concatMap (\x->- "\n | "++showSingle x) cons++";"- where showSingle (nm,ty) = nm++" = "++show ty- show (Query nm ty) = "query "++nm++" = "++show ty+ show (Predicate s nm ty []) = showT s ++ nm ++ " : " ++ show ty ++ ";"+ show (Predicate s nm ty (a:cons)) =+ showT s++ nm ++ " : " ++ show ty ++ "\n" ++ " | " ++ showSingle a ++ concatMap (\x-> "\n | " ++ showSingle x) cons ++ ";"+ where showSingle (nm,ty) = nm ++ " = " ++ show ty+ show (Query nm val) = "query " ++ nm ++ " = " ++ show val+ show (Define s nm val ty) = showT s ++ nm ++ " : " ++ show ty ++"\n as "++show val+ +var !nm = Spine nm []+atomName = "prop"+tipeName = "type"+kindName = "#kind#" --------------------------------------------------------------------------------------------- SUBSTITUTION -----------------------------------------------------------------------------------------------------type Substitution = M.Map Name Tm+atom = var atomName+tipe = var tipeName+kind = var kindName -- can be either a type or an atom+ascribe a t = Spine ("#ascribe#") [t, a]+forall x tyA v = Spine ("#forall#") [tyA, Abs x tyA v]+exists x tyA v = Spine ("#exists#") [tyA, Abs x tyA v]+pack e tau imp tp interface = Spine "pack" [tp, Abs imp tp interface, tau, e]+open cl (imp,ty) (p,iface) cty inexp = Spine "#open#" [cl, ty,Abs imp ty iface, Abs imp ty (Abs p iface cty), Abs imp ty (Abs p iface inexp)] +infer x tyA v = Spine ("#infer#") [tyA, Abs x tyA v] +imp_forall x tyA v = Spine ("#imp_forall#") [tyA, Abs x tyA v]+imp_abs x tyA v = Spine ("#imp_abs#") [tyA, Abs x tyA v]+tycon nm val = Spine "#tycon#" [Spine nm [val]]+---------------------+--- substitution ---+---------------------++type Substitution = M.Map Name Spine+ infixr 1 |-> infixr 0 ***-m1 *** m2 = M.union m2 (subst m2 <$> m1)+m1 *** m2 = M.union m2 $ subst m2 <$> m1 (|->) = M.singleton (!) = flip M.lookup -rebuildSpine :: Tm -> [Tp] -> Tm+findTyconInPrefix nm = fip []+ where fip l (Spine "#tycon#" [Spine nm' [v]]:r) | nm == nm' = Just (v, reverse l++r)+ fip l (a@(Spine "#tycon#" [Spine _ [_]]):r) = fip (a:l) r+ fip _ _ = Nothing++apply :: Spine -> Spine -> Spine+apply !a !l = rebuildSpine a [l]++rebuildSpine :: Spine -> [Spine] -> Spine rebuildSpine s [] = s-rebuildSpine (Spine c apps) apps' = Spine c (apps ++ apps')-rebuildSpine (Abs nm _ rst) (a:apps') = rebuildSpine (subst (nm |-> tpToTm a) $ rst) apps'+rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of + Just (v, apps) -> rebuildSpine (Abs nm ty rst) (v:apps)+ Nothing -> seq sp $ if ty == atom && S.notMember nm (freeVariables rs) then rs else irs + -- proof irrelevance hack+ -- we know we can prove that type "prop" is inhabited+ -- irs - the proof doesn't matter+ -- rs - the proof matters+ -- irs - here, the proof might matter, but we don't know if we can prove the thing, + -- so we need to try+ where nm' = newNameFor nm $ freeVariables apps+ sp = subst (nm |-> var nm') rst+ rs = rebuildSpine sp apps+ irs = infer nm ty rs+rebuildSpine (Spine c apps) apps' = Spine c $ apps ++ apps'+rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) $ rst+ in seq sp $ rebuildSpine sp apps' -newName nm s = (nm',s')- where s' = if nm == nm' then s else M.insert nm (var nm') s +newNameFor :: Name -> S.Set Name -> Name+newNameFor nm fv = nm'+ where nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/?") [0..]+ free k = not $ S.member k fv+ +newName :: Name -> Map Name Spine -> S.Set Name -> (Name, Map Name Spine, S.Set Name)+newName "" so fo = ("",so,fo)+newName nm so fo = (nm',s',f')+ where s = M.delete nm so + -- could reduce the size of the free variable set here, but for efficiency it is not really necessary+ -- for beautification of output it is+ (s',f') = if nm == nm' then (s,fo) else (M.insert nm (var nm') s , S.insert nm' fo) nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/") [0..] fv = mappend (M.keysSet s) (freeVariables s) free k = not $ S.member k fv class Subst a where- subst :: Substitution -> a -> a-instance (Functor f , Subst a) => Subst (f a) where- subst foo t = subst foo <$> t-instance Subst Tm where- subst s (Abs nm t rst) = Abs nm' (subst s t) $ subst s' rst- where (nm',s') = newName nm s- subst s (AbsImp nm t rst) = AbsImp nm' (subst s t) $ subst s' rst- where (nm',s') = newName nm s - subst s (Spine head apps) = let apps' = subst s <$> apps in- case head of- Var nm | Just head' <- s ! nm -> rebuildSpine head' apps'- _ -> Spine head apps'-instance Subst Tp where- subst s t = case t of- Atom t -> Atom $ subst s t- ForallImp nm ty t -> ForallImp nm' (subst s ty) $ subst s' t -- THIS RULE is unsafe capture!- where (nm',s') = newName nm s- Forall nm ty t -> Forall nm' (subst s ty) $ subst s' t -- THIS RULE is unsafe capture!- where (nm',s') = newName nm s-instance Subst Judgement where - subst foo (c :|- s) = subst foo c :|- subst foo s+ substFree :: Substitution -> S.Set Name -> a -> a+ +subst s = substFree s $ freeVariables s --------------------------------------------------------------------------------------------- FREE VARIABLES --------------------------------------------------------------------------------------------------+class Alpha a where + alphaConvert :: S.Set Name -> a -> a+ rebuildFromMem :: Map Name Name -> a -> a + +instance Subst a => Subst [a] where+ substFree s f t = substFree s f <$> t+ +instance Alpha a => Alpha [a] where + alphaConvert s l = alphaConvert s <$> l+ rebuildFromMem s l = rebuildFromMem s <$> l+ +instance (Subst a, Subst b) => Subst (a,b) where+ substFree s f ~(a,b) = (substFree s f a , substFree s f b)+ +instance Subst Spine where+ substFree s f sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of+ False -> imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) f rst+ True -> error $ + "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp + ++ "\n\tfor: "++show s+ substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of+ False -> imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) f rst + True -> error $ + "can not capture free variables because implicit binds can not alpha convert: "++ show sp+ ++ "\n\tfor: "++show s+ substFree s f (Abs nm tp rst) = Abs nm' (substFree s f tp) $ substFree s' f' rst+ where (nm',s',f') = newName nm s f+ substFree s f (Spine "#tycon#" [Spine c [v]]) = Spine "#tycon#" [Spine c [substFree s f v]]+ substFree s f (Spine nm apps) = let apps' = substFree s f <$> apps in+ case s ! nm of+ Just nm -> rebuildSpine nm apps'+ _ -> Spine nm apps'+ +instance Alpha Spine where+ alphaConvert s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty $ alphaConvert (S.insert a s) r+ alphaConvert s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty $ alphaConvert (S.insert a s) r+ alphaConvert s (Abs nm ty r) = Abs nm' (alphaConvert s ty) $ alphaConvert (S.insert nm' s) r+ where nm' = newNameFor nm s+ alphaConvert s (Spine a l) = Spine a $ alphaConvert s l+ + rebuildFromMem s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r+ rebuildFromMem s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r+ rebuildFromMem s (Abs nm ty r) = Abs (fromMaybe nm $ M.lookup nm s) (rebuildFromMem s ty) $ rebuildFromMem s r+ rebuildFromMem s (Spine a l) = Spine a' $ rebuildFromMem s l+ where a' = fromMaybe a $ M.lookup a s+ + +instance Subst Predicate where+ substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(nm,t) -> (nm,substFree sub f t)) <$> cons)+ substFree sub f (Query nm ty) = Query nm (substFree sub f ty)+ substFree sub f (Define s nm val ty) = Define s nm (substFree sub f val) (substFree sub f ty)+ class FV a where freeVariables :: a -> S.Set Name- instance (FV a, F.Foldable f) => FV (f a) where freeVariables m = F.foldMap freeVariables m-instance FV Tp where- freeVariables t = case t of- Forall a ty t -> (S.delete a $ freeVariables t) `S.union` (freeVariables ty)- ForallImp a ty t -> (S.delete a $ freeVariables t) `S.union` (freeVariables ty)- Atom a -> freeVariables a-instance FV Tm where+instance FV Spine where freeVariables t = case t of- Abs nm t p -> S.delete nm $ freeVariables p- AbsImp nm t p -> S.delete nm $ freeVariables p - Spine head others -> mappend (freeVariables head) $ mconcat $ freeVariables <$> others-instance FV Variable where - freeVariables (Var a) = S.singleton a- freeVariables _ = mempty-instance (FV a,FV b) => FV (a,b) where - freeVariables (a,b) = freeVariables a `S.union` freeVariables b+ Abs nm t p -> (S.delete nm $ freeVariables p) `mappend` freeVariables t+ Spine "#tycon#" [Spine nm [v]] -> freeVariables v+ Spine ['\'',_,'\''] [] -> mempty+ Spine head others -> mappend (S.singleton head) $ mconcat $ map freeVariables others++ -class ToTm t where- tpToTm :: t -> Tm-instance ToTm Tp where- tpToTm (Forall n ty t) = Spine (Cons "forall") [Atom $ Abs n ty $ tpToTm t ]- tpToTm (ForallImp n ty t) = AbsImp n ty $ tpToTm t- tpToTm (Atom tm) = tm+-------------------------+--- Constraint types ---+-------------------------++data Quant = Forall | Exists deriving (Eq) ++instance Show Quant where+ show Forall = "∀"+ show Exists = "∃"++-- as ineficient as it is, I'll make this the constraint representation.+infix 2 :=: +infix 2 :@: +infixr 1 :&:++-- we can make this data structure mostly strict since the only time we don't +-- traverse it is when we fail, and in order to fail, we always have to traverse+-- the lhs!+data SCons = !Term :@: !Type+ | !Spine :=: !Spine+ deriving (Eq)+data Constraint = SCons [SCons]+ -- we don't necessarily have to traverse the rhs of a combination+ -- so we can make it lazy+ | !Constraint :&: Constraint + | Bind !Quant !Name !Type !Constraint+ deriving (Eq)+ +instance Show SCons where+ show (a :=: b) = show a++" ≐ "++show b+ show (a :@: b) = show a++" ∈ "++show b+ +instance Show Constraint where+ show (SCons []) = " ⊤ "+ show (SCons l) = concat $ intersperse " ∧ " $ map show l+ show (a :&: b) = show a++" ∧ "++show b+ + show (Bind q n ty c) = show q++" "++ n++" : "++show ty++" . "++showWithParens c+ where showWithParens Bind{} = show c+ showWithParens _ = "( "++show c++" )"++instance Monoid Constraint where+ mempty = SCons []+ + mappend (SCons []) b = b++ mappend a (SCons []) = a+ mappend (SCons a) (SCons b) = SCons $ a++b+ mappend a b = a :&: b++{-# RULES+ "mappendmempty" mappend mempty = id+ #-}++{-# RULES+ "memptymappend" flip mappend mempty = id+ #-}++instance Subst SCons where+ substFree s f c = case c of+ s1 :@: s2 -> subq s f (:@:) s1 s2+ s1 :=: s2 -> subq s f (:=:) s1 s2+ +instance Subst Constraint where+ substFree s f c = case c of+ SCons l -> SCons $ map (substFree s f) l+ s1 :&: s2 -> subq s f (:&:) s1 s2+ Bind q nm t c -> Bind q nm' (substFree s f t) $ substFree s' f' c+ where (nm',s',f') = newName nm s f+ +subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2)++(∃) = Bind Exists+(∀) = Bind Forall+ +infixr 0 <<$>+(<<$>) f m = ( \(a,b) -> (f a, b)) <$> m++regenM e a b = do+ (a',s1) <- regenWithMem a + (b',s2) <- regenWithMem b + return $ (e a' b', M.union s1 s2)+regen e a b = do+ a' <- regenAbsVars a + b' <- regenAbsVars b + return $ e a' b' + +class RegenAbsVars a where+ regenAbsVars :: (Functor f, MonadState c f, ValueTracker c) => a -> f a+ regenWithMem :: (Functor f, MonadState c f, ValueTracker c) => a -> f (a, Map Name Name)+ +instance RegenAbsVars l => RegenAbsVars [l] where+ regenAbsVars cons = mapM regenAbsVars cons+ + regenWithMem cons = together <$> mapM regenWithMem cons+ where together f = (l',foldr M.union mempty ss)+ where (l',ss) = unzip f+ ++ +instance RegenAbsVars Spine where + regenAbsVars (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <$> regenAbsVars r+ regenAbsVars (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <$> regenAbsVars r+ regenAbsVars (Abs a ty r) = do+ a' <- getNewWith $ "@rega"+ ty' <- regenAbsVars ty+ r' <- regenAbsVars $ subst (a |-> var a') r+ return $ Abs a' ty' r'+ regenAbsVars (Spine a l) = Spine a <$> regenAbsVars l+ + regenWithMem (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <<$> regenWithMem r+ regenWithMem (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <<$> regenWithMem r+ regenWithMem (Abs a ty r) = do+ a' <- getNewWith $ "@regm"+ (ty',s1) <- regenWithMem ty+ (r', s2) <- regenWithMem $ subst (a |-> var a') r+ return $ (Abs a' ty' r', M.insert a' a $ M.union s1 s2)+ regenWithMem (Spine a l) = Spine a <<$> regenWithMem l++++instance RegenAbsVars SCons where+ regenAbsVars cons = case cons of+ a :=: b -> regen (:=:) a b+ a :@: b -> regen (:@:) a b+ + regenWithMem cons = case cons of+ a :=: b -> regenM (:=:) a b+ a :@: b -> regenM (:@:) a b + +instance RegenAbsVars Constraint where + regenAbsVars cons = case cons of+ Bind q nm ty cons -> do+ ty' <- regenAbsVars ty+ case nm of+ "" -> do+ nm' <- getNewWith "@newer"+ let sub = nm |-> var nm'+ Bind q nm' ty' <$> regenAbsVars (subst sub cons)+ _ -> Bind q nm ty' <$> regenAbsVars cons+ SCons l -> SCons <$> regenAbsVars l+ a :&: b -> regen (:&:) a b+ + regenWithMem cons = case cons of+ Bind q nm ty cons -> do+ (ty',s1) <- regenWithMem ty+ nm' <- getNewWith "@regm'"+ let sub = nm |-> var nm'+ (cons',s2) <- regenWithMem $ subst sub cons+ return (Bind q nm' ty' cons', M.insert nm' nm $ M.union s1 s2)+ SCons l -> SCons <<$> regenWithMem l+ a :&: b -> regenM (:&:) a b + +getFamily (Spine "#infer#" [_, Abs _ _ lm]) = getFamily lm+getFamily (Spine "#ascribe#" (_:v:l)) = getFamily (rebuildSpine v l)+getFamily (Spine "#forall#" [_, Abs _ _ lm]) = getFamily lm+getFamily (Spine "#imp_forall#" [_, Abs _ _ lm]) = getFamily lm+getFamily (Spine "#exists#" [_, Abs _ _ lm]) = getFamily lm+getFamily (Spine "#open#" (_:_:c:_)) = getFamily c+getFamily (Spine "open" (_:_:c:_)) = getFamily c+getFamily (Spine "pack" [_,_,_,e]) = getFamily e+getFamily (Spine nm' _) = nm'+getFamily v = error $ "values don't have families: "++show v+++consts = [ (atomName , tipe)+ , (tipeName , kind)+ , (kindName , kind)+ -- atom : kind+ + , ("#ascribe#", forall "a" atom $ (var "a") ~> (var "a"))+ + , ("#forall#", forall "a" atom $ (var "a" ~> atom) ~> atom)+ + , ("#imp_forall#", forall "a" atom $ (var "a" ~> atom) ~> atom)+ + , ("#imp_abs#", forall "a" atom $ forall "foo" (var "a" ~> atom) $ imp_forall "z" (var "a") (Spine "foo" [var "z"]))+ + , ("#exists#", forall "a" atom $ (var "a" ~> atom) ~> atom)+ , ("pack", forall "tp" atom + $ forall "iface" (var "tp" ~> atom) + $ forall "tau" (var "tp") + $ forall "e" (Spine "iface" [var "tau"]) + $ exists "z" (var "tp") (Spine "iface" [var "z"]))+ , ("open", forall "a" atom + $ forall "f" (var "a" ~> atom) + $ exists "z" (var "a") (Spine "f" [var "z"])+ ~> (forall "v" (var "a") + $ Spine "f" [var "v"] ~> atom ))+ , ("openDef", forall "a" atom + $ forall "f" (var "a" ~> atom) + $ forall "v" (var "a")+ $ forall "fv" (Spine "f" [var "z"])+ $ Spine "open" [var "a", var "f", Spine "pack" [var "a", var "f", var "v", var "fv"] , var "v", var "fv"])+ ]+++envSet = S.fromList $ map fst consts++toNCCchar c = Spine ['\'',c,'\''] []+toNCCstring s = foldr cons nil $ map toNCCchar s+ where char = Spine "char" []+ nil = Spine "nil" [tycon "a" char]+ cons a l = Spine "cons" [tycon "a" char, a,l]++envConsts = M.fromList consts++isChar ['\'',_,'\''] = True+isChar _ = False
Choice.hs view
@@ -1,78 +1,71 @@-{-# LANGUAGE - DeriveFunctor, +{-# LANGUAGE+ DeriveFunctor, FlexibleContexts,- TypeSynonymInstances+ TypeSynonymInstances,+ FlexibleInstances,+ MultiParamTypeClasses #-} module Choice where+ import Control.Monad import Data.Functor import Control.Applicative-import Control.Monad.Error (ErrorT, runErrorT) import Control.Monad.Error.Class (catchError, throwError, MonadError)-import Control.Monad.State.Class-import Control.Monad.Trans.Class-import Control.Monad.Trans.Maybe-import Data.Maybe -data Choice a = Choice a :<|>: Choice a ++data Choice a = Choice a :<|>: Choice a | Fail String | Success a deriving (Functor) -instance Monad Choice where - fail a = Fail a+instance Monad Choice where+ fail = Fail return = Success Fail a >>= _ = Fail a (m :<|>: m') >>= f = (m >>= f) :<|>: (m' >>= f) Success a >>= f = f a- -instance Applicative Choice where ++instance Applicative Choice where pure = Success mf <*> ma = mf >>= (<$> ma)- + instance Alternative Choice where empty = Fail "" (<|>) = (:<|>:)- -instance MonadPlus Choice where ++instance MonadPlus Choice where mzero = Fail "" mplus = (:<|>:)- -class RunChoice m where ++class RunChoice m where runError :: m a -> Either String a- + instance RunChoice Choice where runError chs = case dropWhile notSuccess lst of- [] -> case dropWhile notFail lst of + [] -> case dropWhile notFail lst of Fail a:_ -> Left a _ -> error "this result makes no sense"- (Success a):_ -> Right a+ Success a : _ -> Right a _ -> error "this result makes no sense" where lst = chs:queue lst 1- - queue l 0 = []++ queue _ 0 = []+ queue [] _ = error "queue size should be empty when queue is empty" queue ((a :<|>: b):l) q = a:b:queue l (q + 1) queue (_:l) q = queue l (q - 1)- - notFail (Fail a) = False++ notFail (Fail _) = False notFail _ = True- - notSuccess (Success a) = False++ notSuccess (Success _) = False notSuccess _ = True- + appendErr :: (MonadError String m) => String -> m a -> m a appendErr s m = catchError m $ \s' -> throwError $ s' ++ "\n" ++ s- + instance MonadError String Choice where- throwError a = Fail a+ throwError = Fail catchError try1 foo_try2 = case runError try1 of Left s -> foo_try2 s Right a -> Success a--getNew :: (MonadState Integer m) => m String-getNew = do - st <- get- let n = 1 + st- put n- return $! show n
+ Context.hs view
@@ -0,0 +1,250 @@+{-# LANGUAGE+ BangPatterns+ #-}+module Context where++import AST+import Data.Monoid+import Data.Functor+import qualified Data.Map as M+import qualified Data.Set as S+import Data.Map (Map)+import Data.Set (Set)+import Control.Monad.State (StateT, runStateT, modify, get, put)+import Control.Monad.RWS (RWST, ask, local, censor, runRWST, get, put,listen)+import Control.Monad.Trans (lift)+import Control.Monad.Trans.Cont+import Choice+import Data.List+import Debug.Trace++--------------------+--- context map ---+--------------------+type ContextMap = Map Name Type++--------------------------------+--- constraint context list ---+--------------------------------+data Binding = Binding { elmQuant :: Quant+ , elmName :: Name+ , elmType :: Type+ , elmPrev :: Maybe Name+ , elmNext :: Maybe Name+ } deriving (Show)+ +instance Subst Binding where+ substFree sub f b = b { elmType = substFree sub f $! elmType b }+ +data Context = Context { ctxtHead :: Maybe Name+ , ctxtMap :: Map Name Binding+ , ctxtTail :: Maybe Name+ } deriving (Show)+ +instance Subst Context where + substFree sub f b = b { ctxtMap = substFree sub f <$> ctxtMap b }++lookupWith s a ctxt = case M.lookup a ctxt of+ Just r -> r+ Nothing -> error s++emptyContext = Context Nothing mempty Nothing++-- assumes the element is not already in the context, or it is and the only thing that is changing is it's type.+addToContext :: String -> Context -> Binding -> Context+addToContext s (Context Nothing ctxt Nothing) elm@(Binding _ nm _ Nothing Nothing) | M.null ctxt = checkContext (s++"\naddToCtxt N N: ") $ + Context (Just nm) (M.singleton nm elm) (Just nm)+addToContext s c (Binding _ _ _ Nothing Nothing) = error $ "context not empty so can't add to tail: "++show c+addToContext s c@(Context h ctxt t) elm@(Binding _ nm _ t'@(Just p) Nothing) | t' == t = checkContext (s++"\naddToCtxt J N: "++show elm ++ "\n\tOLD CONTEXT: "++show c) $ + Context h (M.insert p t'val $ M.insert nm elm $ ctxt) (Just nm)+ where t'val = (lookupWith "looking up p ctxt" p ctxt) { elmNext = Just nm }+addToContext s _ (Binding _ _ _ _ Nothing) = error "can't add this to tail"+addToContext s (Context h ctxt t) elm@(Binding _ nm _ Nothing h'@(Just n)) | h' == h = checkContext (s++"\naddToCtxt N J: ") $ + Context (Just nm) (M.insert n h'val $ M.insert nm elm $ ctxt) t+ where h'val = (lookupWith "looking up n ctxt" n ctxt) { elmPrev = Just nm }+addToContext s _ (Binding _ _ _ Nothing _) = error "can't add this to head"+addToContext s ctxt@Context{ctxtMap = cmap} elm@(Binding _ nm _ (Just p) (Just n)) = checkContext (s++"\naddToCtxt J J: ") $ + ctxt { ctxtMap = M.insert n n'val $ M.insert p p'val $ M.insert nm elm $ cmap }+ where n'val = (lookupWith "looking up n cmap" n cmap) { elmPrev = Just nm }+ p'val = (lookupWith "looking up p cmap" p cmap) { elmNext = Just nm }+ +removeFromContext :: Name -> Context -> Context+removeFromContext nm ctxt@(Context h cmap t) = case M.lookup nm cmap of+ Nothing -> checkContext "removing: nothing" $ ctxt+ Just Binding{ elmPrev = Nothing, elmNext = Nothing } -> emptyContext+ Just Binding{ elmPrev = Nothing, elmNext = Just n } -> isSane (Just nm == h) $ checkContext "removing: N J" $ Context (Just n) (M.insert n h' $ M.delete nm cmap) t+ where h' = (lookupWith "attempting to find new head" n cmap) { elmPrev = Nothing }+ Just Binding{ elmPrev = Just p, elmNext = Nothing } -> isSane (Just nm == t) $ checkContext "removing: J N" $ Context h (M.insert p t' $ M.delete nm cmap) (Just p)+ where t' = (lookupWith "attempting to find new tail" p cmap) { elmNext = Nothing }+ Just Binding{elmPrev = Just cp, elmNext = Just cn } -> case () of+ _ | h == t -> checkContext "removing: J J | h == t " $ Context Nothing mempty Nothing+ _ | h == Just nm -> checkContext "removing: J J | h == Just nm " $ Context (Just cn) (n' $ M.delete nm cmap) t+ _ | t == Just nm -> checkContext "removing: J J | t == Just nm " $ Context h (p' $ M.delete nm cmap) (Just cp)+ _ -> checkContext ("removing: J J | h /= t \n\t"++show ctxt) $ Context h (n' $ p' $ M.delete nm cmap) t+ where n' = M.insert cn $ (lookupWith "looking up a cmap for n'" cn cmap) { elmPrev = Just cp }+ p' = M.insert cp $ (lookupWith "looking up a cmap for p'" cp cmap ) { elmNext = Just cn }+ where isSane bool a = if bool then a else error "This doesn't match intended binding"++addToHead s quant nm tp ctxt = addToContext s ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt)+addToTail s quant nm tp ctxt = addToContext s ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing++removeHead ctxt = case ctxtHead ctxt of + Nothing -> ctxt+ Just a -> removeFromContext a ctxt++removeTail ctxt = case ctxtTail ctxt of + Nothing -> ctxt+ Just a -> removeFromContext a ctxt++getTail (Context _ ctx (Just t)) = lookupWith "getting tail" t ctx+getTail (Context _ _ Nothing) = error "no tail!"++getHead (Context (Just h) ctx _) = lookupWith "getting head" h ctx+getHead (Context Nothing _ _) = error "no head"++-- gets the list of bindings after (below) a given binding+getAfter s bind ctx = tail $ getAfter' s bind ctx +getAfter' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind+ where gb ~(Binding quant nm ty _ n) = (quant, (nm,ty)):case n of+ Nothing -> []+ Just n -> gb $ case M.lookup n ctxt of + Nothing -> error $ "element "++show n++" not in map \n\twith ctxt: "++show ctx++" \n\t for bind: "++show bind++"\n\t"++s+ Just c -> c++-- gets the list of bindings before (above) a given binding+getBefore s bind ctx = tail $ getBefore' s bind ctx +getBefore' s bind ctx@(Context{ ctxtMap = ctxt }) = gb bind+ where gb ~(Binding quant nm ty p _) = (quant, (nm,ty)):case p of+ Nothing -> []+ Just p -> gb $ case M.lookup p ctxt of + Nothing -> error $ "element "++show p++" not in map \n\twith ctxt: "++show ctx++" \n\t for bind: "++show bind++"\n\t"++s+ Just c -> c++--checkContext _ c = c++checkContext _ c@(Context Nothing _ Nothing) = c+checkContext s ctx = foldr (\v c -> seq (checkEquals v) c) ctx $ zip st (reverse $ ta)+ where st = getBefore' s (getTail ctx) ctx+ ta = getAfter' s (getHead ctx) ctx+ checkEquals (a,b) | (a == b) = ()+ checkEquals (a,b) = error $ s++" \n\tNOT THE SAME" ++show (a,b) ++ " \n\t IN "++show ctx+++-------------------------+--- Traversal Monad ---+-------------------------+data ContextState = ContextState { stateNum :: !Integer+ , stateCtxt :: Context + }+ +emptyState = ContextState 0 emptyContext++++instance ValueTracker ContextState where+ putValue i c = c { stateNum = i }+ takeValue c = stateNum c+ +type Env = RWST ContextMap Constraint ContextState Choice++isolateForFail m = do+ s <- get+ c <- m+ case c of+ Nothing -> do+ put s+ return Nothing+ _ -> return c++------------------------ +-- env with a context -- +------------------------+++getElm :: String -> Name -> Env (Either Binding Spine)+getElm _ !x | isChar x = do+ return $ Right $ var "char"+getElm s !x = do+ ty <- lookupConstant x+ case ty of+ Nothing -> Left <$> (\ctxt -> lookupWith ("looking up "++x++"\n\t in context: "++show ctxt++"\n\t"++s) x ctxt) <$> ctxtMap <$> stateCtxt <$> get+ Just a -> return $ Right a++-- | This gets all the bindings outside of a given bind and returns them in a list (not including that binding).+getBindings :: Binding -> Env [(Name,Type)]+getBindings bind = do+ ctx <- stateCtxt <$> get+ return $ snd <$> getBefore "IN: getBindings" bind ctx+ +getAnExist :: Env (Maybe (Name,Type))+getAnExist = do+ ctx <- stateCtxt <$> get+ let til = getTail ctx+ last = (elmQuant til, (elmName til, elmType til))+ return $ case ctx of+ Context _ _ Nothing -> Nothing+ _ -> snd <$> find (\(q,_) -> q == Exists) (last:getBefore "IN: getBindings" til ctx)++getAllBindings = do+ ctx <- stateCtxt <$> get+ case ctx of+ Context _ _ Nothing -> return []+ _ -> (getBindings $ getTail ctx)+ +getForalls :: Env ContextMap+getForalls = do+ ctx <- ctxtMap <$> stateCtxt <$> get+ return $ elmType <$> M.filter (\q -> elmQuant q == Forall) ctx+ +getExists :: Env ContextMap+getExists = do+ ctx <- ctxtMap <$> stateCtxt <$> get+ return $ elmType <$> M.filter (\q -> elmQuant q == Exists) ctx++getConstants :: Env ContextMap+getConstants = ask ++clearContext :: Env ()+clearContext = do+ ContextState i _ <- get+ put $ ContextState i emptyContext+++getFullCtxt :: Env ContextMap+getFullCtxt = do+ constants <- getConstants+ ctx <- ctxtMap <$> stateCtxt <$> get+ return $ M.union (elmType <$> ctx) constants++getVariablesBeforeExists :: Name -> Env ContextMap+getVariablesBeforeExists nm = do+ constants <- getConstants+ ctx <- stateCtxt <$> get + let bind = ctxtMap ctx M.! nm+ return $ M.union constants $ M.fromList $ snd <$> getBefore "IN: getVariablesBeforeExists" bind ctx+ ++modifyCtxt :: (Context -> Context) -> Env ()+modifyCtxt f = modify $ \m -> m { stateCtxt = f $ stateCtxt m }+++-------------------------+--- traversal monads ---+-------------------------+lookupConstant :: Name -> Env (Maybe Type)+lookupConstant x = (M.lookup x) <$> ask ++type TypeChecker = ContT Spine Env++typeCheckToEnv :: TypeChecker Spine -> Env (Spine,Constraint)+typeCheckToEnv m = listen $ runContT m return+++addToEnv :: (Name -> Spine -> Constraint -> Constraint) -> Name -> Spine -> TypeChecker a -> TypeChecker a+addToEnv e x ty = mapContT (censor $ e x ty) . liftLocal ask local (M.insert x ty)++----------------------+--- Universe Monad ---+----------------------++
+ HOU.hs view
@@ -0,0 +1,732 @@+{-# LANGUAGE + FlexibleInstances,+ PatternGuards,+ UnicodeSyntax,+ BangPatterns+ #-}+module HOU where++import Choice+import AST+import Context+import TopoSortAxioms+import Control.Monad.State (StateT, forM_,runStateT, modify, get)+import Control.Monad.RWS (RWST, runRWST, ask, tell)+import Control.Monad.Error (throwError, MonadError)+import Control.Monad (unless, forM, replicateM, void)+import Control.Monad.Trans (lift)+import Control.Applicative+import qualified Data.Foldable as F+import Data.List+import Data.Maybe+import Data.Monoid+import qualified Data.Map as M+import qualified Data.Set as S+import Debug.Trace++import System.IO.Unsafe++{-# INLINE level #-}+level = 0++{-# INLINE vtrace #-}+vtrace !i | i < level = trace+vtrace !i = const id++{-# INLINE vtraceShow #-}+vtraceShow !i1 !i2 s v | i2 < level = trace $ s ++" : "++show v+vtraceShow !i1 !i2 s v | i1 < level = trace s+vtraceShow !i1 !i2 s v = id++{-# INLINE throwTrace #-}+throwTrace !i s = vtrace i s $ throwError s+++-----------------------------------------------+--- the higher order unification algorithm ---+-----------------------------------------------++flatten :: Constraint -> Env [SCons]+flatten (Bind quant nm ty c) = do+ modifyCtxt $ addToTail "-flatten-" quant nm ty+ flatten c+flatten (c1 :&: c2) = do+ l1 <- flatten c1+ l2 <- flatten c2+ return $ l1 ++ l2+flatten (SCons l) = return l++unify :: Constraint -> Env Substitution+unify cons = do+ cons <- vtrace 5 ("CONSTRAINTS1: "++show cons) $ regenAbsVars cons+ cons <- vtrace 5 ("CONSTRAINTS2: "++show cons) $ flatten cons+ let uniWhile :: Substitution -> [SCons] -> Env (Substitution, [SCons])+ uniWhile !sub !c' = do+ exists <- getExists + c <- regenAbsVars c' + let -- eventually we can make the entire algorithm a graph modification algorithm for speed, + -- such that we don't have to topologically sort every time. Currently this only takes us from O(n log n) to O(n) per itteration, it is+ -- not necessarily worth it.+ uniWith !wth !backup = do+ let searchIn [] r = return Nothing+ searchIn (next:l) r = do+ c1' <- wth next + case c1' of+ Just (sub',next') -> return $ Just (sub', (subst sub' $ reverse r)+++ next'+ ++subst sub' l)+ Nothing -> searchIn l (next:r)+ res <- searchIn c []+ case res of+ Nothing -> do+ backup+ Just (!sub', c') -> do+ let !sub'' = sub *** sub'+ modifyCtxt $ subst sub'+ uniWhile sub'' $! c'++ vtrace 3 ("CONST: "++show c)+ ( uniWith unifyOne + $ uniWith unifySearch+ $ uniWith unifySearchAtom+ $ checkFinished c >> + return (sub, c))++ fst <$> uniWhile mempty cons++++checkFinished [] = return ()+checkFinished cval = throwTrace 0 $ "ambiguous constraint: " ++show cval++unifySearch :: SCons -> Env (Maybe (Substitution, [SCons]))+unifySearch (a :@: b) | b /= atom = do+ cons <- rightSearch a b+ return $ case cons of+ Nothing -> Nothing+ Just cons -> Just (mempty, cons)+unifySearch _ = return Nothing++unifySearchAtom (a :@: b) = do+ cons <- rightSearch a b+ return $ case cons of+ Nothing -> Nothing+ Just cons -> Just (mempty, cons)+unifySearchAtom _ = return Nothing++unifyOne :: SCons -> Env (Maybe (Substitution , [SCons]))+unifyOne (a :=: b) = do+ c' <- isolateForFail $ unifyEq $ a :=: b + case c' of + Nothing -> isolateForFail $ unifyEq $ b :=: a+ r -> return r+unifyOne _ = return Nothing++unifyEq cons@(a :=: b) = case (a,b) of + (Spine "#imp_forall#" [ty, l], b) -> vtrace 1 "-implicit-" $ do+ a' <- getNewWith "@aL"+ modifyCtxt $ addToTail "-implicit-" Exists a' ty+ return $ Just (mempty, [l `apply` var a' :=: b , var a' :@: ty])+ (b, Spine "#imp_forall#" [ty, l]) -> vtrace 1 "-implicit-" $ do+ a' <- getNewWith "@aR"+ modifyCtxt $ addToTail "-implicit-" Exists a' ty+ return $ Just (mempty, [b :=: l `apply` var a' , var a' :@: ty])++ (Spine "#imp_abs#" (ty:l:r), b) -> vtrace 1 ("-imp_abs- : "++show a ++ "\n\t"++show b) $ do+ a <- getNewWith "@iaL"+ modifyCtxt $ addToTail "-imp_abs-" Exists a ty+ return $ Just (mempty, [rebuildSpine l (var a:r) :=: b , var a :@: ty])+ (b, Spine "#imp_abs#" (ty:l:r)) -> vtrace 1 "-imp_abs-" $ do+ a <- getNewWith "@iaR"+ modifyCtxt $ addToTail "-imp_abs-" Exists a ty+ return $ Just (mempty, [b :=: rebuildSpine l (var a:r) , var a :@: ty])++ (Spine "#tycon#" [Spine nm [_]], Spine "#tycon#" [Spine nm' [_]]) | nm /= nm' -> throwTrace 0 $ "different type constraints: "++show cons+ (Spine "#tycon#" [Spine nm [val]], Spine "#tycon#" [Spine nm' [val']]) | nm == nm' -> + return $ Just (mempty, [val :=: val'])++ (Abs nm ty s , Abs nm' ty' s') -> vtrace 1 "-aa-" $ do+ modifyCtxt $ addToTail "-aa-" Forall nm ty+ return $ Just (mempty, [ty :=: ty' , s :=: subst (nm' |-> var nm) s'])+ (Abs nm ty s , s') -> vtraceShow 1 2 "-asL-" cons $ do+ modifyCtxt $ addToTail "-asL-" Forall nm ty+ return $ Just (mempty, [s :=: s' `apply` var nm])++ (s, Abs nm ty s' ) -> vtraceShow 1 2 "-asR-" cons $ do+ modifyCtxt $ addToTail "-asR-" Forall nm ty+ return $ Just (mempty, [s `apply` var nm :=: s'])++ (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [])+ (s@(Spine x yl), s') -> vtrace 4 "-ss-" $ do+ bind <- getElm ("all: "++show cons) x+ case bind of+ Left bind@Binding{ elmQuant = Exists } -> vtrace 4 "-g?-" $ do+ raiseToTop bind (Spine x yl) $ \(a@(Spine x yl),ty) sub ->+ case subst sub s' of+ b@(Spine x' y'l) -> vtrace 4 "-gs-" $ do+ bind' <- getElm ("gvar-blah: "++show cons) x'+ case bind' of+ Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const+ --if allElementsAreVariables yl+ --then gvar_const (Spine x yl, ty) (Spine x' y'l, ty') + -- else return Nothing+ gvar_const (Spine x yl, ty) (Spine x' y'l, ty') + Left Binding{ elmQuant = Forall } | not $ S.member x' $ freeVariables yl -> + throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)+ Left Binding{ elmQuant = Forall } | S.member x $ freeVariables y'l -> + throwTrace 0 $ "CANT: occurs check: "++show (a :=: b)+ Left Binding{ elmQuant = Forall, elmType = ty' } -> vtrace 1 "-gui-" $ -- gvar-uvar-inside+ gvar_uvar_inside (Spine x yl, ty) (Spine x' y'l, ty')+ Left bind@Binding{ elmQuant = Exists, elmType = ty' } -> + if not $ allElementsAreVariables yl && allElementsAreVariables y'l + then return Nothing + else if x == x' + then vtraceShow 1 2 "-ggs-" cons $ -- gvar-gvar-same+ gvar_gvar_same (Spine x yl, ty) (Spine x' y'l, ty')+ else -- gvar-gvar-diff+ if S.member x $ freeVariables y'l + then throwTrace 0 $ "CANT: ggd-occurs check: "++show (a :=: b)+ else vtraceShow 1 2 "-ggd-" cons $ gvar_gvar_diff (Spine x yl, ty) (Spine x' y'l, ty') bind+ _ -> vtrace 1 "-ggs-" $ return Nothing+ _ -> vtrace 4 "-u?-" $ case s' of + b@(Spine x' _) | x /= x' -> do+ bind' <- getElm ("const case: "++show cons) x'+ case bind' of+ Left Binding{ elmQuant = Exists } -> return Nothing+ _ -> throwTrace 0 ("CANT: -uud- two different universal equalities: "++show (a :=: b)) -- uvar-uvar ++ Spine x' yl' | x == x' -> vtraceShow 1 2 "-uue-" (a :=: b) $ do -- uvar-uvar-eq+ + let match ((Spine "#tycon#" [Spine nm [a]]):al) bl = case findTyconInPrefix nm bl of+ Nothing -> match al bl+ Just (b,bl) -> ((a :=: b) :) <$> match al bl+ -- in this case we know that al has no #tycon#s in its prefix since we exhausted all of them in the previous case+ match al (Spine "#tycon#" [Spine _ [_]]:bl) = match al bl + match (a:al) (b:bl) = ((a :=: b) :) <$> match al bl + match [] [] = return []+ match _ _ = throwTrace 0 $ "CANT: different numbers of arguments on constant: "++show cons++ cons <- match yl yl'+ return $ Just (mempty, cons)+ _ -> throwTrace 0 $ "CANT: uvar against a pi WITH CONS "++show cons+ +allElementsAreVariables :: [Spine] -> Bool+allElementsAreVariables = all $ \c -> case c of+ Spine _ [] -> True+ _ -> False++typeToListOfTypes (Spine "#forall#" [_, Abs x ty l]) = (x,ty):typeToListOfTypes l+typeToListOfTypes (Spine _ _) = []+typeToListOfTypes a@(Abs _ _ _) = error $ "not a type" ++ show a++-- the problem WAS (hopefully) here that the binds were getting+-- a different number of substitutions than the constraints were.+-- make sure to check that this is right in the future.+raiseToTop bind@Binding{ elmName = x, elmType = ty } sp m = do+ + hl <- reverse <$> getBindings bind+ x' <- getNewWith "@newx"+ + let newx_args = map (var . fst) hl+ sub = x |-> Spine x' newx_args+ + ty' = foldr (\(nm,ty) a -> forall nm ty a) ty hl+ + addSub Nothing = return Nothing+ addSub (Just (sub',cons)) = do+ -- we need to solve subst twice because we might reify twice+ let sub'' = ((subst sub' <$> sub) *** sub') ++ modifyCtxt $ subst sub'+ return $ Just (sub'', cons)+ + modifyCtxt $ addToHead "-rtt-" Exists x' ty' . removeFromContext x+ vtrace 3 ("RAISING: "++x' ++" +@+ "++ show newx_args ++ " ::: "++show ty'+ ++"\nFROM: "++x ++" ::: "++ show ty+ ) modifyCtxt $ subst sub+ + -- now we can match against the right hand side+ r <- addSub =<< m (subst sub sp, ty') sub+ modifyCtxt $ removeFromContext x'+ return r++ +getBase 0 a = a+getBase n (Spine "#forall#" [_, Abs _ _ r]) = getBase (n - 1) r+getBase _ a = a++makeBind xN us tyl arg = foldr (uncurry Abs) (Spine xN $ map var arg) $ zip us tyl++gvar_gvar_same (a@(Spine x yl), aty) (b@(Spine _ y'l), _) = do+ aty <- regenAbsVars aty+ let n = length yl+ + (uNl,atyl) = unzip $ take n $ typeToListOfTypes aty+ + xN <- getNewWith "@ggs"+ + let perm = [iyt | (iyt,_) <- filter (\(_,(a,b)) -> a == b) $ zip (zip uNl atyl) (zip yl y'l) ]+ + l = makeBind xN uNl atyl $ map fst perm+ + xNty = foldr (uncurry forall) (getBase n aty) perm+ + sub = x |-> l+ + modifyCtxt $ addToHead "-ggs-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!+ + return $ Just (sub, []) -- var xN :@: xNty])+ +gvar_gvar_same _ _ = error "gvar-gvar-same is not made for this case"++gvar_gvar_diff (a',aty') (sp, _) bind = raiseToTop bind sp $ \(b'@(Spine x' y'l), bty) subO -> do+ + let (Spine x yl, aty) = (subst subO a', subst subO aty')++ -- now x' comes before x + -- but we no longer care since I tested it, and switching them twice reduces to original+ n = length yl+ m = length y'l+ + aty <- regenAbsVars aty+ bty <- regenAbsVars bty+ + let (uNl,atyl) = unzip $ take n $ typeToListOfTypes aty+ (vNl,btyl) = unzip $ take m $ typeToListOfTypes bty+ + xN <- getNewWith "@ggd"+ + let perm = do+ (iyt,y) <- zip (zip uNl atyl) yl+ (i',_) <- filter (\(_,y') -> y == y') $ zip vNl y'l + return (iyt,i')+ + l = makeBind xN uNl atyl $ map (fst . fst) perm+ l' = makeBind xN vNl btyl $ map snd perm+ + xNty = foldr (uncurry forall) (getBase n aty) (map fst perm)+ + sub = M.fromList [(x ,l), (x',l')]++ modifyCtxt $ addToHead "-ggd-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!!+ + vtrace 3 ("SUBST: -ggd- "++show sub) $ return $ Just (sub, []) -- var xN :@: xNty])+ +gvar_uvar_inside a@(Spine _ yl, _) b@(Spine y _, _) = + case elemIndex (var y) $ reverse yl of+ Nothing -> return Nothing+ Just _ -> gvar_uvar_outside a b+gvar_uvar_inside _ _ = error "gvar-uvar-inside is not made for this case"+ +gvar_const a@(s@(Spine x yl), _) b@(s'@(Spine y _), bty) = vtrace 3 (show a++" ≐ "++show b) $+ case elemIndex (var y) $ yl of + Nothing -> gvar_fixed a b $ var . const y+ Just _ -> do+ gvar_uvar_outside a b <|> gvar_fixed a b (var . const y) ++gvar_const _ _ = error "gvar-const is not made for this case"++gvar_uvar_outside a@(s@(Spine x yl),_) b@(s'@(Spine y _),bty) = do+ let ilst = [i | (i,y') <- zip [0..] yl , y' == var y] + i <- F.asum $ return <$> ilst+ gvar_fixed a b $ (!! i) +++gvar_uvar_outside _ _ = error "gvar-uvar-outside is not made for this case"++getTyNews (Spine "#forall#" [_, Abs _ _ t]) = Nothing:getTyNews t+getTyNews (Spine "#imp_forall#" [_, Abs nm _ t]) = Just nm:getTyNews t+getTyNews _ = []++gvar_fixed (a@(Spine x _), aty) (b@(Spine _ y'l), bty) action = do+ let m = getTyNews bty -- max (length y'l) (getTyLen bty)+ cons = a :=: b+-- getNewTys "@xm" bty ++ + let getArgs (Spine "#forall#" [ty, Abs ui _ r]) = ((var ui,ui),Left ty):getArgs r+ getArgs (Spine "#imp_forall#" [ty, Abs ui _ r]) = ((tycon ui $ var ui,ui),Right ty):getArgs r+ getArgs _ = []+ + untylr = getArgs aty+ (un,_) = unzip untylr + (vun, _) = unzip un+ + xm <- forM m $ \j -> do+ x <- getNewWith "@xm"+ return (x, (Spine x vun, case j of+ Nothing -> Spine x vun+ Just a -> tycon a $ Spine x vun)) + + let xml = map (snd . snd) xm+ -- when rebuilding the spine we want to use typeconstructed variables if bty contains implicit quantifiers+ toLterm (Spine "#forall#" [ty, Abs ui _ r]) = Abs ui ty $ toLterm r+ toLterm (Spine "#imp_forall#" [ty, Abs ui _ r]) = imp_abs ui ty $ toLterm r + toLterm _ = rebuildSpine (action vun) $ xml++ + l = toLterm aty+ + vbuild e = foldr (\((_,nm),ty) a -> case ty of+ Left ty -> forall nm ty a+ Right ty -> imp_forall nm ty a+ ) e untylr++ substBty sub (Spine "#forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi)+ :substBty (M.insert vi (fst xi) sub) r xmr+ substBty sub (Spine "#imp_forall#" [_, Abs vi bi r]) ((x,xi):xmr) = (x,vbuild $ subst sub bi)+ : substBty (M.insert vi (fst xi) sub) r xmr+ substBty _ _ [] = []+ substBty _ s l = error $ "is not well typed: "++show s+ ++"\nFOR "++show l + ++ "\nON "++ show cons+ + sub = x |-> l -- THIS IS THAT STRANGE BUG WHERE WE CAN'T use x in the output substitution!+ addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addToHead "-gf-" Exists s t+ modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm + modifyCtxt $ subst sub+ + return $ Just (sub, [subst sub $ a :=: b])++gvar_fixed _ _ _ = error "gvar-fixed is not made for this case"++--------------------+--- proof search --- +--------------------+++-- need bidirectional search!+rightSearch m goal = vtrace 1 ("-rs- "++show m++" ∈ "++show goal) $ + case goal of+ Spine "#forall#" [a, b] -> do+ y <- getNewWith "@sY"+ x' <- getNewWith "@sX"+ let b' = b `apply` var x'+ modifyCtxt $ addToTail "-rsFf-" Forall x' a+ modifyCtxt $ addToTail "-rsFe-" Exists y b'+ return $ Just [ var y :=: m `apply` var x' , var y :@: b']++ Spine "#imp_forall#" [_, Abs x a b] -> do+ y <- getNewWith "@isY"+ x' <- getNewWith "@isX"+ let b' = subst (x |-> var x') b+ modifyCtxt $ addToTail "-rsIf-" Forall x' a + modifyCtxt $ addToTail "-rsIe-" Exists y b'+ return $ Just [ var y :=: m `apply` (tycon x $ var x')+ , var y :@: b'+ ]+ Spine "putChar" [c@(Spine ['\'',l,'\''] [])] ->+ case unsafePerformIO $ putStr $ l:[] of+ () -> return $ Just [ m :=: Spine "putCharImp" [c]]+ Spine "putChar" [_] -> vtrace 0 "FAILING PUTCHAR" $ return Nothing+ + Spine "readLine" [l] -> + case toNCCstring $ unsafePerformIO $ getLine of+ !s -> do+ y <- getNewWith "@isY"+ let ls = l `apply` s+ modifyCtxt $ addToTail "-rl-" Exists y ls+ return $ Just [m :=: Spine "readLineImp" [l,s, var y], var y :@: Spine "run" [ls]]+ _ | goal == kind -> do+ case m of+ Abs{} -> throwError "not properly typed"+ _ | m == tipe || m == atom -> return $ Just []+ _ -> F.asum $ return . Just . return . (m :=:) <$> [atom , tipe]+ Spine nm _ -> do+ constants <- getConstants+ foralls <- getForalls+ exists <- getExists+ let env = M.union foralls constants+ + isFixed a = isChar a || M.member a env+ + getFixedType a | isChar a = Just $ var "char"+ getFixedType a = M.lookup a env+ + let mfam = case m of + Abs{} -> Nothing+ Spine nm _ -> case getFixedType nm of+ Just t -> Just (nm,t)+ Nothing -> Nothing+ + sameFamily (_, Abs _ _ _) = False+ sameFamily ("pack",s) = "#exists#" == nm+ sameFamily (_,s) = getFamily s == nm+ + targets <- case mfam of+ Just (nm,t) -> return $ [(nm,t)]+ Nothing -> do+ let excludes = S.toList $ S.intersection (M.keysSet exists) $ freeVariables m+ searchMaps <- mapM getVariablesBeforeExists excludes+ + let searchMap = M.union env $ case searchMaps of+ [] -> mempty+ a:l -> foldr (M.intersection) a l+ + return $ filter sameFamily $ M.toList searchMap+ + if all isFixed $ S.toList $ S.union (freeVariables m) (freeVariables goal)+ then return $ Just []+ else case targets of+ [] -> return Nothing+ _ -> Just <$> (F.asum $ leftSearch m goal <$> reverse targets) -- reversing works for now, but not forever! need a heuristics + bidirectional search + control structures++a .-. s = foldr (\k v -> M.delete k v) a s ++leftSearch m goal (x,target) = vtrace 1 ("LS: " ++ show m ++" ∈ "++ show goal+ ++"\n\t@ " ++x++" : " ++show target)+ $ leftCont (var x) target+ where leftCont n target = throwTrace 3 ("DEFER: LS: " ++ show m ++" ∈ "++ show goal+ ++"\n\t@ " ++x++" : " ++show target) <|> case target of+ Spine "#forall#" [a, b] -> do+ x' <- getNewWith "@sla"+ modifyCtxt $ addToTail "-lsF-" Exists x' a+ cons <- leftCont (n `apply` var x') (b `apply` var x')+ return $ cons++[var x' :@: a]++ Spine "#imp_forall#" [_ , Abs x a b] -> do + x' <- getNewWith "@isla"+ modifyCtxt $ addToTail "-lsI-" Exists x' a+ cons <- leftCont (n `apply` (tycon x $ var x')) (subst (x |-> var x') b)+ return $ cons++[var x' :@: a]+ Spine _ _ -> do+ return $ [goal :=: target , m :=: n]+ _ -> error $ "λ does not have type atom: " ++ show target++search :: Type -> Env (Substitution, Term)+search ty = do+ e <- getNewWith "@e"+ sub <- unify $ (∃) e ty $ SCons [var e :@: ty]+ return $ (sub, subst sub $ var e)++-----------------------------+--- constraint generation ---+-----------------------------++(≐) a b = lift $ tell $ SCons [a :=: b]+(.@.) a b = lift $ tell $ SCons [a :@: b]++withKind m = do+ k <- getNewWith "@k"+ addToEnv (∃) k kind $ do+ r <- m $ var k+ var k .@. kind+ return r++check v x = if x == "13@regm+f" then trace ("FOUND AT: "++ v) x else x++checkType :: Spine -> Type -> TypeChecker Spine+checkType sp ty | ty == kind = withKind $ checkType sp+checkType sp ty = case sp of+ Spine "#hole#" [] -> do+ x' <- getNewWith "@hole"+ addToEnv (∃) x' ty $ do+ var x' .@. ty+ return $ var x'+ + Spine "#ascribe#" (t:v:l) -> do+ (v'',mem) <- regenWithMem v+ + t'' <- regenAbsVars t+ v' <- checkType v'' t''+ + r <- getNewWith "@r"+ Spine _ l' <- addToEnv (∀) r t $ checkType (Spine r l) ty+ return $ rebuildSpine (rebuildFromMem mem v') l'++-- checkType (rebuildSpine (rebuildFromMem mem v') l) ty+ + Spine "#infer#" [_, Abs x tyA tyB ] -> do+ tyA <- withKind $ checkType tyA+ + x' <- getNewWith "@inf"+ addToEnv (∃) x' tyA $ do+ var x' .@. tyA+ checkType (subst (x |-> var x') tyB) ty++ Spine "#imp_forall#" [_, Abs x tyA tyB] -> do+ tyA <- withKind $ checkType tyA+ tyB <- addToEnv (∀) (check "imp_forall" x) tyA $ checkType tyB ty+ return $ imp_forall x tyA tyB+ + Spine "#forall#" [_, Abs x tyA tyB] -> do+ tyA <- withKind $ checkType tyA+ forall x tyA <$> (addToEnv (∀) (check "forall" x) tyA $ + checkType tyB ty )++ -- below are the only cases where bidirectional type checking is useful + Spine "#imp_abs#" [_, Abs x tyA sp] -> case ty of+ Spine "#imp_forall#" [_, Abs x' tyA' tyF'] -> do+ unless ("" == x' || x == x') $ + lift $ throwTrace 0 $ "can not show: "++show sp ++ " : "++show ty + ++"since: "++x++ " ≠ "++x'+ tyA <- withKind $ checkType tyA+ tyA ≐ tyA'+ addToEnv (∀) (check "impabs1" x) tyA $ do+ imp_abs x tyA <$> checkType sp tyF'+ + _ -> do+ e <- getNewWith "@e"+ tyA <- withKind $ checkType tyA+ withKind $ \k -> addToEnv (∃) e (forall x tyA k) $ do+ imp_forall x tyA (Spine e [var x]) ≐ ty+ sp <- addToEnv (∀) (check "impabs2" x) tyA $ checkType sp (Spine e [var x])+ return $ imp_abs x tyA $ sp++ Abs x tyA sp -> case ty of+ Spine "#forall#" [_, Abs x' tyA' tyF'] -> do+ tyA <- withKind $ checkType tyA+ tyA ≐ tyA'+ addToEnv (∀) (check "abs1" x) tyA $ do+ Abs x tyA <$> checkType sp (subst (x' |-> var x) tyF')+ _ -> do+ e <- getNewWith "@e"+ tyA <- withKind $ checkType tyA+ withKind $ \k -> addToEnv (∃) e (forall "" tyA k) $ do+ forall x tyA (Spine e [var x]) ≐ ty+ Abs x tyA <$> (addToEnv (∀) (check "abs2" x) tyA $ checkType sp (Spine e [var x]))+ Spine nm [] | isChar nm -> do+ ty ≐ Spine "char" []+ return sp+ Spine head args -> do+ let chop mty [] = do+ ty ≐ mty+ return []+ + chop mty lst@(a:l) = case mty of + + Spine "#imp_forall#" [ty', Abs nm _ tyv] -> case findTyconInPrefix nm lst of+ Nothing -> do+ x <- getNewWith "@xin"+ addToEnv (∃) x ty' $ do+ var x .@. ty' + -- we need to make sure that the type is satisfiable such that we can reapply it!+ (tycon nm (var x):) <$> chop (subst (nm |-> var x) tyv) lst++ Just (val,l) -> do+ val <- checkType val ty'+ (tycon nm val:) <$> chop (subst (nm |-> val) tyv) l+ Spine "#forall#" [ty', c] -> do+ a <- checkType a ty'+ (a:) <$> chop (c `apply` a) l+ _ -> withKind $ \k -> do + x <- getNewWith "@xin"+ z <- getNewWith "@zin"+ tybody <- getNewWith "@v"+ let tybodyty = forall z (var x) k+ withKind $ \k' -> addToEnv (∃) x k' $ addToEnv (∃) tybody tybodyty $ do + a <- checkType a (var x)+ v <- getNewWith "@v"+ forall v (var x) (Spine tybody [var v]) ≐ mty+ (a:) <$> chop (Spine tybody [a]) l++ mty <- (M.lookup head) <$> lift getFullCtxt+ + case mty of + Nothing -> lift $ throwTrace 0 $ "variable: "++show head++" not found in the environment."+ ++ "\n\t from "++ show sp+ ++ "\n\t from "++ show ty+ Just ty' -> Spine head <$> chop ty' args++checkFullType :: Spine -> Type -> Env (Spine, Constraint)+checkFullType val ty = typeCheckToEnv $ checkType val ty++----------------------+--- type inference ---+----------------------+typeInfer :: ContextMap -> (Name,Spine,Type) -> Choice (Term,Type, ContextMap)+typeInfer env (nm,val,ty) = (\r -> (\(a,_,_) -> a) <$> runRWST r (M.union envConsts env) emptyState) $ do+ ty <- return $ alphaConvert mempty ty+ val <- return $ alphaConvert mempty val+ + (ty,mem') <- regenWithMem ty+ (val,mem) <- regenWithMem val+ + (val,constraint) <- checkFullType val ty+ + sub <- appendErr ("which became: "++show val ++ "\n\t : " ++ show ty) $ + unify constraint+ + let resV = rebuildFromMem mem $ unsafeSubst sub val+ resT = rebuildFromMem mem' $ unsafeSubst sub ty++ vtrace 0 ("RESULT: "++nm++" : "++show resV) $+ return $ (resV,resT, M.insert nm resV env)++unsafeSubst s (Spine nm apps) = let apps' = unsafeSubst s <$> apps in case s ! nm of + Just nm -> rebuildSpine nm apps'+ _ -> Spine nm apps'+unsafeSubst s (Abs nm tp rst) = Abs nm (unsafeSubst s tp) (unsafeSubst s rst)+ +----------------------------+--- the public interface ---+----------------------------+typeCheckAxioms :: [(Maybe Name,Bool,Name,Term,Type)] -> Choice ContextMap+typeCheckAxioms lst = do+ + -- check the closedness of families. this gets done+ -- after typechecking since family checking needs to evaluate a little bit+ -- in order to allow defs in patterns+ let notval (_,s,'#':'v':':':_,_,_) = False+ notval (_,s,_,_,_) = True + + unsound (_,s,_,_,_) = not s+ + tys = M.fromList $ map (\(_,_,nm,ty,_) -> (nm,ty)) $ filter notval lst+ uns = S.fromList $ map (\(_,_,nm,ty,_) -> nm) $ filter unsound $ filter notval lst+ + inferAll (l , r, []) = return (r,l)+ inferAll (_ , r, (_,_,nm,_,_):_) | nm == tipeName = throwTrace 0 $ tipeName++" can not be overloaded"+ inferAll (_ , r, (_,_,nm,_,_):_) | nm == atomName = throwTrace 0 $ atomName++" can not be overloaded"+ inferAll (l , r, (fam,s,nm,val,ty):toplst) = do+ (val,ty,l') <- appendErr ("can not infer type for: "++nm++" : "++show val) $ + trace ("Checking: " ++nm) $ + vtrace 0 ("\tVAL: " ++show val + ++"\n\t:: " ++show ty) $+ typeInfer l (nm, val,ty) -- constrain the breadth first search to be local!+ + -- do the family check after ascription removal and typechecking because it can involve computation!+ unless (fam == Nothing || Just (getFamily val) == fam)+ $ throwTrace 0 $ "not the right family: need "++show fam++" for "++nm ++ " = " ++show val + + inferAll $ case nm of+ '#':'v':':':nm' -> (sub <$> l', (fam,s,nm,val,ty):r , fsub <$> toplst) + where sub = subst $ nm' |-> ascribe val ty -- the ascription isn't necessary because we don't have unbound variables+ fsub (fam,s,nm,val,ty) = (fam,s,nm, sub val, sub ty)+ _ -> (l', (fam,s,nm,val,ty):r, toplst)++ (lst',l) <- inferAll (tys, [], topoSortAxioms lst)+ + let doubleCheckAll _ [] = return ()+ doubleCheckAll l ((_,_,nm,val,ty):r) = do+ let usedvars = freeVariables val `S.union` freeVariables ty+ unless (S.isSubsetOf usedvars l)+ $ throwTrace 0 $ "Circular type:"+ ++"\n\t"++nm++" : "++show val ++" : "++show ty+ ++"\n\tcontains the following circular type dependencies: "+ ++"\n\t"++show (S.toList $ S.difference usedvars l)+ ++ "\nPossible Solution: declare it unsound"+ ++ "\nunsound "++nm++" : "++show val+ doubleCheckAll (S.insert nm l) r+ + doubleCheckAll (S.union envSet uns) $ topoSortAxioms lst'+ + return l + +typeCheckAll :: [Predicate] -> Choice [Predicate]+typeCheckAll preds = do+ let toAxioms (Predicate s nm ty cs) = (Just $ atomName,s,nm,ty,tipe):map (\(nm',ty') -> (Just nm,False, nm',ty',atom)) cs+ toAxioms (Query nm val) = [(Nothing, False,nm,val,atom)]+ toAxioms (Define s nm val ty) = [(Nothing,False, nm,ty,kind), (Nothing,s, "#v:"++nm,val,ty)]+ tyMap <- typeCheckAxioms $ concatMap toAxioms preds+ + let newPreds (Predicate t nm _ cs) = Predicate t nm (tyMap M.! nm) $ map (\(nm,_) -> (nm,tyMap M.! nm)) cs+ newPreds (Query nm _) = Query nm (tyMap M.! nm)+ newPreds (Define t nm _ _) = Define t nm (tyMap M.! ("#v:"++nm)) (tyMap M.! nm)+ + return $ newPreds <$> preds+ +solver :: [(Name,Type)] -> Type -> Either String [(Name, Term)]+solver axioms tp = case runError $ runRWST (search tp) (M.union envConsts $ M.fromList axioms) emptyState of+ Right ((_,tm),_,_) -> Right $ [("query", tm)]+ Left s -> Left $ "reification not possible: "++s
Main.hs view
@@ -2,49 +2,64 @@ import AST import Choice-import Solver+import HOU import Parser import System.Environment-import Data.Foldable as F (msum, forM_) import Data.Functor+import Data.Foldable as F (forM_) import Data.List (partition) import Text.Parsec import Data.Monoid+import Control.Arrow (first) ----------------------------------------------------------------------- -------------------------- MAIN --------------------------------------- ----------------------------------------------------------------------- checkAndRun decs = do- ++ putStrLn "\nFILE: "+ forM_ decs $ \s -> putStrLn $ show s++"\n"+ putStrLn "\nTYPE CHECKING: "- decs <- case runError $ typeCheckAll $ decs of+ decs <- case runError $ typeCheckAll decs of Left e -> error e- Right e -> do putStrLn "Type checking success!" >> return e- let (predicates, targets) = flip partition decs $ \x -> case x of - Predicate _ _ _ -> True+ Right e -> putStrLn "Type checking success!" >> return e+ let (defs,others) = flip partition decs $ \x -> case x of+ Define {} -> True _ -> False+ + sub = subst $ foldr (\a r -> r *** (predName a |-> subst r (predValue a))) mempty defs+ (predicates, targets) = flip partition others $ \x -> case x of+ Predicate {} -> True+ _ -> False - - putStrLn $ "\nAXIOMS: "- forM_ predicates $ \s -> putStrLn $ show s++"\n"- - putStrLn $ "\nTARGETS: "- forM_ targets $ \s -> putStrLn $ show s++"\n"+ putStrLn "\nAXIOMS: "+ forM_ (defs++predicates) $ \s -> putStrLn $ show s++"\n" + putStrLn "\nTARGETS: "+ forM_ targets $ \s -> putStrLn $ show s++"\n"+ let allTypes c = (predName c, predType c):predConstructors c- forM_ targets $ \target -> - case solver (concatMap allTypes predicates) $ predType target of+ predicates' = sub predicates+ targets' = sub targets+ forM_ targets' $ \target ->+ case solver (concatMap allTypes predicates') $ predType target of Left e -> putStrLn $ "ERROR: "++e- Right sub -> putStrLn $ + Right sub -> putStrLn $ "\nTARGET: \n"++show target ++"\n\nSOLVED WITH:\n" ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub main = do- [fname] <- getArgs- file <- readFile fname- let mError = runP decls (ParseState 0 mempty) fname file- decs <- case mError of- Left e -> error $ show e- Right l -> return l- checkAndRun decs + fnames <- getArgs+ case fnames of+ [] -> putStrLn "No file specified. Usage is \"caledon file.ncc\""+ [fname] -> do+ file <- readFile fname+ + let mError = runP decls emptyState fname file + decs <- case mError of+ Left e -> error $ show e+ Right l -> return l+ checkAndRun decs+ _ -> putStrLn "Unrecognized arguments. Usage is \"caledon file.ncc\""
Parser.hs view
@@ -1,115 +1,165 @@-{-# LANGUAGE RecordWildCards, TupleSections #-}+{-# LANGUAGE+ RecordWildCards+ #-}+ module Parser where import AST -import Data.Foldable as F (msum, forM_) import Data.Functor-import Text.Parsec.String+import Data.Functor.Identity import Text.Parsec-import Data.Monoid import Control.Monad (unless) import Text.Parsec.Language (haskellDef)-import Text.Parsec.Expr+import Text.Parsec.Expr +import Data.List import Data.Maybe+import Data.Monoid import qualified Text.Parsec.Token as P import qualified Data.Set as S+import Debug.Trace+import qualified Data.Foldable as F ----------------------------------------------------------------------- -------------------------- PARSER ------------------------------------- ----------------------------------------------------------------------- -data ParseState = ParseState { currentVar :: Integer, currentSet :: S.Set Name } +data ParseState = ParseState { currentVar :: Integer+ , currentSet :: S.Set Name+ , currentTable :: FixityTable + , currentOps :: [Name]+ }++data Fixity = FixLeft | FixRight | FixNone++data FixityTable = FixityTable { fixityBinary :: [(Integer,String, Assoc)] + , fixityPrefix :: [(Integer, String, Assoc)]+ , fixityPostfix :: [(Integer, String, Assoc)]+ , opLambdas :: [String]+ , strLambdas :: [String]+ , binds :: [(String,String,String)]+ }++emptyTable = FixityTable [] [] [] [] [] []+emptyState = (ParseState 0 mempty emptyTable [])++type Parser = ParsecT String ParseState Identity++modifySet :: (S.Set Name -> S.Set Name) -> ParseState -> ParseState modifySet f s = s { currentSet = f $ currentSet s }++modifyVar :: (Integer -> Integer) -> ParseState -> ParseState modifyVar f s = s { currentVar = f $ currentVar s } +getNextVar :: Parser String getNextVar = do v <- currentVar <$> getState modifyState $ modifyVar (+1)- return $ show v++"@?_?"+ return $ show v++"'" +decls :: Parser [Predicate] decls = do whiteSpace- lst <- many (query <|> defn <?> "declaration")+ lst <- many (topLevel <?> "declaration") eof return lst -query = do - reserved "query" - (nm,ty) <- named dec_pred+topLevel = fixityDef <|> query <|> defn++fixityDef = do + reserved "fixity"+ infixDef <|> lamDef+ topLevel+ +lamDef = do+ reserved "lambda"+ opLam <|> strLam++opLam = do + op <- operator+ modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { opLambdas = op:opLambdas ct} }+ +strLam = do+ op <- identifier+ modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { strLambdas = op:strLambdas ct} }+ +infixDef = do + -- I wish template haskell worked with record wild cards!+ (setFixity) <- (reserved "left" >> return (\b c -> b { fixityBinary = c AssocLeft $ fixityBinary b} )) + <|> (reserved "none" >> return (\b c -> b { fixityBinary = c AssocNone $ fixityBinary b} )) + <|> (reserved "right" >> return (\b c -> b { fixityBinary = c AssocRight $ fixityBinary b} )) + <|> (reserved "pre" >> return (\b c -> b { fixityPrefix = c undefined $ fixityPrefix b}))+ <|> (reserved "post" >> return (\b c -> b { fixityPostfix = c undefined $ fixityPostfix b}))+ n <- integer+ op <- operator -- <|> identifier+ + let modify assoc = insertBy (\(n,_,_) (m,_,_) -> compare n m) (n,op, assoc)+ modifyState $ \b -> b { currentTable = setFixity (currentTable b) modify+ , currentOps = op:currentOps b}+ ++query :: Parser Predicate+query = do+ reserved "query"+ (nm,ty) <- named decPred optional semi return $ Query nm ty -defn = do- reserved "defn" - (nm,ty) <- named dec_tipe- let more = do reserved "as"- lst <- flip sepBy1 (reservedOp "|") $ named dec_pred+defn :: Parser Predicate+defn = sound <|> unsound+ +sound = do+ reserved "defn"+ vsn True++unsound = do+ reserved "unsound" + vsn False + +vsn s = do + (nm,ty) <- named decTipe+ let more = do reservedOp "|"++ lst <- flip sepBy1 (reservedOp "|") $ do+ (nm,t) <- named decPred+ return (nm,t)+ optional semi- return $ Predicate nm ty lst+ return $ Predicate s nm ty lst none = do optional semi- return $ Predicate nm ty []- more <|> none <?> "definition"+ return $ Predicate s nm ty []+ letbe = do reserved "as"+ val <- pTipe+ return $ Define s nm val ty+ letbe <|> more <|> none <?> "definition" -pAtom = do reserved "_"- nm <- getNextVar- return $ var nm- <|> do r <- id_var- return $ var r- <|> do r <- identifier- mp <- currentSet <$> getState - return $ (if S.member r mp then var else cons) r - <|> (tpToTm <$> parens tipe)- <?> "atom"- -trm = parens trm - <|> do reservedOp "λ" <|> reservedOp "\\"- (nm,tp) <- parens anonNamed <|> anonNamed- reservedOp "."- tp' <- tmpState nm trm- return $ AbsImp nm tp tp'- <|> do reservedOp "?λ" <|> reservedOp "?\\"- (nm,tp) <- parens anonNamed <|> anonNamed- reservedOp "."- tp' <- tmpState nm trm- return $ Abs nm tp tp' - <|> do t <- pAtom- tps <- many $ (parens tipe) <|> (Atom <$> pAtom)- return $ rebuildSpine t tps- <?> "term" -fall = Forall ""-fallImp = ForallImp "" -table = [ [ binary (reservedOp "->" <|> reservedOp "→") fall AssocRight- , binary (reservedOp "=>" <|> reservedOp "⇒") fallImp AssocRight- ] - , [ binary (reservedOp "<-" <|> reservedOp "←") (flip fall) AssocLeft- , binary (reservedOp "<=" <|> reservedOp "⇐") (flip fallImp) AssocLeft ]- ]- where binary name fun assoc = Infix (name >> return fun) assoc- - -dec_tipe = (getId lower, ":")-dec_pred = (getId lower, "=")-id_var = getId $ upper <|> char '\''-dec_anon = (getId $ letter <|> char '\'' , ":")+decTipe :: (Parser String, String)+decTipe = (operator <|> getId lower, ":") +decPred :: (Parser String, String)+decPred = (operator <|> getId lower, "=")++idVar :: Parser String+idVar = getId $ upper++decVar :: (Parser String, String)+decVar = (idVar <|> getId lower, "=")++decAnon :: (Parser String, String)+decAnon = (getId $ letter , ":")++named :: (Parser a, String) -> Parser (a, Type) named (ident, sep) = do nm <- ident reservedOp sep- ty <- tipe+ ty <- pTipe return (nm, ty) -anonNamed = do- let (ident,sep) = dec_anon - nm <- ident- ty <- optionMaybe $ reservedOp sep >> tipe- nm' <- getNextVar- return (nm,fromMaybe (Atom $ var nm') ty)-+tmpState :: String -> Parser a -> Parser a tmpState nm m = do s <- currentSet <$> getState let b = S.member nm s@@ -118,34 +168,158 @@ unless b $ modifyState $ modifySet $ S.delete nm return r -tipe = buildExpressionParser table ( - parens tipe- <|> (Atom <$> trm)- <|> do (nm,tp) <- brackets anonNamed - tp' <- tmpState nm tipe- return $ Forall nm tp tp'- <|> do (nm,tp) <- braces anonNamed - tp' <- tmpState nm tipe- return $ ForallImp nm tp tp' - <|> do reservedOp "∀" <|> reserved "forall"- (nm,tp) <- parens anonNamed <|> anonNamed- reservedOp "."- tp' <- tmpState nm tipe- return $ Forall nm tp tp'- <|> do reservedOp "?∀" <|> reserved "?forall"- (nm,tp) <- parens anonNamed <|> anonNamed- reservedOp "."- tp' <- tmpState nm tipe- return $ ForallImp nm tp tp' - <?> "type")++++pChar = toNCCchar <$> charLiteral+pString = toNCCstring <$> stringLiteral+++pTipe = do+ FixityTable bin prefix postfix opLams strLams binds <- currentTable <$> getState - -P.TokenParser{..} = P.makeTokenParser $ mydef-mydef = haskellDef - { P.identStart = lower- , P.identLetter = alphaNum <|> oneOf "_'-/"- , P.reservedNames = ["defn", "as", "query", "forall", "?forall", "_"]- , P.caseSensitive = True- , P.reservedOpNames = ["->", "=>", "<=", "⇐", "⇒", "→", "<-", "←", ":", "|", "\\","?\\", "λ","?λ","∀","?∀", "."]- }-getId start = P.identifier $ P.makeTokenParser $ mydef { P.identStart = start }+ let getSnd [] = []+ getSnd (a:l) = l+ getFst (a:l) = a+ getFst [] = []+ + union l | all null l = []+ union lst = concatMap getFst lst:union (getSnd <$> lst)+ + reify ((a,op):(a',op'):l) r | a == a' = reify ((a',op'):l) (op:r)+ reify ((a,op):l) r = (op:r):reify l []+ reify [] [] = []+ reify [] r = [r]+ + anonNamed = do+ let (ident,sep) = decAnon+ nml <- many ident+ ty <- optionMaybe $ reservedOp sep >> ptipe+ return (nml,fromMaybe tyhole ty)++ binary fun assoc name = flip Infix assoc $ do + name+ fun <$> getNextVar+ + altPostfix = prefixGen id+ regPostfix bind = prefixGen (bind anonNamed <|>)+ + prefixGen bind opsl nms out = Prefix $ do+ (nml,tp) <- bind $ between + (choice $ (reserved <$> nms)++(reservedOp <$> opsl))+ (symbol ".") + (parens anonNamed <|> anonNamed)+ return $ \input -> foldr (flip out tp) input nml+ + table = [ [ altPostfix ["λ", "\\"] ["lambda"] Abs+ , altPostfix ["?λ", "?\\"] ["?lambda"] imp_abs+ , altPostfix ["∃"] ["exists"] exists+ , regPostfix angles ["??"] ["infer"] infer+ , regPostfix brackets ["∀"] ["forall"] forall+ , regPostfix braces ["?∀"] ["?forall"] imp_forall+ ]++[ altPostfix [op] [] (\nm t s -> Spine op [t,Abs nm tyhole s] ) | op <- opLams ]+ ++[ altPostfix [] [op] (\nm t s -> Spine op [t,Abs nm tyhole s] ) | op <- strLams ]+ , [ binary (forall) AssocRight $ reservedOp "->" <|> reservedOp "→" + , binary (const (~~>)) AssocRight $ reservedOp "=>" <|> reservedOp "⇒"+ ]+ , [ binary (flip . forall) AssocLeft $ reservedOp "<-" <|> reservedOp "←"+ , binary (flip . const (~~>)) AssocLeft $ reservedOp "<=" <|> reservedOp "⇐" + ]+ , [ binary (const ascribe) AssocNone $ reservedOp ":"+ ] ++ + ]+ ++union [ reify (binaryOther <$> bin) [] + , reify (unary Prefix <$> prefix) []+ , reify (unary Postfix <$> postfix) []+ ]+ + binaryOther (v,nm, assoc) = (v,flip Infix assoc $ do+ reservedOp nm+ return $ \a b -> Spine nm [a , b])++ unary fix (v,nm,_) = (v,fix $ do+ reservedOp nm+ return $ \a -> Spine nm [a])++ ptipe = buildExpressionParser (reverse $ table) terminal+ -- now terms must be parsed in pattern normal form+ + terminal = try trm <|> (myParens "terminal" ptipe) <|> ptipe <?> "terminal"+ + trm = do t <- pHead+ tps <- many pArg+ return $ rebuildSpine t tps+ <?> "term"++ + pHead = pParens pAt (pOp <|> ptipe <|> pAsc) "head"+ pArg = pParens (pAt <|> pTycon) (pOp <|> ptipe) "argument"+ + pParens anyAmount atLeast1 nm = anyAmount <|> pothers <?> nm+ where others = atLeast1 <|> anyAmount <|> pothers <?> nm+ pothers = myParens nm others++ pAsc = do+ v <- trm+ let asc = do+ reservedOp ":"+ t <- ptipe + return $ ascribe v t+ (asc <|> return v <?> "function") + + pOp = do operators <- currentOps <$> getState + choice $ flip map operators $ \nm -> do reserved nm + return $ var nm+ <?> "operator" + + pAt = do reserved "_"+ return $ hole+ <|> do r <- idVar+ return $ var r+ <|> do r <- identifier+ return $ var r+ <|> pChar+ <|> pString+ <?> "atom"++ pTycon = braces $ do+ (nm,ty) <- named decVar+ return $ tycon nm ty+ + myParens s m = between (symbol "(" <?> ("("++s)) (symbol ")" <?> (s++")")) m+ + ptipe <?> "tipe"++hole = var "#hole#"+tyhole = var "#hole#"+++reservedOperators = [ "->", "=>", "<=", "⇐", "⇒", "→", "<-", "←", + "\\", "?\\", + "λ","?λ", + "∀", "?∀",+ "?", + "??", "∃", "=", + ":", ";", "|"]+identRegOps = "_'-/" + +reservedNames = ["defn", "as", "query", "unsound"+ , "forall", "exists", "?forall", "lambda", "?lambda"+ , "_" , "infer", "fixity"]++mydef :: P.GenLanguageDef String ParseState Identity+mydef = haskellDef+ { P.identStart = oneOf $ "_"++['a'..'z']+ , P.identLetter = alphaNum <|> oneOf identRegOps+ , P.reservedNames = reservedNames+ , P.caseSensitive = True+ , P.reservedOpNames = reservedOperators+ , P.opStart = noneOf $ "# \n\t\r\f\v"++['a'..'z']++['A'..'Z']+ , P.opLetter = noneOf $ " \n\t\r\f\v"++['a'..'z']++['A'..'Z']+ }+P.TokenParser{..} = P.makeTokenParser mydef++getId :: Parser Char -> Parser String+getId start = P.identifier $ P.makeTokenParser mydef { P.identStart = start }
README.md view
@@ -1,5 +1,5 @@-Caledon Language-================+Caledon Language +==================================================================================== Caledon is a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer. @@ -8,9 +8,9 @@ * This is part of my masters thesis. Feedback would be appreciated. Considering this, it is still in the very early research stages. Syntax is liable to change, there will be bugs, and it doesn't yet have IO (I'm still working out how to do IO cleanly, but this WILL come). -* Its named caledon after the "New Caledonian Crow" - a crow which can make tools and meta tools. Since this language supports meta programming with holes, implicits, polymorphism, and dependent types, I thought this crow might be a good masscot. Also, file extensions are ".ncc"+* It's named caledon after the "New Caledonian Crow" - a crow which can make tools and meta tools. Since this language supports meta programming with holes, implicits, polymorphism, and dependent types, I thought this crow might be a good mascot. Also, file extensions are ".ncc" -* This language was inspired by twelf, haskell and agda. +* This language was inspired by twelf, haskell and agda. Goals -----@@ -21,7 +21,9 @@ * A language/system for conversing with the machine in a manner less one sided and instructional than regular programming. -Philosophies +* Make automated theorem proving intuitive. ++Philosophies ------------ * Metaprogramming should be easy and thus first class.@@ -30,93 +32,185 @@ * Metacode should be optionally typechecked, but well type checked. -* Metaprogramming should not require AST traversal. +* Metaprogramming should not require AST traversal. -* your programming language should be turing complete - totality checking is annoying.+* Your programming language should be turing complete - totality checking is annoying. * Syntax should be elegant. * Primitives should be minimal, libraries should be extensive. Learning a culture is easy if you speak the language. Learning a language by cultural immersion isn't as trivial. +Usage+-----++* To install from hackage:++```+> cabal install caledon+```++* To install directly from source:++```+> git clone git://github.com/mmirman/caledon.git+> cd caledon+> cabal configure+> cabal install+```++* To run:++```+> caledon file.ncc+```++* Unicode syntax is possible in emacs using: ++```+M-x \ TeX <ENTER>+```+ Features -------- -* Logic programming: Currently it uses a breadth first proof search. This is done for completeness, since the proof search is also used in type inference. This could (and should) possibly change in the future for the running semantics of the language. +* Logic programming: Currently it uses a breadth first proof search. This is done for completeness, since the proof search is also used in type inference. This could (and should) possibly change in the future for the running semantics of the language. -``` -defn num : atom- as zero = num+```+defn num : prop+ | zero = num | succ = num -> num -defn add : num -> num -> num -> atom- as add_zero = {N} add zero N N+defn add : num -> num -> num -> prop+ | add_zero = {N} add zero N N | add_succ = {N}{M}{R} add (succ N) M (succ R) <- add N M R -- we can define subtraction from addition! query subtract = add (succ (succ zero)) 'v (succ (succ (succ zero))) ```-* Higher order logic programming: like in twelf and lambda-prolog. This makes HOAS much easier to do. -``` -defn trm : atom- as lam = (trm -> trm) -> trm+* Some basic IO: Using unix pipes, this Caledon can be used more seriously. Somebody plz write a wrapper?++```+query main = run $ do + , putStr "hey!\n"+ , readLine (\A . do + , putStr A+ , putStr "\nbye!\n")+```++* Shell commands: ++```+defn ls : string -> string -> prop+ | ls-imp = [Args Out : string] + ls Args S <- cmd "ls" Args Out+```++* Higher order logic programming: like in twelf and lambda-prolog. This makes HOAS much easier to do.++```+defn trm : prop+ | lam = (trm -> trm) -> trm | app = trm -> trm -> trm -- we can check that a term is linear!-defn linear : (trm → trm) → atom- as linear_var = linear ( λ v . v )- | linear_app1 = {V}{F} linear (λ v . app (F v) V) +defn linear : (trm → trm) → prop+ | linear_var = linear ( λ v . v )+ | linear_lam = {N} linear (λ v . lam (λ x . N x v))+ ← [x] linear (λ v . N x v)+ | linear_app1 = {V}{F} linear (λ v . app (F v) V) ← linear F- | linear_app2 = ?∀ V . ?∀ F . linear (λ v . app F (V v)) + | linear_app2 = ?∀ V . ?∀ F . linear (λ v . app F (V v)) ← linear V ``` -* Polymorphism: This isn't sound. ie, atom : atom. The unsoundness shouldn't be too problematic, since types are used for proof search and to ensure progress and not for theorem proving. This language doesn't support totality, worlds, or universe checking yet, since it's goal is to be a query programming language.+* Calculus of Constructions: This is now consistent, and still has similar expressive power! Now any term must be terminating. Although term/proof search might not be+terminating, proof search can be used to search more intelligently for theorems in the term language. -``` -defn maybe : atom → atom- as nothing = {a} maybe a+```+defn maybe : prop → prop+ | nothing = {a} maybe a | just = {a} a → maybe a++infix 1 =:=+defn =:= : {a : prop} a -> a -> prop+ | eq = {a : prop} a =:= a++infix 0 /\+defn /\ : prop -> prop -> prop+ | and = {a : prop}{b : prop} a -> b -> a /\ b++infixr 0 |->+defn |-> : [a : prop] [b : prop] prop+ as \a : prop . \b : prop . [ha : a] b ``` +* Optional Unsound declarations: Embedding certain terms has never been easier! This way you can create recursive type definitions such as the well known "prop : prop". ++```+unsound tm : {S : tm ty} tm S → prop+ | ty = tm ty+ | ♢ = tm ty -> tm ty+ | Π = [T : tm ty] (tm T → tm T) → tm $ ♢ T+ | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)+ | raise = {T : tm ty} tm T → tm $ ♢ T+```+ * Indulgent type inferring nondeterminism: The entire type checking process is a nondeterministic search for a type check proof. This could be massively slow, but at least it is complete. The size of this search is bounded by the size of the types and not the whole program, so this shouldn't be too slow in practice. (function cases should be small). I'm working on adding search control primitives to make this more efficient. * Holes: types can have holes, terms can have holes. The same proof search that is used in semantics is used in type inference, so you can use the same computational reasoning you use to program to reason about whether the type checker can infer types! Holes get filled by a proof search on their type and the current context. Since the entire type checking process is nondeterministic, if they get filled by a wrong term, they can always be filled again. -``` -defn fsum_maybe : {a}{b} (a -> b -> atom) -> maybe a -> maybe b → atom- as fsum_nothing = {a}{b}[F : a -> b -> atom] maybe_fsum F nothing nothing- | fsum_just = {a}{b}[F : _ -> _ -> atom][av : a][bv : b]+```+defn fsum_maybe : {a}{b} (a -> b -> prop) -> maybe a -> maybe b → prop+ | fsum_nothing = {a}{b}[F : a -> b -> prop] maybe_fsum F nothing nothing+ | fsum_just = {a}{b}[F : _ -> _ -> prop][av : a][bv : b] maybe_fsum F (just av) (just bv) <- F av bv ``` * Implicit arguments: These are arguments that automagically get filled with holes when they need to be. They form the basis for typeclasses (records to be added), although they are far more general. This is also where the language is most modern and interesting. I'm curious to see what uses beyond typeclasses there are for these. -``` -defn functor : (atom → atom) → atom- as isFunctor = ∀ F . ({a}{b : _ } (a → b → atom) → F a → F b → atom) → functor F.+```+defn functor : (prop → prop) → prop+ | isFunctor = ∀ F . ({a}{b : _ } (a → b → prop) → F a → F b → prop) → functor F. -defn fsum : {F} functor F => {a}{b} (a → b → atom) → F a → F b → atom- as get_fsum = [F] functor F -> [FSUM][Foo][Fa][Fb] FSUM Foo Fa Fb -> fsum Foo Fa Fb+defn fsum : {F} functor F => {a}{b} (a → b → prop) → F a → F b → prop+ | get_fsum = [F] functor F -> [FSUM][Foo][Fa][Fb] FSUM Foo Fa Fb -> fsum Foo Fa Fb -defn functor_maybe : functor maybe -> atom.- as is_functor_maybe = functor_maybe (isFunctor fsum_maybe).+defn functor_maybe : functor maybe -> prop.+ | is_functor_maybe = functor_maybe (isFunctor fsum_maybe). --- this syntax is rather verbose for the moment. I have yet to add proper records or typeclass syntax sugar.+-- this syntax is rather verbose for the moment. I have yet to add typeclass syntax sugar. ``` -* Optional unicode syntax: Monad m ⇒ ∀ t : goats . m (λ x : t . t → t). - * implication : "a -> b" or "a → b" or "a <- b" or "a ← b" - * implicits: "a => b" or "a ⇒ b" - * Quantification: "[x:A] t" or "∀ x:A . t" or "forall x:A . t"- * abstraction: "λ x . t" or "\x.t"- * Quantified implicits: "{x:A} t" or "?∀ x:A . t" or "?forall x:A . t"+* Arbitrary operator fixities: combined with the calculus of constructions, you can nearly do agda style syntax (with a bit of creativity)! +```+defn bool : prop+ | true = bool+ | false = bool -Usage------+defn if : bool -> bool+ as \b . b -* To install, cabal install+infix 1 |:|+defn |:| : {a : prop} a -> a -> (a -> a -> a) -> a+ as ?\t : prop . \a b. \f : t -> t -> t. f a b -* To run, caledon file.ncc+infix 0 ==>+defn ==> : {a : prop} bool -> ((a -> a -> a) -> a) -> a -> prop+ | thentrue = [a:prop][f : (a -> a -> a) -> a] (true ==> f) (f (\A B. A))+ | thenfalse = [a:prop][f : (a -> a -> a) -> a] (false ==> f) (f (\A B. B))++defn not : bool -> bool -> prop+ as \v . if v ==> false |:| true++```++* Optional unicode syntax: Monad m ⇒ ∀ t : goats . m (λ x : t . t → t).+ * implication : "a -> b" or "a → b" or "a <- b" or "a ← b"+ * implicits: "a => b" or "a ⇒ b" or "a <= b" or "a ⇐ b"+ * Quantification: "[x:A] t" or "∀ x:A . t" or "forall x:A . t"+ * abstraction: "λ x . t" or "\x.t"+ * Quantified implicits: "{x:A} t" or "?∀ x:A . t" or "?forall x:A . t"+ * implicit abstraction: "?λ x . t" or "?\x.t"
− Solver.hs
@@ -1,356 +0,0 @@-{-# LANGUAGE - FlexibleContexts, - FlexibleInstances,- TupleSections- #-}-module Solver where--import AST-import Choice--import Control.Monad (void)-import Control.Applicative ((<|>), empty)-import Control.Monad.Error (ErrorT, throwError, runErrorT, lift, unless, when)-import Control.Monad.Error.Class-import Control.Monad.State (StateT, get, put, runStateT, modify)-import Control.Monad.State.Class-import Control.Monad.Writer (WriterT, runWriterT, listens)-import Control.Monad.Writer.Class-import Control.Monad.RWS (RWST, RWS, get, put, tell, runRWST, runRWS, ask)-import Control.Monad.Identity (Identity, runIdentity)-import Control.Monad.Trans.Class-import Data.Monoid-import Data.Functor-import Data.Traversable (forM)-import Data.Foldable as F (msum, forM_, foldr', foldl', fold, Foldable, foldl')-import qualified Data.Map as M-import qualified Data.Set as S-import Debug.Trace---------------------------------------------------------------------------------------------- UNIFICATION ------------------------------------------------------------------------------------------------------type VarGen = StateT Integer Choice---class HasVar a where- getV :: a -> Integer- setV :: Integer -> a -> a-instance HasVar Integer where - getV = id- setV a _ = a- -unifyAll envE env [] = return mempty-unifyAll envE env (a:l) = do- s <- appendErr ("IN: "++show a) $ unify envE env a- s' <- unifyAll envE env (subst s l)- return $ s *** s'--unify :: M.Map Name Tp -> M.Map Name Tp -> Constraint Tm -> VarGen Substitution-unify envE env constraint@(a :=: b) = - let badConstraint = throwError $ show constraint- unify'' = unify envE env- unify' = unify envE- doUntoBoth m n = F.foldl' act (return mempty) (zip m n)- act prev (mt,nt) = do- sub <- prev - sub' <- unify' (subst sub env) $ subst sub (tpToTm mt :=: tpToTm nt)- return $ sub *** sub'-- in case a :=: b of- _ :=: _ | a > b -> unify' env $ b :=: a- AbsImp n ty t :=: _ -> do- (v',s) <- solve $ (M.toList envE)++(M.toList env) :|- ty- unify' env $ subst s (subst (n |-> v') t) :=: (subst s b)- Abs n ty t :=: Abs n' ty' t' -> do - s <- unify'' $ tpToTm ty :=: tpToTm ty'- nm <- getNew- s' <- unify' (subst s $ M.insert nm ty env) $ subst (M.insert n (var nm) s) t :=: subst (M.insert n' (var nm) s) t'- return $ s *** M.delete nm s'- Abs n ty t :=: _ -> do - nm <- getNew- s <- unify' (M.insert nm ty env) $ subst (n |-> var nm) t :=: rebuildSpine b [Atom $ var nm]- return $ M.delete nm s- - Spine (Var a) [] :=: Spine (Var a') [] | a == a' -> - return mempty- Spine (Var a) [] :=: _ | not (M.member a env) && (not $ S.member a $ freeVariables b) -> - return $ a |-> b- Spine (Var a) m :=: Spine (Var a') n | a == a' && M.member a env && length m == length n -> -- the var has the same rule whether it is quantified or not.- doUntoBoth m n- - Spine (Cons c) _ :=: Spine (Cons c') _ | c /= c' -> - badConstraint- Spine (Cons c) m :=: Spine (Cons c') n | length m == length n -> - doUntoBoth m n- - Spine (Var x) n :=: Spine (Cons c) m | not $ M.member x env -> do -- Gvar-Const- us <- forM n $ const $ getNew- usty <- forM n $ const $ Atom <$> var <$> getNew- xs <- forM m $ const $ Var <$> getNew- let l = Spine (Cons c) $ (\xi -> Atom $ Spine xi $ Atom <$> var <$> us) <$> xs- s = x |-> foldr' (\(v,ty) t -> Abs v ty t) l (zip us usty)- s' <- unify' (subst s env) $ subst s (a :=: b)- return $ (s *** s')- - Spine (Var a) n :=: Spine (Var a') m | a == a' && length m == length n -> do -- Gvar-Gvar - same- h <- getNew- let act (xi, yi) next = do- vi <- getNew- sub' <- catchError (Just <$> unify'' (tpToTm xi :=: tpToTm yi)) $ \_ -> return Nothing- (xs,zs,sub) <- next- case sub' of- Just sub' -> return (vi:xs,vi:zs, sub' *** sub) - Nothing -> return (vi:xs,zs, sub)- - (xs,zs,sub) <- foldr' act (return (mempty, mempty, mempty)) (zip n m)- - let base = Spine (Var h) (Atom <$> var <$> zs)- f' = foldr' (\v t -> Abs v undefined t) base xs- return (sub *** a |-> f')- - Spine (Var f) xs :=: Spine (Var g) ys | f /= g -> do -- Gvar-Gvar - diff- h <- getNew- let act xi next = do- sub' <- flip catchError (const $ return Nothing) $ msum $ flip fmap ys $ \yi -> do- sub <- unify'' (tpToTm xi :=: tpToTm yi)- return $ Just (yi,sub)- (zs,sub) <- next- case sub' of- Just (yi,sub') -> return ((xi,yi):zs, sub' *** sub) - Nothing -> return (zs, sub)- (zs,sub) <- foldr' act (return (mempty, mempty)) xs- - let toVar (Atom (Spine (Var x) [])) = do- t <- getNew- return (x, Atom $ var t)- toVar _ = badConstraint- - xs' <- mapM toVar xs- ys' <- mapM toVar ys- - let baseF = Spine (Var h) (fst <$> zs)- f' = foldr' (\(v,vt) t -> Abs v vt t) baseF xs'- - baseG = Spine (Var h) (snd <$> zs)- g' = foldr' (\(v,vt) t -> Abs v vt t) baseG ys'- return (sub *** (f |-> f' *** g |-> g'))- - _ :=: _ -> badConstraint--genUnifyEngine env consts = do- s <- unifyAll env mempty consts- return $ finishSubst s- -recSubst :: (Eq b, Subst b) => Substitution -> b -> b-recSubst s f = fst $ head $ dropWhile (not . uncurry (==)) $ iterate (\(_,b) -> (b,subst s b)) (f,subst s f) --finishSubst s = recSubst s s--finishSubstWith w s = case M.lookup w s of- Just (Spine (Var v) []) -> finishSubst $ M.insert v (var w) (M.delete w s)- _ -> s------------------------------------------------------------------------------------------------- LOGIC ENGINE ---------------------------------------------------------------------------------------------------------type Reification = VarGen (Tm,Substitution)-type Deduction = VarGen Substitution--unifier :: [(Name,Tp)] -> Tp -> Reification -unifier cons t = do- t' <- case t of- Atom k -> return k- _ -> empty- i <- get- let isAtom (Atom _) = True- isAtom _ = False- msum $ flip map (filter (isAtom . snd) cons) $ \(x,Atom con) -> do- s <- genUnifyEngine (M.fromList cons) [con :=: t']- return $ (var x,s) --left :: Judgement -> Reification-left judge@((x,f):context :|- r) = case f of- Atom _ -> unifier [(x,f)] r- ForallImp nm t1 t2 -> do- nm' <- getNew- y <- getNew- (m,so) <- left $ (y,subst (nm |-> var nm') t2):context :|- r- let n = case M.lookup nm' so of- Nothing -> var nm'- Just a -> a- s = seq n $ M.delete nm' so- s' <- natural (subst s $ (x,f):context) $ subst s (n,t1)- return (subst s' $ subst (y |-> Spine (Var x) []) m, s *** s')- - Forall nm t1 t2 -> do- nm' <- getNew- y <- getNew- (m,so) <- left $ (y,subst (nm |-> var nm') t2):context :|- r- let n = case M.lookup nm' so of- Nothing -> var nm'- Just a -> a- s = seq n $ M.delete nm' so- s' <- natural (subst s $ (x,f):context) $ subst s (n,t1)- return (subst s' $ subst (y |-> Spine (Var x) [Atom n]) m, s *** s')---right :: Judgement -> Reification-right judge@(context :|- r) = case r of- Atom _ -> unifier context r- ForallImp nm t1 t2 -> do- nm' <- getNew- (v,s) <- solve $ (nm', t1):context :|- subst (nm |-> cons nm') t2- return $ (tpToTm $ ForallImp nm' t1 (Atom v), s)- Forall nm t1 t2 -> do- nm' <- getNew- (v,s) <- solve $ (nm', t1):context :|- subst (nm |-> cons nm') t2- return $ (tpToTm $ Forall nm' t1 (Atom v), s)--solve :: Judgement -> Reification-solve judge@(context :|- r) = right judge <|> (msum $ useSingle (\f ctx -> left $ f:ctx :|- r) context)- where useSingle f lst = sw id lst- where sw _ [] = []- sw placeOnEnd (a:lst) = f a (placeOnEnd lst):sw (placeOnEnd . (a:)) lst--natural :: [(Name, Tp)] -> (Tm,Tp) -> Deduction-natural cont (tm,ty) = do- let env = M.fromList cont- (_, constraints) <- runWriterT $ checkTerm env tm ty- genUnifyEngine (M.fromList cont) constraints- --solver :: [(Name,Tp)] -> Tp -> Either String [(Name, Tm)]-solver axioms t = case runError $ runStateT (solve $ axioms :|- t) 0 of- Right ((tm,s),_) -> Right $ ("query" , varsToCons tm):(recSubst s $ map (\a -> (a,var a)) $ S.toList $ freeVariables t)- where varsToCons = subst $ M.fromList $ map (\(a,_) -> (a,cons a)) axioms- Left s -> Left $ "reification not possible: "++s- ------------------------------------------------------------------------------------------ Type Checker ---------------------------- -------------------------------------------------------------------type Environment = M.Map Name Tp-type NatDeduct = WriterT [Constraint Tm] (StateT Integer Choice)--checkVariable :: Environment -> Variable -> Tp -> NatDeduct Tp-checkVariable env v t = case v of- Cons nm -> case env ! nm of- Nothing -> error $ nm++" was not found in the environment in "++show v- Just t' -> do- tell [tpToTm t' :=: tpToTm t]- return t'- Var nm -> case env ! nm of- Nothing -> do - (t'',s) <- lift $ solve $ M.toList env :|- t- tell $ map (\(s,t) -> var s :=: t ) $ M.toList s - tell [var nm :=: t'']- return t- -- I'm not sure this makes sense at all.- -- in the mean time, assume there is only one use of each unbound variable- Just t' -> do- tell [tpToTm t' :=: tpToTm t]- return t'- -checkTerm :: Environment -> Tm -> Tp -> NatDeduct (Tm,Tp)-checkTerm env v t = case v of- Spine a l -> do- nm <- (++'α':show a) <$> getNew- tv1 <- (++':':show a) <$> getNew- tv2l <- forM l $ \b -> do- bty <- getNew- nm' <- getNew- t' <- checkTerm env (tpToTm b) $ Atom $ var bty- return (nm',t')- - tv1' <- checkVariable env a $ Atom $ var $ tv1- - tell [ tpToTm tv1' :=: tpToTm (foldr (\(nm,b) tp -> Forall nm (snd b) tp) t tv2l ) ]- return $ (Spine a $ map (Atom . fst . snd) tv2l, t)- - AbsImp nm ty tm -> do - ty' <- checkTipe env ty- v1 <- (++':':'<':nm) <$> getNew- nm' <- (++'@':nm) <$> getNew- v2 <- (++':':'>':nm) <$> getNew- tell [ tpToTm (ForallImp v1 ty $ Atom $ var v2) :=: tpToTm t ]- ((tm',t'),constraints) <- listen $ checkTerm (M.insert nm' ty env) (subst (nm |-> var nm') tm) $ Atom $ var v2- s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)- tell $ map (\(s,t) -> var s :=: t ) $ M.toList s- let s' = s *** nm' |-> var nm - return $ (AbsImp nm ty' $ subst s' tm' , ForallImp v1 ty t')- - Abs nm ty tm -> do- ty' <- checkTipe env ty- v1 <- (++':':'<':nm) <$> getNew- nm' <- (++'@':nm) <$> getNew- v2 <- (++':':'>':nm) <$> getNew-- tell [ tpToTm (Forall v1 ty $ Atom $ var v2) :=: tpToTm t ]- - ((tm',t'),constraints) <- listen $ checkTerm (M.insert nm' ty env) (subst (nm |-> var nm') tm) $ Atom $ var v2- s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)- tell $ map (\(s,t) -> var s :=: t ) $ M.toList s- let s' = s *** nm' |-> var nm - return $ (Abs nm ty' $ subst s' tm' , Forall v1 ty t')- -checkTipe :: Environment -> Tp -> NatDeduct Tp-checkTipe env v = case v of- Atom tm -> do- (a,t) <- checkTerm env tm atom- return $ Atom a- ForallImp nm ty t -> do- Forall nm' ty' t' <- checkTipe env (Forall nm ty t)- return $ ForallImp nm' ty' t'- Forall nm ty t -> do- ty' <- checkTipe env ty- nm' <- (++'*':nm) <$> getNew- (a,constraints) <- listen $ checkTipe (M.insert nm' ty env) $ subst (nm |-> var nm') t- s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)- - tell $ map (\(s,t) -> var s :=: t ) $ M.toList s- let s' = s *** nm' |-> var nm - return $ Forall nm ty' (subst s' a)- -getCons tm = case tm of- Spine (Cons t) _ -> return t- Abs _ _ t -> getCons t- _ -> throwError $ "can't place a non constructor term here: "++ show tm--getPred tp = case tp of- Atom t -> getCons t- Forall _ _ t -> getPred t- ForallImp _ _ t -> getPred t---- need to do a topological sort of types and predicates.--- such that types get minimal correct bindings-checkType :: Environment -> Name -> Tp -> Choice Tp-checkType env base ty = fmap fst $ flip runStateT 0 $ appendErr ("FOR: "++show ty) $ do- con <- getPred ty- unless (null base || con == base) - $ throwError $ "non local name \""++con++"\" expecting "++base- (ty',constraints) <- runWriterT $ checkTipe env ty- - s <- appendErr ("CONSTRAINTS: "++show constraints) $ genUnifyEngine env constraints- - return $ subst s ty'--typeCheckPredicate :: Environment -> Predicate -> Choice Predicate-typeCheckPredicate env (Query nm ty) = appendErr ("in query : "++show ty) $ do- ty' <- checkType env "" ty- return $ Query nm ty-typeCheckPredicate env pred@(Predicate pnm pty plst) = appendErr ("in\n"++show pred) $ do- pty' <- appendErr ("in name: "++ pnm ++" : "++show pty) $- checkType env "atom" pty- plst' <- forM plst $ \(nm,ty) -> - appendErr ("in case: " ++nm ++ " = "++show ty) $ (nm,) <$> checkType env pnm ty- return $ Predicate pnm pty' plst'--typeCheckAll :: [Predicate] -> Choice [Predicate]-typeCheckAll preds = forM preds $ typeCheckPredicate assumptions- where assumptions = M.fromList $ - ("atom", atom): -- atom : atom is a given.- ("forall", Atom $ Abs "_" (Atom $ Abs "_" atom $ cons "atom") $ cons "atom"): -- atom : atom is a given.- concatMap (\st -> case st of- Query _ _ -> []- _ -> (predName st, predType st):predConstructors st) preds
+ TopoSortAxioms.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE BangPatterns #-} +module TopoSortAxioms where++import AST++import Data.Graph+import qualified Data.Set as S+getVars val ty = concatMap (\nm -> [nm,"#v:"++nm])+ $ filter (not . flip elem (map fst consts)) + $ S.toList $ freeVariables val `S.union` freeVariables ty ++topoSortAxioms :: [(Maybe Name, Bool, Name,Term,Type)] -> [(Maybe Name, Bool, Name,Term,Type)]+topoSortAxioms axioms = map ((\((fam,s,val,ty),n,_) -> (fam,s,n,val,ty)) . v2nkel) vlst+ where (graph, v2nkel, _) = + graphFromEdges $ map (\(fam,s,nm,val,ty) -> ((fam,s,val,ty), nm , getVars val ty)) axioms+ -- note! this doesn't check that there are no cycles!+ vlst = reverse $ topSort graph+ ++seqList :: [a] -> (b -> b) +seqList [] = id+seqList ((!_):l) = seqList l++finalizeList a = seqList a a++topoSort :: (a -> (Name,S.Set Name)) -> [a] -> [a]+topoSort producer scons = finalizeList $ map ((\(a,_,_) -> a) . v2nkel) $ topSort graph+ where res = finalizeList $ map (\a -> let (nm, e) = producer a in (a,nm,S.toList e)) scons+ (graph,v2nkel,_) = graphFromEdges res
caledon.cabal view
@@ -1,10 +1,10 @@ Name: caledon -Version: 0.0.0.0+Version: 2.0.0.0 -Description: a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.+Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. -Synopsis: a dependently typed, polymorphic, higher order logic programming language+Synopsis: a logic programming language based on the calculus of constructions Homepage: https://github.com/mmirman/caledon @@ -28,7 +28,7 @@ executable caledon main-is: Main.hs- other-modules: Solver, Choice, Parser+ other-modules: HOU, Choice, Parser, AST, TopoSortAxioms, Context Build-depends: base >= 4.0 && < 5.0, mtl >= 2.0 && < 3.0,@@ -36,11 +36,12 @@ containers >= 0.4 && < 1.0, transformers >= 0.3 && < 1.0 - Extensions: DeriveFunctor,- FlexibleContexts,+ Extensions: FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,- PatternGuards, RecordWildCards,- TupleSections,+ BangPatterns, TypeSynonymInstances+ + ghc-options: -O2 -optc-O3 -funfolding-use-threshold=16 -fspec-constr-count=10 -fdo-lambda-eta-expansion+
+ examples/.DS_Store view
binary file changed (absent → 6148 bytes)
+ examples/._.DS_Store view
binary file changed (absent → 82 bytes)
+ examples/circtype.ncc view
@@ -0,0 +1,5 @@+unsound a : b av -> prop+ | av = a bv++unsound b : a bv -> prop+ | bv = b av
+ examples/circtype_bad.ncc view
@@ -0,0 +1,5 @@+defn a : b av -> prop+ | av = a bv++defn b : a bv -> prop+ | bv = b av
+ examples/coc.ncc view
@@ -0,0 +1,15 @@+fixity lambda .λ+fixity lambda Π++defn tm : prop+ | p = tm+ | t = tm+ | .λ = tm → (tm → tm) → tm+ | Π = tm → (tm → tm) → tm++fixity none 0 ::+defn :: : tm -> tm -> prop+ | p_t = p :: t+ | lam_pi = [A : tm][T : tm -> tm][B : tm -> tm]+ ([x] x :: A -> T x :: B x )+ -> (.λ x : A . T x) :: (Π x : A . B x)
+ examples/evenodd.ncc view
@@ -0,0 +1,12 @@+defn nat : prop+ | z = nat+ | s = nat -> nat++defn odd : nat -> prop+ | odd/one = odd (s z)+ | odd/n = [A] even A -> odd (s A)++defn even : nat -> prop+ | even/zero = even z+ | even/succ = [B] odd B -> even (s B)+
+ examples/implicit.ncc view
@@ -0,0 +1,16 @@+defn identity : prop -> prop+ | cons = {f : prop} f -> identity f++infix 1 =:=+defn =:= : {a : prop} a -> a -> prop+ | eq = {a : prop} a =:= a++defn getIdent : {f : prop} identity f -> f -> prop+ as ?\f : prop . \id : identity f . \v : f . (cons v) =:= id+++-- this demonstrates three ways of doing this+defn getIdent' : {foo : prop} identity foo -> foo -> prop+ | getIdentity1 = {f}{V:f} getIdent' {foo = f} (cons V) V+ | getIdentity2 = {f}{V:f} getIdent' (cons V : identity f) V+ | getIdentity3 = {f}{V:f} (getIdent' : identity f -> f -> prop) (cons V) V
+ examples/infer.ncc view
@@ -0,0 +1,15 @@+defn nat : prop+ | zero = nat+ | succ = nat -> nat++defn even : nat -> prop+ | even/zero = even zero+ | even/odd = [N : nat] odd N -> even (succ N)++defn odd : nat -> prop+ | odd/zero = odd (succ zero)+ | odd/even = [N] even N -> odd (succ N)+++defn funny : [N ] odd N -> prop+ | funnyodd = funny (<N> N) (odd/even zero even/zero)
+ examples/linear.ncc view
@@ -0,0 +1,6 @@+defn trm : prop+ | lam = (trm -> trm) -> trm+ | app = trm -> trm -> trm++defn linear : (trm -> trm) -> prop+ | linear_var = linear (λ V : trm . V )
+ examples/prelude.ncc view
@@ -0,0 +1,211 @@+---------------+-- builtins ---+---------------+defn char : prop -- builtin++defn putChar : char -> prop -- builtin+ | putCharImp = [A] putChar A++-- for sequencing io actions+fixity left 1 ,+defn io : prop+ | do = io+ | , = io -> prop -> io +++defn run : io -> prop+ | runDo = run do+ | runSeq = [A][B] run (A , B) <- run A + <- B++defn readLine : (string -> io) -> prop -- builtin + | readLineImp = [Foo : string -> io] [A : string] readLine Foo <- run (Foo A)++defn string : prop+ as list char++---------------+-- searches ---+---------------+defn any : {A : prop} (A -> prop) -> prop+ | is = [a : prop][V : a][F : a -> prop] F V -> any { A = a } F+++defn openAny : [A][F : A -> prop] any F -> [V : A] F V -> prop+ | openAnyDef = [A][F : A -> prop][V : A][FV : F V] openAny A F (is A V F FV) V FV++defn sopen : {a : prop }{f : a -> prop} [V : a] {fv : f V} (exists v : a . f v) -> prop + as ?\a : prop . ?\ f : a -> prop . \vt : a . ?\ fv : f vt . \an : (exists v : a . f v) . open a f an vt fv+++fixity lambda free+defn free : [A : prop] (A -> prop) -> prop+ as \a : prop . any { A = a }++--------------------------+--- useful combinators ---+--------------------------+fixity right 0 $+defn $ : {at bt:prop} (at -> bt) -> at -> bt+ as ?\ at bt . \ f . \a . f a+++fixity right 0 @+defn @ : {at bt ct:prop} (bt -> ct) -> (at -> bt) -> at -> ct+ as ?\at bt ct : prop . \f : bt -> ct . \ g : at -> bt . \ a : at . f (g a)++defn flip : {at bt ct : prop} (at -> bt -> ct) -> bt -> at -> ct+ as ?\ at bt ct : prop . \ foo . \ b . \ a . foo a b++-------------------+--- Constraints ---+-------------------+fixity none 1 =:=+defn =:= : {Q} Q -> Q -> prop+ | eq = [a : prop][b:a] (=:=) {Q = a} b b++-- searching for these is SLOW+fixity none 0 /\+defn /\ : prop -> prop -> prop+ | and = [a b : prop] a -> b -> a /\ b++fixity none 0 \/+defn \/ : prop -> prop -> prop+ | or1 = [a b:prop] a -> a \/ b+ | or2 = [a b:prop] b -> a \/ b++fixity left 0 ==+-- currently we can't do any inference inside of definitional signatures+defn == : {q : prop} (q -> prop) -> q -> prop + as ?\q . \foo : q -> prop . \v : q . foo v+++--------------+--- concat ---+--------------+defn concatable : [M : prop] (M -> M -> M -> prop) -> prop+ | concatableNat = concatable natural add+ | concatableList = [A] concatable (list A) concatList+++-- it correctly infers 169, and M (but it eta expands Foo when it infers it) !!+fixity right 3 +++defn ++ : {M}{Foo}{cm : concatable M Foo} M -> M -> M -> prop+ | ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] + (++) {Foo = Foo} M1 M2 M3 + <- concatable M Foo + <- Foo M1 M2 M3 ++-------------+--- Order ---+-------------+defn orderable : [M : prop] (M -> M -> prop) -> prop+ | orderableNatural = orderable natural lte-nat++fixity right 3 =< +defn =< : {M : prop}{Foo: M -> M -> prop}{co : orderable M Foo} M -> M -> prop+ | ooimp = [M][Foo : M -> M -> prop] [M1 M2 : M] + (=<) {M = M} M1 M2 + <- orderable M Foo+ <- Foo M1 M2++---------------------+--- Unary Numbers ---+---------------------+defn natural : prop+ | zero = natural+ | succ = natural -> natural++query findSat0 = free A : natural . A =:= zero++defn add : natural -> natural -> natural -> prop+ | add_z = [N] add zero N N+ | add_s = [N M R] add N M R -> add (succ N) M (succ R)++query add0 = add (succ zero) zero (succ zero)++query add1 = succ zero ++ zero == succ zero++-- sub N M R is N - M = R+defn sub : natural -> natural -> natural -> prop+ | sub_by_add = [N M R] sub N M R <- add M R N+++defn lte-nat : natural -> natural -> prop+ | leqZero = [B] lte-nat zero B+ | leqSucc = [A B] lte-nat (succ A) (succ B) <- lte-nat A B++fixity none 3 <+defn < : natural -> natural -> prop+ | ltZero = [B] zero < succ B+ | ltSucc = [A B] succ A < succ B <- A < B++query add2 = exists A : natural . add (succ zero) zero A++query add3 = any $ add (succ zero) zero++query findSat1 = succ zero =< succ (succ zero)++query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)++-------------+--- Maybe ---+-------------++defn maybe : prop -> prop+ | nothing = {a} maybe a+ | just = {a} a -> maybe a++-------------+--- Lists ---+-------------+defn list : prop -> prop+ | nil = {a} list a+ | cons = {a} a -> list a -> list a++defn concatList : {A} list A -> list A -> list A -> prop+ | concatListNil = [T][L:list T] concatList {A = T} nil L L+ | concatListCons = [T][A B C : list T][V:T] concatList (cons V A) B (cons V C) <- concatList A B C++----------------+--- printing ---+----------------++defn putStr : string -> prop+ | putStr_Nil = putStr $ nil {a = char}+ | putStr_Cons = [v:char][l: string] + putStr $ cons {a = char} v l + <- putChar v+ <- putStr l++----------------+--- Booleans ---+----------------+defn bool : prop+ | true = bool+ | false = bool++defn if : bool -> bool+ as \b . b++fixity none 1 |:|+defn |:| : {t:prop} t -> t -> (t -> t -> t) -> t+ as ?\t : prop . \a b : t. \f : t -> t -> t. f a b+++fixity none 0 ==>+defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop+ | thentrue = [a : prop][f: _ -> a] (true ==> f) (f (\a1 a2 : a . a1))+ | thenfalse = [b : prop][f: _ -> b] (false ==> f) (f (\a1 a2 : b . a2))++defn not : bool -> bool -> prop+ as \zq . if zq ==> false |:| true++defn ismain : prop + as run $ do + , putStr "hey!\n"+ , readLine (\A . do + , putStr A+ , putStr "\nbye!\n")++-- query main = ismain
+ examples/record.ncc view
@@ -0,0 +1,18 @@+defn functor : (prop -> prop) -> prop+ | functorImp = {f : prop -> prop} ({a : prop }{b : prop} (a -> b -> prop) -> f a -> f b -> prop) -> functor f++defn fmap : {f} functor f => {a}{b} (a -> b -> prop) -> f a -> f b -> prop+ | getFMap = {f : prop -> prop}{fm : {a}{b} (a -> b -> prop) -> f a -> f b -> prop}+ {a : prop}{b : prop}{foo : a -> b -> prop}{fa : f a }{fb : f b }+ fm foo fa fb -> fmap foo fa fb+{-+defn identity : prop -> prop+ | cons = {a} a -> identity a++defn mapIdentity : {a}{b} (a -> b -> prop) -> identity a -> identity b -> prop+ | mapIdentityImp = {foo}{a}{b} foo a b -> mapIdentity foo (cons a) (cons b)+++defn functorIdentity : functor identity+ as functorImp mapIdentity+-}
+ examples/substitution.ncc view
@@ -0,0 +1,2 @@+defn example : [ax : prop] ax -> prop+ as eximp = [atx : prop] example prop atx
+ examples/syntax.ncc view
@@ -0,0 +1,38 @@++infixr -2 ->+defn -> : [a b: prop] prop+ as \a : prop . \b : prop . [ha : a] b++infixr -2 →+defn → : [a b: prop] prop + as (->)++infixl -3 <-+defn <- : [a b: prop] prop+ as \a : prop . \b : prop . b -> a++infixl -1 ←+defn → : [a b: prop] prop + as (<-)++infixr -2 =>+defn => : [a b: prop] prop+ as \a : prop . \b : prop . {ha : a} b++infixr -2 ⇒+defn ⇒ : [a b: prop] prop+ as (=>)++infixl -1 <=+defn <= : [b a : prop] prop+ as \a : prop . \b : prop . b => a++infixl -1 ⇐+defn ⇐ : [a b: prop] prop+ as (<=)+++infixr 0 $+defn $ : {a b:prop} (a -> b) -> a -> b+ as ?\at bt : prop . \f . \ a : at . f a+
+ examples/test.ncc view
@@ -0,0 +1,12 @@++defn num : prop+ | zero = num+ | succ = num → num++defn add : num → num → num → prop+ | add-z = [N] add zero N N+ | add-s = [N][M][R] add N M R → add (succ N) M (succ R)++query sum-1 = exists v . add (succ zero) (succ zero) v+-- query sum-2 = exists v . add (succ zero) v (succ (succ (succ zero)))+-- query sum-3 = exists v . add zero (succ zero) v
+ examples/universe.ncc view
@@ -0,0 +1,30 @@+fixity right 0 $+defn $ : {a b:prop} (a -> b) -> a -> b+ as ?\At Bt :prop . \ F . \A . F A ++fixity pre 1 ♢+fixity lambda Π +fixity lambda lam ++{-+for the moment, circularly defined types are allowed! this violates consistency. +If a dependency analysis is done, and types are checked in order, this will become safe!+-}++{- +the implicit argument is pretty much always intialized to ty+tm basically says+t in tm S T has type T where T has sort S.+-}+unsound tm : {S : tm ty} tm S → prop+ | ty = tm ty+ | ♢ = tm ty -> tm ty+ | Π = [T : tm ty] (tm T → tm T) → tm $ ♢ T+ | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)+ | raise = {T : tm ty} tm T → tm $ ♢ T++defn isTm : {S : tm ty} {A : tm S} tm A -> prop+ | hasValue = [S : tm ty][T : tm S][V : tm T] isTm V++query whattype0 = isTm (Π A : ty . A)+query whattype1 = isTm (lam A : ty . A)
− linear.ncc
@@ -1,6 +0,0 @@-defn trm : atom- as lam = (trm -> trm) -> trm- | app = trm -> trm -> trm--defn linear : (trm -> trm) -> atom- as linearVar = linear ( λ v : trm . v )
+ media/.DS_Store view
binary file changed (absent → 6148 bytes)
+ media/._.DS_Store view
binary file changed (absent → 82 bytes)
+ media/logo.png view
binary file changed (absent → 5107 bytes)
+ media/logo.svg view
@@ -0,0 +1,90 @@+<?xml version="1.0" encoding="UTF-8" standalone="no"?>+<!-- Created with Inkscape (http://www.inkscape.org/) -->++<svg+ xmlns:dc="http://purl.org/dc/elements/1.1/"+ xmlns:cc="http://creativecommons.org/ns#"+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"+ xmlns:svg="http://www.w3.org/2000/svg"+ xmlns="http://www.w3.org/2000/svg"+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"+ width="64px"+ height="64px"+ id="svg2985"+ version="1.1"+ inkscape:version="0.48.2 r9819"+ sodipodi:docname="drawing.svg"+ inkscape:export-filename="/Users/matt/projects/caledon/logo.png"+ inkscape:export-xdpi="332.57077"+ inkscape:export-ydpi="332.57077">+ <defs+ id="defs2987" />+ <sodipodi:namedview+ id="base"+ pagecolor="#ffffff"+ bordercolor="#666666"+ borderopacity="1.0"+ inkscape:pageopacity="0.0"+ inkscape:pageshadow="2"+ inkscape:zoom="22.378814"+ inkscape:cx="28.592229"+ inkscape:cy="27.598954"+ inkscape:current-layer="layer1"+ showgrid="true"+ inkscape:document-units="px"+ inkscape:grid-bbox="true"+ inkscape:window-width="1523"+ inkscape:window-height="1193"+ inkscape:window-x="788"+ inkscape:window-y="93"+ inkscape:window-maximized="0" />+ <metadata+ id="metadata2990">+ <rdf:RDF>+ <cc:Work+ rdf:about="">+ <dc:format>image/svg+xml</dc:format>+ <dc:type+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />+ <dc:title></dc:title>+ </cc:Work>+ </rdf:RDF>+ </metadata>+ <g+ id="layer1"+ inkscape:label="Bird"+ inkscape:groupmode="layer"+ style="display:inline">+ <path+ style="fill:#000000;fill-opacity:1;stroke:none"+ d="m 18.882872,40.622514 c -1.882884,0.373654 -6.450071,9.787095 -7.791963,9.741122 -1.1680346,-0.04002 -3.7909684,-1.403639 -3.2727272,-2 1.3120082,-1.509782 7.8598822,-9.136821 9.8181822,-9.636363 -1.933103,1.207068 -7.205249,4.964178 -7.257339,4.112511 -0.03501,-0.57236 6.65605,-5.997644 8.893702,-7.567057 0.435723,-0.595323 0.06006,-1.659204 0.508523,-2.522314 1.078658,-2.075958 6.244498,-7.049902 11.619378,-9.209575 3.937841,-1.582259 4.653035,-0.511028 7.668737,-1.779652 0.757625,-0.318712 0.763785,-2.008075 0.02154,-2.160275 -2.700878,-0.553826 -4.390193,-0.702891 -6.611684,-1.976858 2.313795,-0.105189 4.380405,0.04745 5.893645,0.283499 -2.171461,-1.193482 -3.406608,-1.04635 -5.93833,-1.255741 -0.342151,-0.745613 5.728812,-1.158736 6.92448,-0.89678 1.374408,-1.748876 2.506529,-1.943285 4.21727,-1.815105 2.409291,0.180521 3.425495,1.468441 4.45141,5.372928 0.992305,3.776574 -0.06537,12.931591 -7.300427,18.32351 -2.8304,2.109352 -8.844305,3.097519 -10.340542,3.242974 -0.487885,0.04743 -0.231151,0.46574 -1.015401,1.149959 -0.575888,0.502434 6.519236,9.013849 6.519236,9.013849 l -1.163293,0.04776 c 0,0 -6.398156,-8.119769 -6.784269,-8.554688 -0.960981,-1.082449 -0.370467,-1.321021 -2.379025,-1.266572 -0.759544,0.02059 -1.624673,0.770728 -1.365175,1.553149 0.442101,1.33299 3.647077,8.449929 3.647077,8.449929 l -1.029238,0 c 0,0 -2.404917,-5.42565 -3.669892,-7.4839 -0.460686,-0.749586 -0.85396,-1.055399 -0.763051,-1.782672 0.181818,-1.454545 -0.150754,-1.569475 -0.964607,-1.603989 -0.653173,-0.0277 -1.538764,0.02241 -2.536217,0.220351 z"+ id="path2995"+ inkscape:connector-curvature="0"+ sodipodi:nodetypes="ssscscssssccccsssssccsssccssss" />+ </g>+ <g+ inkscape:groupmode="layer"+ id="layer2"+ inkscape:label="hammer"+ style="display:inline">+ <path+ style="display:inline;fill:#768181;fill-opacity:1;stroke:none"+ d="m 35.647554,14.202694 c -0.858119,2.442447 -3.971389,15.79193 -3.971389,15.79193 L 29.559208,29.3819 c 0,0 0.07894,-0.163559 4.672387,-15.501739 0.247963,-1.21401 -1.108041,-2.821158 -3.488232,-0.525961 0.401775,-1.92004 2.621814,-2.979331 4.630496,-2.261381 0.661583,0.236465 1.124554,0.424004 1.160416,0.969684 0.06052,0.920809 0.937037,0.53754 1.184156,0.06729 0.263623,-0.501655 1.853631,0.236441 1.291679,1.694383 -0.430872,1.117869 -1.782822,1.513491 -1.963352,0.880835 -0.281657,-0.987048 -0.974388,-0.793403 -1.399204,-0.502316 z"+ id="path3773"+ inkscape:connector-curvature="0"+ sodipodi:nodetypes="cccccsssssc" />+ </g>+ <g+ inkscape:groupmode="layer"+ id="layer3"+ inkscape:label="beak top"+ style="display:inline">+ <path+ sodipodi:nodetypes="cccc"+ inkscape:connector-curvature="0"+ id="use3809"+ d="m 39.090905,19.600911 c 0,0 -4.256138,-0.524151 -6.611684,-1.976858 2.313795,-0.105189 5.893645,0.283499 5.893645,0.283499 z"+ style="opacity:0.92000002000000003;fill-opacity:1;stroke:none;fill:#000000" />+ </g>+</svg>
− prelude.ncc
@@ -1,18 +0,0 @@-defn num : atom- as zero = num- | succ = num → num--defn add : num → num → num → atom- as add_z = {N} add zero N N- | add_s = {N}{M}{R} add N M R → add (succ N) M (succ R)--defn sub : num → num → num → atom- as sub_with_add : {N}{M}{R} sub N M R ← add N R M--defn maybe : atom → atom- as nothing = {a} maybe a- | just = {a} a → maybe a--defn list : atom → atom- as nil = {a} nil a- | cons = {a} a → list a → list a
− test.ncc
@@ -1,11 +0,0 @@-defn num : atom- as zero = num- | succ = num → num--defn add : num → num → num → atom- as add-z = [N] add zero N N- | add-s = [N][M][R] add N M R → add (succ N) M (succ R)--query sum-1 = add (succ zero) (succ (succ zero)) 'v-query sum-2 = add (succ zero) 'v (succ (succ (succ zero)))-query sum-3 = add zero (succ zero) 'v