client/F: support "let rec"

This commit is contained in:
Gabriel Scherer 2023-02-20 18:35:57 +01:00
parent 5471bd8d1f
commit 054ca8434b
5 changed files with 24 additions and 12 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) typ * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * 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
@ -99,6 +99,8 @@ type ('a, 'b) term =
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
@ -222,11 +224,11 @@ module TypeInTerm : DeBruijn.TRAVERSE
let t1' = trav env t1
and t2' = trav env t2 in
App (pos, t1', t2')
| Let (pos, x, ty, t1, t2) ->
| Let (pos, rec_, 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, ty', t1', t2')
Let (pos, rec_, x, ty', t1', t2')
| TyAbs (pos, x, t) ->
let env, x = extend env x in
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) typ * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * 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
@ -100,6 +100,8 @@ type ('a, 'b) term =
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =

View File

@ -61,9 +61,13 @@ let rec translate_term env (t : F.nominal_term) : P.term =
P.Abs (x_annot, self env t)
| F.App (_, t1, t2) ->
P.App (self env t1, self env t2)
| F.Let (_, x, ty, t, u) ->
| F.Let (_, rec_, x, ty, t, u) ->
let rec_ = match rec_ with
| F.Recursive -> P.Recursive
| F.Non_recursive -> P.Non_recursive
in
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)
P.Let (rec_, 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,10 +384,14 @@ 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 (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
| Let (loc, rec_, x, ty, t, u) ->
let env_with_x = extend_with_tevar env x ty in
let def_env = match rec_ with
| Non_recursive -> env
| Recursive -> env_with_x
in
enforce_equal ~loc def_env (typeof def_env t) ty;
typeof env_with_x u
| TyAbs (_, (), t) ->
TyForall ((), typeof (extend_with_tyvar env) t)
| TyApp (loc, t, ty2) ->

View File

@ -130,7 +130,7 @@ let flet ~loc (x, ty, t, u) =
| F.Var (_, y) when smart && x = y ->
u
| t ->
F.Let (loc, x, ty, t, u)
F.Let (loc, F.Non_recursive, x, ty, t, u)
(* -------------------------------------------------------------------------- *)
@ -372,7 +372,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
produced. *)
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',
F.Let (loc, F.Non_recursive, x, sch a, F.ftyabs ~loc a t',
flet ~loc (x, sch b, coerce ~loc a b (F.Var (loc, x)),
u'))