Add type_check binding form

This is similar to the previously added `type_error` binding form except that the expression is expected to pass elaboration without errors.
1ml-prime · Aug 24, 2020 · a01f037 · a01f037
1 parent ad9080b
commit a01f037
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 8 deletions.
diff --git a/elab.ml b/elab.ml
@@ -665,7 +665,11 @@ and elab_bind env bind l =
     );
     s, p, zs, e
 
-  | EL.TypeErrorB(exp) ->
+  | EL.TypeAssertB(true, exp) ->
+    let _ = elab_exp env exp l in
+    ExT([], StrT[]), Pure, [], IL.TupE[]
+
+  | EL.TypeAssertB(false, exp) ->
     (match try Some (elab_exp env exp l) with _ -> None with
     | None -> ExT([], StrT[]), Pure, [], IL.TupE[]
     | Some (s, _, _, _) ->

diff --git a/lexer.mll b/lexer.mll
@@ -265,6 +265,7 @@ rule token = parse
   | "as" { AS }
   | "do" { DO }
   | "else" { ELSE }
+  | "type_check" { TYPE_CHECK }
   | "type_error" { TYPE_ERROR }
   | "fun" { FUN }
   | "if" { IF }

diff --git a/parser.mly b/parser.mly
@@ -34,7 +34,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token LBRACE RBRACE
 %token DOT TICK
 %token COMMA SEMI
-%token TYPE_ERROR
+%token TYPE_CHECK TYPE_ERROR
 %token LOCAL
 %token IMPORT
 %token WRAP_OP UNWRAP_OP
@@ -498,8 +498,10 @@ atbind :
     { inclB($2)@@at() }
   | DO exp
     { doB($2)@@at() }
+  | TYPE_CHECK exp
+    { TypeAssertB(true, $2)@@at() }
   | TYPE_ERROR exp
-    { TypeErrorB($2)@@at() }
+    { TypeAssertB(false, $2)@@at() }
   | LET bind IN exp
     { inclB(letE($2, $4)@@at())@@at() }
   | IMPORT TEXT

diff --git a/syntax.ml b/syntax.ml
@@ -61,7 +61,7 @@ and bind' =
   | SeqB of bind * bind
   | VarB of var * exp
   | InclB of exp
-  | TypeErrorB of exp
+  | TypeAssertB of bool * exp
 
 
 let uniq_count = ref 0
@@ -73,7 +73,7 @@ let rec every_var pr b =
   | SeqB(b1, b2) -> every_var pr b1 && every_var pr b2
   | VarB(v, _) -> pr v
   | InclB(_) -> false
-  | TypeErrorB(_) -> true
+  | TypeAssertB(_) -> true
 
 let index n = "_" ^ string_of_int n
 
@@ -419,7 +419,7 @@ let label_of_bind b =
   | SeqB _ -> "SeqB"
   | VarB _ -> "VarB"
   | InclB _ -> "InclB"
-  | TypeErrorB _ -> "TypeErrorB"
+  | TypeAssertB _ -> "TypeAssertB"
 
 
 let string_of_var x = "\"" ^ x.it ^ "\""
@@ -480,7 +480,7 @@ and string_of_bind b =
   | SeqB(b1, b2) -> node' [string_of_bind b1; string_of_bind b2]
   | VarB(x, e) -> node' [string_of_var x; string_of_exp e]
   | InclB(e) -> node' [string_of_exp e]
-  | TypeErrorB(e) -> node' [string_of_exp e]
+  | TypeAssertB(b, e) -> node' [string_of_bool b; string_of_exp e]
 
 (* Import *)
 
@@ -528,4 +528,4 @@ and imports_bind bind =
   | SeqB(bind1, bind2) -> imports_bind bind1 @ imports_bind bind2
   | VarB(_, exp) -> imports_exp exp
   | InclB exp -> imports_exp exp
-  | TypeErrorB exp -> imports_exp exp
+  | TypeAssertB(_, exp) -> imports_exp exp