caledon 3.0.0.0 → 3.1.0.0
raw patch · 17 files changed
+760/−526 lines, 17 filesdep +lens
Dependencies added: lens
Files
- AST.hs +132/−335
- Context.hs +1/−0
- HOU.hs +116/−85
- Main.hs +23/−15
- Options.hs +52/−0
- Parser.hs +77/−67
- Substitution.hs +291/−0
- caledon.cabal +8/−4
- examples/#test.ncc# +25/−0
- examples/coc.ncc +3/−3
- examples/readlinein.ncc +12/−2
- examples/universe.ncc +6/−7
- prelude/concatable.ncc +4/−4
- prelude/io.ncc +6/−0
- prelude/list.ncc +2/−2
- prelude/logic.ncc +1/−1
- prelude/strings.ncc +1/−1
AST.hs view
@@ -1,67 +1,102 @@ {-# LANGUAGE FlexibleInstances,- PatternGuards, BangPatterns, FlexibleContexts,- TupleSections+ TemplateHaskell,+ NoMonomorphismRestriction #-}- module AST where import qualified Data.Foldable as F-import Data.List-import Data.Maybe-import Data.Monoid import Data.Functor-import qualified Data.Map as M-import Data.Map (Map) import qualified Data.Set as S-import Control.Monad.RWS (RWST)-import Control.Monad.State.Class (MonadState(), get, modify)+import qualified Data.Map as M+import Data.Maybe+import Data.Monoid+import Data.List -import Choice+import Control.Lens ---------------------------------- abstract syntax tree --------------------------------- type Name = String -infixr 0 ~>-infixr 0 ~~>-(~>) = forall ""-(~~>) = imp_forall ""- data Spine = Spine Name [Type] | Abs Name Type Spine deriving (Eq)+ +instance Monoid Spine where + mempty = undefined+ mappend = undefined+instance Monoid Bool where + mempty = undefined+ mappend = undefined +type Kind = Spine type Type = Spine type Term = Spine+data Decl = Predicate { _declIsSound :: !Bool+ , _declName :: !Name+ , _declType :: !Type+ , _declConstructors :: ![(Bool,(Name,Type))] + }+ | Query { _declName :: !Name+ , _declType :: !Type+ }+ | Define { _declIsSound :: !Bool+ , _declName :: !Name+ , _declValue :: !Term+ , _declType :: !Type+ }+ deriving (Eq) -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) -class ValueTracker c where- putValue :: Integer -> c -> c- takeValue :: c -> Integer+data PredData = PredData { _dataFamily :: Maybe Name+ , _dataSequential :: Bool+ , _dataPriority :: Integer+ , _dataSound :: Bool+ } -instance ValueTracker Integer where- putValue _ i = i- takeValue i = i+data FlatPred = FlatPred { _predData :: PredData+ , _predName :: Name+ , _predType :: Type+ , _predKind :: Kind+ }+$(makeLenses ''PredData)+$(makeLenses ''FlatPred)+$(makeLenses ''Decl) -getNew :: (Functor m, MonadState c m, ValueTracker c) => m String-getNew = do- st <- takeValue <$> get- let n = 1 + st- modify $ putValue n- return $ show n- -getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String-getNewWith s = {- (++s) <$> -} getNew+predFamily = predData . dataFamily+predSequential = predData . dataSequential+predPriority = predData . dataPriority+predSound = predData . dataSound +-------------------------+--- Constraint types ---+-------------------------++data Quant = Forall | Exists deriving (Eq) ++infix 2 :=: +infix 2 :@: +infixr 1 :&:++-- we can make this data structure mostly strict since the only time we don't +-- traverse it is when we fail, and in order to fail, we always have to traverse+-- the lhs!+data SCons = !Term :@: !Type+ | !Spine :=: !Spine+ deriving (Eq)+data Constraint = SCons [SCons]+ -- we don't necessarily have to traverse the rhs of a combination+ -- so we can make it lazy+ | !Constraint :&: Constraint + | Bind !Quant !Name !Type !Constraint+ deriving (Eq)+++-------------------------+--- Pretty Printing ---+------------------------- showWithParens t = if (case t of Abs{} -> True Spine "#infer#" _ -> True@@ -78,7 +113,6 @@ isOperator ('#':_) = False isOperator (a:_) = not $ elem a ('_':['a'..'z']++['A'..'Z']++['0'..'9']) - instance Show Spine where show (Spine ['\'',c,'\''] []) = show c show (Spine "#infer#" [_, Abs nm t t']) = "<"++nm++" : "++show t++"> "++show t'@@ -92,209 +126,32 @@ show (Spine "#imp_abs#" [_,Abs nm ty t]) = "?λ "++nm++" : "++showWithParens ty++" . "++show t show (Spine nm l@[_ , Abs _ _ _]) | isOperator nm = "("++nm++") "++show (Spine "" l) show (Spine nm (t:t':l)) | isOperator nm = "( "++showWithParens t++" "++nm++" "++ show t'++" )"++show (Spine "" l)- show (Spine h l) = h++concatMap showWithParens' l- where showWithParens' t = " "++if case t of+ show (Spine h l) = h++concatMap showWithParens l+ where showWithParens t = " "++if case t of Abs{} -> True Spine "#tycon#" _ -> False Spine _ lst -> not $ null lst then "("++show t++")" else show t show (Abs nm ty t) = "λ "++nm++" : "++showWithParens ty++" . "++show t -showT True = "defn "-showT False = "unsound " -instance Show Predicate where- show (Predicate 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 "\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- -var !nm = Spine nm []-atomName = "prop"-tipeName = "type"-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]-open cl (imp,ty) (p,iface) cty inexp = Spine "#open#" [cl, ty,Abs imp ty iface, Abs imp ty (Abs p iface cty), Abs imp ty (Abs p iface inexp)] -infer x tyA v = Spine ("#infer#") [tyA, Abs x tyA v]--imp_forall x tyA v = Spine ("#imp_forall#") [tyA, Abs x tyA v]-imp_abs x tyA v = Spine ("#imp_abs#") [tyA, Abs x tyA v]-tycon nm val = Spine "#tycon#" [Spine nm [val]]-------------------------- substitution ---------------------------type Substitution = M.Map Name Spine--infixr 1 |->-infixr 0 ***-m1 *** m2 = M.union m2 $ subst m2 <$> m1-(|->) = M.singleton-(!) = flip M.lookup---findTyconInPrefix nm = fip []- where fip l (Spine "#tycon#" [Spine nm' [v]]:r) | nm == nm' = Just (v, reverse l++r)- fip l (a@(Spine "#tycon#" [Spine _ [_]]):r) = fip (a:l) r- fip _ _ = Nothing--apply :: Spine -> Spine -> Spine-apply !a !l = rebuildSpine a [l]--rebuildSpine :: Spine -> [Spine] -> Spine-rebuildSpine s [] = s-rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of - Just (v, apps) -> rebuildSpine (Abs nm ty rst) (v:apps)- Nothing -> seq sp $ if ty == atom && S.notMember nm (freeVariables rs) then rs else irs - -- proof irrelevance hack- -- we know we can prove that type "prop" is inhabited- -- irs - the proof doesn't matter- -- rs - the proof matters- -- irs - here, the proof might matter, but we don't know if we can prove the thing, - -- so we need to try- where nm' = newNameFor nm $ freeVariables apps- sp = subst (nm |-> var nm') rst- rs = rebuildSpine sp apps- irs = infer nm ty rs-rebuildSpine (Spine c apps) apps' = Spine c $ apps ++ apps'-rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) $ rst- in seq sp $ rebuildSpine sp apps'--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- --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 - alphaConvert :: S.Set Name -> a -> a- rebuildFromMem :: Map Name Name -> a -> a - -instance Subst a => Subst [a] where- substFree s f t = substFree s f <$> t- -instance Alpha a => Alpha [a] where - alphaConvert s l = alphaConvert s <$> l- rebuildFromMem s l = rebuildFromMem s <$> l- -instance (Subst a, Subst b) => Subst (a,b) where- substFree s f ~(a,b) = (substFree s f a , substFree s f b)- -instance Subst Spine where- substFree s f sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of- False -> imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) f rst- True -> error $ - "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp - ++ "\n\tfor: "++show s- substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of- False -> imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) f rst - True -> error $ - "can not capture free variables because implicit binds can not alpha convert: "++ show sp- ++ "\n\tfor: "++show s- substFree s f (Abs nm tp rst) = Abs nm' (substFree s f tp) $ substFree s' f' rst- where (nm',s',f') = newName nm s f- substFree s f (Spine "#tycon#" [Spine c [v]]) = Spine "#tycon#" [Spine c [substFree s f v]]- substFree s f (Spine nm apps) = let apps' = substFree s f <$> apps in- case s ! nm of- Just nm -> rebuildSpine nm apps'- _ -> Spine nm apps'- -instance Alpha Spine where- alphaConvert s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty $ alphaConvert (S.insert a s) r- alphaConvert s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty $ alphaConvert (S.insert a s) r- alphaConvert s (Abs nm ty r) = Abs nm' (alphaConvert s ty) $ alphaConvert (S.insert nm' s) r- where nm' = newNameFor nm s- alphaConvert s (Spine a l) = Spine a $ alphaConvert s l- - rebuildFromMem s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r- rebuildFromMem s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r- rebuildFromMem s (Abs nm ty r) = Abs (fromMaybe nm $ M.lookup nm s) (rebuildFromMem s ty) $ rebuildFromMem s r- rebuildFromMem s (Spine a l) = Spine a' $ rebuildFromMem s l- where a' = fromMaybe a $ M.lookup a s- - -instance Subst Predicate where- substFree sub f (Predicate s nm ty cons) = Predicate s nm (substFree sub f ty) ((\(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)- -class FV a where - freeVariables :: a -> S.Set Name-instance (FV a, F.Foldable f) => FV (f a) where- freeVariables m = F.foldMap freeVariables m-instance FV Spine where- 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+instance Show Decl where+ show a = case a of+ Predicate s nm ty [] -> showDef s ++ nm ++ " : " ++ show ty+ Predicate s nm ty (a:cons) ->+ showDef s++ nm ++ " : " ++ show ty++showSingle a ++ concatMap (\x-> showSingle x) cons+ where showSingle (b,(nm,ty)) = (if b then "\n >| " else "\n | ") ++nm ++ " = " ++ show ty+ Query nm val -> "query " ++ nm ++ " = " ++ show val+ Define s nm val ty -> showDef s ++ nm ++ " : " ++ show ty ++"\n as "++show val+ where showDef True = "defn "+ showDef False = "unsound " - ------------------------------ Constraint types -------------------------------data Quant = Forall | Exists deriving (Eq) - instance Show Quant where show Forall = "∀"- show Exists = "∃"---- as ineficient as it is, I'll make this the constraint representation.-infix 2 :=: -infix 2 :@: -infixr 1 :&:---- we can make this data structure mostly strict since the only time we don't --- traverse it is when we fail, and in order to fail, we always have to traverse--- the lhs!-data SCons = !Term :@: !Type- | !Spine :=: !Spine- deriving (Eq)-data Constraint = SCons [SCons]- -- we don't necessarily have to traverse the rhs of a combination- -- so we can make it lazy- | !Constraint :&: Constraint - | Bind !Quant !Name !Type !Constraint- deriving (Eq)- + show Exists = "∃" + instance Show SCons where show (a :=: b) = show a++" ≐ "++show b show (a :@: b) = show a++" ∈ "++show b@@ -308,11 +165,12 @@ where showWithParens Bind{} = show c showWithParens _ = "( "++show c++" )" +-----------------------------+--- Constraint Properties --- +----------------------------- instance Monoid Constraint where mempty = SCons []- mappend (SCons []) b = b- mappend a (SCons []) = a mappend (SCons a) (SCons b) = SCons $ a++b mappend a b = a :&: b@@ -325,115 +183,54 @@ "memptymappend" flip mappend mempty = id #-} -instance Subst SCons where- substFree s f c = case c of- s1 :@: s2 -> subq s f (:@:) s1 s2- s1 :=: s2 -> subq s f (:=:) s1 s2- -instance Subst Constraint where- substFree s f c = case c of- SCons l -> SCons $ map (substFree s f) l- s1 :&: s2 -> subq s f (:&:) s1 s2- Bind q nm t c -> Bind q nm' (substFree s f t) $ substFree s' f' c- where (nm',s',f') = newName nm s f- -subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2) -(∃) = Bind Exists-(∀) = Bind Forall- -infixr 0 <<$>-(<<$>) f m = ( \(a,b) -> (f a, b)) <$> m--regenM e a b = do- (a',s1) <- regenWithMem a - (b',s2) <- regenWithMem b - return $ (e a' b', M.union s1 s2)-regen e a b = do- a' <- regenAbsVars a - b' <- regenAbsVars b - return $ e a' b' - -class RegenAbsVars a where- regenAbsVars :: (Functor f, MonadState c f, ValueTracker c) => a -> f a- regenWithMem :: (Functor f, MonadState c f, ValueTracker c) => a -> f (a, Map Name Name)- -instance RegenAbsVars l => RegenAbsVars [l] where- regenAbsVars cons = mapM regenAbsVars cons- - regenWithMem cons = together <$> mapM regenWithMem cons- where together f = (l',foldr M.union mempty ss)- where (l',ss) = unzip f- +----------------------+--- Free Variables ---+----------------------+class FV a where + freeVariables :: a -> S.Set Name+instance (FV a, F.Foldable f) => FV (f a) where+ freeVariables m = F.foldMap freeVariables m+instance FV Spine where+ 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 - -instance RegenAbsVars Spine where - regenAbsVars (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <$> regenAbsVars r- regenAbsVars (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <$> regenAbsVars r- regenAbsVars (Abs a ty r) = do- a' <- getNewWith $ "@rega"- ty' <- regenAbsVars ty- r' <- regenAbsVars $ subst (a |-> var a') r- return $ Abs a' ty' r'- regenAbsVars (Spine a l) = Spine a <$> regenAbsVars l+instance FV FlatPred where+ freeVariables p = freeVariables (p^.predType) `S.union` freeVariables (p^.predKind) - regenWithMem (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <<$> regenWithMem r- regenWithMem (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <<$> regenWithMem r- regenWithMem (Abs a ty r) = do- a' <- getNewWith $ "@regm"- (ty',s1) <- regenWithMem ty- (r', s2) <- regenWithMem $ subst (a |-> var a') r- return $ (Abs a' ty' r', M.insert a' a $ M.union s1 s2)- regenWithMem (Spine a l) = Spine a <<$> regenWithMem l-+--------------------------------+--- Builtin Spines and types ---+--------------------------------+infixr 0 ~>+infixr 0 ~~>+(~>) = forall ""+(~~>) = imp_forall "" +var !nm = Spine nm [] -instance RegenAbsVars SCons where- regenAbsVars cons = case cons of- a :=: b -> regen (:=:) a b- a :@: b -> regen (:@:) a b- - regenWithMem cons = case cons of- a :=: b -> regenM (:=:) a b- a :@: b -> regenM (:@:) a b - -instance RegenAbsVars Constraint where - regenAbsVars cons = case cons of- Bind q nm ty cons -> do- ty' <- regenAbsVars ty- case nm of- "" -> do- nm' <- getNewWith "@newer"- let sub = nm |-> var nm'- Bind q nm' ty' <$> regenAbsVars (subst sub cons)- _ -> Bind q nm ty' <$> regenAbsVars cons- SCons l -> SCons <$> regenAbsVars l- a :&: b -> regen (:&:) a b- - regenWithMem cons = case cons of- Bind q nm ty cons -> do- (ty',s1) <- regenWithMem ty- nm' <- getNewWith "@regm'"- let sub = nm |-> var nm'- (cons',s2) <- regenWithMem $ subst sub cons- return (Bind q nm' ty' cons', M.insert nm' nm $ M.union s1 s2)- SCons l -> SCons <<$> regenWithMem l- a :&: b -> regenM (:&:) a b - -getFamily v = fromMaybe (error ("values don't have families: "++show v)) $ getFamilyM v+atomName = "prop"+tipeName = "type"+kindName = "#kind#" -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+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]+open cl (imp,ty) (p,iface) cty inexp = Spine "#open#" [cl, ty,Abs imp ty iface, Abs imp ty (Abs p iface cty), Abs imp ty (Abs p iface inexp)] +infer x tyA v = Spine ("#infer#") [tyA, Abs x tyA v] +imp_forall x tyA v = Spine ("#imp_forall#") [tyA, Abs x tyA v]+imp_abs x tyA v = Spine ("#imp_abs#") [tyA, Abs x tyA v]+tycon nm val = Spine "#tycon#" [Spine nm [val]] consts = [ (atomName , tipe) , (tipeName , kind)@@ -467,7 +264,7 @@ ] -anonymous ty = ((False,100),ty)+anonymous ty = ((False,10000),ty) envSet = S.fromList $ map fst consts
Context.hs view
@@ -4,6 +4,7 @@ module Context where import AST+import Substitution import Data.Monoid import Data.Functor import qualified Data.Map as M
HOU.hs view
@@ -9,6 +9,7 @@ import Choice import AST+import Substitution import Context import TopoSortAxioms import Control.Monad.State (StateT, forM_,runStateT, modify, get,put, State, runState)@@ -20,28 +21,31 @@ 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 import qualified Data.Set as S import Debug.Trace +import Control.Lens hiding (Choice(..))+ import System.IO.Unsafe+import Data.IORef -{-# INLINE level #-}-level = 0+{-# NOINLINE levelVar #-}+levelVar :: IORef Int+levelVar = unsafePerformIO $ newIORef 0 -{-# INLINE vtrace #-}+{-# NOINLINE level #-}+level = unsafePerformIO $ readIORef levelVar+ vtrace !i | i < level = trace vtrace !i = const id -{-# INLINE vtraceShow #-} vtraceShow !i1 !i2 s v | i2 < level = trace $ s ++" : "++show v vtraceShow !i1 !i2 s v | i1 < level = trace s vtraceShow !i1 !i2 s v = id -{-# INLINE throwTrace #-} throwTrace !i s = vtrace i s $ throwError s mtrace True = trace@@ -62,21 +66,22 @@ return $ l1 ++ l2 flatten (SCons l) = return l -type UnifyResult = Maybe (Substitution, [SCons])+type UnifyResult = Maybe (Substitution, [SCons], Bool) 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' = fail "" <|> do+ uniWhile !sub c' = fail "" <|> do exists <- getExists c <- regenAbsVars c' - let uniWith !wth !backup = searchIn 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)+ Just (sub',next',b) -> finish $ Just (sub', subst sub' (reverse r)+++ (if b then (++next') else (next'++)) (subst sub' l)) Nothing -> searchIn l $ next:r finish Nothing = backup finish (Just (!sub', c')) = do@@ -106,7 +111,7 @@ newReturn return cons = return $ case cons of Nothing -> Nothing- Just cons -> Just (mempty, cons)+ Just cons -> Just (mempty, cons, False) unifySearchAtom :: SCons -> CONT_T b Env UnifyResult unifySearchAtom (a :@: b) return = rightSearch a b $ newReturn return@@ -123,43 +128,43 @@ 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 "#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 a' <- getNewWith "@aL" modifyCtxt $ addToTail "-implicit-" Exists a' ty- return $ Just (mempty, [l `apply` var a' :=: b , var a' :@: ty])+ return $ Just (mempty, [l `apply` var a' :=: b , var a' :@: ty], False) (b, Spine "#imp_forall#" [ty, l]) -> vtrace 1 "-implicit-" $ do a' <- getNewWith "@aR" modifyCtxt $ addToTail "-implicit-" Exists a' ty- return $ Just (mempty, [b :=: l `apply` var a' , var a' :@: ty])+ 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 a <- getNewWith "@iaL" modifyCtxt $ addToTail "-imp_abs-" Exists a ty- return $ Just (mempty, [rebuildSpine l (var a:r) :=: b , var 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 a <- getNewWith "@iaR" modifyCtxt $ addToTail "-imp_abs-" Exists a ty- return $ Just (mempty, [b :=: rebuildSpine l (var a:r) , var a :@: ty])+ return $ Just (mempty, [b :=: rebuildSpine l (var a:r) , var a :@: ty], False) (Spine "#tycon#" [Spine nm [_]], Spine "#tycon#" [Spine nm' [_]]) | nm /= nm' -> throwTrace 0 $ "different type constraints: "++show cons (Spine "#tycon#" [Spine nm [val]], Spine "#tycon#" [Spine nm' [val']]) | nm == nm' -> - return $ Just (mempty, [val :=: val'])+ return $ Just (mempty, [val :=: val'], False) (Abs nm ty s , Abs nm' ty' s') -> vtrace 1 "-aa-" $ do modifyCtxt $ addToTail "-aa-" Forall nm ty- return $ Just (mempty, [ty :=: ty' , s :=: subst (nm' |-> var nm) s'])+ return $ Just (mempty, [ty :=: ty' , s :=: subst (nm' |-> var nm) s'], False) (Abs nm ty s , s') -> vtraceShow 1 2 "-asL-" cons $ do modifyCtxt $ addToTail "-asL-" Forall nm ty- return $ Just (mempty, [s :=: s' `apply` var nm])+ return $ Just (mempty, [s :=: s' `apply` var nm], False) (s, Abs nm ty s' ) -> vtraceShow 1 2 "-asR-" cons $ do modifyCtxt $ addToTail "-asR-" Forall nm ty- return $ Just (mempty, [s `apply` var nm :=: s'])+ return $ Just (mempty, [s `apply` var nm :=: s'], False) - (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [])+ (s , s') | s == s' -> vtrace 1 "-eq-" $ return $ Just (mempty, [], False) (s@(Spine x yl), s') -> vtrace 4 "-ss-" $ do bind <- getElm ("all: "++show cons) x case bind of@@ -170,9 +175,9 @@ bind' <- getElm ("gvar-blah: "++show cons) x' case bind' of Right ty' -> vtraceShow 1 2 "-gc-" cons $ -- gvar-const- --if allElementsAreVariables yl- --then gvar_const (Spine x yl, ty) (Spine x' y'l, ty') - -- else return Nothing+-- if allElementsAreVariables yl+-- then gvar_const (Spine x yl, ty) (Spine x' y'l, ty') +-- else return Nothing gvar_const (Spine x yl, ty) (Spine x' y'l, ty') Left Binding{ elmQuant = Forall } | not $ S.member x' $ freeVariables yl -> throwTrace 0 $ "CANT: gvar-uvar-depends: "++show (a :=: b)@@ -210,7 +215,7 @@ match _ _ = throwTrace 0 $ "CANT: different numbers of arguments on constant: "++show cons cons <- match yl yl'- return $ Just (mempty, cons)+ return $ Just (mempty, cons, False) _ -> throwTrace 0 $ "CANT: uvar against a pi WITH CONS "++show cons allElementsAreVariables :: [Spine] -> Bool@@ -236,12 +241,12 @@ ty' = foldr (\(nm,ty) a -> forall nm ty a) ty hl addSub Nothing = return Nothing- addSub (Just (sub',cons)) = do+ addSub (Just (sub',cons,b)) = do -- we need to solve subst twice because we might reify twice let sub'' = ((subst sub' <$> sub) *** sub') modifyCtxt $ subst sub'- return $ Just (sub'', cons)+ return $ Just (sub'', cons,b) modifyCtxt $ addToHead "-rtt-" Exists x' ty' . removeFromContext x vtrace 3 ("RAISING: "++x' ++" +@+ "++ show newx_args ++ " ::: "++show ty'@@ -278,7 +283,7 @@ modifyCtxt $ addToHead "-ggs-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!! - return $ Just (sub, []) -- var xN :@: xNty])+ return $ Just (sub, [], False) -- var xN :@: xNty]) gvar_gvar_same _ _ = error "gvar-gvar-same is not made for this case" @@ -313,7 +318,8 @@ modifyCtxt $ addToHead "-ggd-" Exists xN xNty -- THIS IS DIFFERENT FROM THE PAPER!!!! - vtrace 3 ("SUBST: -ggd- "++show sub) $ return $ Just (sub, []) -- var xN :@: xNty])+ vtrace 3 ("SUBST: -ggd- "++show sub) $ + return $ Just (sub, [] {- var xN :@: xNty] -}, False) gvar_uvar_inside a@(Spine _ yl, _) b@(Spine y _, _) = case elemIndex (var y) $ reverse yl of@@ -325,7 +331,7 @@ case elemIndex (var y) $ yl of Nothing -> gvar_fixed a b $ var . const y Just _ -> do- gvar_uvar_outside a b <|> gvar_fixed a b (var . const y) + gvar_uvar_outside a b <|> gvar_fixed a b (var . const y) gvar_const _ _ = error "gvar-const is not made for this case" @@ -388,8 +394,11 @@ addExists s t = vtrace 3 ("adding: "++show s++" ::: "++show t) $ addToHead "-gf-" Exists s t modifyCtxt $ flip (foldr ($)) $ uncurry addExists <$> substBty mempty bty xm modifyCtxt $ subst sub- - return $ Just (sub, [subst sub $ a :=: b])+ vtrace 4 ("RES: -gg- "++(show $ subst sub $ a :=: b)) $ + vtrace 4 ("FROM: -gg- "++(show $ a :=: b)) $ + return $ Just (sub, [ subst sub $ a :=: b -- this ensures that the function resolves to the intended output+ + ], False) gvar_fixed _ _ _ = error "gvar-fixed is not made for this case" @@ -439,7 +448,8 @@ 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 [] | nm == tipeName -> + ret $ Just [m :=: atom] Spine nm _ -> do constants <- getConstants foralls <- getForalls@@ -464,6 +474,7 @@ 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 @@ -471,9 +482,12 @@ 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) then ret $ Just [] else case targets of@@ -530,7 +544,7 @@ k <- getNewWith "@k" addToEnv (∃) k kind $ do r <- m $ var k- var k .@. kind+ var k .@. kind return r check v x = if x == "13@regm+f" then trace ("FOUND AT: "++ v) x else x@@ -540,6 +554,7 @@ checkType sp ty = case sp of Spine "#hole#" [] -> do x' <- getNewWith "@hole"+ addToEnv (∃) x' ty $ do var x' .@. ty return $ var x'@@ -701,7 +716,7 @@ else return prev'' getGenTys sp = S.filter isGen $ freeVariables sp- where isGen (c:s) = isUpper c+ where isGen (c:s) = elem c ['A'..'Z'] generateBinding sp = foldr (\a b -> imp_forall a ty_hole b) sp orderedgens where genset = getGenTys sp@@ -714,13 +729,14 @@ ---------------------- 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+ ty <- return $ alphaConvert mempty mempty ty+ val <- return $ alphaConvert mempty mempty val (ty,mem') <- regenWithMem ty- (val,mem) <- regenWithMem val+ (val,mem) <- vtrace 1 ("ALPHAD TO: "++show val) $ regenWithMem val - (val,constraint) <- 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@@ -740,26 +756,34 @@ --- the public interface --- ---------------------------- -type FlatPred = [(Maybe Name,(Bool,Integer,Bool),Name,Term,Type)]-typeCheckAxioms :: Bool -> FlatPred -> Choice Substitution+-- type FlatPred = [((Maybe Name,Bool,Integer,Bool),Name,Type,Kind)]++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 -- in order to allow defs in patterns- let notval (_,_,'#':'v':':':_,_,_) = False- notval (_,_,_,_,_) = True + let notval p = case p ^. predName of + '#':'v':':':_ -> False+ _ -> True - unsound (_,(_,_,s),_,_,_) = not s+ unsound = not . (^. predSound) - 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+ 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 - inferAll :: (ContextMap, FlatPred, FlatPred) -> Choice (FlatPred,ContextMap)+ 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,(b,i,s),nm,val,ty):toplst) = do+ 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+ 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 @@ -770,20 +794,22 @@ unless (fam == Nothing || Just (getFamily val) == fam) $ throwTrace 0 $ "not the right family: need "++show fam++" for "++nm ++ " = " ++show val + let resp = p & predType .~ val & predKind .~ ty inferAll $ case nm of- '#':'v':':':nm' -> (sub' <$> l', (fam,(b,i,s),nm,val,ty):r , fsub <$> toplst) + '#':'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) - -- 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)+ _ -> (l', resp:r, toplst) (lst',l) <- inferAll (tys, [], topoSortAxioms lst) let doubleCheckAll _ [] = return ()- doubleCheckAll l ((_,_,nm,val,ty):r) = do+ doubleCheckAll l (p:r) = do+ let nm = p^.predName+ val = p^.predType+ ty = p^.predKind+ let usedvars = freeVariables val `S.union` freeVariables ty unless (S.isSubsetOf usedvars l) $ throwTrace 0 $ "Circular type:"@@ -799,15 +825,16 @@ return $ snd <$> l -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+topoSortAxioms :: [FlatPred] -> [FlatPred]+topoSortAxioms axioms = topoSortComp (\p -> (p^.predName,) + -- unsound can mean this causes extra cyclical things to occur+ $ (if 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 - where nm2familyLst = catMaybes $ (\(fam,_,nm,_,_) -> (nm,) <$> fam) <$> axioms+ where nm2familyLst = catMaybes $ (\p -> (p^.predName,) <$> (p^.predFamily)) <$> axioms family2nmsMap = foldr (\(fam,nm) m -> M.insert nm (case M.lookup nm m of@@ -815,17 +842,18 @@ 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 + family2impliedsMap = M.fromList $ (\p -> (p^.predName, + mconcat + $ catMaybes + $ map (`M.lookup` family2nmsMap) + $ S.toList + $ getImpliedFamilies + $ p^.predType+ )) <$> axioms getImplieds nm = fromMaybe mempty (M.lookup nm family2impliedsMap) -typeCheckAll :: Bool -> [Predicate] -> Choice [Predicate]+typeCheckAll :: Bool -> [Decl] -> Choice [Decl] typeCheckAll verbose preds = do tyMap <- typeCheckAxioms verbose $ toAxioms True preds@@ -836,20 +864,23 @@ return $ newPreds <$> preds -toAxioms :: Bool -> [Predicate] -> [(Maybe [Char], (Bool, Integer, Bool), Name, Type, Spine)] +toAxioms :: Bool -> [Decl] -> [FlatPred] 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)] + 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)] -toSimpleAxioms :: [Predicate] -> ContextMap-toSimpleAxioms l = M.fromList $ (\(_,(seqi,i,_),nm,t,_) -> (nm,((seqi,i),t))) <$> toAxioms False l+toSimpleAxioms :: [Decl] -> ContextMap+toSimpleAxioms l = M.fromList $ (\p -> (p^.predName, ((p^.predSequential, p^.predPriority), p^.predType))) + <$> 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 -reduceDecsByName :: [Predicate] -> [Predicate]-reduceDecsByName decs = map snd $ M.toList $ M.fromList $ map (\a -> (predName a,a)) decs+reduceDecsByName :: [Decl] -> [Decl]+reduceDecsByName decs = map snd $ M.toList $ M.fromList $ map (\a -> (a ^. declName,a)) decs
Main.hs view
@@ -1,18 +1,22 @@+ module Main where +import Options import AST+import Substitution+ import Choice import HOU import Parser import System.Environment-import Data.Functor import Data.Foldable as F (forM_) import Data.List (partition)-import Text.Parsec import Data.Monoid import Control.Monad (when)-import Control.Arrow (first) +import Data.IORef++import Control.Lens ((^.), (.~), (&)) import Language.Preprocessor.Cpphs -----------------------------------------------------------------------@@ -33,7 +37,7 @@ Define {} -> True _ -> False - sub = subst $ foldr (\a r -> r *** (predName a |-> subst r (predValue a))) mempty defs+ sub = subst $ foldr (\a r -> r *** ((a^.declName) |-> subst r (a^.declValue))) mempty defs (predicates, targets) = flip partition others $ \x -> case x of Predicate {} -> True _ -> False@@ -53,14 +57,18 @@ forM_ targets' $ \target -> do when verbose $ putStrLn $ "\nTARGET: \n"++show target- case solver axioms $ predType target of+ case solver axioms $ target ^. declType of Left e -> putStrLn $ "ERROR: "++e Right sub -> when verbose $ putStrLn $ "SOLVED WITH:\n" ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub -processFile :: Bool -> String -> IO ()-processFile verbose fname = do+processFile :: Options -> IO ()+processFile options = do+ let fname = options ^. optFile+ + writeIORef levelVar $ options ^. optVerbose+ file <- readFile fname file <- runCpphs @@ -78,12 +86,12 @@ decs <- case mError of Left e -> error $ show e Right l -> return l- checkAndRun verbose $ reduceDecsByName decs-+ checkAndRun (not $ options ^. optIO_Only) $ reduceDecsByName decs+ main = do- fnames <- getArgs- case fnames of- [] -> 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\""+ (options, files) <- compilerOpts =<< getArgs+ + processFile $ options & case files of+ [] -> id+ [fname] -> optFile .~ fname+ _ -> error $ "Too many file arguments."++header
+ Options.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE + TemplateHaskell,+ FlexibleContexts+ #-}+module Options where++import Data.Maybe+import Control.Lens (makeLenses, (.~))+import System.Console.GetOpt++data Options = Options + { _optIO_Only :: Bool+ , _optVerbose :: Int+ , _optFile :: String+ } +$(makeLenses ''Options) ++defaultOptions = Options + { _optIO_Only = False+ , _optVerbose = 0+ , _optFile = ""+ }+++options :: [OptDescr (Options -> Options)]+options = + [ Option ['i'] ["io-only"]+ (NoArg $ optIO_Only .~ True)+ "don't print out typechecking info"+ , Option ['v'] ["verbosity"]+ (OptArg ((optVerbose .~) . fromMaybe 0 . fmap read) "VERBOSITY")+ "a number describing how much debugging information to print"+ , Option ['f'] ["file", "infile", "input"]+ (ReqArg (optFile .~) "INFILE")+ "the file to interpret and typecheck"+ ]++helpMessage = "Usage is \"caledon [--io-only] file.ncc\""++arg_lst = [ ["--io-only", "-i"]+ , ["--verbosity", "-V"]+ , ["--help", "-h"]+ , ["--file", "-f"]+ ]+ +compilerOpts :: [String] -> IO (Options,[String])+compilerOpts argv = + case getOpt Permute options argv of+ (o,n,[] ) -> return (foldl (flip id) defaultOptions o, n)+ (_,_,errs) -> ioError $ userError $ concat errs ++ usageInfo header options++header = "Usage: caledon [OPTIONS] file.ncc"
Parser.hs view
@@ -1,15 +1,23 @@ {-# LANGUAGE- RecordWildCards+ RecordWildCards,+ TemplateHaskell,+ FlexibleContexts,+ IncoherentInstances,+ TypeSynonymInstances,+ FlexibleInstances,+ MultiParamTypeClasses #-} module Parser (parseCaledon) where import AST-+import Substitution+import Control.Applicative (Applicative(..)) import Data.Functor import Data.Functor.Identity import Text.Parsec import Control.Monad (unless)+import Control.Monad.State.Class import Text.Parsec.Language (haskellDef) import Text.Parsec.Expr import Data.List@@ -20,98 +28,102 @@ import Debug.Trace import qualified Data.Foldable as F -+import Control.Lens ----------------------------------------------------------------------- -------------------------- PARSER ------------------------------------- ----------------------------------------------------------------------- --- | `parseCaledon` is the external interface-parseCaledon :: SourceName -> String -> Either ParseError [Predicate]-parseCaledon = runP decls emptyState+data Fixity = FixLeft | FixRight | FixNone -data ParseState = ParseState { currentVar :: Integer- , currentSet :: S.Set Name- , currentTable :: FixityTable - , currentOps :: [Name]+data FixityTable = FixityTable { _fixityBinary :: [(Integer,String, Assoc)] + , _fixityPrefix :: [(Integer, String, Assoc)]+ , _fixityPostfix :: [(Integer, String, Assoc)]+ , _opLambdas :: [String]+ , _strLambdas :: [String]+ , _binds :: [(String,String,String)]+ }+ + +data ParseState = ParseState { _currentVar :: Integer+ , _currentSet :: S.Set Name+ , _currentTable :: FixityTable + , _currentOps :: [Name] }+$(makeLenses ''FixityTable) +$(makeLenses ''ParseState) -data Fixity = FixLeft | FixRight | FixNone -data FixityTable = FixityTable { fixityBinary :: [(Integer,String, Assoc)] - , fixityPrefix :: [(Integer, String, Assoc)]- , fixityPostfix :: [(Integer, String, Assoc)]- , opLambdas :: [String]- , strLambdas :: [String]- , binds :: [(String,String,String)]- } +-- | `parseCaledon` is the external interface+parseCaledon :: SourceName -> String -> Either ParseError [Decl]+parseCaledon = runP decls emptyState++ emptyTable = FixityTable [] [] [] [] [] [] emptyState = (ParseState 0 mempty emptyTable []) type Parser = ParsecT String ParseState Identity -modifySet :: (S.Set Name -> S.Set Name) -> ParseState -> ParseState-modifySet f s = s { currentSet = f $ currentSet s }+instance MonadState ParseState Parser where+ get = getState+ put = putState -modifyVar :: (Integer -> Integer) -> ParseState -> ParseState-modifyVar f s = s { currentVar = f $ currentVar s } getNextVar :: Parser String getNextVar = do- v <- currentVar <$> getState- modifyState $ modifyVar (+1)+ v <- use currentVar+ currentVar %= (+1) return $ show v++"'" -decls :: Parser [Predicate]+decls :: Parser [Decl] decls = do whiteSpace lst <- many (topLevel <?> "declaration") eof- return lst--topLevel = fixityDef <|> query <|> defn+ return $ catMaybes lst -fixityDef = do +topLevel = Nothing <$ fixityDef + <|> Just <$> query + <|> Just <$> defn + <* optional (many semi)+ +fixityDef = do reserved "fixity" infixDef <|> lamDef- topLevel lamDef = do reserved "lambda" opLam <|> strLam -opLam = do - op <- operator- modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { opLambdas = op:opLambdas ct} }- -strLam = do- op <- identifier- modifyState $ \b -> b { currentTable = let ct = currentTable b in ct { strLambdas = op:strLambdas ct} }- +opLam = addOpLam operator opLambdas+strLam = addOpLam identifier strLambdas++addOpLam ident lens = do+ op <- ident+ currentTable.lens %= (op:)+ infixDef = do - -- I wish template haskell worked with record wild cards!- (setFixity) <- (reserved "left" >> return (\b c -> b { fixityBinary = c AssocLeft $ fixityBinary b} )) - <|> (reserved "none" >> return (\b c -> b { fixityBinary = c AssocNone $ fixityBinary b} )) - <|> (reserved "right" >> return (\b c -> b { fixityBinary = c AssocRight $ fixityBinary b} )) - <|> (reserved "pre" >> return (\b c -> b { fixityPrefix = c undefined $ fixityPrefix b}))- <|> (reserved "post" >> return (\b c -> b { fixityPostfix = c undefined $ fixityPostfix b}))+ setFixity <- (reserved "left" >> return (\b c -> over fixityBinary (c AssocLeft) b))+ <|> (reserved "none" >> return (\b c -> over fixityBinary (c AssocNone) b))+ <|> (reserved "right" >> return (\b c -> over fixityBinary (c AssocRight) b))+ <|> (reserved "pre" >> return (\b c -> over fixityPrefix (c undefined) b))+ <|> (reserved "post" >> return (\b c -> over fixityPostfix (c undefined) b)) n <- integer- op <- operator -- <|> identifier+ op <- operator let modify assoc = insertBy (\(n,_,_) (m,_,_) -> compare n m) (n,op, assoc)- modifyState $ \b -> b { currentTable = setFixity (currentTable b) modify- , currentOps = op:currentOps b} + currentTable %= flip setFixity modify+ currentOps %= (op:)+ -query :: Parser Predicate+query :: Parser Decl query = do- reserved "query"- (nm,ty) <- named decPred- optional semi- return $ Query nm ty+ reserved "query" + uncurry Query <$> named decPred -defn :: Parser Predicate+defn :: Parser Decl defn = sound <|> unsound sound = do@@ -131,11 +143,8 @@ <|> (reservedOp ">|" >> return True) (nm,t) <- named decPred return (seqi,(nm,t))- - optional semi return $ Predicate s nm ty lst- none = do optional semi- return $ Predicate s nm ty []+ none = do return $ Predicate s nm ty [] letbe = do reserved "as" val <- pTipe return $ Define s nm val ty@@ -168,11 +177,11 @@ tmpState :: String -> Parser a -> Parser a tmpState nm m = do- s <- currentSet <$> getState+ s <- use currentSet let b = S.member nm s- modifyState $ modifySet (S.insert nm)+ currentSet %= S.insert nm r <- m- unless b $ modifyState $ modifySet $ S.delete nm+ unless b $ currentSet %= S.delete nm return r @@ -183,7 +192,7 @@ pTipe = do- FixityTable bin prefix postfix opLams strLams binds <- currentTable <$> getState + FixityTable bin prefix postfix opLams strLams binds <- use currentTable let getSnd [] = [] getSnd (a:l) = l@@ -218,13 +227,14 @@ (parens anonNamed <|> anonNamed) return $ \input -> foldr (flip out tp) input nml + table = [ [ altPostfix ["λ", "\\"] ["lambda"] Abs , altPostfix ["?λ", "?\\"] ["?lambda"] imp_abs , altPostfix ["∃"] ["exists"] exists , regPostfix angles ["??"] ["infer"] infer , regPostfix brackets ["∀"] ["forall"] forall , regPostfix braces ["?∀"] ["?forall"] imp_forall- ]++[ altPostfix [op] [] (\nm t s -> Spine op [t,Abs nm ty_hole s] ) | op <- opLams ]+ ]++[ 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 "⇒"@@ -276,7 +286,7 @@ return $ ascribe v t (asc <|> return v <?> "function") - pOp = do operators <- currentOps <$> getState + pOp = do operators <- use currentOps choice $ flip map operators $ \nm -> do reserved nm return $ var nm <?> "operator" @@ -291,11 +301,9 @@ <|> pString <?> "atom" - pTycon = braces $ do- (nm,ty) <- named decVar- return $ tycon nm ty+ pTycon = braces $ uncurry tycon <$> named decVar - myParens s m = between (symbol "(" <?> ("("++s)) (symbol ")" <?> (s++")")) m+ myParens s m = (symbol "(" <?> ("("++s)) *> m <* (symbol ")" <?> (s++")")) ptipe <?> "tipe" @@ -326,3 +334,5 @@ getId :: Parser Char -> Parser String getId start = P.identifier $ P.makeTokenParser mydef { P.identStart = start }++
+ Substitution.hs view
@@ -0,0 +1,291 @@+{-# LANGUAGE+ FlexibleInstances,+ PatternGuards,+ BangPatterns,+ FlexibleContexts,+ TupleSections+ #-}++module Substitution where++import AST++import qualified Data.Foldable as F+import Data.List+import Data.Maybe+import Data.Monoid+import Data.Functor+import qualified Data.Map as M+import Data.Map (Map)+import qualified Data.Set as S+import Control.Monad.RWS (RWST)+import Control.Monad.State.Class (MonadState(), get, modify)++import Control.Lens hiding (Choice(..))+---------------------+--- New Variables ---+---------------------++class ValueTracker c where+ putValue :: Integer -> c -> c+ takeValue :: c -> Integer++instance ValueTracker Integer where+ putValue _ i = i+ takeValue i = i++getNew :: (Functor m, MonadState c m, ValueTracker c) => m String+getNew = do+ st <- takeValue <$> get+ let n = 1 + st+ modify $ putValue n+ return $ show n+ +getNewWith :: (Functor f, MonadState c f, ValueTracker c) => String -> f String+getNewWith s = {- (++s) <$> -} getNew++ +---------------------+--- substitution ---+---------------------++type Substitution = M.Map Name Spine++infixr 1 |->+infixr 0 ***+m1 *** m2 = M.union m2 $ subst m2 <$> m1+(|->) = M.singleton+(!) = flip M.lookup+++findTyconInPrefix nm = fip []+ where fip l (Spine "#tycon#" [Spine nm' [v]]:r) | nm == nm' = Just (v, reverse l++r)+ fip l (a@(Spine "#tycon#" [Spine _ [_]]):r) = fip (a:l) r+ fip _ _ = Nothing++apply :: Spine -> Spine -> Spine+apply !a !l = rebuildSpine a [l]++rebuildSpine :: Spine -> [Spine] -> Spine+rebuildSpine s [] = s+rebuildSpine (Spine "#imp_abs#" [_, Abs nm ty rst]) apps = case findTyconInPrefix nm apps of + Just (v, apps) -> rebuildSpine (Abs nm ty rst) (v:apps)+ Nothing -> seq sp $ if ty == atom && S.notMember nm (freeVariables rs) then rs else irs + -- proof irrelevance hack+ -- we know we can prove that type "prop" is inhabited+ -- irs - the proof doesn't matter+ -- rs - the proof matters+ -- irs - here, the proof might matter, but we don't know if we can prove the thing, + -- so we need to try+ where nm' = newNameFor nm $ freeVariables apps+ sp = subst (nm |-> var nm') rst+ rs = rebuildSpine sp apps+ irs = infer nm ty rs+rebuildSpine (Spine c apps) apps' = Spine c $ apps ++ apps'+rebuildSpine (Abs nm _ rst) (a:apps') = let sp = subst (nm |-> a) $ rst+ in seq sp $ rebuildSpine sp apps'++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+ ++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 :: 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+ +instance (Subst a, Subst b) => Subst (a,b) where+ substFree s f ~(a,b) = (substFree s f a , substFree s f b)+ +instance Subst Spine where+ substFree s f sp@(Spine "#imp_forall#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of+ False -> imp_forall nm (substFree s f tp) $ substFree (M.delete nm s) f rst+ True -> error $ + "can not capture free variables because implicits quantifiers can not alpha convert: "++ show sp + ++ "\n\tfor: "++show s+ substFree s f sp@(Spine "#imp_abs#" [_, Abs nm tp rst]) = case "" /= nm && S.member nm f && not (S.null $ S.intersection (M.keysSet s) $ freeVariables sp) of+ False -> imp_abs nm (substFree s f tp) $ substFree (M.delete nm s) f rst + True -> error $ + "can not capture free variables because implicit binds can not alpha convert: "++ show sp+ ++ "\n\tfor: "++show s+ substFree s f (Abs nm tp rst) = Abs nm' (substFree s f tp) $ substFree s' f' rst+ where (nm',s',f') = newName nm s f+ substFree s f (Spine "#tycon#" [Spine c [v]]) = Spine "#tycon#" [Spine c [substFree s f v]]+ substFree s f (Spine nm apps) = let apps' = substFree s f <$> apps in+ case s ! nm of+ Just nm -> rebuildSpine nm apps'+ _ -> Spine nm apps'+ +instance Alpha Spine where+ alphaConvert s m (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty $ alphaConvert (S.insert a s) (M.delete a m) r+ alphaConvert s m (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty $ alphaConvert (S.insert a s) (M.delete a m) r+ alphaConvert s m (Abs nm ty r) = Abs nm' (alphaConvert s m ty) $ alphaConvert (S.insert nm' s) (M.insert nm nm' m) r+ where nm' = newNameFor nm s+ alphaConvert s m (Spine "#tycon#" [Spine c [v]]) = tycon c $ alphaConvert s m v + alphaConvert s m (Spine a l) = Spine (fromMaybe a (m ! a)) $ alphaConvert s m l+ + rebuildFromMem s (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r+ rebuildFromMem s (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a (rebuildFromMem s ty) $ rebuildFromMem (M.delete a s) r+ rebuildFromMem s (Abs nm ty r) = Abs (fromMaybe nm $ M.lookup nm s) (rebuildFromMem s ty) $ rebuildFromMem s r+ rebuildFromMem s (Spine a l) = Spine a' $ rebuildFromMem s l+ where a' = fromMaybe a $ M.lookup a s+ + +instance Subst Decl where+ 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)+++instance Subst FlatPred where+ substFree sub f p = p & predType %~ substFree sub f+ & predKind %~ substFree sub f++ +-------------------------+--- Constraint types ---+-------------------------++instance Subst SCons where+ substFree s f c = case c of+ s1 :@: s2 -> subq s f (:@:) s1 s2+ s1 :=: s2 -> subq s f (:=:) s1 s2+ +instance Subst Constraint where+ substFree s f c = case c of+ SCons l -> SCons $ map (substFree s f) l+ s1 :&: s2 -> subq s f (:&:) s1 s2+ Bind q nm t c -> Bind q nm' (substFree s f t) $ substFree s' f' c+ where (nm',s',f') = newName nm s f+ ++subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2)++(∃) = Bind Exists+(∀) = Bind Forall+ +infixr 0 <<$>+(<<$>) f m = ( \(a,b) -> (f a, b)) <$> m++regenM e a b = do+ (a',s1) <- regenWithMem a + (b',s2) <- regenWithMem b + return $ (e a' b', M.union s1 s2)+regen e a b = do+ a' <- regenAbsVars a + b' <- regenAbsVars b + return $ e a' b' + +class RegenAbsVars a where+ regenAbsVars :: (Functor f, MonadState c f, ValueTracker c) => a -> f a+ regenWithMem :: (Functor f, MonadState c f, ValueTracker c) => a -> f (a, Map Name Name)+ +instance RegenAbsVars l => RegenAbsVars [l] where+ regenAbsVars cons = mapM regenAbsVars cons+ + regenWithMem cons = together <$> mapM regenWithMem cons+ where together f = (l',foldr M.union mempty ss)+ where (l',ss) = unzip f+ ++ +instance RegenAbsVars Spine where + regenAbsVars (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <$> regenAbsVars r+ regenAbsVars (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <$> regenAbsVars r+ regenAbsVars (Abs a ty r) = do+ a' <- getNewWith $ "@rega"+ ty' <- regenAbsVars ty+ r' <- regenAbsVars $ subst (a |-> var a') r+ return $ Abs a' ty' r'+ regenAbsVars (Spine a l) = Spine a <$> regenAbsVars l+ + regenWithMem (Spine "#imp_forall#" [_,Abs a ty r]) = imp_forall a ty <<$> regenWithMem r+ regenWithMem (Spine "#imp_abs#" [_,Abs a ty r]) = imp_abs a ty <<$> regenWithMem r+ regenWithMem (Abs a ty r) = do+ a' <- getNewWith $ "@regm"+ (ty',s1) <- regenWithMem ty+ (r', s2) <- regenWithMem $ subst (a |-> var a') r+ return $ (Abs a' ty' r', M.insert a' a $ M.union s1 s2)+ regenWithMem (Spine a l) = Spine a <<$> regenWithMem l++++instance RegenAbsVars SCons where+ regenAbsVars cons = case cons of+ a :=: b -> regen (:=:) a b+ a :@: b -> regen (:@:) a b+ + regenWithMem cons = case cons of+ a :=: b -> regenM (:=:) a b+ a :@: b -> regenM (:@:) a b + +instance RegenAbsVars Constraint where + regenAbsVars cons = case cons of+ Bind q nm ty cons -> do+ ty' <- regenAbsVars ty+ case nm of+ "" -> do+ nm' <- getNewWith "@newer"+ let sub = nm |-> var nm'+ Bind q nm' ty' <$> regenAbsVars (subst sub cons)+ _ -> Bind q nm ty' <$> regenAbsVars cons+ SCons l -> SCons <$> regenAbsVars l+ a :&: b -> regen (:&:) a b+ + regenWithMem cons = case cons of+ Bind q nm ty cons -> do+ (ty',s1) <- regenWithMem ty+ nm' <- getNewWith "@regm'"+ let sub = nm |-> var nm'+ (cons',s2) <- regenWithMem $ subst sub cons+ return (Bind q nm' ty' cons', M.insert nm' nm $ M.union s1 s2)+ SCons l -> SCons <<$> regenWithMem l+ a :&: b -> regenM (:&:) a b +++getFamily 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
caledon.cabal view
@@ -1,6 +1,6 @@ Name: caledon -Version: 3.0.0.0+Version: 3.1.0.0 Description: a dependently typed, polymorphic, higher order logic programming language based on the calculus of constructions designed for easier metaprogramming capabilities. @@ -28,21 +28,25 @@ executable caledon main-is: Main.hs- other-modules: HOU, Choice, Parser, AST, TopoSortAxioms, Context+ other-modules: HOU, Choice, Parser, + AST, TopoSortAxioms, + Context, Options, Substitution Build-depends: base >= 4.0 && < 5.0, mtl >= 2.0 && < 3.0, parsec >= 3.0 && < 4.0, containers >= 0.4 && < 1.0, transformers >= 0.3 && < 1.0,- cpphs >= 1.0 && < 2.0+ cpphs >= 1.0 && < 2.0,+ lens >= 3.0 && < 4.0 Extensions: FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RecordWildCards, BangPatterns,- TypeSynonymInstances+ TypeSynonymInstances,+ TemplateHaskell ghc-options: -O2 -optc-O3 -funfolding-use-threshold=16 -fspec-constr-count=10 -fdo-lambda-eta-expansion
+ examples/#test.ncc# view
@@ -0,0 +1,25 @@+#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/coc.ncc view
@@ -1,10 +1,10 @@-fixity lambda .λ+fixity lambda lam fixity lambda Π defn tm : prop | p = tm | t = tm- | .λ = tm → (tm → tm) → tm+ | lam = tm → (tm → tm) → tm | Π = tm → (tm → tm) → tm fixity none 0 ::@@ -12,4 +12,4 @@ | p_t = p :: t | lam_pi = [A : tm][T : tm -> tm][B : tm -> tm] ([x] x :: A -> T x :: B x )- -> (.λ x : A . T x) :: (Π x : A . B x) + -> (lam x : A . T x) :: (Π x : A . B x)
examples/readlinein.ncc view
@@ -1,5 +1,15 @@-#include <prelude.ncc>+#include "../prelude/prelude.ncc" -- switching the direction of the output to be input with unification!+ defn readLineIn : string -> prop- as \S . readLine $ \R . do , S =:= R+ 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/universe.ncc view
@@ -1,11 +1,10 @@-fixity right 0 $-defn $ : {a b:prop} (a -> b) -> a -> b- as ?\At Bt :prop . \ F . \A . F A +#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!@@ -19,12 +18,12 @@ unsound tm : {S : tm ty} tm S → prop | ty = tm ty | ♢ = tm ty -> tm ty- | Π = [T : tm ty] (tm T → tm T) → tm $ ♢ T+ | Π = [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)- | raise = {T : tm ty} tm T → tm $ ♢ T -defn isTm : {S : tm ty} {A : tm S} tm A -> prop+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 (Π A : ty . A)+query whattype0 = isTm { Kind = ty } { Ty = ♢ ty } ( Π A : ty . A) query whattype1 = isTm (lam A : ty . A)
prelude/concatable.ncc view
@@ -6,13 +6,13 @@ -------------- defn concatable : [M : prop] (M -> M -> M -> prop) -> prop- | concatableNat = concatable natural add- | concatableList = [A] concatable (list A) concatList+ >| 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 + | 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 view
@@ -1,4 +1,5 @@ #include <strings.ncc>+#include <combinators.ncc> --------------- -- builtins ---@@ -31,3 +32,8 @@ | 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 view
@@ -2,8 +2,8 @@ --- Lists --- ------------- defn list : prop -> prop- | nil = list A- | cons = A -> list A -> list A+ >| 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
prelude/logic.ncc view
@@ -20,7 +20,7 @@ ------------------- fixity none 5 =:= defn =:= : Q -> Q -> prop- >| eq = (=:=) {Q = A} B B+ >| eq = (B : A) =:= B -- searching for these is SLOW fixity none 0 /\
prelude/strings.ncc view
@@ -3,7 +3,7 @@ --------------- -- builtins --- ----------------defn char : prop -- builtin+defn char : prop defn string : prop as list char