5 files changed, 54 insertions(+), 3 deletions(-)

A examples/ifcmd.thon
M parse/ast.sml
M parse/thon.grm
M parse/thon.lex
M thon.sml

@@ 0,0 1,7 @@
+(* if cond then ret Z else ret S Z *)
+(* note the order flips *)
+run
+bnd cond <- cmd(ret Z) in
+do ifz cond of
+       Z -> cmd (ret S Z)
+     | S p -> cmd(ret Z)

@@ 157,6 157,7 @@ struct
         case t of
             Nat => f t
           | Unit => f t
+          | TypCmd => f t
           | TypVar (name, i) => f t
           | Arr(d, c) => f (Arr(typMap f d, typMap f c))
           | Prod(l, r) => f (Prod(typMap f l, typMap f r))

@@ 57,6 57,7 @@ structure A = Ast
  | AT
  | CMD
  | RUN
+ | DO
 
 %nonterm
    exp of A.exp


@@ 77,7 78,7 @@ structure A = Ast
 
 (* The precedence grows down *)
 %nonassoc TYPEOR (* Deliberately first *)
-%nonassoc EOF ZERO SUCC LPAREN RPAREN LAM COLON NAT IDX ID REC PIPE POLY COMMA STAR LEFT RIGHT FST SND ALL SOME TYPEREC DOT UNIT FOLD UNFOLD WITH AS USE IN CASE OF IMPL LET DCL BND EQ IFZ FIX FUN DATA RET LBRACE RBRACE BARROW SEMI AT CMD RUN
+%nonassoc EOF ZERO SUCC LPAREN RPAREN LAM COLON NAT IDX ID REC PIPE POLY COMMA STAR LEFT RIGHT FST SND ALL SOME TYPEREC DOT UNIT FOLD UNFOLD WITH AS USE IN CASE OF IMPL LET DCL BND EQ IFZ FIX FUN DATA RET LBRACE RBRACE BARROW SEMI AT CMD RUN DO
 %right SARROW
 %nonassoc APP GO (* Deliberately last *)
 


@@ 115,8 116,9 @@ exp:
 
 cmd:
     RET exp (A.Ret exp)
-  | BND ID BARROW exp SEMI cmd (A.Bnd(ID, exp, cmd))
+  | BND ID BARROW exp IN cmd (A.Bnd(ID, exp, cmd))
   | DCL ID COLON EQ exp IN cmd (A.Dcl(ID, exp, cmd))
+  | DO exp (A.Bnd("", exp, A.Ret(A.Var("", 0))))
   | AT ID (A.Get(ID))
   | ID COLON EQ exp (A.Set(ID, exp))
 


@@ 126,6 128,7 @@ top:
 
 typ:
     NAT (A.Nat)
+  | CMD (A.TypCmd)
   | UNIT (A.Unit)
   | typ SARROW typ (A.Arr(typ1, typ2))
   | typ STAR typ (A.Prod(typ1, typ2))

@@ 59,6 59,7 @@ ws = [\ \t];
 <INITIAL> "rec"    => (Tokens.REC(!pos,!pos));
 <INITIAL> "cmd"    => (Tokens.CMD(!pos,!pos));
 <INITIAL> "run"    => (Tokens.RUN(!pos,!pos));
+<INITIAL> "do"     => (Tokens.DO(!pos,!pos));
 <INITIAL> "go"     => (Tokens.GO(!pos,!pos));
 <INITIAL> "poly"   => (Tokens.POLY(!pos,!pos));
 <INITIAL> "left"   => (Tokens.LEFT(!pos,!pos));

@@ 2,6 2,7 @@
 structure Thon : sig
                    val parse : string -> Ast.exp
                    val parseFile : string -> Ast.exp
+                   val parseTop : string -> Ast.top
                    val parseFileTop : string -> Ast.top
                    val typeof : A.exp -> A.typ
                    val test : unit -> unit


@@ 114,7 115,23 @@ fun decrDeBruijinIndices t =
 
 
 (* Just substitute the srcType in everywhere you see a A.TypVar bindingDepth *)
-fun substTypeInExp' srcType dstExp bindingDepth =
+fun substTypeInCmd' srcType dstCmd bindingDepth =
+    case dstCmd of
+        A.Ret e => A.Ret(substTypeInExp' srcType e bindingDepth)
+      | A.Bnd(name, e, c) =>
+        A.Bnd(name,
+              substTypeInExp' srcType e bindingDepth,
+              substTypeInCmd' srcType c (bindingDepth+1)) (* binds immutable var *)
+      | A.Dcl(name, e, c) =>
+        A.Dcl(name,
+              substTypeInExp' srcType e bindingDepth,
+              (*binds symbol, not a immutable var*)
+              substTypeInCmd' srcType c bindingDepth)
+      | A.Get name => A.Get name
+      | A.Set(name, e) => A.Set(name, substTypeInExp' srcType e bindingDepth)
+
+
+and substTypeInExp' srcType dstExp bindingDepth =
     case dstExp
      of  A.Zero => A.Zero
        | A.Var (name, i) => A.Var (name, i)


@@ 173,6 190,7 @@ fun substTypeInExp' srcType dstExp bindingDepth =
        | A.Fold(t, e') => A.Fold(substType' srcType t bindingDepth,
                              substTypeInExp' srcType e' (bindingDepth+1)) (* binds typ var *)
        | A.Unfold(e') => A.Unfold(substTypeInExp' srcType e' bindingDepth)
+       | A.Cmd c => A.Cmd (substTypeInCmd' srcType c bindingDepth)
 
 
 fun setDeBruijnIndexInType t varnames typnames =


@@ 527,6 545,8 @@ and subst' src dst bindingDepth =
        | A.Pair (l, r) => A.Pair (subst' src l bindingDepth, subst' src r bindingDepth)
        | A.Fold(t, e') => A.Fold(t, (subst' src e' (bindingDepth))) (* binds a typ var *)
        | A.Unfold(e') => A.Unfold(subst' src e' (bindingDepth))
+       | A.Cmd cmd => A.Cmd (substExpInCmd' src cmd bindingDepth)
+       | _ => raise Unimplemented
 
 fun substExpInCmd src c = substExpInCmd' src c 0
 fun subst src dst = subst' src dst 0


@@ 684,6 704,13 @@ fun parse s =
         setDeBruijnIndexInExp ast [] []
     end
 
+fun parseTop s =
+    let val ast : A.top = Parse.parse s
+    in (case ast of
+           A.E e => A.E (setDeBruijnIndexInExp e [] [])
+         | A.Run c => A.Run (setDeBruijnIndexInCmd c [] [] []))
+    end
+
 fun parseFile filename =
     let val ast : A.top = Parse.parseFile filename
     in (case ast of


@@ 1257,6 1284,18 @@ val Dcl ("foo",Succ Zero,Ret (Succ Zero)) : cmd =
 val Ret (Succ Zero) : cmd =
     stepCmd (Dcl ("foo",Succ Zero,Ret (Succ Zero)))
 
+val ifcmd = Run
+    (Bnd
+       ("cond",Cmd (Ret Zero),
+        Bnd
+          ("",Ifz (Var ("cond",0),Cmd (Ret Zero),"p",Cmd (Ret (Succ Zero))),
+           Ret (Var ("",0)))));
+
+val Run (Ret Zero) : top = evalTop ifcmd;
+
+val Run (Ret (Succ Zero)) : top =
+    evalTop (parseFileTop "/home/evan/thon/examples/ifcmd.thon");
+
 in
 ()
 end