aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/classes.ml16
-rw-r--r--toplevel/classes.mli3
-rw-r--r--toplevel/command.ml5
-rw-r--r--toplevel/command.mli1
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/vernacentries.ml71
-rw-r--r--toplevel/vernacexpr.ml2
8 files changed, 79 insertions, 25 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 89bf68bb8..333a26f03 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -117,7 +117,7 @@ open Topconstr
let declare_implicit_proj c proj imps sub =
let len = List.length c.cl_context in
- let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in
+ let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in
let expls =
let rec aux i expls = function
[] -> expls
@@ -130,8 +130,8 @@ let declare_implicit_proj c proj imps sub =
in
let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
if sub then
- declare_instance_cst true proj;
- Impargs.declare_manual_implicits true (ConstRef proj) true expls
+ declare_instance_cst true (snd proj);
+ Impargs.declare_manual_implicits true (ConstRef (snd proj)) true expls
let declare_implicits impls subs cl =
Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
@@ -186,7 +186,7 @@ let declare_structure env id idbuild params arity fields =
let kn = Command.declare_mutual_with_eliminations true mie [] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
- let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
+ let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in
let _build = ConstructRef (rsp,1) in
Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
rsp
@@ -314,11 +314,12 @@ let new_class id par ar sup props =
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
- ConstRef cst, [proj_cst]
+ ConstRef cst, [proj_name, proj_cst]
| _ ->
let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
let kn = declare_structure env0 (snd id) idb params arity fields in
- IndRef kn, (List.map Option.get (Recordops.lookup_projections kn))
+ IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
+ fields (Recordops.lookup_projections kn))
in
let ctx_context =
List.map (fun ((na, b, t) as d) ->
@@ -546,8 +547,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
List.fold_left
(fun (props, rest) (id,_,_) ->
try
- let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+ let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+ Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
c :: props, rest'
with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
([], props) k.cl_props
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index bbb7b85ca..88147b539 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -28,7 +28,8 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
val binders_of_lidents : identifier located list -> local_binder list
-val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> bool -> unit
+val declare_implicit_proj : typeclass -> (identifier * constant) ->
+ Impargs.manual_explicitation list -> bool -> unit
(*
val infer_super_instances : env -> constr list ->
named_context -> named_context -> types list * identifier list * named_context
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7be01c666..11b849c4f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -144,6 +144,7 @@ let declare_global_definition ident ce local imps =
let declare_definition_hook = ref ignore
let set_declare_definition_hook = (:=) declare_definition_hook
+let get_declare_definition_hook () = !declare_definition_hook
let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
@@ -871,13 +872,13 @@ let interp_recursive fixkind l boxed =
let build_recursive l b =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
- let fixl = List.map (fun ((id,_,bl,typ,def),ntn) ->
+ let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
l in
interp_recursive (IsFixpoint g) fixl b
let build_corecursive l b =
- let fixl = List.map (fun ((id,bl,typ,def),ntn) ->
+ let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
l in
interp_recursive IsCoFixpoint fixl b
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8448817f6..595057616 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,6 +30,7 @@ open Redexpr
functions of [Declare]; they return an absolute reference to the
defined object *)
+val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit)
val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
val definition_message : identifier -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f6815d537..83332e823 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,7 +131,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
-let declare_projections indsp ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
@@ -172,7 +172,7 @@ let declare_projections indsp ?name coers fields =
const_entry_type = Some projtyp;
const_entry_opaque = false;
const_entry_boxed = Flags.boxed_definitions() } in
- let k = (DefinitionEntry cie,IsDefinition StructureComponent) in
+ let k = (DefinitionEntry cie,IsDefinition kind) in
let kn = declare_internal_constant fid k in
Flags.if_verbose message (string_of_id fid ^" is defined");
kn
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 5ba8b04e1..c2c6b72ee 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -21,7 +21,7 @@ open Topconstr
as coercions accordingly to [coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+ inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
val definition_structure :
lident with_coercion * local_binder list *
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 49690256c..30d993256 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -300,7 +300,20 @@ let start_proof_and_print k l hook =
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
+let dump_definition (loc, id) s =
+ Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
+
+let dump_variable (loc, id) s = ()
+(* Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) *)
+(* (string_of_kn (Lib.make_kn id))) *)
+
+let dump_constraint ty ((loc, n), _, _) =
+ match n with
+ | Name id -> dump_definition (loc, id) ty
+ | Anonymous -> ()
+
let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
+ if !Flags.dump then dump_definition lid "def";
match def with
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
@@ -319,6 +332,11 @@ let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
declare_definition id k bl red_option c typ_opt hook
let vernac_start_proof kind l lettop hook =
+ if !Flags.dump then
+ List.iter (fun (id, _) ->
+ match id with
+ | Some lid -> dump_definition lid "prf"
+ | None -> ()) l;
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
@@ -351,13 +369,29 @@ let vernac_exact_proof c =
(str "Command 'Proof ...' can only be used at the beginning of the proof")
let vernac_assumption kind l nl=
- List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c false false nl) l
-
-let vernac_inductive f indl = build_mutual indl f
-
-let vernac_fixpoint = build_recursive
-
-let vernac_cofixpoint = build_corecursive
+ let global = fst kind = Global in
+ List.iter (fun (is_coe,(idl,c)) ->
+ if !dump then
+ List.iter (fun lid -> if global then dump_definition lid "ax" else
+ dump_variable lid "var") idl;
+ declare_assumption idl is_coe kind [] c false false nl) l
+
+let vernac_inductive f indl =
+ if !dump then
+ List.iter (fun ((lid, _, _, cstrs), _) ->
+ dump_definition lid "ind";
+ List.iter (fun (_, (lid, _)) ->
+ dump_definition lid "constr") cstrs)
+ indl;
+ build_mutual indl f
+
+let vernac_fixpoint l b =
+ List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid "def") l;
+ build_recursive l b
+
+let vernac_cofixpoint l b =
+ List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "def") l;
+ build_corecursive l b
let vernac_scheme = build_scheme
@@ -487,7 +521,8 @@ let vernac_include = function
let vernac_record struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (snd struc))
- | Some (_,id) -> id in
+ | Some (_,id as lid) ->
+ if !dump then dump_definition lid "constr"; id in
let sigma = Evd.empty in
let env = Global.env() in
let s = interp_constr sigma env sort in
@@ -496,7 +531,13 @@ let vernac_record struc binders sort nameopt cfs =
| Sort s -> s
| _ -> user_err_loc
(constr_loc sort,"definition_structure", str "Sort expected") in
- ignore(Record.definition_structure (struc,binders,cfs,const,s))
+ if !dump then (
+ dump_definition (snd struc) "rec";
+ List.iter (fun (_, x) ->
+ match x with
+ | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) "proj"
+ | _ -> ()) cfs);
+ ignore(Record.definition_structure (struc,binders,cfs,const,s))
(* Sections *)
@@ -537,15 +578,21 @@ let vernac_identity_coercion stre id qids qidt =
(* Type classes *)
let vernac_class id par ar sup props =
+ if !dump then (
+ dump_definition id "class";
+ List.iter (fun (lid, _, _) -> dump_definition lid "meth") props);
Classes.new_class id par ar sup props
-
+
let vernac_instance glob sup inst props pri =
+ if !dump then dump_constraint "inst" inst;
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
+ if !dump then List.iter (dump_constraint "var") l;
Classes.context l
let vernac_declare_instance id =
+ if !dump then dump_definition id "inst";
Classes.declare_instance false id
(***********)
@@ -679,7 +726,9 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
let vernac_hints = Auto.add_hints
-let vernac_syntactic_definition = Command.syntax_definition
+let vernac_syntactic_definition lid =
+ dump_definition lid "syndef";
+ Command.syntax_definition (snd lid)
let vernac_declare_implicits local r = function
| Some imps ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cce6f9a62..8f54e699e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -288,7 +288,7 @@ type vernac_expr =
| VernacDeclareTacticDefinition of
rec_flag * (reference * bool * raw_tactic_expr) list
| VernacHints of locality_flag * lstring list * hints
- | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
+ | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
locality_flag * onlyparsing_flag
| VernacDeclareImplicits of locality_flag * lreference *
(explicitation * bool * bool) list option
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 12:06:27 +0000