~thon/thon

d7b95aee41e162fcd9dacf5f39a59081f33b9092 — Evan Bergeron 4 months ago 42b8893 mut
Add do keyword and example conditional command execution
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
A examples/ifcmd.thon => examples/ifcmd.thon +7 -0
@@ 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)

M parse/ast.sml => parse/ast.sml +1 -0
@@ 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))

M parse/thon.grm => parse/thon.grm +5 -2
@@ 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))

M parse/thon.lex => parse/thon.lex +1 -0
@@ 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));

M thon.sml => thon.sml +40 -1
@@ 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