aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Smurf.dcl2
-rw-r--r--Smurf.icl31
-rw-r--r--SmurfParse.dcl9
-rw-r--r--SmurfParse.icl82
-rw-r--r--proof.icl34
-rw-r--r--reverse-ward.smf6
-rw-r--r--tree.icl4
7 files changed, 121 insertions, 47 deletions
diff --git a/Smurf.dcl b/Smurf.dcl
index 2c4fd1b..0ca45b2 100644
--- a/Smurf.dcl
+++ b/Smurf.dcl
@@ -66,6 +66,8 @@ instance toLaTeX DerivationTree
step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io)
run :: !Program State io (IO io) -> (Maybe State, io)
+quotify :: Expr -> Expr
+
listIO :: IO ListIO
prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
Program State ListIO (IO ListIO) -> Maybe DerivationTree
diff --git a/Smurf.icl b/Smurf.icl
index fa5cd00..b6b7b90 100644
--- a/Smurf.icl
+++ b/Smurf.icl
@@ -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
diff --git a/SmurfParse.dcl b/SmurfParse.dcl
index fb06ab3..e0ad868 100644
--- a/SmurfParse.dcl
+++ b/SmurfParse.dcl
@@ -2,7 +2,14 @@ definition module SmurfParse
from Data.Maybe import ::Maybe
-from Smurf import ::Program, ::Stm
+from Smurf import ::Program, ::Stm, ::Expr
+
+:: VarChar = Char Char
+ | VarString String
+ | Quoted Expr
+
+eToVarChars :: Expr -> [VarChar]
parse :: ![Char] -> Maybe Program
+parsev :: ![VarChar] -> Maybe Program
diff --git a/SmurfParse.icl b/SmurfParse.icl
index 81f6c2f..bf59b64 100644
--- a/SmurfParse.icl
+++ b/SmurfParse.icl
@@ -1,8 +1,10 @@
implementation module SmurfParse
from StdFunc import o, flip
+import StdArray
import StdChar
import StdList
+import StdMisc
import StdFile
import StdTuple
import StdString
@@ -14,36 +16,66 @@ import Control.Monad
import Smurf
+eToVarChars :: Expr -> [VarChar]
+eToVarChars (Lit s) = map Char $ fromString s
+eToVarChars (Var v) = [VarString v]
+eToVarChars (ECat a b) = eToVarChars a ++ eToVarChars b
+eToVarChars (EHead (Var v)) = abort "head of var\n"
+eToVarChars (EHead a) = [hd $ eToVarChars a]
+eToVarChars (ETail (Var v)) = abort "tail of var\n"
+eToVarChars (ETail a) = tl $ eToVarChars a
+eToVarChars (EQuotify a) = [Quoted a]
+
parse :: ![Char] -> Maybe Program
-parse [] = pure []
-parse ['"':cs] = parseString cs >>= \(s,cs`) -> append (Push $ Lit s) $ parse cs`
-parse ['i':cs] = apparse Input cs
-parse ['o':cs] = apparse Output cs
-parse ['+':cs] = apparse Cat cs
-parse ['h':cs] = apparse Head cs
-parse ['t':cs] = apparse Tail cs
-parse ['q':cs] = apparse Quotify cs
-parse ['p':cs] = apparse Put cs
-parse ['g':cs] = apparse Get cs
-parse ['x':cs] = apparse Exec cs
-parse [c:cs] = if (isSpace c) (parse cs) empty
-
-apparse :: Stm -> [Char] -> Maybe Program
-apparse stm = append stm o parse
+parse cs = parsev $ map Char cs
+
+parsev :: ![VarChar] -> Maybe Program
+parsev [] = pure []
+parsev [Char '"':cs] = parseString cs >>= \(s,cs`) -> append (Push s) $ parsev cs`
+parsev [Char 'i':cs] = apparse Input cs
+parsev [Char 'o':cs] = apparse Output cs
+parsev [Char '+':cs] = apparse Cat cs
+parsev [Char 'h':cs] = apparse Head cs
+parsev [Char 't':cs] = apparse Tail cs
+parsev [Char 'q':cs] = apparse Quotify cs
+parsev [Char 'p':cs] = apparse Put cs
+parsev [Char 'g':cs] = apparse Get cs
+parsev [Char 'x':cs] = apparse Exec cs
+parsev [Char c:cs] = if (isSpace c) (parsev cs) empty
+parsev [Quoted e:cs] = apparse (Push e) cs
+parsev _ = empty
+
+apparse :: Stm -> [VarChar] -> Maybe Program
+apparse stm = append stm o parsev
append :: a (m [a]) -> m [a] | Monad m
append x mx = mx >>= \xs -> pure [x:xs]
-parseString :: ![Char] -> Maybe (String, [Char])
+parseString :: ![VarChar] -> Maybe (Expr, [VarChar])
parseString cs = pS [] cs
where
- pS :: ![Char] ![Char] -> Maybe (String, [Char])
- pS _ [] = empty
- pS s ['"':cs] = pure (toString $ reverse s, cs)
- pS s ['\\':'n':cs] = pS ['\n':s] cs
- pS s ['\\':'r':cs] = pS ['\r':s] cs
- pS s ['\\':'t':cs] = pS ['\t':s] cs
- pS s ['\\':'\\':cs] = pS ['\\':s] cs
- pS s ['\\':'"':cs] = pS ['"':s] cs
- pS s [c:cs] = pS [c:s] cs
+ pS :: ![VarChar] ![VarChar] -> Maybe (Expr, [VarChar])
+ pS _ [] = empty
+ pS s [Char '"':cs]
+ = pure (toExpr $ reverse s, cs)
+ pS s [Char '\\':Char 'n':cs] = pS [Char '\n':s] cs
+ pS s [Char '\\':Char 'r':cs] = pS [Char '\r':s] cs
+ pS s [Char '\\':Char 't':cs] = pS [Char '\t':s] cs
+ pS s [Char '\\':Char '\\':cs] = pS [Char '\\':s] cs
+ pS s [Char '\\':Char '"':cs] = pS [Char '"':s] cs
+ pS s [c:cs] = pS [c:s] cs
+ toExpr :: [VarChar] -> Expr
+ toExpr cs = simplify $ te cs
+ where
+ te :: [VarChar] -> Expr
+ te [] = Lit ""
+ te [VarString v:cs] = ECat (Var v) (te cs)
+ te [Char c:cs] = ECat (Lit {c}) (te cs)
+ te [Quoted e:cs2] = ECat e (te cs2)
+
+ simplify :: Expr -> Expr
+ simplify (ECat a b) = case (simplify a, simplify b) of
+ (Lit x, Lit y) = Lit $ x +++ y
+ (x, y) = ECat x y
+ simplify e = e
diff --git a/proof.icl b/proof.icl
index 3ea9b1a..a836190 100644
--- a/proof.icl
+++ b/proof.icl
@@ -5,14 +5,30 @@ import StdEnv, StdDebug
from Data.Func import $
import Data.Maybe
-import Smurf, SmurfParse
+import Smurf, SmurfParse, LaTeX
-Start = toString (devtree ass) +++ "\n"
+Start w //= trigger
+# (_,f,w) = fopen "reverse-ward.smf" FReadText w
+# (pgm,f) = readFile f
+# (ok,w) = fclose f w
+# (Just pgm) = parse [c \\ c <-: pgm]
+# tree = devtree ass pgm
+# tree = trace (toString tree +++ "\n") tree
+= toString (toLaTeX tree)
where
- ass (pgm, ip, st)
- | pgm == [Tail,Tail] && st.stack == [Lit "bcd"]
- = Just ([], [], {st & stack=[Lit "d"]})
- = Nothing
- pgm = fromJust $ parse ['ittt']
- devtree ass
- = fromJust (prover ass pgm zero { zero & input = [Lit "abcd"] } listIO)
+ ass :: (Program, Stack, State) -> Maybe (Stack, Stack, State)
+ ass (pgm, [], {stack=[Var "s":Lit x:[]], store=[]})
+ | pgm == trigger = Just ([], [ECat (Var "s^R") (Lit x)], zero)
+ ass (pgm, ip, st) = Nothing
+
+ trigger = fromJust (parse ['""\"\\\"u\\\"p\\\"v\\\"p\\\"w\\\"p\\\"w\\\"gh\\\"v\\\"g+\\\"v\\\"p\\\"w\\\"gt\\\"w\\\"p\\\"w\\\"g\\\"v\\\"gq\\\"o\\\"+\\\"w\\\"gq\\\"v\\\"gq\\\"u\\\"gq++\\\"u\\\"g+\\\"w\\\"gp\\\"\\\"pgx\"\"u\"p\"v\"p\"w\"p\"w\"gh\"v\"g+\"v\"p\"w\"gt\"w\"p\"w\"g\"v\"gq\"o\"+\"w\"gq\"v\"gq\"u\"gq++\"u\"g+\"w\"gp\"\"pgx'])
+ devtree ass pgm
+ = fromJust (prover ass pgm zero { zero & input = [ECat (Lit "c") (Var "s")] } listIO)
+
+ readFile :: !*File -> *(!String, !*File)
+ readFile f
+ # (end,f) = fend f
+ | end = ("", f)
+ # (s,f) = freadline f
+ # (ss,f) = readFile f
+ = (s +++ ss, f)
diff --git a/reverse-ward.smf b/reverse-ward.smf
new file mode 100644
index 0000000..8e99850
--- /dev/null
+++ b/reverse-ward.smf
@@ -0,0 +1,6 @@
+i "input" p
+"input" g q
+"\"\"\"\\\"u\\\"p\\\"v\\\"p\\\"w\\\"p\\\"w\\\"gh\\\"v\\\"g+\\\"v\\\"p\\\"w\\\"gt\\\"w\\\"p\\\"w\\\"g\\\"v\\\"gq\\\"o\\\"+\\\"w\\\"gq\\\"v\\\"gq\\\"u\\\"gq++\\\"u\\\"g+\\\"w\\\"gp\\\"\\\"pgx\"\"u\"p\"v\"p\"w\"p\"w\"gh\"v\"g+\"v\"p\"w\"gt\"w\"p\"w\"g\"v\"gq\"o\"+\"w\"gq\"v\"gq\"u\"gq++\"u\"g+\"w\"gp\"\"pgx" +
+"input" g p
+"\"\"o" "" p
+"input" g g x
diff --git a/tree.icl b/tree.icl
index 5472b40..e2524a9 100644
--- a/tree.icl
+++ b/tree.icl
@@ -12,7 +12,7 @@ import SmurfParse
import LaTeX
Start w
-# (_,f,w) = fopen "reverse.smf" FReadText w
+# (_,f,w) = fopen "reverse-ward.smf" FReadText w
# (pgm,f) = readFile f
# (ok,w) = fclose f w
# (Just pgm) = parse [c \\ c <-: pgm]
@@ -20,7 +20,7 @@ Start w
# tree = trace (toString tree +++ "\n") tree
= toString (toLaTeX tree)
where
- devtree pgm = fromJust (tree pgm zero { zero & input = [Lit ""] } listIO)
+ devtree pgm = fromJust (tree pgm zero { zero & input = [Lit "xy"] } listIO)
readFile :: !*File -> *(!String, !*File)
readFile f
generated by cgit v1.2.3 (git 2.39.1) at 2025-03-12 20:32:03 +0000