Skip to content

Commit

Permalink
Add type_check binding form
Browse files Browse the repository at this point in the history
This is similar to the previously added `type_error` binding form except that
the expression is expected to pass elaboration without errors.
  • Loading branch information
polytypic committed Aug 24, 2020
1 parent f3b86c4 commit 1c5ddb9
Show file tree
Hide file tree
Showing 4 changed files with 15 additions and 8 deletions.
6 changes: 5 additions & 1 deletion elab.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, _, _, _) ->
Expand Down
1 change: 1 addition & 0 deletions lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
6 changes: 4 additions & 2 deletions parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -429,7 +429,7 @@ let label_of_bind b =
| SeqB _ -> "SeqB"
| VarB _ -> "VarB"
| InclB _ -> "InclB"
| TypeErrorB _ -> "TypeErrorB"
| TypeAssertB _ -> "TypeAssertB"


let string_of_var x = "\"" ^ x.it ^ "\""
Expand Down Expand Up @@ -490,7 +490,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 *)

Expand Down Expand Up @@ -538,4 +538,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

0 comments on commit 1c5ddb9

Please sign in to comment.