diff --git a/AST.hs b/AST.hs --- a/AST.hs +++ b/AST.hs @@ -107,7 +107,7 @@ show (Predicate s nm ty []) = showT s ++ nm ++ " : " ++ show ty show (Predicate s nm ty (a:cons)) = showT s++ nm ++ " : " ++ show ty++showSingle a ++ concatMap (\x-> showSingle x) cons - where showSingle (b,(nm,ty)) = (if b then "\n >| " else " | ") ++nm ++ " = " ++ show ty + where showSingle (b,(nm,ty)) = (if b then "\n >| " else "\n | ") ++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 @@ -117,9 +117,11 @@ kindName = "#kind#" atom = var atomName +ty_hole = var "#hole#" tipe = var tipeName kind = var kindName -- can be either a type or an atom 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] @@ -188,6 +190,15 @@ class Subst a where substFree :: Substitution -> S.Set Name -> a -> a + +getImpliedFamilies s = S.intersection fs $ gif s + where fs = freeVariables s + gif (Spine "#imp_forall#" [ty,a]) = (case getFamilyM ty of + Nothing -> id + Just f -> S.insert f) $ gif ty `S.union` gif a + gif (Spine a l) = mconcat $ gif <$> l + gif (Abs _ ty l) = S.union (gif ty) (gif l) + subst s = substFree s $ freeVariables s class Alpha a where @@ -250,6 +261,7 @@ freeVariables t = case t of Abs nm t p -> (S.delete nm $ freeVariables p) `mappend` freeVariables t Spine "#tycon#" [Spine nm [v]] -> freeVariables v + Spine "#dontcheck#" [v] -> freeVariables v Spine ['\'',_,'\''] [] -> mempty Spine head others -> mappend (S.singleton head) $ mconcat $ map freeVariables others @@ -408,18 +420,21 @@ 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 +getFamily v = fromMaybe (error ("values don't have families: "++show v)) $ getFamilyM v +getFamilyM (Spine "#infer#" [_, Abs _ _ lm]) = getFamilyM lm +getFamilyM (Spine "#ascribe#" (_:v:l)) = getFamilyM (rebuildSpine v l) +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 nm' _) = Just nm' +getFamilyM v = Nothing + consts = [ (atomName , tipe) , (tipeName , kind) , (kindName , kind) @@ -459,8 +474,8 @@ 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] + nil = Spine "nil" [ tycon "A" char] + cons a l = Spine "cons" [tycon "A" char, a,l] envConsts = anonymous <$> M.fromList consts diff --git a/Context.hs b/Context.hs --- a/Context.hs +++ b/Context.hs @@ -50,6 +50,8 @@ 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. @@ -87,8 +89,17 @@ 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 +addToHead s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of + Nothing -> addToContext s ctxt $ Binding quant nm tp Nothing (ctxtHead ctxt) + Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> + addToContext s ctxt' $ Binding quant nm tp Nothing (ctxtHead ctxt') + where ctxt' = removeFromContext nm ctxt + _ -> error $ "Can't add to head, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt + +addToTail s quant nm tp ctxt@Context{ctxtMap = cmap} = case M.lookup nm cmap of + Nothing -> addToContext s ctxt $ Binding quant nm tp (ctxtTail ctxt) Nothing + Just (Binding{ elmQuant = quant', elmType = tp'}) | quant' == quant && tp' == tp && quant == Forall -> ctxt + _ -> error $ "Can't add to tail, already in context: "++show nm++" : "++show tp++"\n@"++show ctxt removeHead ctxt = case ctxtHead ctxt of Nothing -> ctxt diff --git a/HOU.hs b/HOU.hs --- a/HOU.hs +++ b/HOU.hs @@ -2,7 +2,8 @@ FlexibleInstances, PatternGuards, UnicodeSyntax, - BangPatterns + BangPatterns, + TupleSections #-} module HOU where @@ -10,14 +11,16 @@ import AST import Context import TopoSortAxioms -import Control.Monad.State (StateT, forM_,runStateT, modify, get) +import Control.Monad.State (StateT, forM_,runStateT, modify, get,put, State, runState) import Control.Monad.RWS (RWST, runRWST, ask, tell) import Control.Monad.Error (throwError, MonadError) -import Control.Monad (unless, forM, replicateM, void, (<=<)) +import Control.Monad (unless, forM, replicateM, void, (<=<), when) import Control.Monad.Trans (lift) import Control.Applicative import qualified Data.Foldable as F +import Data.Foldable (foldlM) import Data.List +import Data.Char (isUpper) import Data.Maybe import Data.Monoid import qualified Data.Map as M @@ -41,7 +44,10 @@ {-# INLINE throwTrace #-} throwTrace !i s = vtrace i s $ throwError s +mtrace True = trace +mtrace False = const id + ----------------------------------------------- --- the higher order unification algorithm --- ----------------------------------------------- @@ -86,7 +92,9 @@ $ checkFinished c >> return (sub, c)) - fst <$> uniWhile mempty cons + sub <- fst <$> uniWhile mempty cons + + return $ sub checkFinished [] = return () @@ -115,6 +123,9 @@ unifyOne _ return = return Nothing unifyEq cons@(a :=: b) = case (a,b) of + (Spine "#ascribe#" (ty:v:l), b) -> return $ Just (mempty, [rebuildSpine v l :=: b]) + (b,Spine "#ascribe#" (ty:v:l)) -> return $ Just (mempty, [b :=: rebuildSpine v l]) + (Spine "#imp_forall#" [ty, l], b) -> vtrace 1 "-implicit-" $ do a' <- getNewWith "@aL" modifyCtxt $ addToTail "-implicit-" Exists a' ty @@ -535,16 +546,16 @@ Spine "#ascribe#" (t:v:l) -> do (v'',mem) <- regenWithMem v - + t <- withKind $ checkType t t'' <- regenAbsVars t - v' <- checkType v'' t'' - + v' <- checkType v'' t r <- getNewWith "@r" - Spine _ l' <- addToEnv (∀) r t $ checkType (Spine r l) ty + Spine _ l' <- addToEnv (∀) r t'' $ checkType (Spine r l) ty return $ rebuildSpine (rebuildFromMem mem v') l' - --- checkType (rebuildSpine (rebuildFromMem mem v') l) ty + Spine "#dontcheck#" [v] -> do + return v + Spine "#infer#" [_, Abs x tyA tyB ] -> do tyA <- withKind $ checkType tyA @@ -640,6 +651,64 @@ checkFullType :: Spine -> Type -> Env (Spine, Constraint) checkFullType val ty = typeCheckToEnv $ checkType val ty + +--------------------------------- +--- Generalize Free Variables --- +--------------------------------- + +{- +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. +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 + return $ S.union prev1 prev2 + + Spine nm l -> do + mp <- get + prev' <- if S.member nm gen + then do + let prevs = mp M.! nm + put $ M.insert nm (S.union prev prevs) mp + return $ mempty + else return prev + + prev'' <- foldlM (buildOrderGraph gen) prev' l + + if S.member nm gen + then do + 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) = isUpper c + +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 + ---------------------- --- type inference --- ---------------------- @@ -656,8 +725,8 @@ 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 $ val + resT = rebuildFromMem mem' $ unsafeSubst sub $ ty vtrace 0 ("RESULT: "++nm++" : "++show resV) $ return $ (resV,resT, M.insert nm (seqi,resV) env) @@ -672,8 +741,8 @@ ---------------------------- type FlatPred = [(Maybe Name,(Bool,Integer,Bool),Name,Term,Type)] -typeCheckAxioms :: FlatPred -> Choice Substitution -typeCheckAxioms lst = do +typeCheckAxioms :: Bool -> FlatPred -> Choice Substitution +typeCheckAxioms verbose lst = do -- check the closedness of families. this gets done -- after typechecking since family checking needs to evaluate a little bit @@ -692,10 +761,10 @@ inferAll (_ , r, (_,_,nm,_,_):_) | nm == atomName = throwTrace 0 $ atomName++" can not be overloaded" inferAll (l , r, (fam,(b,i,s),nm,val,ty):toplst) = do (val,ty,l') <- appendErr ("can not infer type for: "++nm++" : "++show val) $ - trace ("Checking: " ++nm) $ + mtrace verbose ("Checking: " ++nm) $ vtrace 0 ("\tVAL: " ++show val ++"\n\t:: " ++show ty) $ - typeInfer l ((b,i),nm, val,ty) -- constrain the breadth first search to be local! + typeInfer l ((b,i),nm, generateBinding 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) @@ -704,7 +773,10 @@ inferAll $ case nm of '#':'v':':':nm' -> (sub' <$> l', (fam,(b,i,s),nm,val,ty):r , fsub <$> toplst) where sub' (b,a)= (b, sub a) - sub = subst $ nm' |-> ascribe val ty -- the ascription isn't necessary because we don't have unbound variables + sub = subst $ nm' |-> ascribe val (dontcheck ty) + -- the ascription isn't necessary because we don't have unbound variables, + -- and we already know that val : ty, but it pauses computation + -- ascribe val ty fsub (fam,s,nm,val,ty) = (fam,s,nm, sub val, sub ty) _ -> (l', (fam,(b,i,s),nm,val,ty):r, toplst) @@ -725,12 +797,39 @@ doubleCheckAll (S.union envSet uns) $ topoSortAxioms lst' return $ snd <$> l - -typeCheckAll :: [Predicate] -> Choice [Predicate] -typeCheckAll preds = do - tyMap <- typeCheckAxioms $ toAxioms True preds + +topoSortAxioms :: [(Maybe Name, (Bool,Integer,Bool), Name,Term,Type)] -> [(Maybe Name, (Bool,Integer,Bool), Name,Term,Type)] +topoSortAxioms axioms = topoSortComp (\(fam,s,nm,val,ty) -> (nm,) + $ S.union (getImplieds nm) + $ S.fromList + $ concatMap (\nm -> [nm,"#v:"++nm]) + $ filter (not . flip elem (map fst consts)) + $ S.toList $ freeVariables val `S.union` freeVariables ty ) axioms + + where nm2familyLst = catMaybes $ (\(fam,_,nm,_,_) -> (nm,) <$> fam) <$> axioms + + + family2nmsMap = foldr (\(fam,nm) m -> M.insert nm (case M.lookup nm m of + Nothing -> S.singleton fam + Just s -> S.insert fam s) m + ) mempty nm2familyLst + + family2impliedsMap = M.fromList $ (\(_,_,nm,val,_) -> (nm, + mconcat + $ catMaybes + $ map (`M.lookup` family2nmsMap) + $ S.toList + $ getImpliedFamilies val + )) <$> axioms + + getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap) + +typeCheckAll :: Bool -> [Predicate] -> Choice [Predicate] +typeCheckAll verbose preds = do + 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) @@ -751,3 +850,6 @@ solver axioms tp = case runError $ runRWST (search tp) (M.union envConsts axioms) emptyState of Right ((_,tm),_,_) -> Right $ [("query", tm)] Left s -> Left $ "reification not possible: "++s + +reduceDecsByName :: [Predicate] -> [Predicate] +reduceDecsByName decs = map snd $ M.toList $ M.fromList $ map (\a -> (predName a,a)) decs diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -10,20 +10,25 @@ import Data.List (partition) import Text.Parsec import Data.Monoid +import Control.Monad (when) import Control.Arrow (first) +import Language.Preprocessor.Cpphs + ----------------------------------------------------------------------- -------------------------- MAIN --------------------------------------- ----------------------------------------------------------------------- -checkAndRun decs = do - - putStrLn "\nFILE: " - forM_ decs $ \s -> putStrLn $ show s++"\n" +checkAndRun verbose decs = do + + when verbose $ do + putStrLn "\nFILE: " + forM_ decs $ \s -> putStrLn $ show s++"\n" - putStrLn "\nTYPE CHECKING: " - decs <- case runError $ typeCheckAll decs of + when verbose $ putStrLn "\nTYPE CHECKING: " + decs <- case runError $ typeCheckAll verbose decs of Left e -> error e - Right e -> putStrLn "Type checking success!" >> return e + Right e -> do when verbose $ putStrLn "Type checking success!" + return e let (defs,others) = flip partition decs $ \x -> case x of Define {} -> True _ -> False @@ -32,12 +37,14 @@ (predicates, targets) = flip partition others $ \x -> case x of Predicate {} -> True _ -> False - - putStrLn "\nAXIOMS: " - forM_ (defs++predicates) $ \s -> putStrLn $ show s++"\n" + + when verbose $ do + putStrLn "\nAXIOMS: " + forM_ (defs++predicates) $ \s -> putStrLn $ show s++"\n" - putStrLn "\nTARGETS: " - forM_ targets $ \s -> putStrLn $ show s++"\n" + when verbose $ do + putStrLn "\nTARGETS: " + forM_ targets $ \s -> putStrLn $ show s++"\n" let predicates' = sub predicates targets' = sub targets @@ -45,22 +52,38 @@ axioms = toSimpleAxioms predicates' forM_ targets' $ \target -> do - putStrLn $ "\nTARGET: \n"++show target + when verbose $ putStrLn $ "\nTARGET: \n"++show target case solver axioms $ predType target of Left e -> putStrLn $ "ERROR: "++e - Right sub -> putStrLn $ "SOLVED WITH:\n" + Right sub -> when verbose $ putStrLn $ "SOLVED WITH:\n" ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub + +processFile :: Bool -> String -> IO () +processFile verbose fname = do + file <- readFile fname + + file <- runCpphs + (defaultCpphsOptions{ + boolopts = defaultBoolOptions{ hashline = False + , lang = False + , ansi = True + , layout = True + } + } + ) + fname file + + let mError = parseCaledon fname file + decs <- case mError of + Left e -> error $ show e + Right l -> return l + checkAndRun verbose $ reduceDecsByName decs + main = do 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\"" + [] -> putStrLn "No file specified. Usage is \"caledon [--io-only] file.ncc\"" + [fname] -> processFile True fname + ["--io-only", fname] -> processFile False fname + _ -> putStrLn "Unrecognized arguments. Usage is \"caledon [--io-only] file.ncc\"" diff --git a/Parser.hs b/Parser.hs --- a/Parser.hs +++ b/Parser.hs @@ -2,7 +2,7 @@ RecordWildCards #-} -module Parser where +module Parser (parseCaledon) where import AST @@ -20,10 +20,15 @@ import Debug.Trace import qualified Data.Foldable as F + + ----------------------------------------------------------------------- -------------------------- PARSER ------------------------------------- ----------------------------------------------------------------------- +-- | `parseCaledon` is the external interface +parseCaledon :: SourceName -> String -> Either ParseError [Predicate] +parseCaledon = runP decls emptyState data ParseState = ParseState { currentVar :: Integer , currentSet :: S.Set Name @@ -197,7 +202,7 @@ let (ident,sep) = decAnon nml <- many ident ty <- optionMaybe $ reservedOp sep >> ptipe - return (nml,fromMaybe tyhole ty) + return (nml,fromMaybe ty_hole ty) binary fun assoc name = flip Infix assoc $ do name @@ -219,8 +224,8 @@ , 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 ] + ]++[ altPostfix [op] [] (\nm t s -> Spine op [t,Abs nm ty_hole s] ) | op <- opLams ] + ++[ altPostfix [] [op] (\nm t s -> Spine op [t,Abs nm ty_hole s] ) | op <- strLams ] , [ binary (forall) AssocRight $ reservedOp "->" <|> reservedOp "→" , binary (const (~~>)) AssocRight $ reservedOp "=>" <|> reservedOp "⇒" ] @@ -277,7 +282,7 @@ "operator" pAt = do reserved "_" - return $ hole + return $ ty_hole <|> do r <- idVar return $ var r <|> do r <- identifier @@ -293,10 +298,6 @@ myParens s m = between (symbol "(" ("("++s)) (symbol ")" (s++")")) m ptipe "tipe" - -hole = var "#hole#" -tyhole = var "#hole#" - reservedOperators = [ "->", "=>", "<=", "⇐", "⇒", "→", "<-", "←", "\\", "?\\", diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -81,8 +81,8 @@ | succ = num -> num 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 + | 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 @@ -123,12 +123,12 @@ ``` defn maybe : prop → prop - | nothing = {a} maybe a - | just = {a} a → maybe a + | nothing = maybe A + | just = A → maybe A infix 1 =:= -defn =:= : {a : prop} a -> a -> prop - | eq = {a : prop} a =:= a +defn =:= : A -> A -> prop + | eq = (=:=) {A = A} V V infix 0 /\ defn /\ : prop -> prop -> prop @@ -155,9 +155,9 @@ * 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 -> 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] +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 ``` @@ -181,21 +181,21 @@ ``` defn runBoth : bool -> prop - >| run0 = [A] runBoth A - <- putStr "tttt " - <- A =:= true + >| run0 = runBoth A + <- putStr "tttt " + <- A =:= true - | run1 = [A] runBoth A - <- putStr "vvvv" - <- A =:= true + | run1 = runBoth A + <- putStr "vvvv" + <- A =:= true - | run2 = [A] runBoth A - <- putStr "qqqq" - <- A =:= true + | run2 = runBoth A + <- putStr "qqqq" + <- A =:= true - >| run3 = [A] runBoth A - <- putStr " jjjj" - <- A =:= false + >| run3 = runBoth A + <- putStr " jjjj" + <- A =:= false query main = runBoth false @@ -219,8 +219,8 @@ 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)) + | 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 @@ -234,3 +234,21 @@ * 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) + + diff --git a/TopoSortAxioms.hs b/TopoSortAxioms.hs --- a/TopoSortAxioms.hs +++ b/TopoSortAxioms.hs @@ -1,21 +1,11 @@ -{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BangPatterns, TupleSections #-} 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,Integer,Bool), Name,Term,Type)] -> [(Maybe Name, (Bool,Integer,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 @@ -27,3 +17,8 @@ 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 + +topoSortComp 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 + graph = transposeG graph' diff --git a/caledon.cabal b/caledon.cabal --- a/caledon.cabal +++ b/caledon.cabal @@ -1,6 +1,6 @@ Name: caledon -Version: 2.1.1.0 +Version: 3.0.0.0 Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. @@ -34,7 +34,8 @@ mtl >= 2.0 && < 3.0, parsec >= 3.0 && < 4.0, containers >= 0.4 && < 1.0, - transformers >= 0.3 && < 1.0 + transformers >= 0.3 && < 1.0, + cpphs >= 1.0 && < 2.0 Extensions: FlexibleContexts, FlexibleInstances, diff --git a/examples/evenodd.ncc b/examples/evenodd.ncc deleted file mode 100644 --- a/examples/evenodd.ncc +++ /dev/null @@ -1,12 +0,0 @@ -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) - diff --git a/examples/infer.ncc b/examples/infer.ncc deleted file mode 100644 --- a/examples/infer.ncc +++ /dev/null @@ -1,15 +0,0 @@ -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) (odd/even zero even/zero) diff --git a/examples/meta.ncc b/examples/meta.ncc new file mode 100644 --- /dev/null +++ b/examples/meta.ncc @@ -0,0 +1,23 @@ +#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 diff --git a/examples/nondet.ncc b/examples/nondet.ncc --- a/examples/nondet.ncc +++ b/examples/nondet.ncc @@ -1,42 +1,20 @@ -defn char : prop -- builtin -defn putChar : char -> prop -- builtin - | putCharImp = [A] putChar A - -defn bool : prop - | true = bool - | false = bool - -fixity none 1 =:= -defn =:= : {Q} Q -> Q -> prop - | eq = [a : prop][b:a] (=:=) {Q = a} b b +#include "../prelude/prelude.ncc" defn runBoth : bool -> prop >| run0 = [A] runBoth A - <- putChar 't' - <- putChar 't' - <- putChar 't' - <- putChar 't' + <- putStr "ttt " <- A =:= true | run1 = [A] runBoth A - <- putChar 'v' - <- putChar 'v' - <- putChar 'v' - <- putChar 'v' + <- putStr "vvvv" <- A =:= true | run2 = [A] runBoth A - <- putChar 'q' - <- putChar 'q' - <- putChar 'q' - <- putChar 'q' + <- putStr "qqqq" <- A =:= true >| run3 = [A] runBoth A - <- putChar 'j' - <- putChar 'j' - <- putChar 'j' - <- putChar 'j' + <- putStr " jjj\n" <- A =:= false query main = runBoth false diff --git a/examples/prelude.ncc b/examples/prelude.ncc deleted file mode 100644 --- a/examples/prelude.ncc +++ /dev/null @@ -1,210 +0,0 @@ ---------------- --- 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 diff --git a/examples/readlinein.ncc b/examples/readlinein.ncc new file mode 100644 --- /dev/null +++ b/examples/readlinein.ncc @@ -0,0 +1,5 @@ +#include + +-- switching the direction of the output to be input with unification! +defn readLineIn : string -> prop + as \S . readLine $ \R . do , S =:= R diff --git a/examples/record.ncc b/examples/record.ncc deleted file mode 100644 --- a/examples/record.ncc +++ /dev/null @@ -1,18 +0,0 @@ -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 --} diff --git a/examples/substitution.ncc b/examples/substitution.ncc deleted file mode 100644 --- a/examples/substitution.ncc +++ /dev/null @@ -1,2 +0,0 @@ -defn example : [ax : prop] ax -> prop - as eximp = [atx : prop] example prop atx diff --git a/examples/test.ncc b/examples/test.ncc --- a/examples/test.ncc +++ b/examples/test.ncc @@ -1,12 +1,25 @@ +#include "../prelude/prelude.ncc" -defn num : prop - | zero = num - | succ = num → num +query add0 = add (succ zero) zero (succ zero) -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 add1 = succ zero ++ zero == succ zero -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 +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 diff --git a/media/logo.png b/media/logo.png new file mode 100644 Binary files /dev/null and b/media/logo.png differ diff --git a/media/logo.svg b/media/logo.svg new file mode 100644 --- /dev/null +++ b/media/logo.svg @@ -0,0 +1,90 @@ + + + + + + + + + + image/svg+xml + + + + + + + + + + + + + + + diff --git a/prelude/booleans.ncc b/prelude/booleans.ncc new file mode 100644 --- /dev/null +++ b/prelude/booleans.ncc @@ -0,0 +1,29 @@ +---------------- +--- 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 = [F: _ -> A] (true ==> F ) (F (\a1 a2 : A . a1) ) + >| thenfalse = [F: _ -> B] (false ==> F) (F (\a1 a2 : B . a2)) + +defn not : bool -> bool -> prop + as \zq . if zq ==> false |:| true + + +#include + +defn string_bool : bool -> string -> prop + >| string_bool/true = string_bool true "true" + >| string_bool/false = string_bool false "false" diff --git a/prelude/combinators.ncc b/prelude/combinators.ncc new file mode 100644 --- /dev/null +++ b/prelude/combinators.ncc @@ -0,0 +1,14 @@ +-------------------------- +--- 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 diff --git a/prelude/concatable.ncc b/prelude/concatable.ncc new file mode 100644 --- /dev/null +++ b/prelude/concatable.ncc @@ -0,0 +1,18 @@ +#include +#include + +-------------- +--- 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 diff --git a/prelude/io.ncc b/prelude/io.ncc new file mode 100644 --- /dev/null +++ b/prelude/io.ncc @@ -0,0 +1,33 @@ +#include + +--------------- +-- 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 diff --git a/prelude/list.ncc b/prelude/list.ncc new file mode 100644 --- /dev/null +++ b/prelude/list.ncc @@ -0,0 +1,10 @@ +------------- +--- 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 diff --git a/prelude/logic.ncc b/prelude/logic.ncc new file mode 100644 --- /dev/null +++ b/prelude/logic.ncc @@ -0,0 +1,38 @@ +--------------- +-- 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 = (=:=) {Q = A} B 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 diff --git a/prelude/maybe.ncc b/prelude/maybe.ncc new file mode 100644 --- /dev/null +++ b/prelude/maybe.ncc @@ -0,0 +1,6 @@ +------------- +--- Maybe --- +------------- +defn maybe : prop -> prop + | nothing = {a} maybe a + | just = {a} a -> maybe a diff --git a/prelude/naturals.ncc b/prelude/naturals.ncc new file mode 100644 --- /dev/null +++ b/prelude/naturals.ncc @@ -0,0 +1,35 @@ +--------------------- +--- 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) diff --git a/prelude/prelude.ncc b/prelude/prelude.ncc new file mode 100644 --- /dev/null +++ b/prelude/prelude.ncc @@ -0,0 +1,14 @@ +{- +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 +#include +#include +#include +#include +#include +#include +#include +#include diff --git a/prelude/strings.ncc b/prelude/strings.ncc new file mode 100644 --- /dev/null +++ b/prelude/strings.ncc @@ -0,0 +1,9 @@ +#include + +--------------- +-- builtins --- +--------------- +defn char : prop -- builtin + +defn string : prop + as list char