Skip to content

GitLab

Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

Rename the ContextTerm type into NormalTerm, for clarity

parent 31fb5a94
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 195 additions and 188 deletions
capricon/src/CaPriCon/Run.hs
View file @ cf2e953c
......@@ -15,7 +15,7 @@ instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
liftSubIO ma = lift $ liftSubIO ma
type COCAxiom str = str
data COCValue io str = COCExpr (ContextTerm str (COCAxiom str))
data COCValue io str = COCExpr (NormalTerm str (COCAxiom str))
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
| COCAlgebraic (Algebraic str)
......@@ -46,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 (UniverseConstraints uc) e) -> -- "<"+show d+">:"+
fromString (show (take d uc)) + toRaw (showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e)
COCExpr (NormalTerm (NormalType _ c _) e) -> -- "<"+show d+">:"+
toRaw (showNode' dir (map (second snd) $ takeLast (length c) (freshContext ctx)) e)
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
......@@ -166,13 +166,13 @@ literate = liftA2 (\pref r -> pref + [Left (TextComment $ fromString r)])
data COCState str = COCState {
_endState :: Bool,
_context :: Env str (ContextTerm str (COCAxiom str)),
_context :: Env str (NormalTerm str (COCAxiom str)),
_showDir :: NodeDir str (COCAxiom str) ([str],StringPattern str),
_outputText :: str -> str
}
endState :: Lens' (COCState str) Bool
endState = lens _endState (\x y -> x { _endState = y })
context :: Lens' (COCState str) (Env str (ContextTerm str (COCAxiom str)))
context :: Lens' (COCState str) (Env str (NormalTerm str (COCAxiom str)))
context = lens _context (\x y -> x { _context = y })
showDir :: Lens' (COCState str) (NodeDir str (COCAxiom str) ([str],StringPattern str))
showDir = lens _showDir (\x y -> x { _showDir = y })
......@@ -186,7 +186,7 @@ runInContext :: ax -> MaybeT ((->) ax) a -> Maybe a
runInContext c v = (v^..maybeT) c
modifyAllExprs :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m
=> (ContextTerm str (COCAxiom str) -> ContextTerm str (COCAxiom str)) -> m ()
=> (NormalTerm str (COCAxiom str) -> NormalTerm str (COCAxiom str)) -> m ()
modifyAllExprs f = do
let modStack (StackCOC (COCExpr e)) = StackCOC (COCExpr (f e))
modStack (StackDict d) = StackDict (map modStack d)
......@@ -195,7 +195,7 @@ modifyAllExprs f = do
runStackState $ modify $ map modStack
runDictState $ modify $ map modStack
modifyCOCEnv :: MonadStack (COCState str) str (COCBuiltin io str) (COCValue io str) m
=> Maybe (ContextTerm str (COCAxiom str) -> ContextTerm str (COCAxiom str),Env str (ContextTerm str (COCAxiom str))) -> m ()
=> Maybe (NormalTerm str (COCAxiom str) -> NormalTerm str (COCAxiom str),Env str (NormalTerm str (COCAxiom str))) -> m ()
modifyCOCEnv Nothing = unit
modifyCOCEnv (Just (modE,ctx)) = do
runExtraState (context =- ctx)
......@@ -221,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 zero (Cons (Ap (Axiom e s) [])))):st
StackCOC (COCExpr (NormalTerm (NormalType _ [] _) e)):StackSymbol s:st -> StackCOC (COCExpr (NormalTerm (NormalType 0 zero e) (Cons (Ap (Axiom e s) [])))):st
st -> st
runCOCBuiltin COCB_Format = do
......@@ -229,9 +229,9 @@ runCOCBuiltin COCB_Format = do
let format ('%':'s':s) (StackSymbol h:t) = first (h+) (format s t)
format ('%':'a':s) (StackSymbol h:t) = first (htmlQuote h+) (format s t)
format ('%':'n':s) (StackSymbol h:t) = first (markSyntax h+) (format s t)
format ('%':'v':s) (x:t) = first (showStackVal doc2raw (ex^.showDir) (ex^.context) x+) (format s t)
format ('%':'g':s) (x:t) = first (showStackVal doc2svg (ex^.showDir) (ex^.context) x+) (format s t)
format ('%':'l':s) (x:t) = first (showStackVal doc2latex (ex^.showDir) (ex^.context) x+) (format s t)
format ('%':'v':s) (x:t) = first (showStackVal doc2raw (ex^.showDir) (map (second snd) (ex^.context)) x+) (format s t)
format ('%':'g':s) (x:t) = first (showStackVal doc2svg (ex^.showDir) (map (second snd) (ex^.context)) x+) (format s t)
format ('%':'l':s) (x:t) = first (showStackVal doc2latex (ex^.showDir) (map (second snd) (ex^.context)) x+) (format s t)
format (c:s) t = first (fromString [c]+) (format s t)
format "" t = ("",t)
runStackState $ modify $ \case
......@@ -273,8 +273,8 @@ runCOCBuiltin COCB_Ap = do
runCOCBuiltin (COCB_Bind close bt) = do
ctx <- runExtraState (getl context)
let dctx = length ctx
setVal (StackCOC (COCExpr e@(ContextTerm d _ _)))
| d==dctx || not close
setVal (StackCOC (COCExpr e))
| normalDepth e==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)
......@@ -297,39 +297,45 @@ 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 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) uc (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) uc e'))
runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom d u uc t e st' =
case (t,e) of
(Bind Prod _ _ te',Bind Lambda x tx e') -> tailCall onLambda $ do
runExtraState $ context =~ ((x,(u,tx)):)
runStackState $ put (StackCOC (COCExpr (NormalTerm (NormalType u (Just 0:fill Nothing uc) (raiseRefs 1 tx))
(Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (NormalTerm (NormalType (d+1) uc te') e'))
:st')
Bind Prod x tx e' -> tailCall onProduct $ do
runExtraState $ context =~ ((x,tx):)
runStackState $ put (StackCOC (COCExpr (ContextTerm (d+1) uc (Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (ContextTerm (d+1) uc e'))
(_,Bind Lambda _ _ _) -> do
runStackState $ put (StackCOC (COCError "Invalid non-product type for lambda-term. Something must be very wrong."):st')
(_,Bind Prod x tx e') -> tailCall onProduct $ do
runExtraState $ context =~ ((x,(u,tx)):)
runStackState $ put (StackCOC (COCExpr (NormalTerm (NormalType u (Just 0:fill Nothing uc) (raiseRefs 1 tx))
(Cons (Ap (Sym 0) []))))
:StackCOC (COCExpr (NormalTerm (NormalType (d+1) uc (Universe u)) e'))
:st')
Cons (Ap h []) -> do
(_,Cons (Ap h [])) -> do
case h of
Sym i | (x,_):_ <- takeLast (d-i) cctx -> tailCall onVar $ runStackState $ put (StackSymbol x:st')
| 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 uc a'))
:st')
Axiom t a -> tailCall onAxiom $ do
tailCall onMu $ runStackState $ put (StackCOC (withType a'):st')
Axiom ta a -> tailCall onAxiom $ do
runStackState $ put (StackSymbol a
:StackCOC (COCExpr (ContextTerm 0 uc t))
:StackCOC (COCExpr (NormalTerm (NormalType (u+1) uc (Universe u)) ta))
:st')
Cons (Ap h args) -> tailCall onApply $ do
runStackState $ put (StackList (map (StackCOC . COCExpr . ContextTerm d uc) args)
:StackCOC (COCExpr (ContextTerm d uc (Cons (Ap h []))))
(_,Cons (Ap h args)) -> tailCall onApply $ do
runStackState $ put (StackList (map (StackCOC . withType) args)
:StackCOC (withType (Cons (Ap h [])))
:st')
Universe n -> tailCall onUniverse $ runStackState $ put (StackInt n:st')
(_,Universe n) -> tailCall onUniverse $ runStackState $ put (StackInt n:st')
where withType x | Just tx <- type_of x (restrictEnv uc $ map (second snd) cctx) = COCExpr $ NormalTerm (NormalType u uc tx) x
withType _ = COCNull
case st of
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'
StackList [onUniverse,onLambda,onProduct,onApply,onMu,onVar,onAxiom]:StackCOC (COCExpr (NormalTerm (NormalType u c t) e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom (length c) u c t e st'
onUniverse:onLambda:onProduct:onApply:onMu:onVar:onAxiom:StackCOC (COCExpr (NormalTerm (NormalType u c t) e)):st' -> runMatch onUniverse onLambda onProduct onApply onMu onVar onAxiom (length c) u c t e st'
_ -> unit
runCOCBuiltin COCB_TypeOf = do
......@@ -412,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 (NormalTerm (NormalType _ c _) e)):t -> StackCOC (COCAlgebraic (fromTerm e ([],map (second snd) $ takeLast (length c) ctx))):t
st -> st
runCOCBuiltin COCB_GetShowDir = do
......@@ -429,8 +435,8 @@ 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 ->
StackCOC (COCDir (insert e (map fst (takeLast d ctx),x) dir)):t
x:StackCOC (COCExpr (NormalTerm (NormalType _ c _) e)):StackCOC (COCDir dir):t ->
StackCOC (COCDir (insert e (map fst (takeLast (length c) ctx),x) dir)):t
st -> st
runCOCBuiltin COCB_Render = runStackState $ modify $ \case
......
capricon/src/Data/CaPriCon.hs
View file @ cf2e953c
This diff is collapsed.
capricon/src/Data/CaPriCon/Extraction.hs
View file @ cf2e953c
......@@ -32,7 +32,7 @@ instance Serializable bytes str => Serializable bytes (AType str)
instance Format bytes str => Format bytes (Algebraic str)
instance Format bytes str => Format bytes (AType str)
fromTerm :: (Show ax,IsCapriconString str,MonadReader ([Bool],Env str (Term str ax)) m) => Term str ax -> m (Algebraic str)
fromTerm :: (Show ax,IsCapriconString str,MonadReader ([Bool],[(str,Term str ax)]) m) => Term str ax -> m (Algebraic str)
fromTerm (Bind Lambda x tx e) = do
let isT = isTypeType tx
e' <- local ((not isT:)<#>((x,tx):)) (fromTerm e)
......@@ -41,17 +41,17 @@ fromTerm (Bind Lambda x tx e) = do
fromTerm (Cons a) = fromApplication a
fromTerm _ = error "Cannot produce a type-term in a language without first-class types"
fromApplication :: (Show ax,IsCapriconString str, MonadReader ([Bool],Env str (Term str ax)) m) => Application str ax -> m (Algebraic str)
fromApplication :: (Show ax,IsCapriconString str, MonadReader ([Bool],[(str,Term str ax)]) m) => Application str ax -> m (Algebraic str)
fromApplication (Ap ah args) = do
(varKinds,env) <- ask
let concreteArgs = [arg | (arg,Just t) <- map (\x -> (x,(checkType x^..maybeT) env)) args
let concreteArgs = [arg | (arg,Just t) <- map (\x -> (x,type_of x env)) args
, not (isTypeType t)]
case ah of
Sym s -> foldl' (liftA2 AApply) (pure $ AVar $ sum [if isV then 1 else 0 | isV <- take s varKinds]) (map fromTerm concreteArgs)
Mu _ _ a -> foldl' (liftA2 AApply) (fromApplication a) (map fromTerm concreteArgs)
Axiom _ _ -> undefined
fromTypeTerm :: MonadReader ([Bool],Env str (Term str ax)) m => Term str ax -> m (AType str)
fromTypeTerm :: MonadReader ([Bool],[(str,Term str ax)]) m => Term str ax -> m (AType str)
fromTypeTerm (Bind Prod x tx e) = do
let isT = isTypeType tx
e' <- local ((not isT:)<#>((x,tx):)) (fromTypeTerm e)
......
curly/data/bash/completions/curly.arg.shf
View file @ cf2e953c
......@@ -174,7 +174,7 @@ function C.curly.arg() {
C.alt C.rawWordOf "${#compFlags[@]}" "${compFlags[@]}" "$@"
fi
C.alt C.curly.flags flag 6 -h --help -v --version -i --interactive "$@"
C.alt C.curly.flags opt 4 -l --list-instances -s --serve-instance "$@"
C.alt C.curly.flags flag 4 -l --list-instances -s --serve-instance "$@"
C.alt C.curly.flags opt 2 -r --run C.curly.run_arg "$@"
C.alt C.curly.flags opt 2 -M --mount C.curly.input "$@"
C.alt C.curly.flags opt 2 -t --translate C.curly.translate "$@"
......
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