From 09cf0f0791f8d05dbec240917e2010b161bb24f6 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Fri, 10 Jun 2016 08:45:09 +0200 Subject: Minimalistic prover --- Smurf.icl | 125 +++++++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 79 insertions(+), 46 deletions(-) (limited to 'Smurf.icl') diff --git a/Smurf.icl b/Smurf.icl index 9afefb8..fa5cd00 100644 --- a/Smurf.icl +++ b/Smurf.icl @@ -3,6 +3,7 @@ implementation module Smurf from StdFunc import o, flip import StdArray import StdList +import StdMisc import StdString import StdTuple import StdFile @@ -20,19 +21,32 @@ import GenPrint import SmurfParse import LaTeX -derive gEq Stm -derive gPrint (,) - -(<+) infixr 5 :: a b -> String | toString a & toString b -(<+) a b = toString a +++ toString b +derive gEq Stm, Expr, State +derive gPrint (,), Expr instance == Stm where == a b = a === b +instance == Expr where == a b = a === b +instance == State where == a b = a === b instance zero [a] where zero = [] +/// Utilities ... + +(<+) infixr 5 :: a b -> String | toString a & toString b +(<+) a b = toString a +++ toString b + +instance toString Expr +where + toString (Lit s) = s + toString (Var v) = "$" <+ v + toString (ECat a b) = a <+ b + toString (EHead a) = "hd(" <+ a <+ ")" + toString (ETail a) = "tl(" <+ a <+ ")" + toString (EQuotify a) = "q(" <+ a <+ ")" + instance toString Stm where - toString (Push s) = quotify s + toString (Push s) = toString $ quotify s toString Input = "i" toString Output = "o" toString Cat = "+" @@ -47,7 +61,7 @@ instance toChar Stm where toChar stm = (toString stm).[0] instance fromChar Stm where - fromChar '"' = Push "" + fromChar '"' = Push $ Lit "" fromChar 'i' = Input fromChar 'o' = Output fromChar '+' = Cat @@ -86,7 +100,7 @@ where toString ts = concat $ intersperse "\n" $ map toString $ reverse ts instance toLaTeX Stm where - toLaTeX (Push s) = List [Command "StmPush" [], Raw "~", sToLaTeX s] + toLaTeX (Push s) = List [Command "StmPush" [], Raw "~", eToLaTeX s] toLaTeX Input = Command "StmInput" [] toLaTeX Output = Command "StmOutput" [] toLaTeX Cat = Command "StmCat" [] @@ -113,12 +127,12 @@ where intersperse (Raw ",") (map assToLaTeX ass) ++ [Command "}" []]) where - assToLaTeX :: (String,String) -> LaTeX + assToLaTeX :: (Expr,Expr) -> LaTeX assToLaTeX (var,val) = List - [ sToLaTeX var + [ eToLaTeX var , Command "mapsto" [] - , sToLaTeX val + , eToLaTeX val ] instance toLaTeX State @@ -146,12 +160,12 @@ where , toLaTeX st2 ] -stackToLaTeX :: [String] -> LaTeX -stackToLaTeX ss - = List $ intersperse (Text ":") (map sToLaTeX ss ++ [Command "Nil" []]) +stackToLaTeX :: Stack -> LaTeX +stackToLaTeX es + = List $ intersperse (Text ":") (map eToLaTeX es ++ [Command "Nil" []]) -sToLaTeX :: String -> LaTeX -sToLaTeX s = Command "texttt" [List [Raw "\"", Text s, Raw "\""]] +eToLaTeX :: Expr -> LaTeX +eToLaTeX e = Command "texttt" [List [Raw "\"", Text (toString e), Raw "\""]] instance toLaTeX DerivationTree where @@ -187,6 +201,17 @@ where [Get:_] = "rgetns" [Exec:_] = "rexecns" +/// End utilities + +instance +++ Expr +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 @@ -226,32 +251,36 @@ 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 fromString o fst >>= \p -> + = (pop st.stack >>= parse o eToCharList o fst >>= \p -> pure (p, zero), io) -push :: String Stack -> Stack +push :: Expr Stack -> Stack push s st = [s:st] -pop :: Stack -> Maybe (String, Stack) +pop :: Stack -> Maybe (Expr, Stack) pop [] = empty pop [s:ss] = pure (s, ss) -head :: String -> Maybe String -head "" = empty -head s = pure $ s % (0,0) +head :: Expr -> Maybe Expr +head (Lit "") = empty +head (Lit s) = pure $ Lit $ s % (0,0) +head e = pure $ EHead e -tail :: String -> Maybe String -tail "" = empty -tail s = pure $ s % (1, size s - 1) +tail :: Expr -> Maybe Expr +tail (Lit "") = empty +tail (Lit s) = pure $ Lit $ s % (1, size s - 1) +tail e = pure $ ETail e -put :: String String Store -> Store +put :: Expr Expr Store -> Store put var val store = [(var,val) : filter ((<>)var o fst) store] -get :: String Store -> String -get var store = case filter ((==)var o fst) store of [] = ""; [(_,val):_] = val +get :: Expr Store -> Expr +get var store = case filter ((==)var o fst) store of + [] = Lit "" + [(_,val):_] = val -quotify :: (String -> String) -quotify = (flip (+++) "\"") o ((+++)"\"") o toString o quot o fromString +quotify :: Expr -> Expr +quotify (Lit s) = Lit $ flip (+++) "\"" $ (+++)"\"" $ toString $ quot $ fromString s where quot :: [Char] -> [Char] quot [] = [] @@ -261,27 +290,31 @@ where quot ['\t':cs] = ['\\':'t':quot cs] quot ['"':cs] = ['\\':'"':quot cs] quot [c:cs] = [c:quot cs] +quotify e = EQuotify e listIO :: IO ListIO listIO = IO read write where - read :: ListIO -> (String, ListIO) + read :: ListIO -> (Expr, ListIO) read io=:{input} = (hd input, { io & input=tl input }) - write :: String ListIO -> ListIO + write :: Expr ListIO -> ListIO write s io=:{output} = { io & output=output ++ [s] } -tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree -tree pgm st io iof - # init = (pgm, io.input, st) - # (mbPgmSt, io) = step pgm st io iof - | isNothing mbPgmSt = empty - # (pgm, st) = fromJust mbPgmSt - | isEmpty pgm = pure [ init --> (io.input, io.output, st) - , ([],io.input,st) --> (io.input,[],st) - ] - # mbTree = tree pgm st io iof - | isNothing mbTree = empty - # tree = fromJust mbTree - # [child=:(_ --> final):children] = fromJust mbTree - = pure [init --> final:child:children] +prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State)) + Program State ListIO (IO ListIO) -> Maybe DerivationTree +prover assumptions pgm st io iof +# init = (pgm, io.input, st) +# mbAssumption = assumptions init +| isJust mbAssumption + = Just [init --> fromJust mbAssumption] +# (mbPgmSt, io) = step pgm st io iof +| isNothing mbPgmSt = empty +# (pgm, st) = fromJust mbPgmSt +| isEmpty pgm = pure [ init --> (io.input, io.output, st) + , ([],io.input,st) --> (io.input,[],st) + ] +# mbTree = prover assumptions pgm st io iof +| isNothing mbTree = empty +# [child=:(_ --> final):children] = fromJust mbTree += pure [init --> final:child:children] -- cgit v1.2.3