Add support let binding

wata727 · Aug 2, 2020 · 306fb90 · 306fb90
1 parent 10328aa
commit 306fb90
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 0 deletions.
diff --git a/11_fullsimple/README.md b/11_fullsimple/README.md
@@ -46,6 +46,8 @@ T = Nat -> Nat
 (lambda x:Nat. x): T
 
 # 11.5 Let Bindings
+% ./f "let x=true in x;"
+true: Bool
 
 # 11.7 Tuples
 

diff --git a/11_fullsimple/core.ml b/11_fullsimple/core.ml
@@ -15,6 +15,7 @@ type term =
     TmVar of info * int * int
   | TmAbs of info * string * ty * term
   | TmApp of info * term * term
+  | TmLet of info * string * term * term
   | TmTrue of info
   | TmFalse of info
   | TmIf of info * term * term * term
@@ -32,6 +33,7 @@ let tmInfo t = match t with
     TmVar(fi, _, _) -> fi
   | TmAbs(fi, _, _, _) -> fi
   | TmApp(fi, _, _) -> fi
+  | TmLet(fi, _, _, _) -> fi
   | TmTrue(fi) -> fi
   | TmFalse(fi) -> fi
   | TmIf(fi, _, _, _) -> fi
@@ -105,6 +107,8 @@ let rec printtm ctx t = match t with
       pr "(lambda "; pr x'; pr ":"; printty ctx tyT1; pr ". "; printtm ctx' t1; pr ")"
   | TmApp(fi, t1, t2) ->
       pr "("; printtm ctx t1; pr " "; printtm ctx t2; pr ")"
+  | TmLet(fi, x, t1, t2) ->
+      pr "let "; pr x; pr " = "; printtm ctx t1; pr " in "; printtm (addname ctx x) t2
   | TmVar(fi, x, n) ->
       if ctxlength ctx = n then
         pr (index2name fi ctx x)
@@ -155,6 +159,7 @@ let termShift d t =
                        else TmVar(fi, x, n+d)
   | TmAbs(fi, x, tyT1, t1) -> TmAbs(fi, x, tyT1, walk (c+1) t1)
   | TmApp(fi, t1, t2) -> TmApp(fi, walk c t1, walk c t2)
+  | TmLet(fi, x, t1, t2) -> TmLet(fi, x, walk c t1, walk (c+1) t2)
   | TmTrue(fi) as t -> t
   | TmFalse(fi) as t -> t
   | TmIf(fi, t1, t2, t3) -> TmIf(fi, walk c t1, walk c t2, walk c t3)
@@ -174,6 +179,7 @@ let termSubst j s t =
     TmVar(fi, x, n) -> if x = j+c then termShift c s else TmVar(fi, x, n)
   | TmAbs(fi, x, tyT1, t1) -> TmAbs(fi, x, tyT1, walk (c+1) t1)
   | TmApp(fi, t1, t2) -> TmApp(fi, walk c t1, walk c t2)
+  | TmLet(fi, x, t1, t2) -> TmLet(fi, x, walk c t1, walk (c+1) t2)
   | TmTrue(fi) as t -> t
   | TmFalse(fi) as t -> t
   | TmIf(fi, t1, t2, t3) -> TmIf(fi, walk c t1, walk c t2, walk c t3)
@@ -217,6 +223,11 @@ let rec eval1 ctx t = match t with
   | TmApp(fi, t1, t2) ->
       let t1' = eval1 ctx t1 in
       TmApp(fi, t1', t2)
+  | TmLet(fi, x, v1, t2) when isval ctx v1 ->
+      termSubstTop v1 t2
+  | TmLet(fi, x, t1, t2) ->
+      let t1' = eval1 ctx t1 in
+      TmLet(fi, x, t1', t2)
   | TmIf(_, TmTrue(_), t2, t3) -> t2
   | TmIf(_, TmFalse(_), t2, t3) -> t3
   | TmIf(fi, t1, t2, t3) ->
@@ -303,6 +314,10 @@ let rec typeof ctx t = match t with
             if (=) tyT2 tyT11 then tyT12
             else error fi "parameter type mismatch"
         | _ -> error fi "arrow type expected")
+  | TmLet(fi, x, t1, t2) ->
+      let tyT1 = typeof ctx t1 in
+      let ctx' = addbinding ctx x (VarBind(tyT1)) in
+      typeShift (-1) (typeof ctx' t2)
   | TmTrue(fi) -> TyBool
   | TmFalse(fi) -> TyBool
   | TmIf(fi, t1, t2, t3) ->

diff --git a/11_fullsimple/lexer.mll b/11_fullsimple/lexer.mll
@@ -14,6 +14,8 @@ let text = Lexing.lexeme
 rule main = parse
     [' ' '\n' '\r' '\t']+            { main lexbuf }
   | "lambda"                         { Parser.LAMBDA(info lexbuf) }
+  | "let"                            { Parser.LET(info lexbuf) }
+  | "in"                             { Parser.IN(info lexbuf) }
   | "as"                             { Parser.AS(info lexbuf) }
   | "if"                             { Parser.IF(info lexbuf) }
   | "then"                           { Parser.THEN(info lexbuf) }

diff --git a/11_fullsimple/parser.mly b/11_fullsimple/parser.mly
@@ -4,6 +4,8 @@ open Support
 %}
 
 %token <Support.info> LAMBDA
+%token <Support.info> LET
+%token <Support.info> IN
 %token <Support.info> AS
 %token <Support.info> IF
 %token <Support.info> THEN
@@ -73,6 +75,8 @@ Term: AppTerm                           { $1 }
     | LAMBDA LCID COLON Type DOT Term   { fun ctx -> let ctx1 = addname ctx $2.v in TmAbs($1,$2.v,$4 ctx, $6 ctx1) }
     | LAMBDA USCORE COLON Type DOT Term { fun ctx -> let ctx1 = addname ctx "_" in TmAbs($1,"_",$4 ctx, $6 ctx1) }
     | IF Term THEN Term ELSE Term       { fun ctx -> TmIf($1, $2 ctx, $4 ctx, $6 ctx) }
+    | LET LCID EQ Term IN Term          { fun ctx -> TmLet($1, $2.v, $4 ctx, $6 (addname ctx $2.v)) }
+    | LET USCORE EQ Term IN Term        { fun ctx -> TmLet($1, "_", $4 ctx, $6 (addname ctx "_")) }
 
 AppTerm: AscribeTerm                        { $1 }
        | AppTerm AscribeTerm                { fun ctx -> let e1 = $1 ctx in