Stefan pushed to branch main at Stefan / Typer
Commits:
8ba2cf0f by Maxim Bernard at 2024-12-03T14:19:27-05:00
In elaboration, check residues only under certain conditions.
* src/elab.ml (infer_and_generalize_def): Check only for residues that
contain no uninstantiated metavariables in an outer scope.
Also perform such a check after elaboration of top-level definitions,
although this should not be absolutely necessary.
* src/unification.ml (check_no_residues): Replace with a function that
signals errors for residues that have no chance of being solvable later
during elaboration.
- - - - -
2 changed files:
- src/elab.ml
- src/unification.ml
Changes:
=====================================
src/elab.ml
=====================================
@@ -1434,8 +1434,9 @@ and infer_and_generalize_type (ctx : elab_context) se name =
and infer_and_generalize_def (ctx : elab_context) se =
let nctx = ectx_new_scope ctx in
let (e,t) = infer se nctx in
- Unif.check_no_residues (location e);
- Unif.clean_residues ();
+ Unif.raise_errors_on_out_of_scope_residues
+ (sexp_location se)
+ (ectx_to_scope_level ctx);
let g = resolve_instances_and_generalize nctx e in
let e' = g wrapLambda e in
let t' = g (fun ne name t _l e
@@ -1447,8 +1448,8 @@ and infer_and_generalize_def (ctx : elab_context) se =
and lexp_decls_1
(sdecls : sexp list) (* What's already parsed *)
(tokens : token list) (* Rest of input *)
- (ectx : elab_context) (* External ctx. *)
- (nctx : elab_context) (* New context. *)
+ (ectx : elab_context) (* External ctx. *)
+ (nctx : elab_context) (* New context. *)
(pending_decls : location SMap.t) (* Pending type decls. *)
(pending_defs : (symbol * sexp) list) (* Pending definitions. *)
: (vname * lexp * ltype) list * sexp list * token list * elab_context =
@@ -1594,7 +1595,10 @@ and lexp_decls_1
to each other (i.e. they can be mutually recursive).
- hence the overall "list of lists" is a sequence of such blocs of
mutually-recursive definitions. *)
-and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context)
+and lexp_p_decls ?(check_residues = true)
+ (sdecls : sexp list)
+ (tokens : token list)
+ (ctx : elab_context)
: ((vname * lexp * ltype) list list * elab_context) =
let rec impl sdecls tokens ctx =
match (sdecls, tokens) with
@@ -1602,6 +1606,11 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context)
| _ ->
let decls, sdecls, tokens, nctx =
lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in
+ if check_residues then
+ (* This is merely a sanity check. No residues should remain after
+ * the elaboration of a top-level definition (i.e. not in a `let`
+ * statement). *)
+ Unif.raise_error_on_all_residues ();
Log.stop_on_error ();
let declss, nnctx = impl sdecls tokens nctx in
decls :: declss, nnctx in
@@ -1865,7 +1874,7 @@ let rec sform_case ctx sinfo sargs ot = match sargs with
let sform_letin ctx loc sargs ot = match sargs with
| [sdecls; sbody]
- -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in
+ -> let declss, nctx = lexp_p_decls ~check_residues:false [sdecls] [] ctx in
let s, off =
List.fold_left (fun (s, off) decls ->
(OL.lexp_defs_subst loc s decls, off + List.length decls))
=====================================
src/unification.ml
=====================================
@@ -21,6 +21,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *)
open Ir
open Lexp
+open Util
module OL = Opslexp
module DB = Debruijn
@@ -52,19 +53,43 @@ let current_residues = ref ([] : (lexp_context * lexp * lexp) list)
let add_residue (ctx : lexp_context) (e1 : lexp) (e2 : lexp) =
current_residues := (ctx, e1, e2) :: !current_residues
-let check_no_residues (first_def_loc : Source.Location.t) : unit =
- (* Raises an error for every remaining residue. *)
+let signal_residue (loc : location) (e1 : lexp) (e2 : lexp) =
+ Log.log_error
+ ~section:"UNIF"
+ ~loc:loc
+ ("@[<v>Remaining residue. Can't unify:"
+ ^^ "@, @[<hov 2>%a@]"
+ ^^ "@,with:"
+ ^^ "@, @[<hov 2>%a@]@]")
+ pp_print_clean_lexp e1
+ pp_print_clean_lexp e2
+
+let raise_errors_on_out_of_scope_residues
+ (location : location)
+ (scope_level : scope_level) =
+ (* For each residue that caused an error to be logged, remove it from
+ * `current_residues`. *)
+ let new_residue_list = List.filter
+ (fun (_ctx, e1, e2) ->
+ let (_, e1_free_mv) = OL.fv e1 in
+ let (_, e2_free_mv) = OL.fv e2 in
+ let (free_mv_map, _) = OL.mv_set_union e1_free_mv e2_free_mv in
+ (* Only raise an error if no metavariables appear outside of
+ * `scope_level`. *)
+ let to_flag = IMap.for_all
+ (fun _ (mv_scope_level, _, _, _) ->
+ mv_scope_level >= scope_level)
+ free_mv_map in
+ if to_flag then
+ signal_residue location e1 e2;
+ not to_flag)
+ !current_residues in
+ current_residues := new_residue_list
+
+let raise_error_on_all_residues () : unit =
List.iter
- (fun (_ctx, lxp1, lxp2) ->
- Log.log_error
- ~section:"UNIF"
- ~loc:first_def_loc
- ("@[<v>Remaining residue. Can't unify:"
- ^^ "@, @[<hov 2>%a@]"
- ^^ "@,with:"
- ^^ "@, @[<hov 2>%a@]@]")
- Fmt.pp_print_lexp (clean lxp1)
- Fmt.pp_print_lexp (clean lxp2))
+ (fun (_ctx, e1, e2) ->
+ signal_residue dummy_location e1 e2)
!current_residues
let clean_residues () : unit =
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8ba2cf0f847e40905cde3e14478e6be50…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8ba2cf0f847e40905cde3e14478e6be50…
You're receiving this email because of your account on gitlab.com.