Skip to content

GitLab

Commit aba21bbc authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Wed May 1 21:22:22 CEST 2019)

parent caf4456d
Hide whitespace changes
Inline Side-by-side
capricon/src/CaPriCon/Run.hs
View file @ aba21bbc
......@@ -52,8 +52,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 uc e) -> -- "<"+show d+">:"+
fromString (show uc) + toRaw (showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e)
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
......@@ -227,7 +227,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 +279,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 +303,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 +321,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 +418,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 +435,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 @ aba21bbc
......@@ -136,7 +136,21 @@ 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 +161,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
......
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