client/F: keep bound variable type in 'let'

This commit is contained in:
Gabriel Scherer 2023-02-19 23:24:21 +01:00
parent 3fdb9a141e
commit 5471bd8d1f
5 changed files with 31 additions and 23 deletions

View File

@ -87,7 +87,7 @@ type ('a, 'b) term =
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * tevar * ('a, 'b) term * ('a, 'b) term
| Let of loc * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list
@ -201,36 +201,39 @@ module TypeInTerm : DeBruijn.TRAVERSE
let rec traverse lookup extend env t =
let trav env = traverse lookup extend env in
let trav_ty env ty =
TypeInType.traverse lookup extend env ty in
match t with
| Var (pos, x) ->
Var (pos, x)
| Hole (pos, ty, ts) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
let ts' = List.map (trav env) ts in
Hole (pos, ty', ts')
| Annot (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
Annot (pos, t', ty')
| Abs (pos, x, ty, t) ->
let ty' = TypeInType.traverse lookup extend env ty
let ty' = trav_ty env ty
and t' = trav env t in
Abs (pos, x, ty', t')
| App (pos, t1, t2) ->
let t1' = trav env t1
and t2' = trav env t2 in
App (pos, t1', t2')
| Let (pos, x, t1, t2) ->
| Let (pos, x, ty, t1, t2) ->
let ty' = trav_ty env ty in
let t1' = trav env t1
and t2' = trav env t2 in
Let (pos, x, t1', t2')
Let (pos, x, ty', t1', t2')
| TyAbs (pos, x, t) ->
let env, x = extend env x in
let t' = trav env t in
TyAbs (pos, x, t')
| TyApp (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
TyApp (pos, t', ty')
| Tuple (pos, ts) ->
let ts' = List.map (trav env) ts in
@ -247,15 +250,15 @@ module TypeInTerm : DeBruijn.TRAVERSE
and t' = trav env t in
Variant (pos, lbl, dty', t')
| Match (pos, ty, t, brs) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
let t' = trav env t
and brs' = List.map (traverse_branch lookup extend env) brs in
Match (pos, ty', t', brs')
| Absurd (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
Absurd (pos, ty')
| Refl (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
Refl (pos, ty')
| Use (pos, t, u) ->
let t' = trav env t in

View File

@ -88,7 +88,7 @@ type ('a, 'b) term =
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * tevar * ('a, 'b) term * ('a, 'b) term
| Let of loc * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list

View File

@ -48,20 +48,22 @@ let print_type ty =
let rec translate_term env (t : F.nominal_term) : P.term =
let self = translate_term in
let annot env ty = (P.Flexible, [], translate_type env ty) in
match t with
| F.Var (_, x) ->
P.Var x
| F.Hole (_, ty, ts) ->
P.Hole (Some (translate_type env ty), List.map (self env) ts)
| F.Annot (_, t, ty) ->
P.Annot (self env t, (P.Flexible, [], translate_type env ty))
P.Annot (self env t, annot env ty)
| F.Abs (_, x, ty, t) ->
let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
P.Abs (annot, self env t)
let x_annot = P.PAnnot (P.PVar x, annot env ty) in
P.Abs (x_annot, self env t)
| F.App (_, t1, t2) ->
P.App (self env t1, self env t2)
| F.Let (_, x, t, u) ->
P.Let (P.Non_recursive, P.PVar x, self env t, self env u)
| F.Let (_, x, ty, t, u) ->
let x_annot = P.PAnnot (P.PVar x, annot env ty) in
P.Let (P.Non_recursive, x_annot, self env t, self env u)
| F.TyAbs (_, x, t) ->
let alpha = new_tyvar () in
P.TyAbs (alpha, self ((x, alpha) :: env) t)

View File

@ -384,8 +384,9 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
let ty1, ty2 = as_arrow ~loc (typeof env t) in
enforce_equal ~loc env (typeof env u) ty1;
ty2
| Let (_, x, t, u) ->
let env = extend_with_tevar env x (typeof env t) in
| Let (loc, x, ty, t, u) ->
enforce_equal ~loc env (typeof env t) ty;
let env = extend_with_tevar env x ty in
typeof env u
| TyAbs (_, (), t) ->
TyForall ((), typeof (extend_with_tyvar env) t)

View File

@ -125,12 +125,12 @@ let constr c xs =
let smart =
true
let flet ~loc (x, t, u) =
let flet ~loc (x, ty, t, u) =
match t with
| F.Var (_, y) when smart && x = y ->
u
| t ->
F.Let (loc, x, t, u)
F.Let (loc, x, ty, t, u)
(* -------------------------------------------------------------------------- *)
@ -362,7 +362,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
end;
(* Construct a ``let'' constraint. *)
let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
let+ (a, (b, ty), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
(* [a] are the type variables that we must bind (via Lambda abstractions)
while type-checking [t]. [(b, _)] is the type scheme that [x] must
receive while type-checking [u]. Its quantifiers [b] are guaranteed to
@ -370,8 +370,10 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
application of a suitable coercion to [x]. We use smart constructors so
that, if the lists [a] and [b] happen to be equal, no extra code is
produced. *)
F.Let (loc, x, F.ftyabs ~loc a t',
flet ~loc (x, coerce ~loc a b (F.Var (loc, x)),
let sch tyvars =
List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) tyvars ty in
F.Let (loc, x, sch a, F.ftyabs ~loc a t',
flet ~loc (x, sch b, coerce ~loc a b (F.Var (loc, x)),
u'))
| ML.Annot (loc, t, annot) ->