Commit 5aacb188 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Generalize the CaPriCon operations into a class, to better manage de Bruijn...

Generalize the CaPriCon operations into a class, to better manage de Bruijn indices in dynamically-created terms
parent c8951c8a
......@@ -2,7 +2,7 @@
-- see http://haskell.org/cabal/users-guide/
name: capricon
version: 0.8.1.1
version: 0.8.2
-- synopsis:
-- description:
license: GPL-3
......
......@@ -90,10 +90,11 @@ setBytes :: String -> [Word8] -> JS.CIO ()
setBytes f v = setString f (map (toEnum . fromIntegral) v)
hasteDict :: COCDict JS.CIO String
hasteDict = cocDict ("0.8.1.3-js" :: String) getString getBytes setString setBytes
hasteDict = cocDict ("0.8.2-js" :: String) getString getBytes setString setBytes
main :: IO ()
main = JS.concurrent $ void $ do
maybe unit JS.focus =<< JS.elemById "content-scroll"
JS.wait 200
let runWordsState ws st = ($st) $ from (stateT.concatT) $^ do
......
......@@ -13,6 +13,28 @@ instance MonadSubIO IO IO where liftSubIO = id
instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
liftSubIO ma = lift $ liftSubIO ma
type MaxDelta = Int
type UniverseConstraint = [Maybe MaxDelta]
data UniverseConstraints = UniverseConstraints [UniverseConstraint]
instance Semigroup UniverseConstraints where
UniverseConstraints x + UniverseConstraints y = UniverseConstraints $ zipWith (zipWith (\_x _y -> zipWith max _x _y + _x + _y)) x y
instance Monoid UniverseConstraints where zero = UniverseConstraints (repeat (repeat Nothing))
data COCValue io str = COCExpr (ContextNode str)
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
| COCDir (NodeDir str ([str],StackVal str (COCBuiltin io str) (COCValue io str)))
deriving Generic
instance (ListSerializable s,ListSerializable b,ListSerializable a) => ListSerializable (StackVal s b a)
instance (IsCapriconString s,ListFormat s,ListFormat b,ListFormat a) => ListFormat (StackVal s b a)
instance (ListSerializable b) => ListSerializable (StackBuiltin b)
instance (ListFormat b) => ListFormat (StackBuiltin b)
instance (ListSerializable a) => ListSerializable (Opaque a)
instance (ListFormat a) => ListFormat (Opaque a)
instance ListSerializable str => ListSerializable (COCValue io str)
instance (IsCapriconString str,ListFormat str,IOListFormat io str) => ListFormat (COCValue io str)
type COCDict io str = Map str (StackVal str (COCBuiltin io str) (COCValue io str))
pattern StackCOC v = StackExtra (Opaque v)
takeLast n l = drop (length l-n) l
......@@ -20,7 +42,7 @@ takeLast n l = drop (length l-n) l
showStackVal :: IsCapriconString str => (NodeDoc str -> str) -> NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> StackVal str (COCBuiltin io str) (COCValue io str) -> str
showStackVal toRaw dir ctx = fix $ \go _x -> case _x of
StackCOC _x -> case _x of
COCExpr d e -> -- "<"+show d+">:"+
COCExpr (ContextNode d e) -> -- "<"+show d+">:"+
toRaw $ showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
......@@ -114,6 +136,25 @@ outputText = lens _outputText (\x y -> x { _outputText = y })
pushError :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m => str -> m ()
pushError s = runStackState $ modify $ (StackCOC (COCError s):)
runInContext :: Env str -> MaybeT ((->) (Env str)) a -> Maybe a
runInContext c v = (v^..maybeT) c
modifyAllExprs :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m
=> (ContextNode str -> ContextNode str) -> m ()
modifyAllExprs f = do
let modStack (StackCOC (COCExpr e)) = StackCOC (COCExpr (f e))
modStack (StackDict d) = StackDict (map modStack d)
modStack (StackList l) = StackList (map modStack l)
modStack x = x
runStackState $ modify $ map modStack
runDictState $ modify $ map modStack
modifyCOCEnv :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m
=> Maybe (ContextNode str -> ContextNode str,Env str) -> m ()
modifyCOCEnv Nothing = unit
modifyCOCEnv (Just (modE,ctx)) = do
runExtraState (context =- ctx)
modifyAllExprs modE
runCOCBuiltin :: (MonadSubIO io m,IsCapriconString str, MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m,IOListFormat io str,ListFormat str) => COCBuiltin io str -> m ()
runCOCBuiltin COCB_Quit = runExtraState (endState =- True)
runCOCBuiltin COCB_Print = do
......@@ -151,32 +192,25 @@ runCOCBuiltin COCB_Concat = runStackState $ modify $ \case
runCOCBuiltin COCB_Uni = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackInt n:t -> StackCOC (COCExpr (length ctx) (Universe n)):t
StackInt u:t | Just x <- runInContext ctx (mkUniverse u) -> StackCOC (COCExpr x):t
st -> st
runCOCBuiltin COCB_Var = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackSymbol name:t | Just i <- lookup name (zipWith (second . const) [0..] (freshContext ctx)) ->
StackCOC (COCExpr (length ctx) (Cons (Ap (Sym i) []))):t
StackSymbol name:t | Just e <- runInContext ctx (pullTerm =<< mkVariable name) -> StackCOC (COCExpr e):t
st -> st
runCOCBuiltin COCB_Ap = do
ctx <- runExtraState (getl context)
let adj d dd x = inc_depth (dd+nctx-d) x
nctx = length ctx
env = map snd ctx
runStackState $ modify $ \case
(StackCOC (COCExpr df f):StackCOC (COCExpr dx x):t) ->
let x' = adj dx 1 x ; f' = adj df 0 f in
StackCOC (COCExpr nctx (subst f' (Cons (Ap (Sym 0) [x'])) env)):t
(StackCOC (COCExpr f):StackCOC (COCExpr x):t)
| Just e <- runInContext ctx (mkApply f x) -> StackCOC (COCExpr e):t
x -> x
runCOCBuiltin (COCB_Bind close bt) = do
ctx <- runExtraState (getl context)
let d = length ctx
setVal (StackCOC (COCExpr d' e'))
| i <- d-d'
, d==d' || not close
, (_,(x,tx):_) <- splitAt i ctx
= StackCOC (COCExpr (d'-1) (Bind bt x tx e'))
let dctx = length ctx
setVal (StackCOC (COCExpr e@(ContextNode d _)))
| d==dctx || not close
, Just e' <- runInContext ctx (mkBind bt e) = StackCOC (COCExpr e')
setVal (StackDict dict) = StackDict (map setVal dict)
setVal (StackList l) = StackList (map setVal l)
setVal x = x
......@@ -188,30 +222,22 @@ runCOCBuiltin (COCB_Bind close bt) = do
runExtraState (context =- ctx')
runCOCBuiltin COCB_Mu = do
ctx <- runExtraState (getl context)
let locEnv d = map snd (takeLast d ctx)
runStackState $ modify $ \case
StackCOC (COCExpr d e):t ->
case type_of e (locEnv d) >>= \te -> mu_type te (locEnv d) of
Just mte -> let args (Bind Prod _ tx e') = tx:args e'
args _ = []
in (:t) $ StackExtra $ Opaque $ COCExpr d $
subst e (Cons (Ap (Mu [] (args mte) (Ap (Sym 0) [])) [])) (locEnv d)
Nothing -> StackCOC COCNull:t
StackCOC (COCExpr e):t | Just e' <- runInContext ctx (mkMu e) -> StackCOC (COCExpr e'):t
| otherwise -> StackCOC COCNull:t
st -> st
runCOCBuiltin COCB_TypeOf = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackCOC (COCExpr d (Cons (Ap (Sym i) []))):t
| (_,ti):_ <- drop i ctx ->
StackCOC (COCExpr (d-i-1) ti):t
StackCOC (COCExpr d e):t -> (:t) $ StackExtra $ Opaque $ case type_of e (takeLast d (map snd ctx)) of
Just te -> COCExpr d te
Nothing -> COCNull
StackCOC (COCExpr e):t | Just e' <- runInContext ctx (checkType e) -> StackCOC (COCExpr e'):t
| otherwise -> StackCOC COCNull:t
st -> st
runCOCBuiltin COCB_Convertible = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackCOC (COCExpr e):StackCOC (COCExpr e'):t ->
StackCOC (COCConvertible (runInContext ctx $ conversionDelta e e')):t
st -> st
runCOCBuiltin COCB_Convertible = runStackState $ modify $ \case
StackCOC (COCExpr d e):StackCOC (COCExpr d' e'):t ->
StackCOC (COCConvertible (flip convertible (inc_depth (max (d-d') 0) e) (inc_depth (max (d'-d) 0) e'))):t
st -> st
runCOCBuiltin (COCB_ExecModule (WriteImpl writeResource)) = do
st <- runStackState get
......@@ -242,52 +268,27 @@ runCOCBuiltin (COCB_Cache (ReadImpl getResource) (WriteImpl writeResource)) = do
_ -> pushError "Invalid argument types for builtin 'cache'. Usage: <prog> <string> cache."
runCOCBuiltin COCB_Hyp = do
ass <- runStackState $ id <~ \case
StackSymbol name:StackCOC (COCExpr d typ):t -> (t,Just (d,(name,typ)))
ctx <- runExtraState (getl context)
s <- runStackState $ id <~ \case
StackSymbol name:StackCOC (COCExpr e):t
-> (t,runInContext ctx (insertHypBefore Nothing name e))
st -> (st,Nothing)
case ass of
Just (d,x) -> runExtraState $ context =~ \ctx -> (second (inc_depth (length ctx-d)) x:ctx)
Nothing -> return ()
modifyCOCEnv s
runCOCBuiltin COCB_HypBefore = do
ctx <- runExtraState (getl context)
let csz = length ctx
adj hi i j = if i+j>=hi then j+1 else j
ctx' <- runStackState $ id <~ \case
StackSymbol h:StackSymbol h':StackCOC (COCExpr d e):t
| (hi,_):_ <- select ((==h) . fst . snd) (zip [0..] ctx)
, all (>hi+d-csz) (free_vars e) ->
let ctx' = foldr (\x k i -> case compare hi i of
LT -> x:k (i+1)
EQ -> second (adjust_depth (adj hi i)) x:(h',inc_depth (csz-(d+hi+1)) e):k (i+1)
GT -> second (adjust_depth (adj hi i)) x:k (i+1))
(\_ -> []) ctx 0
adjE x@(StackCOC (COCExpr d' e')) =
let i = csz-d'
in if i<=hi then StackCOC (COCExpr (d+1) (adjust_depth (adj (hi+1) i) e'))
else x
adjE x = x
in (map adjE t,ctx')
st -> (st,ctx)
runExtraState (context =- ctx')
s <- runStackState $ id <~ \case
StackSymbol h:StackSymbol h':StackCOC (COCExpr e):t
-> (t,runInContext ctx (insertHypBefore (Just h) h' e))
st -> (st,Nothing)
modifyCOCEnv s
runCOCBuiltin COCB_Subst = do
ctx <- runExtraState (getl context)
let csz = length ctx
ctx' <- runStackState $ id <~ \case
StackSymbol h:StackCOC (COCExpr d e):t
| (hi,_):_ <- select ((==h) . fst . snd) (zip [0..] ctx)
, all (>hi+d-csz) (free_vars e) ->
let ctx' = foldr (\x k i env -> case compare i hi of
LT -> second (\xv -> substn e (hi-i) xv env) x:k (i+1) (tail env)
EQ -> k (i+1) (tail env)
GT -> x:k (i+1) (tail env)) (\_ _ -> []) ctx 0 (map snd ctx)
adjE x@(StackCOC (COCExpr d' e')) =
let i = csz - d'
in if i<=hi then StackCOC (COCExpr (d-1) ((substn e (hi-i) e' (map snd (drop i ctx)))))
else x
adjE x = x
in (map adjE t,ctx')
st -> (st,ctx)
runExtraState (context =- ctx')
s <- runStackState $ id <~ \case
StackSymbol h:StackCOC (COCExpr e):t -> (t,runInContext ctx (substHyp h e))
st -> (st,Nothing)
modifyCOCEnv s
runCOCBuiltin COCB_Rename = do
ctx <- runExtraState (getl context)
ctx' <- runStackState $ id <~ \case
......@@ -312,32 +313,10 @@ runCOCBuiltin COCB_SetShowDir = do
runCOCBuiltin COCB_InsertNodeDir = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
x:StackCOC (COCExpr d e):StackCOC (COCDir dir):t ->
x:StackCOC (COCExpr (ContextNode d e)):StackCOC (COCDir dir):t ->
StackCOC (COCDir (insert e (map fst (takeLast d ctx),x) dir)):t
st -> st
type MaxDelta = Int
type UniverseConstraint = [Maybe MaxDelta]
data UniverseConstraints = UniverseConstraints [UniverseConstraint]
instance Semigroup UniverseConstraints where
UniverseConstraints x + UniverseConstraints y = UniverseConstraints $ zipWith (zipWith (\_x _y -> zipWith max _x _y + _x + _y)) x y
instance Monoid UniverseConstraints where zero = UniverseConstraints (repeat (repeat Nothing))
data COCValue io str = COCExpr Int (Node str)
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
| COCDir (NodeDir str ([str],StackVal str (COCBuiltin io str) (COCValue io str)))
deriving Generic
instance (ListSerializable s,ListSerializable b,ListSerializable a) => ListSerializable (StackVal s b a)
instance (IsCapriconString s,ListFormat s,ListFormat b,ListFormat a) => ListFormat (StackVal s b a)
instance (ListSerializable b) => ListSerializable (StackBuiltin b)
instance (ListFormat b) => ListFormat (StackBuiltin b)
instance (ListSerializable a) => ListSerializable (Opaque a)
instance (ListFormat a) => ListFormat (Opaque a)
instance ListSerializable str => ListSerializable (COCValue io str)
instance (IsCapriconString str,ListFormat str,IOListFormat io str) => ListFormat (COCValue io str)
type COCDict io str = Map str (StackVal str (COCBuiltin io str) (COCValue io str))
cocDict :: forall io str. IsCapriconString str => str -> (str -> io (Maybe str)) -> (str -> io (Maybe [Word8])) -> (str -> str -> io ()) -> (str -> [Word8] -> io ()) -> COCDict io str
cocDict version getResource getBResource writeResource writeBResource =
mkDict ((".",StackProg []):("steps.",StackProg []):("mustache.",StackProg []):("version",StackSymbol version):
......
{-# LANGUAGE UndecidableInstances, OverloadedStrings, NoMonomorphismRestriction, DeriveGeneric, ConstraintKinds #-}
module Data.CaPriCon(
-- * Expression nodes
IsCapriconString(..),BindType(..),Node(..),ApHead(..),Application(..),
IsCapriconString(..),BindType(..),Node(..),ApHead(..),Application(..),ContextNode(..),Env,COCExpression(..),
-- ** Managing De Bruijin indices
adjust_depth,adjust_telescope_depth,inc_depth,free_vars,is_free_in,
-- ** General term substitution, type inference and convertibility
subst,substn,type_of,mu_type,convertible,
-- ** Expression directories
StringPattern,NodeDir(..),AHDir(..),ApDir,
findPattern,freshContext,
......@@ -45,17 +43,20 @@ instance SerialStream Word8 ListBuilder ListStream where
toSerialStream k = k []
-- | Inductive types
type UniverseSize = Int
type SymbolRef = Int
data BindType = Lambda | Prod
deriving (Show,Eq,Ord,Generic)
data Node str = Bind BindType str (Node str) (Node str)
data Node str = Bind BindType str (NodeType str) (Node str)
| Cons (Application str)
| Universe Int
| Universe UniverseSize
deriving (Show,Generic)
data ApHead str = Sym Int | Mu [(str,Node str,Node str)] [Node str] (Application str)
type NodeType str = Node str
data ApHead str = Sym SymbolRef | Mu [(str,Node str,Node str)] [Node str] (Application str)
deriving (Show,Generic)
data Application str = Ap (ApHead str) [Node str]
deriving (Show,Generic)
type Env str = [Node str]
type Env str = [(str,NodeType str)]
type ListSerializable a = (Serializable Word8 ListBuilder ListStream a)
type ListFormat a = (Format Word8 ListBuilder ListStream a)
......@@ -68,6 +69,99 @@ instance ListFormat str => ListFormat (ApHead str)
instance ListSerializable str => ListSerializable (Application str)
instance ListFormat str => ListFormat (Application str)
class Monad m => COCExpression str m e | e -> str where
mkUniverse :: UniverseSize -> m e
mkVariable :: str -> m e
mkBind :: BindType -> e -> m e
mkApply :: e -> e -> m e
mkMu :: e -> m e
checkType :: e -> m e
conversionDelta :: e -> e -> m (UniverseSize,UniverseSize)
substHyp :: str -> e -> m (e -> e,Env str)
pullTerm :: e -> m e
insertHypBefore :: Maybe str -> str -> e -> m (e -> e,Env str)
instance (IsCapriconString str,Monad m,MonadReader (Env str) m) => COCExpression str (MaybeT m) (Node str) where
mkUniverse = pure . Universe
mkVariable v = hypIndex v <&> \i -> Cons (Ap (Sym i) [])
mkBind b e = ask >>= \case
(x,tx):_ -> pure $ Bind b x tx e
_ -> zero
mkApply f x = return (subst f (Cons (Ap (Sym 0) [inc_depth 1 x])))
mkMu e = do
te <- checkType e
mte <- mu_type te^.maybeT
let args (Bind Prod _ tx e') = tx:args e'
args _ = []
return (subst e (Cons (Ap (Mu [] (args mte) (Ap (Sym 0) [])) [])))
checkType e = type_of e^.maybeT
conversionDelta a b = return (convertible a b)^.maybeT
substHyp h x = do
i <- hypIndex h
lift $ do
ctx <- ask
return (substn x i,let (ch,ct) = splitAt i ctx in zipWith (\j -> second $ substn (inc_depth (negate (1+j)) x) (i-j-1)) [0..] ch+drop 1 ct)
pullTerm = return
insertHypBefore Nothing h th = lift $ do
ctx <- ask
return (inc_depth 1,(h,th):ctx)
insertHypBefore (Just h) h' th' = do
hi <- hypIndex h
lift $ do
ctx <- ask
let adj i j = if i+j>=hi then j+1 else j
return (
adjust_depth (adj (-1)),
foldr (\x k i -> case compare hi i of
LT -> x:k (i+1)
EQ -> second (adjust_depth (adj i)) x:(h',inc_depth (negate (hi+1)) th'):k (i+1)
GT -> second (adjust_depth (adj i)) x:k (i+1))
(\_ -> []) ctx 0)
hypIndex :: (IsCapriconString str,MonadReader (Env str) m) => str -> MaybeT m Int
hypIndex h = ask >>= \l -> case [i | (i,x) <- zip [0..] l, fst x==h] of
i:_ -> return i
_ -> zero
data ContextNode str = ContextNode SymbolRef (Node str)
deriving (Show,Generic)
instance ListSerializable str => ListSerializable (ContextNode str)
instance ListFormat str => ListFormat (ContextNode str)
restrictEnv :: SymbolRef -> Env str -> Env str
restrictEnv n e = drop (length e-n) e
instance (IsCapriconString str,MonadReader (Env str) m,Monad m) => COCExpression str (MaybeT m) (ContextNode str) where
mkUniverse u = ask >>= \ctx -> ContextNode (length ctx)<$>mkUniverse u
mkVariable i = local (dropWhile ((/=i) . fst)) (ask >>= \ctx -> ContextNode (length ctx)<$>mkVariable i)
mkBind t ce@(ContextNode de e) | de>0 = ContextNode (de-1) <$> local (restrictEnv de) (mkBind t e)
| otherwise = return ce
mkApply (ContextNode df f) (ContextNode dx x) = do
let dm = max df dx
ContextNode dm <$> mkApply (inc_depth (dm-df) f) (inc_depth (dm-dx) x)
mkMu (ContextNode d e) = ContextNode d <$> local (restrictEnv d) (mkMu e)
checkType (ContextNode d e) = ContextNode d <$> local (restrictEnv d) (checkType e)
conversionDelta (ContextNode da a) (ContextNode db b) =
let dm = max da db in
local (restrictEnv dm)
$ conversionDelta (inc_depth (dm-da) a) (inc_depth (dm-db) b)
pullTerm (ContextNode d e) = ask <&> \l -> ContextNode (length l) (inc_depth (length l-d) e)
substHyp h vh = do
hi <- hypIndex h
ContextNode dm vh' <- pullTerm vh
first (\f cv@(ContextNode d v) ->
if d+hi <= dm then cv
else ContextNode (d-1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
substHyp h vh'
insertHypBefore h h' cth' = do
ContextNode dh th' <- pullTerm cth'
hi <- maybe (return (-1)) hypIndex h
first (\f cx@(ContextNode d x) ->
if d+hi < dh then cx
else ContextNode (d+1) (inc_depth (d-dh) $ f $ inc_depth (dh-d) x))
<$> insertHypBefore h h' th'
data NodeDir str a = NodeDir
(Map BindType (NodeDir str (NodeDir str a)))
(ApDir str a)
......@@ -204,14 +298,14 @@ is_free_in = map2 not go
go_a v (Ap (Sym v') subs) = v/=v' && all (go v) subs
go_a v (Ap (Mu env _ a) subs) = go_a (v+length env) a && all (go v) subs
subst :: (IsCapriconString str, MonadReader (Env str) m) => Node str -> Node str -> m (Node str)
subst :: Show str => Node str -> Node str -> Node str
subst = flip substn 0
substn :: (IsCapriconString str, MonadReader (Env str) m) => Node str -> Int -> Node str -> m (Node str)
substn val n | n>=0 = go n
substn :: Show str => Node str -> Int -> Node str -> Node str
substn val n | n>=0 = getId . go n
| otherwise = error "'subst' should not be called with a negative index"
where go d (Bind t x tx e) = do
tx' <- go d tx
Bind t x tx' <$> local (tx':) (go (d+1) e)
Bind t x tx' <$> go (d+1) e
go _ (Universe u) = pure (Universe u)
go d (Cons a) = go_a d a
......@@ -238,17 +332,17 @@ substn val n | n>=0 = go n
a' <- Cons . Ap (Sym i) <$>
sequence (fold [if nonempty (free_vars x - fromKList [0..envS-1])
then [ return $ inc_depth envS $ foldl' (\e (x',tx,_) -> Bind Lambda x' tx e) x env
, subst x (Cons (Ap (Mu [] muEnv (Ap (Sym 0) [])) [Cons (Ap (Sym j) []) | j <- reverse [1..envS]]))]
, return $ subst x (Cons (Ap (Mu [] muEnv (Ap (Sym 0) [])) [Cons (Ap (Sym j) []) | j <- reverse [1..envS]]))]
else [return x]
| x <- xs])
return $ foldl' (\e (x,_,tx) -> Bind Lambda x tx e) a' env
go_mu _ e t (Cons a) = return $ Cons (Ap (Mu e t a) [])
go_mu _ _ _ x' = error $ fromString "Cannot produce an induction principle for a term : "+fromString (show x')
go_mu _ _ _ x' = error $ "Cannot produce an induction principle for a term : "+show x'
rec_subst (y:t) (Bind Lambda _ _ e) = rec_subst t =<< subst y e
rec_subst (y:t) (Bind Lambda _ _ e) = rec_subst t (subst y e)
rec_subst xs (Cons (Ap h hxs)) = return (Cons (Ap h (hxs+xs)))
rec_subst [] x = return x
rec_subst _ x = error $ fromString "Invalid substitution of non-lambda expression : "+fromString (show x)
rec_subst _ x = error $ "Invalid substitution of non-lambda expression : "+show x
fresh env v = head $ select (not . (`elem` env)) (v:[v+fromString (show i) | i <- [0..]])
freshContext = go []
......@@ -336,10 +430,10 @@ showNode' dir = go 0
type_of :: (IsCapriconString str,MonadReader (Env str) m) => Node str -> m (Maybe (Node str))
type_of = yb maybeT . go
where go (Bind Lambda x tx e) = Bind Prod x tx <$> local (tx:) (go e)
go (Bind Prod _ tx e) = do
where go (Bind Lambda x tx e) = Bind Prod x tx <$> local ((x,tx):) (go e)
go (Bind Prod x tx e) = do
a <- go tx
b <- local (tx:) $ go e
b <- local ((x,tx):) $ go e
case (a,b) of
(Universe ua,Universe ub) -> return (Universe (max ua ub))
_ -> zero
......@@ -348,14 +442,14 @@ type_of = yb maybeT . go
where go' (Ap (Sym i) subs) = do
e <- ask
case drop i e of
ti:_ -> rec_subst subs (inc_depth (i+1) ti)
(_,ti):_ -> rec_subst subs (inc_depth (i+1) ti)
_ -> zero
go' (Ap (Mu env _ a') subs) = do
ta <- local (map (by l'2) env +) (go' a')
ta <- local (map (\(x,tx,_) -> (x,tx)) env +) (go' a')
preret <- maybeT $^ mu_type $ foldl' (\e (x,tx,_) -> Bind Prod x tx e) ta env
rec_subst subs =<< subst (Cons a') preret
rec_subst subs (subst (Cons a') preret)
rec_subst (y:t) (Bind Prod _ _ e) = rec_subst t =<< subst y e
rec_subst (y:t) (Bind Prod _ _ e) = rec_subst t (subst y e)
rec_subst [] x = return x
rec_subst _ _ = zero
......@@ -371,7 +465,7 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
go d (Bind Prod x tx e) = do
tx' <- go_col d x tx
e' <- local (tx:) (go (d+1) e)
e' <- local ((x,tx):) (go (d+1) e)
return (Bind Prod x tx' e')
go _ (Cons (Ap (Sym i) args)) = return $ Cons (Ap (Sym i) $ args + [Cons (Ap (Sym nargs) [])])
go _ _ = zero
......@@ -382,10 +476,10 @@ mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
let tx' = bind Prod (adjust_telescope_depth second (+(d+d')) root_args)
(adjust_depth (\i' -> if constr_ind d d' i' then (i'-d')+(nargs-d) else i'+nargs) tx)
tIx = Cons $ Ap (Sym (i+1)) $ map (inc_depth 1) subs + [Cons (Ap (Sym 0) [])]
e' <- local ((tx:) . (undefined:)) (go_col' (d'+2) (touch (1 :: Int) (map (+2) recs))
(adjust_depth (\j -> if j==0 then j else j+1) e))
e' <- local (((x,tx):) . (undefined:)) (go_col' (d'+2) (touch (1 :: Int) (map (+2) recs))
(adjust_depth (\j -> if j==0 then j else j+1) e))
return $ Bind Prod x tx' (Bind Prod x tIx e')
go_col' d' recs (Bind Prod x tx e) = Bind Prod x tx <$> local (tx:) (go_col' (d'+1) (map (+1) recs) e)
go_col' d' recs (Bind Prod x tx e) = Bind Prod x tx <$> local ((x,tx):) (go_col' (d'+1) (map (+1) recs) e)
go_col' d' recs (Cons (Ap (Sym i) xs))
| constr_ind d d' i = do
let args = reverse $ select (not . (`isKeyIn`recs)) [0..d'-1]
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment