diff options
Diffstat (limited to 'Smurf.icl')
| -rw-r--r-- | Smurf.icl | 31 |
1 files changed, 21 insertions, 10 deletions
@@ -2,6 +2,7 @@ implementation module Smurf from StdFunc import o, flip import StdArray +import StdDebug import StdList import StdMisc import StdString @@ -22,7 +23,7 @@ import SmurfParse import LaTeX derive gEq Stm, Expr, State -derive gPrint (,), Expr +derive gPrint (,), Expr, VarChar instance == Stm where == a b = a === b instance == Expr where == a b = a === b @@ -165,7 +166,15 @@ stackToLaTeX es = List $ intersperse (Text ":") (map eToLaTeX es ++ [Command "Nil" []]) eToLaTeX :: Expr -> LaTeX -eToLaTeX e = Command "texttt" [List [Raw "\"", Text (toString e), Raw "\""]] +eToLaTeX e = Command "texttt" [List [Raw "\"", etl e, Raw "\""]] +where + etl :: Expr -> LaTeX + etl (Lit s) = Text s + etl (Var v) = Math False [Raw v] + etl (ECat a b) = List [etl a, etl b] + etl (EHead e) = List [Command "textit" [Text "hd"], Raw "(", etl e, Raw ")"] + etl (ETail e) = List [Command "textit" [Text "tl"], Raw "(", etl e, Raw ")"] + etl (EQuotify e) = List [Command "textit" [Text "q"], Raw "(", etl e, Raw ")"] instance toLaTeX DerivationTree where @@ -177,8 +186,12 @@ where = List [ Command "axjustifies" [] , toLaTeX t - , Command "using" [Command "rlambdans" []] + , Command "using" [rule] ] + where + rule = case t of + (([], _, _) --> (_, _, _)) = Command "rlambdans" [] + _ = Command "rule" [Text "assumption", Text ""] toL [t=:((p1,_,_)-->_):ts] = List [ Command "[" [] @@ -208,10 +221,6 @@ where (+++) (Lit s) (Lit t) = Lit $ s +++ t (+++) a b = ECat a b -eToCharList :: Expr -> [Char] -eToCharList (Lit s) = fromString s -eToCharList _ = abort "unimplemented\n" - run :: !Program State io (IO io) -> (Maybe State, io) run prog st io iofuncs # (mbProgSt, io) = step prog st io iofuncs @@ -251,8 +260,7 @@ step [Get:p] st io _ = (pop st.stack >>= \(var,stk) -> pure (p, { st & stack = push (get var st.store) stk }), io) step [Exec:p] st io _ - = (pop st.stack >>= parse o eToCharList o fst >>= \p -> - pure (p, zero), io) + = (pop st.stack >>= \(pgm,_) -> pure (let vcs = eToVarChars pgm in fromJust $ parsev $ trace (printToString vcs +++ "\n") vcs, zero), io) push :: Expr Stack -> Stack push s st = [s:st] @@ -290,7 +298,10 @@ where quot ['\t':cs] = ['\\':'t':quot cs] quot ['"':cs] = ['\\':'"':quot cs] quot [c:cs] = [c:quot cs] -quotify e = EQuotify e +quotify (ECat a b) = ECat (quotify a) (quotify b) +quotify (EHead a) = EHead (quotify a) +quotify (ETail a) = ETail (quotify a) +quotify (Var v) = EQuotify (Var v) listIO :: IO ListIO listIO = IO read write |