diff options
| -rw-r--r-- | Smurf.icl | 32 | ||||
| -rw-r--r-- | SmurfParse.icl | 20 | ||||
| -rw-r--r-- | proof.icl | 25 |
3 files changed, 50 insertions, 27 deletions
@@ -172,6 +172,7 @@ where etl (Lit s) = Text s etl (Var v) = Math False [Raw v] etl (ECat a b) = List [etl a, etl b] + //etl (ECat a b) = List [etl a, Raw "+(", etl b, Raw ")"] 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 ")"] @@ -260,7 +261,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 >>= \(pgm,_) -> pure (let vcs = eToVarChars pgm in fromJust $ parsev $ trace (printToString vcs +++ "\n") vcs, zero), io) + = (pop st.stack >>= \(pgm,_) -> pure (let vcs = eToVarChars (trace pgm pgm) in fromJust $ parsev $ trace (printToString vcs +++ "\n") vcs, zero), io) push :: Expr Stack -> Stack push s st = [s:st] @@ -272,6 +273,7 @@ pop [s:ss] = pure (s, ss) head :: Expr -> Maybe Expr head (Lit "") = empty head (Lit s) = pure $ Lit $ s % (0,0) +head (ECat a b) = head a <|> head b head e = pure $ EHead e tail :: Expr -> Maybe Expr @@ -288,20 +290,22 @@ get var store = case filter ((==)var o fst) store of [(_,val):_] = val quotify :: Expr -> Expr -quotify (Lit s) = Lit $ flip (+++) "\"" $ (+++)"\"" $ toString $ quot $ fromString s +quotify e = ECat (Lit "\"") (ECat (quotify` e) (Lit "\"")) where - quot :: [Char] -> [Char] - quot [] = [] - quot ['\\':cs] = ['\\':'\\':quot cs] - quot ['\n':cs] = ['\\':'n':quot cs] - quot ['\r':cs] = ['\\':'r':quot cs] - quot ['\t':cs] = ['\\':'t':quot cs] - quot ['"':cs] = ['\\':'"':quot cs] - quot [c:cs] = [c:quot cs] -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) + quotify` (Lit s) = Lit $ toString $ quot $ fromString s + where + quot :: [Char] -> [Char] + quot [] = [] + quot ['\\':cs] = ['\\':'\\':quot cs] + quot ['\n':cs] = ['\\':'n':quot cs] + quot ['\r':cs] = ['\\':'r':quot cs] + quot ['\t':cs] = ['\\':'t':quot cs] + quot ['"':cs] = ['\\':'"':quot cs] + quot [c:cs] = [c:quot cs] + 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.icl b/SmurfParse.icl index bf59b64..385747c 100644 --- a/SmurfParse.icl +++ b/SmurfParse.icl @@ -20,10 +20,14 @@ 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 (EHead a) = case eToVarChars a of + [Char c:cs] = [Char c] + [VarString s:cs] = [VarString (s % (0,0))] + [Quoted e:_] = abort "head of quoted\n" +eToVarChars (ETail a) = case eToVarChars a of + [Char _:cs] = cs + [VarString s:cs] = [VarString (s % (1,size s - 1)):cs] + [Quoted e:_] = abort "tail of quoted\n" eToVarChars (EQuotify a) = [Quoted a] parse :: ![Char] -> Maybe Program @@ -76,6 +80,10 @@ where 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 + (Lit "", Lit y) = Lit y + (Lit x, Lit "") = Lit x + (Lit x, Lit y) = Lit $ x +++ y + (x, y) = ECat x y + simplify (EHead a) = EHead $ simplify a + simplify (ETail a) = ETail $ simplify a simplify e = e @@ -8,11 +8,16 @@ import Data.Maybe import Smurf, SmurfParse, LaTeX 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 +//# (_,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 zero {zero & input=[Lit "cs"]} +// --- +# tree = devtree assbs innerpgm {zero & stack=[Var "s", ECat (Lit "c") (Var "t")]} zero +// --- +//# tree = devtree assbs innerpgm {zero & stack=[Var "s", ECat (Lit "c") (Var "t")]} zero +// --- # tree = trace (toString tree +++ "\n") tree = toString (toLaTeX tree) where @@ -21,9 +26,15 @@ where | pgm == trigger = Just ([], [ECat (Var "s^R") (Lit x)], zero) ass (pgm, ip, st) = Nothing + assbs :: (Program, Stack, State) -> Maybe (Stack, Stack, State) + assbs (pgm, [], {stack=[ECat (Lit "c") (ECat (Var "s") (Lit "")),ECat (Var "t") (Lit "")]}) + | pgm == innerpgm = Just ([], [ECat (Var "t^R") (ECat (Lit "c") (Var "s"))], zero) + assbs _ = 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) + innerpgm = 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 state io + = fromJust (prover ass pgm state io listIO) readFile :: !*File -> *(!String, !*File) readFile f |