Skip to content

GitLab

Commit 31fb5a94 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Make the notion of "term in context" more explicit in CaPriCon

parent 677b5fbe
Hide whitespace changes
Inline Side-by-side
capricon/exe/CaPriCon_Engine.hs
View file @ 31fb5a94
......@@ -35,6 +35,7 @@ instance StackSymbol JS.JSString where
'$' | JSS.length c==2 && c JSS.! 1 == '{' -> Open (Splice CloseExec)
'}' | JSS.length c==1 -> Close
'\'' -> Quoted (drop 1 c)
'\8217' -> Quoted (drop 1 c)
'"' -> Quoted (take (JSS.length c-2) (drop 1 c))
':' -> Comment (TextComment $ drop 1 c)
_ -> maybe (Other c) Number $ matches Just readable (toString c)
......
capricon/src/Algebra/Monad/Concatenative.hs
View file @ 31fb5a94
......@@ -135,7 +135,7 @@ instance StackSymbol String where
atomClass "${" = Open (Splice CloseExec)
atomClass "}" = Close
atomClass ('\'':t) = Quoted t
atomClass ('\x8217':t) = Quoted t
atomClass ('\8217':t) = Quoted t
atomClass ('"':t) = Quoted (init t)
atomClass (':':t) = Comment (TextComment t)
atomClass x = maybe (Other x) Number (matches Just readable x)
......
capricon/src/CaPriCon/Run.hs
View file @ 31fb5a94
......@@ -15,12 +15,6 @@ instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
liftSubIO ma = lift $ liftSubIO ma
type COCAxiom str = str
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 (ContextTerm str (COCAxiom str))
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
......@@ -52,8 +46,8 @@ takeLast n l = drop (length l-n) l
showStackVal :: IsCapriconString str => (NodeDoc str -> str) -> NodeDir str (COCAxiom str) ([str],StringPattern str) -> [(str,Term str (COCAxiom 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 (ContextTerm d e) -> -- "<"+show d+">:"+
toRaw $ showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e
COCExpr (ContextTerm d (UniverseConstraints uc) e) -> -- "<"+show d+">:"+
fromString (show (take d uc)) + toRaw (showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e)
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
......@@ -227,7 +221,7 @@ runCOCBuiltin COCB_Print = do
_ -> return ()
runCOCBuiltin COCB_Axiom = runStackState $ modify $ \case
StackCOC (COCExpr (ContextTerm 0 e)):StackSymbol s:st -> StackCOC (COCExpr (ContextTerm 0 (Cons (Ap (Axiom e s) [])))):st
StackCOC (COCExpr (ContextTerm 0 _ e)):StackSymbol s:st -> StackCOC (COCExpr (ContextTerm 0 zero (Cons (Ap (Axiom e s) [])))):st
st -> st
runCOCBuiltin COCB_Format = do
......@@ -279,7 +273,7 @@ runCOCBuiltin COCB_Ap = do
runCOCBuiltin (COCB_Bind close bt) = do
ctx <- runExtraState (getl context)
let dctx = length ctx
setVal (StackCOC (COCExpr e@(ContextTerm d _)))
setVal (StackCOC (COCExpr e@(ContextTerm d _ _)))
| d==dctx || not close
, Just e' <- runInContext ctx (mkBind bt e) = StackCOC (COCExpr e')
setVal (StackDict dict) = StackDict (map setVal dict)
......@@ -303,17 +297,17 @@ runCOCBuiltin COCB_MatchTerm = do
st <- runStackState get
cctx <- runExtraState (getl context)
let tailCall v go = go >> execValue runCOCBuiltin (const unit) v
runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d e st' =
runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d uc e st' =
case e of
Bind Lambda x tx e' -> tailCall onLambda $ do
runExtraState $ context =~ ((x,tx):)
runStackState $ put (StackCOC (COCExpr (ContextTerm (d+1) (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) e'))
runStackState $ put (StackCOC (COCExpr (ContextTerm (d+1) uc (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) uc e'))
:st')
Bind Prod x tx e' -> tailCall onProduct $ do
runExtraState $ context =~ ((x,tx):)
runStackState $ put (StackCOC (COCExpr (ContextTerm (d+1) (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) e'))
runStackState $ put (StackCOC (COCExpr (ContextTerm (d+1) uc (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) uc e'))
:st')
Cons (Ap h []) -> do
case h of
......@@ -321,21 +315,21 @@ runCOCBuiltin COCB_MatchTerm = do
| otherwise -> tailCall onVar $ runStackState $ put (StackSymbol ("#"+fromString (show i)):st')
Mu ctx _ a -> do
let a' = foldl' (\e' (x,tx,_) -> Bind Lambda x tx e') (Cons a) ctx
tailCall onMu $ runStackState $ put (StackCOC (COCExpr (ContextTerm d a'))
tailCall onMu $ runStackState $ put (StackCOC (COCExpr (ContextTerm d uc a'))
:st')
Axiom t a -> tailCall onAxiom $ do
runStackState $ put (StackSymbol a
:StackCOC (COCExpr (ContextTerm 0 t))
:StackCOC (COCExpr (ContextTerm 0 uc t))
:st')
Cons (Ap h args) -> tailCall onApply $ do
runStackState $ put (StackList (map (StackCOC . COCExpr . ContextTerm d) args)
:StackCOC (COCExpr (ContextTerm d (Cons (Ap h []))))
runStackState $ put (StackList (map (StackCOC . COCExpr . ContextTerm d uc) args)
:StackCOC (COCExpr (ContextTerm d uc (Cons (Ap h []))))
:st')
Universe n -> tailCall onUniverse $ runStackState $ put (StackInt n:st')
case st of
StackList [onUniverse,onLambda,onProduct,onApply,onMu,onVar,onAxiom]:StackCOC (COCExpr (ContextTerm d e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d e st'
onUniverse:onLambda:onProduct:onApply:onMu:onVar:onAxiom:StackCOC (COCExpr (ContextTerm d e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d e st'
StackList [onUniverse,onLambda,onProduct,onApply,onMu,onVar,onAxiom]:StackCOC (COCExpr (ContextTerm d uc e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d uc e st'
onUniverse:onLambda:onProduct:onApply:onMu:onVar:onAxiom:StackCOC (COCExpr (ContextTerm d uc e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d uc e st'
_ -> unit
runCOCBuiltin COCB_TypeOf = do
......@@ -418,7 +412,7 @@ runCOCBuiltin COCB_ContextVars = do
runCOCBuiltin COCB_Extract = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackCOC (COCExpr (ContextTerm d e)):t -> StackCOC (COCAlgebraic (fromTerm e ([],takeLast d ctx))):t
StackCOC (COCExpr (ContextTerm d _ e)):t -> StackCOC (COCAlgebraic (fromTerm e ([],takeLast d ctx))):t
st -> st
runCOCBuiltin COCB_GetShowDir = do
......@@ -435,7 +429,7 @@ runCOCBuiltin COCB_SetShowDir = do
runCOCBuiltin COCB_InsertNodeDir = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
x:StackCOC (COCExpr (ContextTerm d e)):StackCOC (COCDir dir):t ->
x:StackCOC (COCExpr (ContextTerm d _ e)):StackCOC (COCDir dir):t ->
StackCOC (COCDir (insert e (map fst (takeLast d ctx),x) dir)):t
st -> st
......
capricon/src/Data/CaPriCon.hs
View file @ 31fb5a94
{-# LANGUAGE UndecidableInstances, OverloadedStrings, NoMonomorphismRestriction, DeriveGeneric, ConstraintKinds #-}
module Data.CaPriCon(
-- * Expression nodes
IsCapriconString(..),BindType(..),Term(..),ApHead(..),Application(..),ContextTerm(..),Env,DependentLogic(..),
IsCapriconString(..),BindType(..),Term(..),ApHead(..),Application(..),ContextTerm(..),Env,UniverseConstraints(..),DependentLogic(..),
-- ** Managing De Bruijin indices
adjust_depth,adjust_telescope_depth,inc_depth,free_vars,is_free_in,
adjust_depth,adjust_telescope_depth,inc_depth,map_univs,free_vars,is_free_in,
-- ** Expression directories
StringPattern,NodeDir(..),AHDir(..),ApDir,
findPattern,freshContext,
......@@ -56,7 +56,9 @@ data Term str a = Bind BindType str (TypeTerm str a) (Term str a)
| Universe UniverseSize
deriving (Show,Generic)
type TypeTerm str a = Term str a
data ApHead str a = Sym SymbolRef | Mu [(str,TypeTerm str a,TypeTerm str a)] [Term str a] (Application str a) | Axiom (Term str a) a
data ApHead str a = Sym SymbolRef
| Mu [(str,TypeTerm str a,TypeTerm str a)] [Term str a] (Application str a)
| Axiom (Term str a) a
deriving (Show,Generic)
data Application str a = Ap (ApHead str a) [Term str a]
deriving (Show,Generic)
......@@ -136,7 +138,22 @@ instance (Show a,IsCapriconString str,Monad m,MonadReader (Env str (Term str a))
(\_ -> []) ctx 0)
data ContextTerm str a = ContextTerm SymbolRef (Term str a)
newtype UniverseConstraints = UniverseConstraints [Maybe UniverseSize]
deriving (Generic,Show)
instance Format [Word8] UniverseConstraints
instance Serializable [Word8] UniverseConstraints
instance Semigroup UniverseConstraints where
UniverseConstraints a + UniverseConstraints b = UniverseConstraints (zipWith (\x y -> zipWith max x y + x + y) a b)
instance Monoid UniverseConstraints where
zero = UniverseConstraints (repeat Nothing)
singleConstraint :: Int -> UniverseSize -> UniverseConstraints
singleConstraint h u = UniverseConstraints $ take h (repeat Nothing)+(Just u:repeat Nothing)
shiftConstraints :: Int -> UniverseConstraints -> UniverseConstraints
shiftConstraints n (UniverseConstraints x) | n < 0 = UniverseConstraints (drop (-n) x)
| otherwise = UniverseConstraints (take n (repeat Nothing) + x)
data ContextTerm str a = ContextTerm SymbolRef UniverseConstraints (Term str a)
deriving (Show,Generic)
instance (ListSerializable a,ListSerializable str) => ListSerializable (ContextTerm str a)
instance (ListFormat a,ListFormat str) => ListFormat (ContextTerm str a)
......@@ -147,41 +164,41 @@ instance (Show a,IsCapriconString str,MonadReader (Env str (Term str a)) m,Monad
type Axiom (ContextTerm str a) = a
type Binding (ContextTerm str a) = Term str a
mkUniverse u = ask >>= \ctx -> ContextTerm (length ctx)<$>mkUniverse u
mkVariable i = local (dropWhile ((/=i) . fst)) (ask >>= \ctx -> ContextTerm (length ctx)<$>mkVariable i)
mkBind t ce@(ContextTerm de e) | de>0 = ContextTerm (de-1) <$> local (restrictEnv de) (mkBind t e)
| otherwise = return ce
mkApply (ContextTerm df f) (ContextTerm dx x) = do
mkUniverse u = ask >>= \ctx -> ContextTerm (length ctx) zero<$>mkUniverse u
mkVariable i = local (dropWhile ((/=i) . fst)) (ask >>= \ctx -> ContextTerm (length ctx) (singleConstraint 0 0)<$>mkVariable i)
mkBind t ce@(ContextTerm de uc e) | de>0 = ContextTerm (de-1) (shiftConstraints (-1) uc) <$> local (restrictEnv de) (mkBind t e)
| otherwise = return ce
mkApply (ContextTerm df ucf f) (ContextTerm dx ucx x) = do
let dm = max df dx
ContextTerm dm <$> mkApply (inc_depth (dm-df) f) (inc_depth (dm-dx) x)
mkMu (ContextTerm d e) = ContextTerm d <$> local (restrictEnv d) (mkMu e)
checkType (ContextTerm d e) = ContextTerm d <$> local (restrictEnv d) (checkType e)
conversionDelta (ContextTerm da a) (ContextTerm db b) =
ContextTerm dm (ucf+ucx) <$> mkApply (inc_depth (dm-df) f) (inc_depth (dm-dx) x)
mkMu (ContextTerm d uc e) = ContextTerm d uc <$> local (restrictEnv d) (mkMu e)
checkType (ContextTerm d uc e) = ContextTerm d uc <$> local (restrictEnv d) (checkType e)
conversionDelta (ContextTerm da _ a) (ContextTerm db _ b) =
let dm = max da db in
local (restrictEnv dm)
$ conversionDelta (inc_depth (dm-da) a) (inc_depth (dm-db) b)
pullTerm Nothing (ContextTerm d e) = ask <&> \l -> ContextTerm (length l) (inc_depth (length l-d) e)
pullTerm (Just v) (ContextTerm d e) = do
pullTerm Nothing (ContextTerm d uc e) = ask <&> \l -> ContextTerm (length l) (shiftConstraints (length l - d) uc) (inc_depth (length l-d) e)
pullTerm (Just v) (ContextTerm d uc e) = do
nctx <- length <$> ask
i <- hypIndex v
let d' = nctx-(i+1)
guard (d'>=d || all (\j -> d'+j >= d) (free_vars e))
return (ContextTerm d' $ inc_depth (d'-d) e)
return (ContextTerm d' (shiftConstraints (d'-d) uc) $ inc_depth (d'-d) e)
substHyp h vh = do
ContextTerm dh vh' <- pullTerm (Just h) vh
ContextTerm dh uc vh' <- pullTerm (Just h) vh
dm <- length <$> ask
first (\f cv@(ContextTerm d v) ->
first (\f cv@(ContextTerm d uc' v) ->
if d <= dh then cv
else ContextTerm (d-1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
else ContextTerm (d-1) (uc+uc') (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
substHyp h vh'
insertHypBefore h h' cth' = do
ContextTerm dh th' <- pullTerm h cth'
ContextTerm dh uc th' <- pullTerm h cth'
dm <- length <$> ask
first (\f cx@(ContextTerm d x) ->
first (\f cx@(ContextTerm d uc' x) ->
if d <= dh then cx
else ContextTerm (d+1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) x))
else ContextTerm (d+1) (uc+uc') (inc_depth (d-dm) $ f $ inc_depth (dm-d) x))
<$> insertHypBefore h h' th'
data NodeDir str ax a = NodeDir
......@@ -308,6 +325,15 @@ adjust_depth f = go 0
(go_a (d+length env) a')) (map (go d) subs)
go_a d (Ap x@(Axiom _ _) subs) = Ap x (map (go d) subs)
map_univs f = go
where go (Bind t x tx e) = Bind t x (go tx) (go e)
go (Universe u) = Universe (f u)
go (Cons a) = Cons (go_a a)
go_a (Ap h subs) = Ap (go_ah h) (map go subs)
go_ah (Mu e t a) = Mu (map (\(x,y,z) -> (x,go y,go z)) e) (map go t) (go_a a)
go_ah (Axiom t a) = Axiom (go t) a
go_ah x = x
inc_depth 0 = \x -> x
inc_depth dx = adjust_depth (+dx)
adjust_telescope_depth field f = zipWith (field . adjust_depth . \i j -> if j<i then j else i+f (j-i)) [0..]
......@@ -539,7 +565,8 @@ type_of = yb maybeT . go
rec_subst (y:t) (Bind Prod _ tx e) = do
ty <- go y
_ <- return (convertDelta tx ty)^.maybeT
(dx,_) <- return (convertDelta ty tx)^.maybeT
guard (dx<=0)
rec_subst t (subst y e)
rec_subst [] x = return x
rec_subst _ _ = zero
......
Markdown is supported
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