diff --git a/AST.hs b/AST.hs --- a/AST.hs +++ b/AST.hs @@ -2,7 +2,8 @@ FlexibleInstances, PatternGuards, BangPatterns, - FlexibleContexts + FlexibleContexts, + TupleSections #-} module AST where @@ -38,7 +39,7 @@ type Type = Spine type Term = Spine -data Predicate = Predicate { predIsSound :: !Bool, predName :: !Name, predType :: !Type, predConstructors :: ![(Name,Type)] } +data Predicate = Predicate { predIsSound :: !Bool, predName :: !Name, predType :: !Type, predConstructors :: ![(Bool,(Name,Type))] } | Query { predName :: !Name, predType :: !Spine} | Define { predIsSound :: !Bool, predName :: !Name, predValue :: !Spine, predType :: !Type} deriving (Eq) @@ -103,10 +104,10 @@ showT False = "unsound " instance Show Predicate where - show (Predicate s nm ty []) = showT s ++ nm ++ " : " ++ show ty ++ ";" + show (Predicate s nm ty []) = showT s ++ nm ++ " : " ++ show ty show (Predicate s nm ty (a:cons)) = - showT s++ nm ++ " : " ++ show ty ++ "\n" ++ " | " ++ showSingle a ++ concatMap (\x-> "\n | " ++ showSingle x) cons ++ ";" - where showSingle (nm,ty) = nm ++ " = " ++ show ty + 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 show (Query nm val) = "query " ++ nm ++ " = " ++ show val show (Define s nm val ty) = showT s ++ nm ++ " : " ++ show ty ++"\n as "++show val @@ -237,7 +238,7 @@ instance Subst Predicate where - substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(nm,t) -> (nm,substFree sub f t)) <$> cons) + substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(b,(nm,t)) -> (b,(nm,substFree sub f t))) <$> cons) substFree sub f (Query nm ty) = Query nm (substFree sub f ty) substFree sub f (Define s nm val ty) = Define s nm (substFree sub f val) (substFree sub f ty) @@ -383,7 +384,7 @@ regenWithMem cons = case cons of a :=: b -> regenM (:=:) a b a :@: b -> regenM (:@:) a b - + instance RegenAbsVars Constraint where regenAbsVars cons = case cons of Bind q nm ty cons -> do @@ -451,6 +452,8 @@ ] +anonymous ty = ((False,100),ty) + envSet = S.fromList $ map fst consts toNCCchar c = Spine ['\'',c,'\''] [] @@ -459,7 +462,7 @@ nil = Spine "nil" [tycon "a" char] cons a l = Spine "cons" [tycon "a" char, a,l] -envConsts = M.fromList consts +envConsts = anonymous <$> M.fromList consts isChar ['\'',_,'\''] = True isChar _ = False diff --git a/Choice.hs b/Choice.hs --- a/Choice.hs +++ b/Choice.hs @@ -12,7 +12,7 @@ import Data.Functor import Control.Applicative import Control.Monad.Error.Class (catchError, throwError, MonadError) - +import Control.Monad.Cont data Choice a = Choice a :<|>: Choice a | Fail String @@ -69,3 +69,13 @@ catchError try1 foo_try2 = case runError try1 of Left s -> foo_try2 s Right a -> Success a + +type CONT_T a m c = ((c -> m a) -> m a) + +-- why doesn't this exist in the standard library? +instance (Monad m, Alternative m) => Alternative (ContT a m) where + empty = lift $ empty + c1 <|> c2 = ContT $ \cont -> m1f cont <|> m2f cont + where m1f = runContT c1 + m2f = runContT c2 + diff --git a/Context.hs b/Context.hs --- a/Context.hs +++ b/Context.hs @@ -21,8 +21,10 @@ -------------------- --- context map --- -------------------- -type ContextMap = Map Name Type +type ContextMap = Map Name ((Bool,Integer),Type) +type ContextMapT = Map Name Type + -------------------------------- --- constraint context list --- -------------------------------- @@ -194,12 +196,12 @@ getForalls :: Env ContextMap getForalls = do ctx <- ctxtMap <$> stateCtxt <$> get - return $ elmType <$> M.filter (\q -> elmQuant q == Forall) ctx + return $ anonymous <$> elmType <$> M.filter (\q -> elmQuant q == Forall) ctx getExists :: Env ContextMap getExists = do ctx <- ctxtMap <$> stateCtxt <$> get - return $ elmType <$> M.filter (\q -> elmQuant q == Exists) ctx + return $ anonymous <$> elmType <$> M.filter (\q -> elmQuant q == Exists) ctx getConstants :: Env ContextMap getConstants = ask @@ -214,14 +216,15 @@ getFullCtxt = do constants <- getConstants ctx <- ctxtMap <$> stateCtxt <$> get - return $ M.union (elmType <$> ctx) constants + return $ M.union (anonymous <$> elmType <$> ctx) constants getVariablesBeforeExists :: Name -> Env ContextMap getVariablesBeforeExists nm = do constants <- getConstants ctx <- stateCtxt <$> get let bind = ctxtMap ctx M.! nm - return $ M.union constants $ M.fromList $ snd <$> getBefore "IN: getVariablesBeforeExists" bind ctx + return $ M.union constants + $ M.fromList $ (\(nm,v) -> (nm, anonymous v)) <$> snd <$> getBefore "IN: getVariablesBeforeExists" bind ctx modifyCtxt :: (Context -> Context) -> Env () @@ -232,7 +235,7 @@ --- traversal monads --- ------------------------- lookupConstant :: Name -> Env (Maybe Type) -lookupConstant x = (M.lookup x) <$> ask +lookupConstant x = fmap snd <$> (M.lookup x) <$> ask type TypeChecker = ContT Spine Env @@ -240,11 +243,7 @@ typeCheckToEnv m = listen $ runContT m return -addToEnv :: (Name -> Spine -> Constraint -> Constraint) -> Name -> Spine -> TypeChecker a -> TypeChecker a -addToEnv e x ty = mapContT (censor $ e x ty) . liftLocal ask local (M.insert x ty) ----------------------- ---- Universe Monad --- ----------------------- - +addToEnv :: (Name -> Type -> Constraint -> Constraint) -> Name -> Type -> TypeChecker a -> TypeChecker a +addToEnv e x ty = mapContT (censor $ e x ty) . liftLocal ask local (M.insert x $ anonymous ty) diff --git a/HOU.hs b/HOU.hs --- a/HOU.hs +++ b/HOU.hs @@ -13,7 +13,7 @@ import Control.Monad.State (StateT, forM_,runStateT, modify, get) import Control.Monad.RWS (RWST, runRWST, ask, tell) import Control.Monad.Error (throwError, MonadError) -import Control.Monad (unless, forM, replicateM, void) +import Control.Monad (unless, forM, replicateM, void, (<=<)) import Control.Monad.Trans (lift) import Control.Applicative import qualified Data.Foldable as F @@ -56,35 +56,29 @@ return $ l1 ++ l2 flatten (SCons l) = return l +type UnifyResult = Maybe (Substitution, [SCons]) + unify :: Constraint -> Env Substitution unify cons = do cons <- vtrace 5 ("CONSTRAINTS1: "++show cons) $ regenAbsVars cons cons <- vtrace 5 ("CONSTRAINTS2: "++show cons) $ flatten cons let uniWhile :: Substitution -> [SCons] -> Env (Substitution, [SCons]) - uniWhile !sub !c' = do + uniWhile !sub !c' = fail "" <|> do exists <- getExists c <- regenAbsVars c' - let -- eventually we can make the entire algorithm a graph modification algorithm for speed, - -- such that we don't have to topologically sort every time. Currently this only takes us from O(n log n) to O(n) per itteration, it is - -- not necessarily worth it. - uniWith !wth !backup = do - let searchIn [] r = return Nothing - searchIn (next:l) r = do - c1' <- wth next - case c1' of - Just (sub',next') -> return $ Just (sub', (subst sub' $ reverse r)++ - next' - ++subst sub' l) - Nothing -> searchIn l (next:r) - res <- searchIn c [] - case res of - Nothing -> do - backup - Just (!sub', c') -> do - let !sub'' = sub *** sub' - modifyCtxt $ subst sub' - uniWhile sub'' $! c' - + let uniWith !wth !backup = searchIn c [] + where searchIn [] r = finish Nothing + searchIn (next:l) r = + wth next $ \c1' -> case c1' of + Just (sub',next') -> finish $ Just (sub', subst sub' (reverse r)++next'++subst sub' l) + Nothing -> searchIn l $ next:r + finish Nothing = backup + finish (Just (!sub', c')) = do + let !sub'' = sub *** sub' + modifyCtxt $ subst sub' + uniWhile sub'' $! c' + + vtrace 3 ("CONST: "++show c) ( uniWith unifyOne $ uniWith unifySearch @@ -95,32 +89,30 @@ fst <$> uniWhile mempty cons - checkFinished [] = return () checkFinished cval = throwTrace 0 $ "ambiguous constraint: " ++show cval -unifySearch :: SCons -> Env (Maybe (Substitution, [SCons])) -unifySearch (a :@: b) | b /= atom = do - cons <- rightSearch a b - return $ case cons of - Nothing -> Nothing - Just cons -> Just (mempty, cons) -unifySearch _ = return Nothing +unifySearch :: SCons -> CONT_T b Env UnifyResult +unifySearch (a :@: b) return | b /= atom = rightSearch a b $ newReturn return +unifySearch _ return = return Nothing -unifySearchAtom (a :@: b) = do - cons <- rightSearch a b - return $ case cons of - Nothing -> Nothing - Just cons -> Just (mempty, cons) -unifySearchAtom _ = return Nothing +newReturn return cons = return $ case cons of + Nothing -> Nothing + Just cons -> Just (mempty, cons) -unifyOne :: SCons -> Env (Maybe (Substitution , [SCons])) -unifyOne (a :=: b) = do +unifySearchAtom :: SCons -> CONT_T b Env UnifyResult +unifySearchAtom (a :@: b) return = rightSearch a b $ newReturn return +unifySearchAtom _ return = return Nothing + + + +unifyOne :: SCons -> CONT_T b Env UnifyResult +unifyOne (a :=: b) return = do c' <- isolateForFail $ unifyEq $ a :=: b case c' of - Nothing -> isolateForFail $ unifyEq $ b :=: a + Nothing -> return =<< (isolateForFail $ unifyEq $ b :=: a) r -> return r -unifyOne _ = return Nothing +unifyOne _ return = return Nothing unifyEq cons@(a :=: b) = case (a,b) of (Spine "#imp_forall#" [ty, l], b) -> vtrace 1 "-implicit-" $ do @@ -164,7 +156,7 @@ raiseToTop bind (Spine x yl) $ \(a@(Spine x yl),ty) sub -> case subst sub s' of b@(Spine x' y'l) -> vtrace 4 "-gs-" $ do - bind' <- getElm ("gvar-blah: "++show cons) x' + bind' <- getElm ("gvar-blah: "++show cons) x' case bind' of Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const --if allElementsAreVariables yl @@ -396,7 +388,8 @@ -- need bidirectional search! -rightSearch m goal = vtrace 1 ("-rs- "++show m++" ∈ "++show goal) $ +rightSearch :: Term -> Type -> CONT_T b Env (Maybe [SCons]) +rightSearch m goal ret = vtrace 1 ("-rs- "++show m++" ∈ "++show goal) $ fail (show m++" ∈ "++show goal) <|> case goal of Spine "#forall#" [a, b] -> do y <- getNewWith "@sY" @@ -404,7 +397,7 @@ let b' = b `apply` var x' modifyCtxt $ addToTail "-rsFf-" Forall x' a modifyCtxt $ addToTail "-rsFe-" Exists y b' - return $ Just [ var y :=: m `apply` var x' , var y :@: b'] + ret $ Just [ var y :=: m `apply` var x' , var y :@: b'] Spine "#imp_forall#" [_, Abs x a b] -> do y <- getNewWith "@isY" @@ -412,26 +405,30 @@ let b' = subst (x |-> var x') b modifyCtxt $ addToTail "-rsIf-" Forall x' a modifyCtxt $ addToTail "-rsIe-" Exists y b' - return $ Just [ var y :=: m `apply` (tycon x $ var x') - , var y :@: b' - ] - Spine "putChar" [c@(Spine ['\'',l,'\''] [])] -> - case unsafePerformIO $ putStr $ l:[] of - () -> return $ Just [ m :=: Spine "putCharImp" [c]] - Spine "putChar" [_] -> vtrace 0 "FAILING PUTCHAR" $ return Nothing + ret $ Just [ var y :=: m `apply` (tycon x $ var x') + , var y :@: b' + ] + Spine "putChar" [c@(Spine ['\'',l,'\''] [])] -> ret $ Just $ (m :=: Spine "putCharImp" [c]):seq action [] + where action = unsafePerformIO $ putStr $ l:[] + + Spine "putChar" [_] -> vtrace 0 "FAILING PUTCHAR" $ ret Nothing Spine "readLine" [l] -> case toNCCstring $ unsafePerformIO $ getLine of - !s -> do + s -> do -- ensure this is lazy so we don't check for equality unless we have to. y <- getNewWith "@isY" let ls = l `apply` s modifyCtxt $ addToTail "-rl-" Exists y ls - return $ Just [m :=: Spine "readLineImp" [l,s, var y], var y :@: Spine "run" [ls]] + ret $ Just [m :=: Spine "readLineImp" [l,s {- this is only safe because lists are lazy -}, var y], var y :@: Spine "run" [ls]] _ | goal == kind -> do case m of Abs{} -> throwError "not properly typed" - _ | m == tipe || m == atom -> return $ Just [] - _ -> F.asum $ return . Just . return . (m :=:) <$> [atom , tipe] + _ | m == tipe || m == atom -> ret $ Just [] + _ -> breadth -- we should pretty much always use breadth first search here maybe, since this is type search + where srch r1 r2 = r1 $ F.asum $ r2 . Just . return . (m :=:) <$> [atom , tipe] -- for breadth first + breadth = srch (ret =<<) return + depth = srch id (appendErr "" . ret) + Spine nm _ -> do constants <- getConstants foralls <- getForalls @@ -440,7 +437,7 @@ isFixed a = isChar a || M.member a env - getFixedType a | isChar a = Just $ var "char" + getFixedType a | isChar a = Just $ anonymous $ var "char" getFixedType a = M.lookup a env let mfam = case m of @@ -448,10 +445,10 @@ Spine nm _ -> case getFixedType nm of Just t -> Just (nm,t) Nothing -> Nothing - - sameFamily (_, Abs _ _ _) = False - sameFamily ("pack",s) = "#exists#" == nm - sameFamily (_,s) = getFamily s == nm + + sameFamily (_, (_,Abs{})) = False + sameFamily ("pack",_) = "#exists#" == nm + sameFamily (_,(_,s)) = getFamily s == nm targets <- case mfam of Just (nm,t) -> return $ [(nm,t)] @@ -459,25 +456,36 @@ let excludes = S.toList $ S.intersection (M.keysSet exists) $ freeVariables m searchMaps <- mapM getVariablesBeforeExists excludes - let searchMap = M.union env $ case searchMaps of + let searchMap :: ContextMap + searchMap = M.union env $ case searchMaps of [] -> mempty a:l -> foldr (M.intersection) a l return $ filter sameFamily $ M.toList searchMap if all isFixed $ S.toList $ S.union (freeVariables m) (freeVariables goal) - then return $ Just [] + then ret $ Just [] else case targets of - [] -> return Nothing - _ -> Just <$> (F.asum $ leftSearch m goal <$> reverse targets) -- reversing works for now, but not forever! need a heuristics + bidirectional search + control structures - + [] -> ret Nothing + _ -> inter [] $ sortBy (\a b -> compare (getVal a) (getVal b)) targets + where ls (nm,target) = leftSearch (m,goal) (var nm, target) + getVal = snd . fst . snd + + inter [] [] = throwError "no more options" + inter cg [] = appendErr "" $ F.asum $ reverse cg + inter cg ((nm,((sequ,_),targ)):l) = do + 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 + else inter (ret res:cg) l + + a .-. s = foldr (\k v -> M.delete k v) a s -leftSearch m goal (x,target) = vtrace 1 ("LS: " ++ show m ++" ∈ "++ show goal - ++"\n\t@ " ++x++" : " ++show target) - $ leftCont (var x) target - where leftCont n target = throwTrace 3 ("DEFER: LS: " ++ show m ++" ∈ "++ show goal - ++"\n\t@ " ++x++" : " ++show target) <|> case target of +leftSearch (m,goal) (x,target) = vtrace 1 ("LS: " ++ show x++" ∈ " ++show target++" >> " ++show m ++" ∈ "++ show goal) + $ leftCont x target + where leftCont n target = case target of Spine "#forall#" [a, b] -> do x' <- getNewWith "@sla" modifyCtxt $ addToTail "-lsF-" Exists x' a @@ -490,9 +498,10 @@ cons <- leftCont (n `apply` (tycon x $ var x')) (subst (x |-> var x') b) return $ cons++[var x' :@: a] Spine _ _ -> do - return $ [goal :=: target , m :=: n] + return $ [goal :=: target, m :=: n] _ -> error $ "λ does not have type atom: " ++ show target + search :: Type -> Env (Substitution, Term) search ty = do e <- getNewWith "@e" @@ -626,7 +635,7 @@ Nothing -> lift $ throwTrace 0 $ "variable: "++show head++" not found in the environment." ++ "\n\t from "++ show sp ++ "\n\t from "++ show ty - Just ty' -> Spine head <$> chop ty' args + Just ty' -> Spine head <$> chop (snd ty') args checkFullType :: Spine -> Type -> Env (Spine, Constraint) checkFullType val ty = typeCheckToEnv $ checkType val ty @@ -634,8 +643,8 @@ ---------------------- --- type inference --- ---------------------- -typeInfer :: ContextMap -> (Name,Spine,Type) -> Choice (Term,Type, ContextMap) -typeInfer env (nm,val,ty) = (\r -> (\(a,_,_) -> a) <$> runRWST r (M.union envConsts env) emptyState) $ do +typeInfer :: ContextMap -> ((Bool,Integer),Name,Spine,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 ty val <- return $ alphaConvert mempty val @@ -651,7 +660,7 @@ resT = rebuildFromMem mem' $ unsafeSubst sub ty vtrace 0 ("RESULT: "++nm++" : "++show resV) $ - return $ (resV,resT, M.insert nm resV env) + return $ (resV,resT, M.insert nm (seqi,resV) env) unsafeSubst s (Spine nm apps) = let apps' = unsafeSubst s <$> apps in case s ! nm of Just nm -> rebuildSpine nm apps' @@ -661,39 +670,43 @@ ---------------------------- --- the public interface --- ---------------------------- -typeCheckAxioms :: [(Maybe Name,Bool,Name,Term,Type)] -> Choice ContextMap + +type FlatPred = [(Maybe Name,(Bool,Integer,Bool),Name,Term,Type)] +typeCheckAxioms :: FlatPred -> Choice Substitution typeCheckAxioms lst = do -- check the closedness of families. this gets done -- after typechecking since family checking needs to evaluate a little bit -- in order to allow defs in patterns - let notval (_,s,'#':'v':':':_,_,_) = False - notval (_,s,_,_,_) = True + let notval (_,_,'#':'v':':':_,_,_) = False + notval (_,_,_,_,_) = True - unsound (_,s,_,_,_) = not s + unsound (_,(_,_,s),_,_,_) = not s - tys = M.fromList $ map (\(_,_,nm,ty,_) -> (nm,ty)) $ filter notval lst + tys = M.fromList $ map (\(_,(b,i,_),nm,ty,_) -> (nm,((b,i),ty))) $ filter notval lst uns = S.fromList $ map (\(_,_,nm,ty,_) -> nm) $ filter unsound $ filter notval lst + inferAll :: (ContextMap, FlatPred, FlatPred) -> Choice (FlatPred,ContextMap) inferAll (l , r, []) = return (r,l) inferAll (_ , r, (_,_,nm,_,_):_) | nm == tipeName = throwTrace 0 $ tipeName++" can not be overloaded" inferAll (_ , r, (_,_,nm,_,_):_) | nm == atomName = throwTrace 0 $ atomName++" can not be overloaded" - inferAll (l , r, (fam,s,nm,val,ty):toplst) = do + 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) $ vtrace 0 ("\tVAL: " ++show val ++"\n\t:: " ++show ty) $ - typeInfer l (nm, val,ty) -- constrain the breadth first search to be local! + typeInfer l ((b,i),nm, val,ty) -- constrain the breadth first search to be local! -- do the family check after ascription removal and typechecking because it can involve computation! unless (fam == Nothing || Just (getFamily val) == fam) $ throwTrace 0 $ "not the right family: need "++show fam++" for "++nm ++ " = " ++show val inferAll $ case nm of - '#':'v':':':nm' -> (sub <$> l', (fam,s,nm,val,ty):r , fsub <$> toplst) - where sub = subst $ nm' |-> ascribe val ty -- the ascription isn't necessary because we don't have unbound variables + '#':'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 fsub (fam,s,nm,val,ty) = (fam,s,nm, sub val, sub ty) - _ -> (l', (fam,s,nm,val,ty):r, toplst) + _ -> (l', (fam,(b,i,s),nm,val,ty):r, toplst) (lst',l) <- inferAll (tys, [], topoSortAxioms lst) @@ -711,22 +724,30 @@ doubleCheckAll (S.union envSet uns) $ topoSortAxioms lst' - return l + return $ snd <$> l typeCheckAll :: [Predicate] -> Choice [Predicate] typeCheckAll preds = do - let toAxioms (Predicate s nm ty cs) = (Just $ atomName,s,nm,ty,tipe):map (\(nm',ty') -> (Just nm,False, nm',ty',atom)) cs - toAxioms (Query nm val) = [(Nothing, False,nm,val,atom)] - toAxioms (Define s nm val ty) = [(Nothing,False, nm,ty,kind), (Nothing,s, "#v:"++nm,val,ty)] - tyMap <- typeCheckAxioms $ concatMap toAxioms preds + + tyMap <- typeCheckAxioms $ toAxioms True preds - let newPreds (Predicate t nm _ cs) = Predicate t nm (tyMap M.! nm) $ map (\(nm,_) -> (nm,tyMap M.! nm)) cs + 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) return $ newPreds <$> preds + +toAxioms :: Bool -> [Predicate] -> [(Maybe [Char], (Bool, Integer, Bool), Name, Type, Spine)] +toAxioms b = concat . zipWith toAxioms' [0..] + where toAxioms' j (Predicate s nm ty cs) = (Just $ atomName,(False,j,s),nm,ty,tipe):zipWith (\(sequ,(nm',ty')) i -> (Just nm,(sequ,i,False), nm',ty',atom)) cs [0..] + toAxioms' j (Query nm val) = [(Nothing, (False,j,False),nm,val,atom)] + toAxioms' j (Define s nm val ty) = (if b then ((Nothing,(False,j,s), "#v:"++nm,val,ty):) else id) + [(Nothing,(False,j,False), nm,ty,kind)] -solver :: [(Name,Type)] -> Type -> Either String [(Name, Term)] -solver axioms tp = case runError $ runRWST (search tp) (M.union envConsts $ M.fromList axioms) emptyState of +toSimpleAxioms :: [Predicate] -> ContextMap +toSimpleAxioms l = M.fromList $ (\(_,(seqi,i,_),nm,t,_) -> (nm,((seqi,i),t))) <$> toAxioms False l + +solver :: ContextMap -> Type -> Either String [(Name, Term)] +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 diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -39,15 +39,16 @@ putStrLn "\nTARGETS: " forM_ targets $ \s -> putStrLn $ show s++"\n" - let allTypes c = (predName c, predType c):predConstructors c - predicates' = sub predicates + let predicates' = sub predicates targets' = sub targets - forM_ targets' $ \target -> - case solver (concatMap allTypes predicates') $ predType target of + + axioms = toSimpleAxioms predicates' + + forM_ targets' $ \target -> do + putStrLn $ "\nTARGET: \n"++show target + case solver axioms $ predType target of Left e -> putStrLn $ "ERROR: "++e - Right sub -> putStrLn $ - "\nTARGET: \n"++show target - ++"\n\nSOLVED WITH:\n" + Right sub -> putStrLn $ "SOLVED WITH:\n" ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub main = do diff --git a/Parser.hs b/Parser.hs --- a/Parser.hs +++ b/Parser.hs @@ -115,15 +115,17 @@ unsound = do reserved "unsound" - vsn False - + vsn False + + + vsn s = do (nm,ty) <- named decTipe - let more = do reservedOp "|" - - lst <- flip sepBy1 (reservedOp "|") $ do - (nm,t) <- named decPred - return (nm,t) + let more = do lst <- many1 $ do + seqi <- (reservedOp "|" >> return False) + <|> (reservedOp ">|" >> return True) + (nm,t) <- named decPred + return (seqi,(nm,t)) optional semi return $ Predicate s nm ty lst diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -81,11 +81,13 @@ | 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 = [N] add zero N N + | add_succ = [N M R] add (succ N) M (succ R) <- add N M R -- we can define subtraction from addition! -query subtract = add (succ (succ zero)) 'v (succ (succ (succ zero))) +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? @@ -98,14 +100,6 @@ , putStr "\nbye!\n") ``` -* Shell commands: - -``` -defn ls : string -> string -> prop - | ls-imp = [Args Out : string] - ls Args S <- cmd "ls" Args Out -``` - * Higher order logic programming: like in twelf and lambda-prolog. This makes HOAS much easier to do. ``` @@ -182,6 +176,32 @@ -- 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 = [A] runBoth A + <- putStr "tttt " + <- A =:= true + + | run1 = [A] runBoth A + <- putStr "vvvv" + <- A =:= true + + | run2 = [A] runBoth A + <- putStr "qqqq" + <- A =:= true + + >| run3 = [A] 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)! diff --git a/TopoSortAxioms.hs b/TopoSortAxioms.hs --- a/TopoSortAxioms.hs +++ b/TopoSortAxioms.hs @@ -9,7 +9,7 @@ $ filter (not . flip elem (map fst consts)) $ S.toList $ freeVariables val `S.union` freeVariables ty -topoSortAxioms :: [(Maybe Name, Bool, Name,Term,Type)] -> [(Maybe Name, Bool, Name,Term,Type)] +topoSortAxioms :: [(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 diff --git a/caledon.cabal b/caledon.cabal --- a/caledon.cabal +++ b/caledon.cabal @@ -1,6 +1,6 @@ Name: caledon -Version: 2.0.0.0 +Version: 2.1.0.0 Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. diff --git a/examples/nondet.ncc b/examples/nondet.ncc new file mode 100644 --- /dev/null +++ b/examples/nondet.ncc @@ -0,0 +1,43 @@ +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 + +defn runBoth : bool -> prop + >| run0 = [A] runBoth A + <- putChar 't' + <- putChar 't' + <- putChar 't' + <- putChar 't' + <- A =:= true + + | run1 = [A] runBoth A + <- putChar 'v' + <- putChar 'v' + <- putChar 'v' + <- putChar 'v' + <- A =:= true + + | run2 = [A] runBoth A + <- putChar 'q' + <- putChar 'q' + <- putChar 'q' + <- putChar 'q' + <- A =:= true + + >| run3 = [A] runBoth A + <- putChar 'j' + <- putChar 'j' + <- putChar 'j' + <- putChar 'j' + <- A =:= false + +query main = runBoth false + diff --git a/examples/prelude.ncc b/examples/prelude.ncc --- a/examples/prelude.ncc +++ b/examples/prelude.ncc @@ -12,10 +12,9 @@ | do = io | , = io -> prop -> io - defn run : io -> prop - | runDo = run do - | runSeq = [A][B] run (A , B) <- run A + >| runDo = run do + >| runSeq = [A][B] run (A , B) <- run A <- B defn readLine : (string -> io) -> prop -- builtin @@ -62,12 +61,12 @@ ------------------- fixity none 1 =:= defn =:= : {Q} Q -> Q -> prop - | eq = [a : prop][b:a] (=:=) {Q = a} b b + >| 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 + >| and = [a b : prop] a -> b -> a /\ b fixity none 0 \/ defn \/ : prop -> prop -> prop @@ -91,7 +90,7 @@ -- 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] + >| ppimp = [M][Foo : M -> M -> M -> prop][M1 M2 M3 : M] (++) {Foo = Foo} M1 M2 M3 <- concatable M Foo <- Foo M1 M2 M3 @@ -100,11 +99,11 @@ --- Order --- ------------- defn orderable : [M : prop] (M -> M -> prop) -> prop - | orderableNatural = orderable natural lte-nat + >| 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] + >| ooimp = [M][Foo : M -> M -> prop] [M1 M2 : M] (=<) {M = M} M1 M2 <- orderable M Foo <- Foo M1 M2 @@ -119,8 +118,8 @@ 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) + >| 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) @@ -132,13 +131,13 @@ 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 + >| 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 + >| ltZero = [B] zero < succ B + >| ltSucc = [A B] succ A < succ B <- A < B query add2 = exists A : natural . add (succ zero) zero A @@ -164,16 +163,16 @@ | 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 + >| 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_Nil = putStr $ nil {a = char} + >| putStr_Cons = [v:char][l: string] putStr $ cons {a = char} v l <- putChar v <- putStr l @@ -195,8 +194,8 @@ 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)) + >| 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 diff --git a/media/.DS_Store b/media/.DS_Store deleted file mode 100644 Binary files a/media/.DS_Store and /dev/null differ diff --git a/media/._.DS_Store b/media/._.DS_Store deleted file mode 100644 Binary files a/media/._.DS_Store and /dev/null differ diff --git a/media/logo.png b/media/logo.png deleted file mode 100644 Binary files a/media/logo.png and /dev/null differ diff --git a/media/logo.svg b/media/logo.svg deleted file mode 100644 --- a/media/logo.svg +++ /dev/null @@ -1,90 +0,0 @@ - - - - - - - - - - image/svg+xml - - - - - - - - - - - - - - -