From 054ca8434b1b9be9b89f83193da877a5b26f2ba5 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Mon, 20 Feb 2023 18:35:57 +0100
Subject: [PATCH] client/F: support "let rec"
---
client/F.ml | 8 +++++---
client/F.mli | 4 +++-
client/FPrinter.ml | 8 ++++++--
client/FTypeChecker.ml | 12 ++++++++----
client/Infer.ml | 4 ++--
5 files changed, 24 insertions(+), 12 deletions(-)
diff --git a/client/F.ml b/client/F.ml
index a064d0c..5fc2eb8 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -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
diff --git a/client/F.mli b/client/F.mli
index 1ceb0a4..eed4d7f 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -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 =
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index 21bfcbe..7d5b922 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -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)
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 76f1052..332d1c7 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -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) ->
diff --git a/client/Infer.ml b/client/Infer.ml
index 742a71b..0e57b3d 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -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'))
--
GitLab