caledon 3.2.1.0 → 3.2.2.0
raw patch · 34 files changed
+246/−1007 lines, 34 filesdep ~lens
Dependency ranges changed: lens
Files
- AST.hs +12/−22
- HOU.hs +140/−112
- Main.hs +4/−2
- Parser.hs +3/−4
- README.md +0/−254
- Substitution.hs +85/−52
- caledon.cabal +2/−2
- examples/circtype.ncc +0/−5
- examples/circtype_bad.ncc +0/−5
- examples/coc.ncc +0/−15
- examples/divergent.ncc +0/−10
- examples/double.ncc +0/−15
- examples/implicit.ncc +0/−16
- examples/linear.ncc +0/−6
- examples/listTest.ncc +0/−11
- examples/meta.ncc +0/−23
- examples/nondet.ncc +0/−21
- examples/readlinein.ncc +0/−15
- examples/syntax.ncc +0/−38
- examples/tactics.ncc +0/−23
- examples/test.ncc +0/−25
- examples/universe.ncc +0/−29
- media/logo.png binary
- media/logo.svg +0/−90
- prelude/booleans.ncc +0/−29
- prelude/combinators.ncc +0/−14
- prelude/concatable.ncc +0/−18
- prelude/io.ncc +0/−39
- prelude/list.ncc +0/−10
- prelude/logic.ncc +0/−38
- prelude/maybe.ncc +0/−6
- prelude/naturals.ncc +0/−35
- prelude/prelude.ncc +0/−14
- prelude/strings.ncc +0/−9
AST.hs view
@@ -55,12 +55,21 @@ , _dataPriority :: Integer , _dataSound :: Bool } -+ deriving Show data FlatPred = FlatPred { _predData :: PredData , _predName :: Name+ , _predValue :: Maybe Term , _predType :: Type , _predKind :: Kind }+instance Show FlatPred where+ show (FlatPred a b c d e) = "FlatPred ("+ ++show a++") ("+ ++show b++") ("+ ++show c++") ("+ ++show d++") ("+ ++show e++") ("+ $(makeLenses ''PredData) $(makeLenses ''FlatPred) $(makeLenses ''Decl)@@ -201,6 +210,7 @@ instance FV FlatPred where freeVariables p = freeVariables (p^.predType) `S.union` freeVariables (p^.predKind)+ `S.union` freeVariables (p^.predValue) -------------------------------- --- Builtin Spines and types ---@@ -223,9 +233,6 @@ ascribe a t = Spine ("#ascribe#") [t, a] dontcheck t = Spine ("#dontcheck#") [t] 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]@@ -244,27 +251,10 @@ , ("#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"]) ] -anonymous ty = ((False,10000),ty)+anonymous ty = ((False,0),ty) envSet = S.fromList $ map fst consts
HOU.hs view
@@ -3,7 +3,8 @@ PatternGuards, UnicodeSyntax, BangPatterns,- TupleSections+ TupleSections,+ FlexibleContexts #-} module HOU where @@ -32,6 +33,8 @@ import System.IO.Unsafe import Data.IORef +(.∀) = Bind Forall+ {-# NOINLINE levelVar #-} levelVar :: IORef Int levelVar = unsafePerformIO $ newIORef 0@@ -107,7 +110,7 @@ checkFinished cval = throwTrace 0 $ "ambiguous constraint: " ++show cval unifySearch :: SCons -> CONT_T b Env UnifyResult-unifySearch (a :@: b) return | b /= atom = rightSearch a b $ newReturn return+unifySearch (a :@: b) return | b /= atom && b /= kind = rightSearch a b $ newReturn return unifySearch _ return = return Nothing newReturn return cons = return $ case cons of@@ -128,24 +131,48 @@ r -> return r unifyOne _ return = return Nothing +impForallPrefix (Spine "#imp_forall#" [ty, Abs nm _ l]) = nm:impForallPrefix l+impForallPrefix _ = []++impAbsPrefix (Spine "#imp_abs#" (ty:(Abs nm _ l):r)) = nm:impAbsPrefix l+impAbsPrefix _ = []+ unifyEq cons@(a :=: b) = case (a,b) of (Spine "#ascribe#" (ty:v:l), b) -> return $ Just (mempty, [rebuildSpine v l :=: b], False) (b,Spine "#ascribe#" (ty:v:l)) -> return $ Just (mempty, [b :=: rebuildSpine v l], False) - (Spine "#imp_forall#" [ty, l], b) -> vtrace 1 "-implicit-" $ do+ (Spine "#imp_forall#" [ty, Abs nm _ l], Spine "#imp_forall#" [ty',Abs nm' _ l']) | nm == nm' -> do+ a <- getNewWith "@aL"+ modifyCtxt $ addToTail "-implicit-" Forall a ty+ return $ Just (mempty, [Abs nm ty l `apply` var a :=: Abs nm' ty' l' `apply` var a , ty :=: ty'], False)++ -- this case doesn't cover the case where we have + -- ?\/x : t . A =:= ?\/x :t . A, but "x in t" isn't necessarily solvable.+ + -- this is solvable if we defer instantiation of x if we see x in b.+ -- by these rules though, ?\/x y : t1 . A =:= ?\/ y x : t1 . A is not provable.+ -- this appears to be fine for the moment, although it won't imediately be derivable from the implicit CoC + -- where such a statement is true. + (Spine "#imp_forall#" [ty, l@(Abs nm _ _)], b) | not $ elem nm $ impForallPrefix 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], False)- (b, Spine "#imp_forall#" [ty, l]) -> vtrace 1 "-implicit-" $ do+ + (b, Spine "#imp_forall#" [ty, l@(Abs nm _ _)]) | not $ elem nm $ impForallPrefix b -> vtrace 1 "-implicit-" $ do a' <- getNewWith "@aR" modifyCtxt $ addToTail "-implicit-" Exists a' ty return $ Just (mempty, [b :=: l `apply` var a' , var a' :@: ty], False)-- (Spine "#imp_abs#" (ty:l:r), b) -> vtrace 1 ("-imp_abs- : "++show a ++ "\n\t"++show b) $ do+ + (Spine "#imp_abs#" (ty:(Abs nm _ l):r), Spine "#imp_abs#" (ty':(Abs nm' _ l'):r')) | nm == nm' -> do+ a <- getNewWith "@aL"+ modifyCtxt $ addToTail "-implicit-" Forall a ty+ return $ Just (mempty, [rebuildSpine (Abs nm ty l) (var a:r) :=: rebuildSpine (Abs nm' ty' l') (var a:r'), ty :=: ty'], False)+ + (Spine "#imp_abs#" (ty:(l@(Abs nm _ _)):r), b) | not $ elem nm $ impAbsPrefix 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], False)- (b, Spine "#imp_abs#" (ty:l:r)) -> vtrace 1 "-imp_abs-" $ do+ (b, Spine "#imp_abs#" (ty:(l@(Abs nm _ _)):r)) | not $ elem nm $ impAbsPrefix b -> 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], False)@@ -471,7 +498,8 @@ foralls <- getForalls exists <- getExists let env = M.union foralls constants- + + isBound a = M.member a exists || M.member a env isFixed a = isChar a || M.member a env getFixedType a | isChar a = Just $ anonymous $ var "char"@@ -484,24 +512,13 @@ Nothing -> Nothing sameFamily (_, (_,Abs{})) = False- sameFamily ("pack",_) = "#exists#" == nm- sameFamily (_,(_,s)) = getFamily s == nm+ sameFamily ("pack",_) = "exists" == nm -- if we are searching for exists, try to pack!+ sameFamily (_,(_,s)) = ( getFamily s == nm ) && + all isBound (S.toList $ freeVariables s) 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 :: ContextMap- searchMap = M.union env $ case searchMaps of- [] -> mempty- a:l -> foldr (M.intersection) a l- - return $ filter sameFamily $ M.toList searchMap- -}- return $ filter sameFamily $ M.toList constants ++ M.toList foralls if all isFixed $ S.toList $ S.union (freeVariables m) (freeVariables goal)@@ -518,7 +535,7 @@ res <- Just <$> ls (nm,targ) if sequ then (if not $ null cg then (appendErr "" (F.asum $ reverse cg) <|>) else id) $ - (appendErr ""$ ret res) <|> inter [] l+ (appendErr "" $ ret res) <|> inter [] l else inter (ret res:cg) l @@ -574,14 +591,15 @@ addToEnv (∃) x' ty $ do var x' .@. ty return $ var x'- + Spine "#ascribe#" (t:v:l) -> do (v'',mem) <- regenWithMem v- t <- withKind $ checkType t+ t <- withKind $ checkType t t'' <- regenAbsVars t- v' <- checkType v'' t- r <- getNewWith "@r"- Spine _ l' <- addToEnv (∀) r t'' $ checkType (Spine r l) ty+ v' <- checkType v'' t+ r <- getNewWith "@r"+ Spine _ l' <- addToEnv (.∀) r t'' $ checkType (Spine r l) ty+ return $ rebuildSpine (rebuildFromMem mem v') l' Spine "#dontcheck#" [v] -> do@@ -589,7 +607,6 @@ Spine "#infer#" [_, Abs x tyA tyB ] -> do tyA <- withKind $ checkType tyA- x' <- getNewWith "@inf" addToEnv (∃) x' tyA $ do var x' .@. tyA@@ -597,45 +614,50 @@ Spine "#imp_forall#" [_, Abs x tyA tyB] -> do tyA <- withKind $ checkType tyA- tyB <- addToEnv (∀) (check "imp_forall" x) tyA $ checkType tyB ty+ 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 $ + 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'+ Spine "#imp_forall#" [_, Abs x' tyA' tyF'] | x == x' || "" == x' -> do tyA <- withKind $ checkType tyA tyA ≐ tyA'- addToEnv (∀) (check "impabs1" x) tyA $ do+ addToEnv (.∀) (check "impabs1" x) tyA $ do imp_abs x tyA <$> checkType sp tyF'- _ -> do+ -- here this acts like "infers" since we can always initialize a ?\ like an infers!+ tyA <- withKind $ checkType tyA+ x' <- getNewWith "@inf"+ addToEnv (∃) x' tyA $ do+ var x' .@. tyA+ checkType (subst (x |-> var x') sp) ty +{-+ _ -> 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-+ 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+ 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]))+ Abs x tyA <$> (addToEnv (.∀) (check "abs2" x) tyA $ checkType sp (Spine e [var x])) Spine nm [] | isChar nm -> do ty ≐ Spine "char" [] return sp@@ -686,32 +708,32 @@ --------------------------------- --- Generalize Free Variables --- ---------------------------------+type Graph k = M.Map k (S.Set k)+ +isGen [] = False+isGen (c:s) = elem c ['A'..'Z']+getGenTys sp = S.filter isGen $ freeVariables sp {- Employ the use order heuristic, where variables are ordered by use on the same level in terms.--S A F (F A) = {(F,{A,F}), (A,{})} [A,F,S]-S F A (F A) = {(F,{A,F}), (A,{F})} [F,A,S]-S F (F A S) = {(F,{}), (A,{}), (S,{A,F})} [S,F,A]-S A (F S A) = {(F,{}), (A,{})} -}- buildOrderGraph :: S.Set Name -- the list of variables to be generalized -> S.Set Name -- the list of previously seen variables -> Spine - -> State (M.Map Name (S.Set Name)) (S.Set Name) -- an edge in the graph if a variable has occured before this one.+ -> State (Graph Name) -- an edge in the graph if a variable has occured before this one.+ (S.Set Name) -- the generalizable variables that occured in said term. buildOrderGraph gen prev s = case s of Abs nm t v -> do- prev' <- buildOrderGraph gen prev t- prev'' <- buildOrderGraph (S.delete nm gen) prev v- return $ S.union prev' prev''- Spine "#tycon#" [Spine _ [l]] -> buildOrderGraph gen prev l - Spine s [t, l] | elem s ["#exists#", "#forall#", "#imp_forall#", "#imp_abs#"] -> do prev1 <- buildOrderGraph gen prev t- prev2 <- buildOrderGraph gen prev l+ prev2 <- buildOrderGraph (S.delete nm gen) prev v return $ S.union prev1 prev2- + Spine s [t, l] | elem s [ "#imp_abs#"] -> do+ prev1 <- buildOrderGraph gen prev t+ prev2 <- buildOrderGraph gen prev l+ return $ S.union prev1 prev2 + Spine "#tycon#" [Spine _ [l]] -> buildOrderGraph gen prev l + Spine nm l -> do mp <- get prev' <- if S.member nm gen@@ -728,22 +750,20 @@ mp <- get let prevs = mp M.! nm put $ M.insert nm (S.union prev'' prevs) mp- return $ S.insert nm $ S.union prev prev'' - else return prev''- -getGenTys sp = S.filter isGen $ freeVariables sp- where isGen (c:s) = elem c ['A'..'Z']+ return $ S.singleton nm+ else return mempty+ generateBinding sp = foldr (\a b -> imp_forall a ty_hole b) sp orderedgens where genset = getGenTys sp genlst = S.toList genset (_,graph) = runState (buildOrderGraph genset mempty sp) (M.fromList $ map (,mempty) genlst)- orderedgens = topoSortComp (\a -> (a, graph M.! a)) genlst+ orderedgens = vtrace 0 ("ARG_GRAPH: "++show graph) $ topoSortComp (\a -> (a, graph M.! a)) genlst ---------------------- --- type inference --- -----------------------typeInfer :: ContextMap -> ((Bool,Integer),Name,Spine,Type) -> Choice (Term,Type, ContextMap)+typeInfer :: ContextMap -> ((Bool,Integer),Name,Term,Type) -> Choice (Term, Type, ContextMap) typeInfer env (seqi,nm,val,ty) = (\r -> (\(a,_,_) -> a) <$> runRWST r (M.union envConsts env) emptyState) $ do ty <- return $ alphaConvert mempty mempty ty val <- return $ alphaConvert mempty mempty val@@ -751,16 +771,15 @@ (ty,mem') <- regenWithMem ty (val,mem) <- vtrace 1 ("ALPHAD TO: "++show val) $ regenWithMem val - (val,constraint) <- vtrace 1 ("REGENED TO: "++show val) $ - checkFullType val ty+ (val,constraint) <- vtrace 1 ("REGENED TO: "++show val) $ 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+ let resV = rebuildFromMem mem $ unsafeSubst sub $ eta_expandAll (snd <$> env) val+ resT = rebuildFromMem mem' $ unsafeSubst sub $ eta_expandAll (snd <$> env) ty - vtrace 0 ("RESULT: "++nm++" : "++show resV) $+ vtrace 0 ("result: "++show resV) $ return $ (resV,resT, M.insert nm (seqi,resV) env) unsafeSubst s (Spine nm apps) = let apps' = unsafeSubst s <$> apps in case s ! nm of @@ -772,53 +791,63 @@ --- the public interface --- ---------------------------- --- type FlatPred = [((Maybe Name,Bool,Integer,Bool),Name,Type,Kind)]--typeCheckAxioms :: Bool -> [FlatPred] -> Choice Substitution+typePipe verbose lt (b,nm,ty,kind) = do+ (ty,kind,lt) <- mtrace verbose ("Inferring: " ++nm) $ + typeInfer lt (b,nm, ty,kind) -- type infer+ (ty,kind,lt) <- mtrace verbose ("Elaborating: " ++nm) $ + typeInfer lt (b,nm, ty,kind) -- elaborate+ (ty,kind,lt) <- mtrace verbose ("Checking: " ++nm) $ + typeInfer lt (b,nm, ty,kind) -- type check+ return (ty,kind,lt)+ +typeCheckAxioms :: Bool -> [FlatPred] -> Choice (Substitution, Substitution) typeCheckAxioms verbose 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 p = case p ^. predName of - '#':'v':':':_ -> False- _ -> True- - unsound = not . (^. predSound)+ let unsound = not . (^. predSound) - tys = M.fromList $ map (\p -> ( p^.predName, ((p^.predSequential,p^.predPriority),p^.predType))) $ filter notval lst- uns = S.fromList $ map (^.predName) $ filter unsound $ filter notval lst+ tys = M.fromList $ map (\p -> ( p^.predName, ((p^.predSequential,p^.predPriority),p^.predType))) lst+ uns = S.fromList $ map (^.predName) $ filter unsound $ lst - inferAll :: (ContextMap, [FlatPred], [FlatPred]) -> Choice ([FlatPred],ContextMap)- inferAll (l , r, []) = return (r,l)+ inferAll :: ((Substitution,ContextMap), [FlatPred], [FlatPred]) -> Choice ([FlatPred],(Substitution, ContextMap))+ inferAll (l, r, []) = return (r,l) inferAll (_ , r, p:_) | p^.predName == tipeName = throwTrace 0 $ tipeName++" can not be overloaded" inferAll (_ , r, p:_) | p^.predName == atomName = throwTrace 0 $ atomName++" can not be overloaded"- inferAll (l , r, p:toplst) = do+ inferAll ((lv,lt) , r, p:toplst) = do let fam = p^.predFamily b = p^.predSequential i = p^.predPriority nm = p^.predName- val = p^.predType- ty = p^.predKind- (val,ty,l') <- appendErr ("can not infer type for: "++nm++" : "++show val) $ - mtrace verbose ("Checking: " ++nm) $ - vtrace 0 ("\tVAL: " ++show val - ++"\n\t:: " ++show ty) $- typeInfer l ((b,i),nm, generateBinding val,ty) -- constrain the breadth first search to be local!- + val = p^.predValue+ ty = p^.predType+ kind = p^.predKind+ + (ty,kind,lt) <- appendErr ("can not infer type for: "++nm++" : "++show ty) $ + mtrace verbose "\nCompiling: type" $ vtrace 0 ("\t : " ++show ty ++"\n\t :: " ++show kind) $ + typePipe verbose lt ((b,i),nm, generateBinding ty,kind) -- constrain the breadth first search to be local!+ + val <- case val of+ Just val -> appendErr ("can not infer type for: \n"++nm++" : "++show ty ++"\nnm = "++show val ) $ + mtrace verbose "\nCompiling: value " $ vtrace 0 ("\t : " ++show val ++"\n\t:: " ++show ty) $ + Just <$> typePipe verbose lt ((b,i),nm, generateBinding val,ty) + Nothing -> return Nothing + -- 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 + unless (fam == Nothing || Just (getFamily ty) == fam)+ $ throwTrace 0 $ "not the right family: need "++show fam++" for "++nm ++ " = " ++show ty - let resp = p & predType .~ val & predKind .~ ty- inferAll $ case nm of- '#':'v':':':nm' -> (sub' <$> l', resp:r , sub <$> toplst) - where sub' (b,a)= (b, sub a)- sub :: Subst a => a -> a- sub = subst $ nm' |-> ascribe val (dontcheck ty) - _ -> (l', resp:r, toplst)+ let resp = p & predType .~ ty + & predKind .~ kind + inferAll $ case val of+ Just (val,_,_) -> ((M.insert nm val lv, sub' <$> lt), (resp & predValue .~ Just val) :r , sub <$> toplst) + where sub' (b,a) = (b, sub a)+ sub :: (Show a, Subst a) => a -> a+ sub = subst $ nm |-> ascribe val (dontcheck ty) + _ -> ((lv, lt), resp:r, toplst) - (lst',l) <- inferAll (tys, [], topoSortAxioms True lst)+ (lst',(lv,lt)) <- inferAll ((mempty,tys), [], topoSortAxioms True lst) let doubleCheckAll _ [] = return () doubleCheckAll l (p:r) = do@@ -826,7 +855,7 @@ val = p^.predType ty = p^.predKind - let usedvars = freeVariables val `S.union` freeVariables ty+ let usedvars = freeVariables val `S.union` freeVariables ty `S.union` freeVariables val unless (S.isSubsetOf usedvars l) $ throwTrace 0 $ "Circular type:" ++"\n\t"++nm++" : "++show val ++" : "++show ty@@ -838,7 +867,7 @@ doubleCheckAll (S.union envSet uns) $ topoSortAxioms False lst' - return $ snd <$> l + return $ (lv, snd <$> lt) topoSortAxioms :: Bool -> [FlatPred] -> [FlatPred] topoSortAxioms accountPot axioms = showRes $ topoSortComp (\p -> (p^.predName,) @@ -846,7 +875,6 @@ -- unsound can mean this causes extra cyclical things to occur $ (if accountPot && p^.predSound then S.union (getImplieds $ p^.predName) else id) $ S.fromList - $ concatMap (\nm -> [nm,"#v:"++nm]) $ filter (not . flip elem (map fst consts)) $ S.toList $ freeVariables p ) axioms @@ -865,8 +893,7 @@ $ catMaybes $ map (`M.lookup` family2nmsMap) $ S.toList - $ getImpliedFamilies - $ p^.predType+ $ S.union (getImpliedFamilies $ p^.predType) (fromMaybe mempty $ freeVariables <$> p^.predValue) )) <$> axioms getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap)@@ -884,22 +911,23 @@ typeCheckAll :: Bool -> [Decl] -> Choice [Decl] typeCheckAll verbose preds = do - tyMap <- typeCheckAxioms verbose $ toAxioms True preds+ (valMap, tyMap) <- typeCheckAxioms verbose $ toAxioms True preds let newPreds (Predicate t nm _ cs) = Predicate t nm (tyMap M.! nm) $ map (\(b,(nm,_)) -> (b,(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)+ newPreds (Define t nm _ _) = Define t nm (valMap M.! nm) (tyMap M.! nm) return $ newPreds <$> preds toAxioms :: Bool -> [Decl] -> [FlatPred]-toAxioms b = concat . zipWith toAxioms' [0..]+toAxioms b = concat . zipWith toAxioms' [1..] where toAxioms' j (Predicate s nm ty cs) = - (FlatPred (PredData (Just $ atomName) False j s) nm ty tipe)- :zipWith (\(sequ,(nm',ty')) i -> (FlatPred (PredData (Just nm) sequ i False) nm' ty' atom)) cs [0..]- toAxioms' j (Query nm val) = [(FlatPred (PredData Nothing False j False) nm val atom)]- toAxioms' j (Define s nm val ty) = (if b then ((FlatPred (PredData Nothing False j s) ("#v:"++nm) val ty):) else id)- [(FlatPred (PredData Nothing False j False) nm ty kind)] + (FlatPred (PredData (Just $ atomName) False j s) nm Nothing ty tipe)+ :zipWith (\(sequ,(nm',ty')) i -> (FlatPred (PredData (Just nm) sequ i False) nm' Nothing ty' atom)) cs [0..]+ toAxioms' j (Query nm val) = [(FlatPred (PredData Nothing False j False) nm Nothing val atom)]+ toAxioms' j (Define s nm val ty) = [ FlatPred (PredData Nothing False j s) nm (Just val) ty kind]+ + toSimpleAxioms :: [Decl] -> ContextMap toSimpleAxioms l = M.fromList $ (\p -> (p^.predName, ((p^.predSequential, p^.predPriority), p^.predType)))
Main.hs view
@@ -28,11 +28,12 @@ putStrLn "\nFILE: " forM_ decs $ \s -> putStrLn $ show s++"\n" - when verbose $ putStrLn "\nTYPE CHECKING: "+ when verbose $ putStrLn "\nCOMPILING: " decs <- case runError $ typeCheckAll verbose decs of Left e -> error e- Right e -> do when verbose $ putStrLn "Type checking success!"+ Right e -> do when verbose $ putStrLn "DONE: compilation success!\n" return e+ let (defs,others) = flip partition decs $ \x -> case x of Define {} -> True _ -> False@@ -49,6 +50,7 @@ when verbose $ do putStrLn "\nTARGETS: " forM_ targets $ \s -> putStrLn $ show s++"\n"+ let predicates' = sub predicates targets' = sub targets
Parser.hs view
@@ -28,7 +28,7 @@ import Debug.Trace import qualified Data.Foldable as F -import Control.Lens +import Control.Lens hiding (noneOf) ----------------------------------------------------------------------- -------------------------- PARSER -------------------------------------@@ -230,7 +230,6 @@ table = [ [ altPostfix ["λ", "\\"] ["lambda"] Abs , altPostfix ["?λ", "?\\"] ["?lambda"] imp_abs- , altPostfix ["∃"] ["exists"] exists , regPostfix angles ["??"] ["infer"] infer , regPostfix brackets ["∀"] ["forall"] forall , regPostfix braces ["?∀"] ["?forall"] imp_forall@@ -312,12 +311,12 @@ "λ","?λ", "∀", "?∀", "?", - "??", "∃", "=", + "??", "=", ":", ";", "|"] identRegOps = "_'-/" reservedNames = ["defn", "as", "query", "unsound"- , "forall", "exists", "?forall", "lambda", "?lambda"+ , "forall", "?forall", "lambda", "?lambda" , "_" , "infer", "fixity"] mydef :: P.GenLanguageDef String ParseState Identity
− README.md
@@ -1,254 +0,0 @@-Caledon Language -====================================================================================--Caledon is a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.--Background-------------* 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).--* 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.--Goals--------* Make logic programming less repetative--* A logic programming language that is good at defining DSLs--* A language/system for conversing with the machine in a manner less one sided and instructional than regular programming.--* Make automated theorem proving intuitive. --Philosophies---------------* Metaprogramming should be easy and thus first class.--* User facing code should not crash - runtime code should be type checked.--* Metacode should be optionally typechecked, but well type checked.--* Metaprogramming should not require AST traversal.--* 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.--```-defn num : prop- | zero = num- | succ = num -> num--defn add : num -> num -> num -> prop- | add_zero = add zero N N- | add_succ = add (succ N) M (succ R) <- add N M R---- we can define subtraction from addition!-defn subtract : num -> num -> num -> prop- as \a b c : num . add b c a--```--* 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")-```--* 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) → 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 V-```--* 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 : prop → prop- | nothing = maybe A- | just = A → maybe A--infix 1 =:=-defn =:= : A -> A -> prop- | eq = (=:=) {A = A} V V--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 -> prop) -> maybe A -> maybe B → prop- | fsum_nothing = [F : A -> B -> prop] maybe_fsum F nothing nothing- | fsum_just = [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 : (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 → 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 -> prop.- | is_functor_maybe = functor_maybe (isFunctor fsum_maybe).---- this syntax is rather verbose for the moment. I have yet to add typeclass syntax sugar.-```--* Nondeterminism control: You can now control what patterns to match against sequentially versus in concurrently. This gives you massive control over program execution, and in the future might be implemented with REAL threads!--```-defn runBoth : bool -> prop- >| run0 = runBoth A - <- putStr "tttt "- <- A =:= true-- | run1 = runBoth A- <- putStr "vvvv"- <- A =:= true-- | run2 = runBoth A- <- putStr "qqqq"- <- A =:= true-- >| run3 = runBoth A- <- putStr " jjjj"- <- A =:= false--query main = runBoth false---- main should print out something along the lines of "tttt vvqvqvqq jjjj"-```---* 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--defn if : bool -> bool- as \b . b--infix 1 |:|-defn |:| : {a : prop} a -> a -> (a -> a -> a) -> a- as ?\t : prop . \a b. \f : t -> t -> t. f a b--infix 0 ==>-defn ==> : {a : prop} bool -> ((a -> a -> a) -> a) -> a -> prop- | thentrue = [f : _ -> A] (true ==> f) (f (\a b : A. a))- | thenfalse = [f : _ -> A] (false ==> f) (f (\a b : A. 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"----Primary Contributers-----------------------* Author: Matthew Mirman--* Advisor: Frank Pfenning--Secondary Contributers-------------------------* Samuel Gélineau (gelisam)--* Devin Nusbaum (el-devo)--
Substitution.hs view
@@ -42,8 +42,7 @@ return $ show n getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String-getNewWith s = (++s) <$> getNew-+getNewWith s = {- (++s) <$> -} getNew --------------------- --- substitution ---@@ -66,6 +65,45 @@ apply :: Spine -> Spine -> Spine apply !a !l = rebuildSpine a [l] +newNameFor :: Name -> S.Set Name -> Name+newNameFor "" fv = newNameFor "x" fv+newNameFor nm fv = nm'+ where nm' = fromJust $ find free $ nm:map (\s -> nm++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 = newName "x" so fo -- ("",so, S.delete "" fo)+newName nm so fo' = (nm',s',f')+ where fo = S.delete nm fo'+ 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 , fo)+ nm' = fromJust $ find free $ nm:map (\s -> nm++show s ) [0..]+ fv = mappend (M.keysSet s) (freeVariables s)+ free k = not $ S.member k fv++ +freeWithout sp [] = freeVariables sp+freeWithout (Abs nm tp rst) (a:lst) = S.delete nm $ freeWithout rst lst+freeWithout (Spine "#imp_abs#" [_, Abs nm tp rst]) apps = case findTyconInPrefix nm apps of+ Just (v,apps) -> S.delete nm $ freeWithout rst apps+ Nothing -> S.delete nm $ freeWithout rst apps+freeWithout l apps = freeVariables l+++subst :: (Show a, Subst a) => Substitution -> a -> a+subst s a = substFree s mempty a+ ++class Subst a where+ substFree :: Substitution -> S.Set Name -> a -> a+ +class Alpha a where+ alphaConvert :: S.Set Name -> Map Name Name -> a -> a+ rebuildFromMem :: Map Name Name -> a -> a ++ rebuildSpine :: Spine -> [Spine] -> Spine rebuildSpine s [] = s rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of @@ -78,42 +116,16 @@ -- 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+ 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+rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) rst in seq sp $ rebuildSpine sp apps'--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- substFree :: Substitution -> S.Set Name -> a -> a--subst :: Subst a => Substitution -> a -> a-subst s = substFree s $ freeVariables s--class Alpha a where - alphaConvert :: S.Set Name -> Map Name 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 m l = alphaConvert s m <$> l rebuildFromMem s l = rebuildFromMem s <$> l@@ -122,22 +134,25 @@ 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 sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) =+ imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) (S.insert nm f) rst ++ substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) =+ imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) (S.insert nm f) rst + 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+ substFree s f sp@(Spine nm apps) = let apps' = substFree s f <$> apps in case s ! nm of- Just nm -> rebuildSpine nm apps'+ Just new -> case S.null $ S.intersection f (freeWithout new apps') of+ True -> rebuildSpine new apps'+ False -> error $ + "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp + ++ "\n\tfor: "++show s+ ++ "\n\tbound by: "++show f _ -> Spine nm apps' instance Alpha Spine where@@ -160,11 +175,13 @@ 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) -+instance Subst a => Subst (Maybe a) where+ substFree sub f p = substFree sub f <$> p+ instance Subst FlatPred where substFree sub f p = p & predType %~ substFree sub f & predKind %~ substFree sub f-+ & predValue %~ substFree sub f ------------------------- --- Constraint types ---@@ -181,7 +198,6 @@ 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) @@ -274,9 +290,26 @@ getFamilyM (Spine "#dontcheck#" [v]) = getFamilyM v getFamilyM (Spine "#forall#" [_, Abs _ _ lm]) = getFamilyM lm getFamilyM (Spine "#imp_forall#" [_, Abs _ _ lm]) = getFamilyM lm-getFamilyM (Spine "#exists#" [_, Abs _ _ lm]) = getFamilyM lm-getFamilyM (Spine "#open#" (_:_:c:_)) = getFamilyM c-getFamilyM (Spine "open" (_:_:c:_)) = getFamilyM c-getFamilyM (Spine "pack" [_,_,_,e]) = getFamilyM e+getFamilyM (Spine "exists" [_, Abs _ _ lm]) = getFamilyM lm+getFamilyM (Spine "open" l) | [_,_,c] <- removeTyconPrefix l = getFamilyM c+getFamilyM (Spine "pack" l) | (c: _) <- removeTyconPrefix l = getFamilyM c getFamilyM (Spine nm' _) = Just nm' getFamilyM v = Nothing++removeTyconPrefix (Spine "#tycon#" _:l) = removeTyconPrefix l+removeTyconPrefix l = l+++eta_expand :: Spine -> Name -> Spine+eta_expand (Spine "#imp_forall#" [_, Abs a t1 t2]) n | n /= a = imp_abs a t1 $ Spine n [tycon a $ eta_expand t1 a]+eta_expand (Spine "#forall#" [_, Abs a t1 t2]) n = Abs a' t1 $ Spine n [eta_expand t1 a']+ where a' = newNameFor a $ S.singleton n+eta_expand _ n = var n+++eta_expandAll :: M.Map Name Type -> Spine -> Spine+eta_expandAll mp (Abs a ty l) = let ty' = eta_expandAll mp ty + in Abs a ty' $ eta_expandAll (M.insert a ty' mp) l+eta_expandAll mp (Spine s l) = case mp ! s of+ Nothing -> Spine s (eta_expandAll mp <$> l)+ Just t -> rebuildSpine (eta_expand t s) (eta_expandAll mp <$> l)
caledon.cabal view
@@ -1,6 +1,6 @@ Name: caledon -Version: 3.2.1.0+Version: 3.2.2.0 Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. @@ -38,7 +38,7 @@ containers >= 0.4 && < 1.0, transformers >= 0.3 && < 1.0, cpphs >= 1.0 && < 2.0,- lens >= 3.0 && < 4.0+ lens >= 3.0 Extensions: FlexibleContexts, FlexibleInstances,
− examples/circtype.ncc
@@ -1,5 +0,0 @@-unsound a : b av -> prop- | av = a bv--unsound b : a bv -> prop- | bv = b av
− examples/circtype_bad.ncc
@@ -1,5 +0,0 @@-defn a : b av -> prop- | av = a bv--defn b : a bv -> prop- | bv = b av
− examples/coc.ncc
@@ -1,15 +0,0 @@-fixity lambda lam-fixity lambda Π--defn tm : prop- | p = tm- | t = tm- | lam = 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 )- -> (lam x : A . T x) :: (Π x : A . B x)
− examples/divergent.ncc
@@ -1,10 +0,0 @@-defn unit : prop- >| u1 = unit--defn divergent : unit -> prop- | divergentImp = divergent u1 -> divergent S---defn moop : prop- | moopimp = moop <- divergent T-query main = moop
− examples/double.ncc
@@ -1,15 +0,0 @@-fixity none 5 =:=-defn =:= : char -> char -> prop- | eq = (B) =:= B--defn char : prop--defn putChar : char -> prop -- builtin- | putCharImp = [A : char] putChar A--defn main : prop- | mainImp = main - <- S =:= 'h'- <- putChar S--query main1 = main
− examples/implicit.ncc
@@ -1,16 +0,0 @@-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/linear.ncc
@@ -1,6 +0,0 @@-defn trm : prop- | lam = (trm -> trm) -> trm- | app = trm -> trm -> trm--defn linear : (trm -> trm) -> prop- | linear_var = linear (λ V : trm . V )
− examples/listTest.ncc
@@ -1,11 +0,0 @@--------------------- Booleans ---------------------defn bool : prop- | true = bool- | false = bool--fixity none 0 ==>-defn ==> : {A : prop} bool -> ((A -> A -> A) -> A) -> A -> prop- | thentrue = [F] (true ==> F ) (F (\a1 a2 : A . a1) )- | thenfalse = [F] (false ==> F) (F (\a1 a2 : B . a2))
− examples/meta.ncc
@@ -1,23 +0,0 @@-#include "../prelude/combinators.ncc"-#include "../prelude/logic.ncc"-#include "../prelude/booleans.ncc"-#include "../prelude/naturals.ncc"-#include "../prelude/io.ncc"--defn chooseProp : bool -> prop -> prop- | chooseTrue = chooseProp true natural- | chooseFalse = chooseProp false bool--defn getWorld : bool -> prop- | getWorldImp = getWorld B- <- putStr "f/t" - <- readLine ( \S . do - , string_bool B S )--defn getProp : prop -> prop- | getPropImp = getProp P- <- getWorld B2- <- chooseProp B2 P--defn thing : {Pp : prop } getProp Pp => Pp -> prop- | heynow = thing zero
− examples/nondet.ncc
@@ -1,21 +0,0 @@-#include "../prelude/prelude.ncc"--defn runBoth : bool -> prop- >| run0 = [A] runBoth A - <- putStr "ttt "- <- A =:= true-- | run1 = [A] runBoth A- <- putStr "vvvv"- <- A =:= true-- | run2 = [A] runBoth A- <- putStr "qqqq"- <- A =:= true-- >| run3 = [A] runBoth A- <- putStr " jjj\n"- <- A =:= false- -query main = runBoth false-
− examples/readlinein.ncc
@@ -1,15 +0,0 @@-#include "../prelude/prelude.ncc"---- switching the direction of the output to be input with unification!--defn readLineIn : string -> prop- as \S . readLine $ \R . do , R =:= S--defn main : prop- | mainImp = [S] main - <- putStrLn "hi"- <- S =:= "FOO"- <- putStrLn S- <- putStrLn "ho"--query main1 = main
− examples/syntax.ncc
@@ -1,38 +0,0 @@--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/tactics.ncc
@@ -1,23 +0,0 @@-#include "../prelude/logic.ncc"---- just because we can define the theorem --- doesn't mean we can prove it (we don't have switch?)--defn natural : prop- as ∀ a : prop . a → (a → a) → a--defn zero : natural- as λ a : prop . λ z : a . λ s : a → a . z--defn succ : natural → natural- as λ n : natural . λ a : prop . λ z : a . λ s : a → a . s (n a z s)--defn even : natural → prop- | even-zero = even zero- | even-succ = [A : natural] even A -> even (succ (succ A))--defn add : natural → natural → natural- as λ n₁ n₂ : natural . n₁ natural n₂ succ--defn thm : prop- as ∀ N . even (add N N)
− examples/test.ncc
@@ -1,25 +0,0 @@-#include "../prelude/prelude.ncc"--query add0 = add (succ zero) zero (succ zero)--query add1 = succ zero ++ zero == succ zero--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)--query findSat0 = free A : natural . A =:= zero---defn ismain : prop - as run $ do - , putStr "hey!\n"- , readLine (\A . do - , putStr A- , putStr "\nbye!\n")--query main = ismain
− examples/universe.ncc
@@ -1,29 +0,0 @@-#include "../prelude/combinators.ncc"--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- | raise = {T : tm ty} tm T → tm $ ♢ T- | lam = [T : tm ty][F : tm T → tm T] tm {S = ♢ T} (Π A : T . F A)--defn isTm : {Kind : tm ty} {Ty : tm Kind} tm Ty -> prop- | hasValue = [S : tm ty][T : tm S][V : tm T] isTm V--query whattype0 = isTm { Kind = ty } { Ty = ♢ ty } ( Π A : ty . A)-query whattype1 = isTm (lam A : ty . A)
− media/logo.png
binary file changed (5107 → absent bytes)
− media/logo.svg
@@ -1,90 +0,0 @@-<?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/booleans.ncc
@@ -1,29 +0,0 @@--------------------- 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 = (true ==> F) (F (\a1 a2 : A . a1) )- >| thenfalse = (false ==> F) (F (\a1 a2 : B . a2))--defn not : bool -> bool -> prop- as \zq . if zq ==> false |:| true---#include <strings.ncc>--defn string_bool : bool -> string -> prop- >| string_bool/true = string_bool true "true"- >| string_bool/false = string_bool false "false"
− prelude/combinators.ncc
@@ -1,14 +0,0 @@------------------------------- 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
− prelude/concatable.ncc
@@ -1,18 +0,0 @@-#include <naturals.ncc>-#include <list.ncc>-------------------- concat --------------------defn concatable : [M : prop] (M -> M -> M -> prop) -> prop- >| concatableNat = concatable natural add- >| concatableList = 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
− prelude/io.ncc
@@ -1,39 +0,0 @@-#include <strings.ncc>-#include <combinators.ncc>-------------------- builtins ---------------------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 = run (Av , Bv) <- run Av- <- Bv--defn readLine : (string -> io) -> prop -- builtin - | readLineImp = [Foo : string -> io] [A : string] readLine Foo <- run (Foo A)----------------------- printing ----------------------defn putStr : string -> prop- | putStr_Nil = putStr nil- | putStr_Cons = putStr (cons V L)- <- putChar V- <- putStr L--defn putStrLn : string -> prop- as \S . run $ do - , putStr S- , putChar '\n'
− prelude/list.ncc
@@ -1,10 +0,0 @@------------------ Lists ------------------defn list : prop -> prop- | nil = list A- | cons = A -> list A -> list A--defn concatList : list A -> list A -> list A -> prop- >| concatListNil = concatList {A = T} nil L L- >| concatListCons = concatList (cons (V : T) A) B (cons V C) <- concatList A B C
− prelude/logic.ncc
@@ -1,38 +0,0 @@------------------- searches --------------------defn any : (A -> prop) -> prop- | is = [V : A][F : A -> prop] F V -> any F--defn openAny : [A][F : A -> prop] any F -> [V : A] F V -> prop- | openAnyDef = openAny A F (is 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 }------------------------- Constraints ------------------------fixity none 5 =:=-defn =:= : Q -> Q -> prop- >| eq = (B : A) =:= B---- searching for these is SLOW-fixity none 0 /\-defn /\ : prop -> prop -> prop- >| and = A -> B -> A /\ B--fixity none 0 \/-defn \/ : prop -> prop -> prop- | or1 = A -> A \/ B- | or2 = 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
− prelude/maybe.ncc
@@ -1,6 +0,0 @@------------------ Maybe ------------------defn maybe : prop -> prop- | nothing = {a} maybe a- | just = {a} a -> maybe a
− prelude/naturals.ncc
@@ -1,35 +0,0 @@-------------------------- Unary Numbers ---------------------------defn natural : prop- | zero = natural- | succ = natural -> natural--defn add : natural -> natural -> natural -> prop- >| add_z = add zero N N- >| add_s = add N M R -> add (succ N) M (succ R)---- sub N M R is N - M = R-defn sub : natural -> natural -> natural -> prop- >| sub_by_add = sub N M R <- add M R N--fixity none 3 =<-defn =< : natural -> natural -> prop- >| leqZero = {B} zero =< B- >| leqSucc = {A B} (succ A) =< (succ B) <- A =< B--fixity none 3 <-defn < : natural -> natural -> prop- >| ltZero = zero < succ B- >| ltSucc = succ A < succ B <- A < B----defn odd : natural -> prop- >| odd/one = odd (succ zero)- >| odd/n = even A -> odd (succ A)--defn even : natural -> prop- >| even/zero = even zero- >| even/succ = odd B -> even (succ B)
− prelude/prelude.ncc
@@ -1,14 +0,0 @@-{- -we can include multiple files that include the same thing - diamond problem is -solved by everything being parsed twice, but typechecked once (names are placed-into an unambiguous map)!--}-#include <combinators.ncc>-#include <logic.ncc>-#include <booleans.ncc>-#include <concatable.ncc>-#include <maybe.ncc>-#include <list.ncc>-#include <strings.ncc>-#include <naturals.ncc>-#include <io.ncc>
− prelude/strings.ncc
@@ -1,9 +0,0 @@-#include <list.ncc>-------------------- builtins --------------------defn char : prop--defn string : prop- as list char