diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 15 | ||||
| -rw-r--r-- | toplevel/record.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 6 |
4 files changed, 18 insertions, 10 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index a7f7b2458..ee190d350 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -334,7 +334,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; Classes.set_typeclass_transparency (EvalConstRef cst) false false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); - let sub = if List.hd coers then Some (List.hd priorities) else None in + let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in cref, [Name proj_name, sub, Some proj_cst] | _ -> let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in @@ -342,7 +342,10 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls params (Option.default (Termops.new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in - let coers = List.map2 (fun coe pri -> if coe then Some pri else None) coers priorities in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) + coers priorities + in IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y)) (List.rev fields) coers (Recordops.lookup_projections ind)) in @@ -374,8 +377,9 @@ let interp_and_check_sort sort = open Vernacexpr open Autoinstance -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean - list telling if the corresponding fields must me declared as coercion *) +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances *) let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in @@ -404,6 +408,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil let arity = Option.default (Termops.new_Type ()) sc in let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in + let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs + fields is_coe (List.map (fun coe -> coe <> None) coers) sign in if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; IndRef ind diff --git a/toplevel/record.mli b/toplevel/record.mli index 131a5b9e1..45670f1fa 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -20,7 +20,7 @@ open Libnames val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> - bool list -> manual_explicitation list list -> rel_context -> + coercion_flag list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list val declare_structure : Decl_kinds.recursivity_kind -> @@ -35,5 +35,5 @@ val declare_structure : Decl_kinds.recursivity_kind -> val definition_structure : inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list * - (local_decl_expr with_coercion with_priority with_notation) list * + (local_decl_expr with_instance with_priority with_notation) list * identifier * constr_expr option -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 07454337f..cd30eaf5c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -415,7 +415,8 @@ let vernac_inductive finite infer indl = | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in - (((coe, AssumExpr ((loc, Name id), ce)), None), []) + let coe' = if coe then Some false else None in + (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ea7d0c6e2..32ea70baf 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -125,7 +125,8 @@ type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type opacity_flag = bool (* true = Opaque; false = Transparent *) type locality_flag = bool (* true = Local; false = Global *) -type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *) +type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) +type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind @@ -164,12 +165,13 @@ type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a +type 'a with_instance = instance_flag * 'a type 'a with_notation = 'a * decl_notation list type 'a with_priority = 'a * int option type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_coercion with_priority with_notation list + | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr |