Commit 2385e34b authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Implement a basic LaTeX generator from term in the 'format' builtin

parent 2731302c
......@@ -2,7 +2,7 @@
-- see http://haskell.org/cabal/users-guide/
name: capricon
version: 0.8.1
version: 0.8.1.1
-- synopsis:
-- description:
license: GPL-3
......
......@@ -90,7 +90,7 @@ setBytes :: String -> [Word8] -> JS.CIO ()
setBytes f v = setString f (map (toEnum . fromIntegral) v)
hasteDict :: COCDict JS.CIO String
hasteDict = cocDict ("0.8.1-js" :: String) getString getBytes setString setBytes
hasteDict = cocDict ("0.8.1.2-js" :: String) getString getBytes setString setBytes
main :: IO ()
main = JS.concurrent $ void $ do
......@@ -116,7 +116,7 @@ main = JS.concurrent $ void $ do
if isCode
then do
p <- JS.getProp root "textContent"
next state (pref+" "+p)
next state (pref+p+" pop ")
else do
JS.wait 10
......
......@@ -10,7 +10,7 @@ newtype Opaque a = Opaque a
instance Show (Opaque a) where show _ = "#<opaque>"
data StackBuiltin b = Builtin_ListBegin | Builtin_ListEnd
| Builtin_Clear | Builtin_Stack
| Builtin_Pick
| Builtin_Pick | Builtin_Shift | Builtin_Shaft
| Builtin_Pop | Builtin_PopN
| Builtin_Dup | Builtin_DupN
| Builtin_Swap | Builtin_SwapN
......@@ -112,6 +112,12 @@ execBuiltin runExtra onComment = go
(x:tx,y:ty) -> y:tx+(x:ty)
_ -> st
_ -> st
go Builtin_Shift = stack =~ \case
StackInt n:st' | (h,v:t) <- splitAt n st' -> v:(h+t)
st -> st
go Builtin_Shaft = stack =~ \case
StackInt n:v:st' | (h,t) <- splitAt n st' -> h+(v:t)
st -> st
go Builtin_Dup = stack =~ \st -> case st of x:t -> x:x:t ; _ -> st
go Builtin_DupN = stack =~ \st -> case st of StackInt n:t | x:_ <- drop n t -> x:t ; _ -> st
go Builtin_Range = stack =~ \st -> case st of StackInt n:t -> StackList [StackInt i | i <- [0..n-1]]:t ; _ -> st
......
......@@ -15,11 +15,11 @@ instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
takeLast n l = drop (length l-n) l
showStackVal :: IsCapriconString str => NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> StackVal str (COCBuiltin io str) (COCValue io str) -> str
showStackVal dir ctx _x = case _x of
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 _x = case _x of
StackExtra (Opaque _x) -> case _x of
COCExpr d e -> -- "<"+show d+">:"+
showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e
toRaw $ showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
......@@ -119,7 +119,8 @@ runCOCBuiltin COCB_Print = do
runCOCBuiltin COCB_Format = do
ex <- runExtraState get
let format ('%':'s':s) (StackSymbol h:t) = first (h+) (format s t)
format ('%':'v':s) (x:t) = first (showStackVal (ex^.showDir) (ex^.context) x+) (format s t)
format ('%':'v':s) (x:t) = first (showStackVal doc2raw (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 (c:s) t = first (fromString [c]+) (format s t)
format "" t = ("",t)
runStackState $ modify $ \case
......@@ -305,6 +306,7 @@ runCOCBuiltin COCB_InsertNodeDir = do
StackExtra (Opaque (COCDir (insert e (map fst (takeLast d ctx),x) dir))):t
st -> st
data UniverseConstraints = UniverseConstraints Int [Int]
data COCValue io str = COCExpr Int (Node str)
| COCNull | COCError str
| COCDir (NodeDir str ([str],StackVal str (COCBuiltin io str) (COCValue io str)))
......@@ -332,6 +334,8 @@ cocDict version getResource getBResource writeResource writeBResource =
("stack" , Builtin_Stack ),
("clear" , Builtin_Clear ),
("shift" , Builtin_Shift ),
("shaft" , Builtin_Shaft ),
("pop" , Builtin_Pop ),
("popn" , Builtin_PopN ),
("dup" , Builtin_Dup ),
......
......@@ -10,7 +10,7 @@ module Data.CaPriCon(
StringPattern,NodeDir(..),AHDir(..),ApDir,
findPattern,freshContext,
-- * Showing nodes
showNode,showNode'
NodeDoc(..),doc2raw,doc2latex,showNode,showNode'
) where
import Definitive
......@@ -250,54 +250,87 @@ substn val n | n>=0 = go n
rec_subst [] x = return x
rec_subst _ x = error $ fromString "Invalid substitution of non-lambda expression : "+fromString (show x)
par lvl d msg | d>lvl = "("+msg+")"
| otherwise = msg
fresh env v = head $ select (not . (`elem` env)) (v:[v+fromString (show i) | i <- [0..]])
freshContext = go []
where go env ((n,v):t) = let n' = fresh env n in (n',(n,v)):go (n':env) t
go _ [] = []
data NodeDoc str = DocSeq [NodeDoc str]
| DocParen (NodeDoc str)
| DocMu (NodeDoc str)
| DocSubscript (NodeDoc str) (NodeDoc str)
| DocAssoc str (NodeDoc str)
| DocText str
| DocArrow
| DocSpace
deriving Show
par lvl d msg | d>lvl = DocParen msg
| otherwise = msg
instance IsString str => IsString (NodeDoc str) where fromString = DocText . fromString
doc2raw :: IsCapriconString str => NodeDoc str -> str
doc2raw (DocSeq l) = fold (map doc2raw l)
doc2raw (DocParen p) = "("+doc2raw p+")"
doc2raw (DocMu m) = "μ("+doc2raw m+")"
doc2raw (DocSubscript v x) = doc2raw v+doc2raw x
doc2raw (DocAssoc x v) = "("+x+" : "+doc2raw v+")"
doc2raw DocArrow = " -> "
doc2raw (DocText x) = x
doc2raw DocSpace = " "
doc2latex :: IsCapriconString str => NodeDoc str -> str
doc2latex (DocSeq l) = fold (map doc2latex l)
doc2latex (DocParen p) = "("+doc2latex p+")"
doc2latex (DocMu m) = "\\mu("+doc2latex m+")"
doc2latex (DocSubscript v x) = doc2latex v+"_{"+doc2latex x+"}"
doc2latex (DocAssoc x v) = "("+x+":"+doc2latex v+")"
doc2latex DocArrow = " \\rightarrow "
doc2latex (DocText x) = x
doc2latex DocSpace = "\\,"
showNode = showNode' zero
showNode' :: IsCapriconString str => NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> Node str -> str
showNode' :: IsCapriconString str => NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> Node str -> NodeDoc str
showNode' dir = go 0
where go d env x | Just ret <- toPat d env x = ret
go _ _ (Universe u) = "Set"+fromString (show u)
go d env whole@(Bind t aname atype body) | t == Lambda || 0`is_free_in`body = par 0 d $ bind_head t + drop 1 (bind_tail env whole)
| otherwise = par 0 d $ go 1 env atype + fromString " -> " + go 0 ((aname,atype):env) body
go _ _ (Universe u) = DocSubscript "Set" (fromString (show u))
go d env whole@(Bind t aname atype body) | t == Lambda || 0`is_free_in`body = par 0 d $ DocSeq (DocText (bind_head t):drop 1 (bind_tail env whole))
| otherwise = par 0 d $ DocSeq [go 1 env atype,DocArrow,go 0 ((aname,atype):env) body]
where bind_head Lambda = "λ"
bind_head Prod = "∀"
bind_tail env' x | Just ret <- toPat 0 (env'+env) x = ", "+ret
bind_tail env' (Bind t' x tx e) | t==t' && (t==Lambda || 0`is_free_in`e) = fromString " ("+x'+fromString ":"+go 0 env' tx+fromString ")"+bind_tail ((x',tx):env') e
bind_tail env' x | Just ret <- toPat 0 (env'+env) x = [",",DocSpace,ret]
bind_tail env' (Bind t' x tx e) | t==t' && (t==Lambda || 0`is_free_in`e) =
[DocSpace,DocAssoc x' (go 0 env' tx)] + bind_tail ((x',tx):env') e
where x' = fresh (map fst env') x
bind_tail env' x = ", "+go 0 env' x
bind_tail env' x = [",",DocSpace,go 0 env' x]
go d env (Cons a) = showA d a
where showA _ (Ap h xs) =
let ni = case h of
Sym i -> case drop i env of
(h',_):_ -> h'
_ -> "#"+fromString (show i)
Mu _ _ a' -> "μ("+showA 0 a'+")"
Sym i -> DocText $ case drop i env of
(h',_):_ -> h'
_ -> "#"+fromString (show i)
Mu _ _ a' -> DocMu (showA 0 a')
lvl = if empty xs then 1000 else 1
in par lvl d $ ni+foldMap ((" "+) . go 2 env) xs
in par lvl d $ DocSeq $ intercalate [DocSpace] $ map pure (ni:map (go 2 env) xs)
toPat d env x
| (pats,(_,k)):_ <- findPattern dir x =
let holes = c'map $ fromAList [(i,(env',hole)) | (env',i,hole) <- pats] in
Just $ par (if empty pats then 1000 else 1 :: Int) d $ intercalate (fromString " ")
Just $ par (if all (has t'1) k then 1000 else 1 :: Int) d $ DocSeq $ intercalate [DocSpace] $ map pure $
[case word of
Left w -> w
Left w -> DocText w
Right i | Just (env',hole) <- lookup i holes ->
go 2 env $
let (hole',env'') =
fix (\kj -> \case
(Cons (Ap h t@(_:_)),_:env0)
| Cons (Ap (Sym 0) []) <- debug $ last t
| Cons (Ap (Sym 0) []) <- last t
, not (is_free_in 0 (Cons (Ap h (init t))))
-> kj (inc_depth (-1) (Cons (Ap h (init t))),env0)
(Cons (Ap (Sym j') []),_:env0) | j'>0 -> kj (Cons (Ap (Sym (j'-1)) []),env0)
e -> e) (hole,env')
in foldl' (\e (n,t) -> Bind Lambda n t e) hole' env''
| otherwise -> zero
| otherwise -> DocText "?"
| word <- k]
| otherwise = Nothing
......
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