diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Smurf.dcl | 30 | ||||
| -rw-r--r-- | Smurf.icl | 125 | ||||
| -rw-r--r-- | SmurfParse.icl | 2 | ||||
| -rw-r--r-- | proof.icl | 18 | ||||
| -rw-r--r-- | proof.prj | 61 | ||||
| -rw-r--r-- | run.icl | 15 | ||||
| -rw-r--r-- | tree.icl | 2 |
8 files changed, 192 insertions, 62 deletions
@@ -3,6 +3,7 @@ *.out run tree +proof # Directory used to store object files, abc files and assembly files Clean System Files/ @@ -8,36 +8,46 @@ from StdOverloaded import from GenEq import generic gEq -from Data.Maybe import ::Maybe +from Data.Maybe import ::Maybe(Nothing) from LaTeX import class toLaTeX -:: Stm = Push String +:: Expr = Lit String + | Var String + | ECat Expr Expr + | EHead Expr + | ETail Expr + | EQuotify Expr + +:: Stm = Push Expr | Input | Output | Cat | Head | Tail | Quotify | Put | Get | Exec :: Program :== [Stm] -:: Stack :== [String] -:: Store :== [(String, String)] +:: Stack :== [Expr] +:: Store :== [(Expr, Expr)] :: State = { stack :: Stack , store :: Store } -:: IO io = IO (io -> .(String, io)) (String io -> io) +:: IO io = IO (io -> .(Expr, io)) (Expr io -> io) -:: ListIO = { input :: [String] - , output :: [String] +:: ListIO = { input :: [Expr] + , output :: [Expr] } :: Transition = (-->) infix 1 (Program, Stack, State) (Stack, Stack, State) :: DerivationTree :== [Transition] -derive gEq Stm +derive gEq Stm, Expr, State instance == Stm +instance == Expr +instance == State + instance toString Stm instance toChar Stm instance fromChar Stm @@ -57,4 +67,6 @@ step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io) run :: !Program State io (IO io) -> (Maybe State, io) listIO :: IO ListIO -tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree +prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State)) + Program State ListIO (IO ListIO) -> Maybe DerivationTree +tree :== prover (\_ -> Nothing) @@ -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] diff --git a/SmurfParse.icl b/SmurfParse.icl index 71bfc34..81f6c2f 100644 --- a/SmurfParse.icl +++ b/SmurfParse.icl @@ -16,7 +16,7 @@ import Smurf parse :: ![Char] -> Maybe Program parse [] = pure [] -parse ['"':cs] = parseString cs >>= \(s,cs`) -> append (Push s) $ parse cs` +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 diff --git a/proof.icl b/proof.icl new file mode 100644 index 0000000..3ea9b1a --- /dev/null +++ b/proof.icl @@ -0,0 +1,18 @@ +module proof + +import StdEnv, StdDebug + +from Data.Func import $ +import Data.Maybe + +import Smurf, SmurfParse + +Start = toString (devtree ass) +++ "\n" +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) diff --git a/proof.prj b/proof.prj new file mode 100644 index 0000000..0519a34 --- /dev/null +++ b/proof.prj @@ -0,0 +1,61 @@ +Version: 1.4 +Global + ProjectRoot: . + Target: StdEnv + Exec: {Project}/proof + CodeGen + CheckStacks: False + CheckIndexes: True + Application + HeapSize: 2097152 + StackSize: 512000 + ExtraMemory: 8192 + IntialHeapSize: 204800 + HeapSizeMultiplier: 4096 + ShowExecutionTime: False + ShowGC: False + ShowStackSize: False + MarkingCollector: False + DisableRTSFlags: False + StandardRuntimeEnv: True + Profile + Memory: False + MemoryMinimumHeapSize: 0 + Time: False + Stack: False + Output + Output: BasicValuesOnly + Font: Monaco + FontSize: 9 + WriteStdErr: False + Link + LinkMethod: Static + GenerateRelocations: False + GenerateSymbolTable: False + GenerateLinkMap: False + LinkResources: False + ResourceSource: + GenerateDLL: False + ExportedNames: + Paths + Path: {Project}/ + Path: {Application}/lib/Generics/ + Path: {Application}/lib/StdLib/ + Path: {Application}/lib/clean-platform/OS-Independent/ + Path: {Application}/lib/clean-platform/OS-Linux-64/ + Precompile: + Postlink: +MainModule + Name: proof + Dir: {Project} + Compiler + NeverMemoryProfile: False + NeverTimeProfile: False + StrictnessAnalysis: True + ListTypes: StrictExportTypes + ListAttributes: True + Warnings: True + Verbose: True + ReadableABC: False + ReuseUniqueNodes: True + Fusion: False @@ -17,6 +17,11 @@ import SmurfParse derive gEq SmurfOpt instance == SmurfOpt where == a b = a === b +instance <<< Expr +where + (<<<) f (Lit s) = f <<< s + // TODO Rest unimplemented for now + Start :: *World -> *World Start w // Options @@ -25,7 +30,7 @@ Start w | errs <> [] = error errs w # breakstms = if (isMember BreakAll opts) - [Push "", Input, Output, Cat, Head, Tail, Quotify, Put, Get, Exec] + [Push (Lit ""), Input, Output, Cat, Head, Tail, Quotify, Put, Get, Exec] [fromChar c \\ (Break c) <- opts] # inputs = [f \\ (IFile f) <- opts] | length inputs <> 1 = error ["Exactly one input file required"] w @@ -61,18 +66,18 @@ where where isBrk :: Program -> Bool isBrk [] = False - isBrk [(Push _):_] = isMember (Push "") brk + isBrk [(Push _):_] = isMember (Push (Lit "")) brk isBrk [stm:_] = isMember stm brk iofunc :: *IO *File iofunc = IO read show where - read :: *File -> *(String, *File) + read :: *File -> *(Expr, *File) read f # (s, f) = freadline f - = (s % (0, size s - 2), f) + = (Lit (s % (0, size s - 2)), f) - show :: String *File -> *File + show :: Expr *File -> *File show s f = f <<< s options = [ Option ['i'] ["infile"] @@ -20,7 +20,7 @@ Start w # tree = trace (toString tree +++ "\n") tree = toString (toLaTeX tree) where - devtree pgm = fromJust (tree pgm zero { zero & input = [""] } listIO) + devtree pgm = fromJust (tree pgm zero { zero & input = [Lit ""] } listIO) readFile :: !*File -> *(!String, !*File) readFile f |