diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 38 | ||||
| -rw-r--r-- | interp/constrintern.ml | 32 |
2 files changed, 37 insertions, 33 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3cabf52197..f687c4a640 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -27,6 +27,7 @@ open Glob_term open Glob_ops open Pattern open Detyping +open Structures module NamedDecl = Context.Named.Declaration (*i*) @@ -232,7 +233,7 @@ let get_record_print = let is_record indsp = try - let _ = Recordops.lookup_structure indsp in + let _ = Structure.find indsp in true with Not_found -> false @@ -407,7 +408,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) = let extern_record_pattern cstrsp args = try if !Flags.raw_print then raise Exit; - let projs = Recordops.lookup_projections (fst cstrsp) in + let projs = Structure.find_projections (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () else if PrintingConstructor.active (fst cstrsp) then @@ -614,9 +615,12 @@ let is_gvar id c = match DAst.get c with let is_projection nargs r = if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then try - let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then Some n - else None + match r with + | GlobRef.ConstRef c -> + let n = Structure.projection_nparams c + 1 in + if n <= nargs then Some n + else None + | _ -> None with Not_found -> None else None @@ -689,33 +693,29 @@ let extern_record ref args = try if !Flags.raw_print then raise Exit; let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in - let struc = Recordops.lookup_structure (fst cstrsp) in + let struc = Structure.find (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () else if PrintingConstructor.active (fst cstrsp) then raise Exit else if not (get_record_print ()) then raise Exit; - let projs = struc.Recordops.s_PROJ in - let locals = struc.Recordops.s_PROJKIND in + let projs = struc.Structure.projections in let rec cut args n = if Int.equal n 0 then args else match args with | [] -> raise No_match | _ :: t -> cut t (n - 1) in - let args = cut args struc.Recordops.s_EXPECTEDPARAM in - let rec ip projs locs args acc = + let args = cut args struc.Structure.nparams in + let rec ip projs args acc = match projs with | [] -> acc - | None :: q -> raise No_match - | Some c :: q -> - match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | { Recordops.pk_true_proj = false } :: locs' -> + | { Structure.proj_body = None } :: _ -> raise No_match + | { Structure.proj_body = Some c; proj_true = false } :: q -> (* we don't want to print locals *) - ip q locs' args acc - | { Recordops.pk_true_proj = true } :: locs' -> + ip q args acc + | { Structure.proj_body = Some c; proj_true = true } :: q -> match args with | [] -> raise No_match (* we give up since the constructor is not complete *) @@ -723,9 +723,9 @@ let extern_record ref args = let arg = Lazy.force arg in let loc = arg.CAst.loc in let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in - ip q locs' tail ((ref, arg) :: acc) + ip q tail ((ref, arg) :: acc) in - Some (List.rev (ip projs locals args [])) + Some (List.rev (ip projs args [])) with | Not_found | No_match | Exit -> None diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c63ebda3a..958e1408f8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,6 +24,7 @@ open Glob_term open Glob_ops open Patternops open Pretyping +open Structures open Cases open Constrexpr open Constrexpr_ops @@ -34,6 +35,7 @@ open Inductiveops open Context.Rel.Declaration open NumTok + (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - it replaces notations by their value (scopes stuff are here) @@ -100,7 +102,7 @@ type internalization_error = | NonLinearPattern of Id.t | BadPatternsNumber of int * int | NotAProjection of qualid - | ProjectionsOfDifferentRecords of Recordops.struc_typ * Recordops.struc_typ + | ProjectionsOfDifferentRecords of Structure.t * Structure.t exception InternalizationError of internalization_error @@ -126,8 +128,8 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 -let inductive_of_record record = - let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in +let inductive_of_record s = + let inductive = GlobRef.IndRef (s.Structure.name) in Nametab.shortest_qualid_of_global Id.Set.empty inductive let explain_field_not_a_projection field_id = @@ -1130,8 +1132,10 @@ let intern_reference qid = let intern_projection qid = try - let gr = Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) in - (gr, Recordops.find_projection gr) + match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with + | GlobRef.ConstRef c as gr -> + (gr, Structure.find_from_projection c) + | _ -> raise Not_found with Not_found -> Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) @@ -1296,8 +1300,8 @@ let check_applied_projection isproj realref qid = let is_prim = match realref with | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false | Some (ConstRef c) -> - if Recordops.is_primitive_projection c then true - else if Recordops.is_projection c then false + if PrimitiveProjections.mem c then true + else if Structure.is_projection c then false else error_nonprojection_syntax ?loc:qid.loc qid (* TODO check projargs, note we will need implicit argument info *) in @@ -1498,18 +1502,18 @@ let sort_fields ~complete loc fields completer = | (first_field_ref, _):: _ -> let (first_field_glob_ref, record) = intern_projection first_field_ref in (* the number of parameters *) - let nparams = record.Recordops.s_EXPECTEDPARAM in + let nparams = record.Structure.nparams in (* the reference constructor of the record *) - let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in + let base_constructor = GlobRef.ConstructRef (record.Structure.name,1) in let () = check_duplicate ?loc fields in - let build_proj idx proj kind = - if proj = None && complete then + let build_proj idx proj = + if proj.Structure.proj_body = None && complete then (* we don't want anonymous fields *) user_err ?loc (str "This record contains anonymous fields.") else - (idx, proj, kind.Recordops.pk_true_proj) in + (idx, proj.Structure.proj_body, proj.Structure.proj_true) in let proj_list = - List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in + List.map_i build_proj 1 record.Structure.projections in (* now we want to have all fields assignments indexed by their place in the constructor *) let rec index_fields fields remaining_projs acc = @@ -1538,7 +1542,7 @@ let sort_fields ~complete loc fields completer = (* For terms, we keep only regular fields *) None else - Some (idx, completer idx field_ref record.Recordops.s_CONST) in + Some (idx, completer idx field_ref (record.Structure.name,1)) in List.map_filter complete_field remaining_projs in List.rev_append remaining_fields acc in |