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/8ba2cf0f847e40905cde3e14478e6be50b... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/8ba2cf0f847e40905cde3e14478e6be50b... You're receiving this email because of your account on gitlab.com.