diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 61 |
1 files changed, 51 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6b22261a15..02db8f6aab 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -120,6 +120,9 @@ type internalization_error = | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int + | NotAProjection of qualid + | NotAProjectionOf of qualid * qualid + | ProjectionsOfDifferentRecords of qualid * qualid exception InternalizationError of internalization_error Loc.located @@ -145,6 +148,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let explain_field_not_a_projection field_id = + pr_qualid field_id ++ str ": Not a projection" + +let explain_field_not_a_projection_of field_id inductive_id = + pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id + +let explain_projections_of_diff_records inductive1_id inductive2_id = + str "This record contains fields of both " ++ pr_qualid inductive1_id ++ + str " and " ++ pr_qualid inductive2_id + let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' @@ -153,6 +166,11 @@ let explain_internalization_error e = | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | NotAProjection field_id -> explain_field_not_a_projection field_id + | NotAProjectionOf (field_id, inductive_id) -> + explain_field_not_a_projection_of field_id inductive_id + | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> + explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." let error_bad_inductive_type ?loc = @@ -719,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in try let gc = intern nenv c in - Id.Map.add id (gc, Some c) map + Id.Map.add id (gc, None) map with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = @@ -1281,6 +1299,10 @@ let check_duplicate loc fields = user_err ?loc (str "This record defines several times the field " ++ pr_qualid r ++ str ".") +let inductive_of_record loc record = + let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1303,8 +1325,7 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc ~hdr:"intern" - (pr_qualid first_field_ref ++ str": Not a projection") + raise (InternalizationError(loc, NotAProjection first_field_ref)) in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in @@ -1363,12 +1384,18 @@ let sort_fields ~complete loc fields completer = with Not_found -> user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in + let this_field_record = try Recordops.find_projection field_glob_ref + with Not_found -> + let inductive_ref = inductive_of_record loc record in + raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) + in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> - user_err ?loc - (str "This record contains fields of different records.") + let ind1 = inductive_of_record loc record in + let ind2 = inductive_of_record loc this_field_record in + raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> @@ -2024,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; - let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in + (* We inform ltac that the interning vars and the notation vars are bound *) + (* but we could instead rely on the "intern_sign" *) let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in - let lvars = Id.Set.union lvars ntnvars in + let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in let ltacvars = Id.Set.union lvars env.ids in + (* Propagating enough information for mutual interning with tac-in-term *) + let intern_sign = { + Genintern.intern_ids = env.ids; + Genintern.notation_variable_status = ntnvars + } in let ist = { Genintern.genv = globalenv; ltacvars; extra; + intern_sign; } in let (_, glb) = Genintern.generic_intern ist gen in Some glb @@ -2317,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) + { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = + let tmp_scope = scope_of_type_kind sigma kind in + let impls = empty_internalization_env in + internalize env {ids; unb = false; tmp_scope; scopes = []; impls} + pattern_mode (ltacvars, vl) c + let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = + let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in - let c = internalize (Global.env()) {ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = impls} + let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls} false (empty_ltac_sign, vl) a in + (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in - (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in |