Add type_error binding form

A binding of the form

    type_error exp

produces an error unless the elaboration of `exp` produces an error.

This is an experimental feature to help with testing both the compiler itself
and possibly for testing and documenting 1ML code.

elab.ml

@@ -597,6 +597,13 @@ and elab_bind env bind l =
     );
     s, p, zs, e
 
+  | EL.TypeErrorB(exp) ->
+    (match try Some (elab_exp env exp l) with _ -> None with
+    | None -> ExT([], StrT[]), Pure, [], IL.TupE[]
+    | Some (s, _, _, _) ->
+       error exp.at ("expected error, but got: " ^ Types.string_of_extyp s)
+    )
+
   | EL.EmptyB ->
     ExT([], StrT[]), Pure, [], IL.TupE[]
 

lexer.mll

@@ -73,6 +73,7 @@ rule token = parse
   | "do" { DO }
   | "else" { ELSE }
   | "end" { END }
+  | "type_error" { TYPE_ERROR }
   | "fun" { FUN }
   | "if" { IF }
   | "in" { IN }

paper.1ml

@@ -86,7 +86,7 @@ Map (Key : EQ) :> MAP with (type key = Key.t) =
 F = (fun (a : type) => type {x : a}) :> type => type;
 G = (fun (a : type) => type {x : a}) :> type -> type;
 H = fun (a : type) => (type {x : a} :> type);
-;; J = G :> type => type;  ;; ill-typed!
+type_error G :> type => type;
 
 ;; Higher Polymorphism
 
@@ -188,10 +188,10 @@ type T5 = (a : type) => {};
 type T6 = {type u a = bool};
 
 type Ti = T1;
-;; type U = pair Ti Ti;  ;; error
-;; A = (type Ti) : type;  ;; error
-;; B = {type u = Ti} :> {type u};  ;; error
-;; C = if true then Ti else int : type;  ;; error
+type_error type pair Ti Ti;
+type_error (type Ti) : type;
+type_error {type u = Ti} :> {type u};
+type_error if true then Ti else int : type;
 
 type T1' = (= type int);
 type T2' = {type u = int};
@@ -210,7 +210,7 @@ C = if true then Ti else int : type;
 
 type MONSTER =
   (= (fun (x : {}) => ({type t = int; v = 0} :> {type t; v : t}).v));
-;; Test (X : MONSTER) = X : MONSTER;  ;; error
+type_error { Test (X : MONSTER) = X : MONSTER };
 
 
 ;; Section 4: Full 1ML
@@ -248,7 +248,7 @@ FirstClassImplicit =
 id : 'a => a -> a = fun x => x;
 G (x : int) = {M = {type t = int; v = x} :> {type t; v : t}; f = id id};
 C = G 3;
-;; x = C.f C.M.v;  ;; error
+type_error C.f C.M.v;
 
 ;; ...works with pure 'id' function:
 id = fun x => x;
@@ -268,7 +268,7 @@ G (x : int) = {M = {type t = int; v = x} :> {type t; v : t}; f = id id};
 C = G 3;
 C' = G 3;
 x = C'.f C.M.v;
-;; x = C.f C'.M.v;  ;; but this is an error
+type_error C.f C'.M.v;
 
 
 ;; Appendix C: Impredicativity

parser.mly

@@ -34,6 +34,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token LBRACE RBRACE
 %token DOT AT TICK
 %token COMMA SEMI
+%token TYPE_ERROR
 
 %token EOF
 
@@ -368,6 +369,8 @@ atbind :
     { letB($2, $4)@@at() }
   | DO exp
     { doB($2)@@at() }
+  | TYPE_ERROR exp
+    { TypeErrorB($2)@@at() }
 /*
   | LPAR bind RPAR
     { $2 }

regression.1ml

@@ -24,11 +24,17 @@ Equivalence: {
 
 ;;
 
+type_error { type_error 101 };
+
+;;
+
 Pure : () => {type t = bool; existentials: t} = fun () =>
   {type t = bool; existentials = false} :> {type t = bool; existentials: t};
 
-;; Impure : () => {type t; existentials: t} = fun () =>
-;;   {type t = bool; existentials = true} :> {type t = bool; existentials: t};
+type_error {
+  Impure : () => {type t; existentials: t} = fun () =>
+    {type t = bool; existentials = true} :> {type t = bool; existentials: t};
+};
 
 ;;
 

syntax.ml

@@ -58,6 +58,7 @@ and bind' =
   | SeqB of bind * bind
   | VarB of var * exp
   | InclB of exp
+  | TypeErrorB of exp
 
 
 let var_counts = ref []
@@ -373,6 +374,7 @@ let label_of_bind b =
   | SeqB _ -> "SeqB"
   | VarB _ -> "VarB"
   | InclB _ -> "InclB"
+  | TypeErrorB _ -> "TypeErrorB"
 
 
 let string_of_var x = "\"" ^ x.it ^ "\""
@@ -431,3 +433,4 @@ 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]

test.1ml

@@ -290,7 +290,7 @@ in
   y1 = (G(type bool)).y : list int;
   y2 = (G(type bool)).y : list bool;
   M = G(type bool);
-;;  y3 = M.y : list (M.u);
+  type_error M.y : list (M.u);
 end;