diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 10 | ||||
| -rw-r--r-- | interp/constrintern.ml | 35 | ||||
| -rw-r--r-- | interp/declare.mli | 5 |
3 files changed, 41 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 601099c6ff..838ef40545 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -480,6 +480,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> @@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) |None -> raise No_match in assert (List.is_empty substlist); - mkPat ?loc qid (List.rev_append l1 l2') + insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> @@ -1131,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function binderlists in insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in - CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in + insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in if List.is_empty args then e else let args = fill_arg_scopes args argsscopes allscopes in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6b22261a15..c03a5fee90 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 = @@ -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) | [] -> diff --git a/interp/declare.mli b/interp/declare.mli index 02e73cd66c..468e056909 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Libnames open Constr open Entries open Decl_kinds @@ -29,7 +28,7 @@ type section_variable_entry = type variable_declaration = DirPath.t * section_variable_entry * logical_kind -val declare_variable : variable -> variable_declaration -> object_name +val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -69,7 +68,7 @@ val set_declare_scheme : (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> object_name * bool +val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool (** Declaration messages *) |