Add support for Refl in the parser.
This commit is contained in:
parent
4389661b23
commit
658f84a0c0
|
@ -91,7 +91,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
|
|||
| F.Absurd (_, ty) ->
|
||||
P.Absurd (Some (translate_type env ty))
|
||||
| F.Refl (_, ty) ->
|
||||
P.Refl (translate_type env ty)
|
||||
P.Refl (Some (translate_type env ty))
|
||||
| F.Use (_, t, u) ->
|
||||
let t' = self env t in
|
||||
let u' = self env u in
|
||||
|
|
|
@ -311,7 +311,7 @@ let get_loc t =
|
|||
| ML.App (pos, _, _) | ML.Let (pos, _, _, _, _) | ML.Annot (pos, _, _)
|
||||
| ML.For (pos, _, _) | ML.Some_ (pos, _, _) | ML.Tuple (pos, _)
|
||||
| ML.LetProd (pos, _, _, _) | ML.Variant (pos, _, _) | ML.Absurd pos
|
||||
| ML.Match (pos, _, _) | ML.Refl (pos, _) | ML.Use (pos, _, _)
|
||||
| ML.Match (pos, _, _) | ML.Refl pos | ML.Use (pos, _, _)
|
||||
-> pos
|
||||
|
||||
let correlate loc c =
|
||||
|
@ -549,8 +549,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
and+ ty = decode w
|
||||
in F.Absurd (loc, ty)
|
||||
|
||||
| ML.Refl (loc, ty) ->
|
||||
let@ v = convert typedecl_env tyvar_env ty in
|
||||
| ML.Refl loc ->
|
||||
let@ v = exist in
|
||||
let+ () = w --- tyeq v v
|
||||
and+ ty = decode v
|
||||
in F.Refl (loc, ty)
|
||||
|
|
|
@ -43,7 +43,7 @@ type term =
|
|||
| Variant of loc * Datatype.LabelId.t * term Option.t
|
||||
| Match of loc * term * branch list
|
||||
| Absurd of loc
|
||||
| Refl of loc * typ
|
||||
| Refl of loc
|
||||
| Use of loc * term * term
|
||||
|
||||
and branch = pattern * term
|
||||
|
|
|
@ -17,6 +17,7 @@
|
|||
"of", OF;
|
||||
"some", SOME;
|
||||
"for", FOR;
|
||||
"refl", REFL;
|
||||
"use", USE;
|
||||
]
|
||||
|
||||
|
|
|
@ -34,6 +34,7 @@
|
|||
%token COLON ":"
|
||||
%token SOME
|
||||
%token FOR
|
||||
%token REFL
|
||||
%token USE
|
||||
|
||||
%token IMPORT "#use"
|
||||
|
@ -86,6 +87,8 @@ let term_abs :=
|
|||
| SOME ; tyvars = list(tyvar) ; IN ; t = term_abs ;
|
||||
{ Some_ (Some $loc, tyvars, t) }
|
||||
|
||||
| REFL ; { Refl (Some $loc) }
|
||||
|
||||
| USE ; t = term_abs ; IN ; u = term_abs ;
|
||||
{ Use (Some $loc, t, u) }
|
||||
|
||||
|
@ -172,12 +175,14 @@ let type_arrow :=
|
|||
|
||||
|
||||
let type_tyconstr :=
|
||||
| ~ = tyname ; typarams = list (type_atom) ;
|
||||
| ~ = tyname ; typarams = nonempty_list (type_atom) ;
|
||||
{ TyConstr (Some $loc, tyname, typarams)}
|
||||
|
||||
| ~ = type_atom ; <>
|
||||
|
||||
let type_atom :=
|
||||
| ~ = tyname ; { TyConstr (Some $loc, tyname, []) }
|
||||
|
||||
| x = tyvar ; { TyVar (Some $loc, x) }
|
||||
|
||||
| "{" ; tys = separated_list ("*", typ) ; "}" ;
|
||||
|
|
|
@ -47,8 +47,8 @@ let rec translate_term (t : ML.term) : P.term =
|
|||
P.Match (None, self t, List.map translate_branch brs)
|
||||
| ML.Absurd _ ->
|
||||
P.Absurd None
|
||||
| ML.Refl (_, ty) ->
|
||||
P.Refl (translate_type ty)
|
||||
| ML.Refl _ ->
|
||||
P.Refl None
|
||||
| ML.Use (_, t, u) ->
|
||||
P.Use (self t, self u)
|
||||
|
||||
|
|
|
@ -36,7 +36,7 @@ type term =
|
|||
| Variant of Datatype.label_id * datatype option * term option
|
||||
| Match of typ option * term * branch list
|
||||
| Absurd of typ option
|
||||
| Refl of typ
|
||||
| Refl of typ option
|
||||
| Use of term * term
|
||||
|
||||
and branch = pattern * term
|
||||
|
|
|
@ -200,11 +200,8 @@ and print_term_app t =
|
|||
^^ space ^^ print_term_atom t
|
||||
| Variant (lbl, dty, t) ->
|
||||
print_variant lbl dty print_term_atom t
|
||||
| Refl ty ->
|
||||
group (
|
||||
string "Refl"
|
||||
^^ print_angle_type ty
|
||||
)
|
||||
| Refl _ ->
|
||||
string "refl"
|
||||
| t ->
|
||||
print_term_atom t
|
||||
|
||||
|
|
|
@ -47,8 +47,8 @@ module Shrinker = struct
|
|||
ML.Match (pos, subst t x u, List.map (fun br -> subst_branch br x u) brs)
|
||||
| ML.Absurd pos ->
|
||||
ML.Absurd pos
|
||||
| ML.Refl (pos, ty) ->
|
||||
ML.Refl (pos, ty)
|
||||
| ML.Refl pos ->
|
||||
ML.Refl pos
|
||||
| ML.Use (pos, t1, t2) ->
|
||||
ML.Use (pos, subst t1 x u, subst t2 x u)
|
||||
|
||||
|
|
|
@ -725,8 +725,19 @@ adjusting the level of the type nodes below the arrow.
|
|||
(refl : eq 'b 'a)
|
||||
|
||||
$ midml introduce-equality-symmetry.midml
|
||||
File "introduce-equality-symmetry.midml", line 6, characters 10-11:
|
||||
Syntax error.
|
||||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
FUN a1 a0 ->
|
||||
(FUN s[0]2 s[1]3 ->
|
||||
fun (y : eq s[0]2 s[1]3) ->
|
||||
let (y : eq s[0]2 s[1]3) = (y : eq s[0]2 s[1]3) in
|
||||
use (y : eq s[0]2 s[1]3) in
|
||||
(refl : eq s[1]3 s[0]2))
|
||||
[a0]
|
||||
[a1]
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
The above example is correct. The equality between 'a and {} is used to
|
||||
correctly typecheck the application (fun x -> x : 'a -> 'a) (). The type
|
||||
|
@ -1166,5 +1177,5 @@ Absurd typing environment
|
|||
|
||||
$ midml absurd2.midml
|
||||
Type inference and translation to System F...
|
||||
Fatal error: exception File "src/Generalization.ml", line 1603, characters 2-8: Assertion failed
|
||||
Fatal error: exception File "src/Generalization.ml", line 1596, characters 2-8: Assertion failed
|
||||
[2]
|
||||
|
|
Loading…
Reference in New Issue