diff options
41 files changed, 554 insertions, 213 deletions
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index 4b3492b12..71f483fb6 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -183,7 +183,7 @@ VERNAC ARGUMENT EXTEND rec_definition2 | Some an -> check_exists_args an in - (id, ni, bl, type_, def) ] + ((Util.dummy_loc,id), ni, bl, type_, def) ] END diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index fa49d4aa8..a071add63 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -160,7 +160,7 @@ let build_newrecursive in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (recname,_,bl,arityc,_) -> + (fun (env,impls) ((_,recname),_,bl,arityc,_) -> let arityc = Command.generalize_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = @@ -297,7 +297,7 @@ let generate_principle on_error is_general do_built fix_rec_l recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in + let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in @@ -318,7 +318,7 @@ let generate_principle on_error f_R_mut) in let fname_kn (fname,_,_,_,_) = - let f_ref = Ident (dummy_loc,fname) in + let f_ref = Ident fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -351,7 +351,7 @@ let generate_principle on_error let register_struct is_rec fixpoint_exprl = match fixpoint_exprl with - | [(fname,_,bl,ret_type,body),_] when not is_rec -> + | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> Command.declare_definition fname (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition) @@ -475,7 +475,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with - | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> + | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle on_error @@ -488,7 +488,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp if register_built then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook; false - | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> + | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle on_error @@ -503,7 +503,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true | _ -> let fix_names = - List.map (function (name,_,_,_,_) -> name) fixpoint_exprl + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_one_rec = is_rec fix_names in let old_fixpoint_exprl = @@ -535,7 +535,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp in (* ok all the expressions are structural *) let fix_names = - List.map (function (name,_,_,_,_) -> name) fixpoint_exprl + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in if register_built then register_struct is_rec old_fixpoint_exprl; @@ -724,7 +724,7 @@ let make_graph (f_ref:global_reference) = nal_tas ) in - let b' = add_args id new_args b in + let b' = add_args (snd id) new_args b in (id, Some (Struct rec_id),nal_tas@bl,t,b') ) fixexprl @@ -732,13 +732,13 @@ let make_graph (f_ref:global_reference) = l | _ -> let id = id_of_label (con_label c) in - [(id,None,nal_tas,t,b)] + [((dummy_loc,id),None,nal_tas,t,b)] in do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter - (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) + (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) expr_list diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 169ec0dc2..c2569a142 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -414,13 +414,13 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function xlate_error "Second order variable not supported" | CEvar _ -> xlate_error "CEvar not supported" | CCoFix (_, (_, id), lm::lmi) -> - let strip_mutcorec (fid, bl,arf, ardef) = + let strip_mutcorec ((_, fid), bl,arf, ardef) = CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, xlate_formula arf, xlate_formula ardef) in CT_cofixc(xlate_ident id, (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))) | CFix (_, (_, id), lm::lmi) -> - let strip_mutrec (fid, (n, ro), bl, arf, ardef) = + let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) = let struct_arg = make_fix_struct (n, bl) in let arf = xlate_formula arf in let ardef = xlate_formula ardef in @@ -1939,7 +1939,7 @@ let rec xlate_vernac = (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi)) | VernacFixpoint ([],_) -> xlate_error "mutual recursive" | VernacFixpoint ((lm :: lmi),boxed) -> - let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) = + let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) = let struct_arg = make_fix_struct (n, bl) in let arf = xlate_formula arf in let ardef = xlate_formula ardef in @@ -1952,7 +1952,7 @@ let rec xlate_vernac = (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi)) | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive" | VernacCoFixpoint ((lm :: lmi),boxed) -> - let strip_mutcorec ((fid, bl, arf, ardef), _ntn) = + let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) = CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, xlate_formula arf, xlate_formula ardef) in CT_cofix_decl @@ -1974,9 +1974,9 @@ let rec xlate_vernac = CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" - | VernacSyntacticDefinition (id, ([],c), false, _) -> + | VernacSyntacticDefinition ((_,id), ([],c), false, _) -> CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None) - | VernacSyntacticDefinition (id, _, _, _) -> + | VernacSyntacticDefinition ((_,id), _, _, _) -> xlate_error"TODO: Local abbreviations and abbreviations with parameters" (* Modules and Module Types *) | VernacInclude (_) -> xlate_error "TODO : Include " diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 06c67e60b..3a4122b83 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -56,7 +56,8 @@ let solve_tccs_in_type env id isevars evm c typ = (** Make all obligations transparent so that real dependencies can be sorted out by the user *) let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in match Subtac_obligations.add_definition stmt_id c' typ obls with - Subtac_obligations.Defined cst -> constant_value (Global.env()) cst + Subtac_obligations.Defined cst -> constant_value (Global.env()) + (match cst with ConstRef kn -> kn | _ -> assert false) | _ -> errorlabstrm "start_proof" (str "The statement obligations could not be resolved automatically, " ++ spc () ++ @@ -105,9 +106,24 @@ let declare_assumption env isevars idl is_coe k bl c nl = errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let vernac_assumption env isevars kind l nl = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l +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_constraint ty ((loc, n), _, _) = + match n with + | Name id -> dump_definition (loc, id) ty + | Anonymous -> () +let dump_variable lid = () + +let vernac_assumption env isevars kind l nl = + let global = fst kind = Global in + List.iter (fun (is_coe,(idl,c)) -> + if !Flags.dump then + List.iter (fun lid -> + if global then dump_definition lid "ax" + else dump_variable lid) idl; + declare_assumption env isevars idl is_coe kind [] c nl) l let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; @@ -118,6 +134,7 @@ let subtac (loc, command) = try match command with VernacDefinition (defkind, (_, id as lid), expr, hook) -> + dump_definition lid "def"; (match expr with | ProveBody (bl, t) -> if Lib.is_modtype () then @@ -126,12 +143,14 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon)) + ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon)) | VernacFixpoint (l, b) -> + List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid "fix") l; let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> + if !Flags.dump then dump_definition id "prf"; if not(Pfedit.refining ()) then if lettop then errorlabstrm "Subtac_command.StartProof" @@ -146,11 +165,12 @@ let subtac (loc, command) = vernac_assumption env isevars stre l nl | VernacInstance (glob, sup, is, props, pri) -> + if !Flags.dump then dump_constraint "inst" is; ignore(Subtac_classes.new_instance ~global:glob sup is props pri) | VernacCoFixpoint (l, b) -> - let _ = trace (str "Building cofixpoint") in - ignore(Subtac_command.build_corecursive l b) + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + ignore(Subtac_command.build_corecursive l b) (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 01f530d19..3ebc3bb5c 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -173,8 +173,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class 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 @@ -198,12 +199,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class (* ExplByPos (i, Some na), (true, true)) *) (* 1 ctx *) (* in *) - let hook cst = + let hook gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in let inst = Typeclasses.new_instance k pri global cst in - Impargs.declare_manual_implicits false (ConstRef cst) false imps; + Impargs.declare_manual_implicits false gr false imps; Typeclasses.add_instance inst in let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in - ignore(Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls); + ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls); id diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 3b4067ce8..5bff6ad1a 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -58,10 +58,9 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in -(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' - + let interp_constr isevars env c = interp_gen (OfType None) isevars env c @@ -276,11 +275,6 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* str "Intern body " ++ pr intern_body_lam) *) with _ -> () in - let _impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits top_env top_arity - else [] - in let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in (* Lift to get to constant arguments *) let lift_cst = List.length after + 1 in @@ -309,7 +303,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in let evm = non_instanciated_map env isevars evm in let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in - Subtac_obligations.add_definition recname evars_def evars_typ evars + Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> @@ -436,14 +430,14 @@ let out_n = function let build_recursive l b = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - [(n, CWfRec r)], [((id,_,bl,typ,def),ntn)] -> + [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false) - | [(n, CMeasureRec r)], [((id,_,bl,typ,def),ntn)] -> + | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] -> ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false) | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> - let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive (Command.IsFixpoint g) fixl b | _, _ -> @@ -451,7 +445,7 @@ let build_recursive l b = (str "Well-founded fixpoints not allowed in mutually recursive blocks") 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) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive Command.IsCoFixpoint fixl b diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 1e6a55a0e..cdfb40b26 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -12,8 +12,9 @@ open Entries open Decl_kinds open Util open Evd +open Declare -type definition_hook = constant -> unit +type definition_hook = global_reference -> unit let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -48,7 +49,7 @@ type program_info = { prg_fixkind : Command.fixpoint_kind option ; prg_implicits : (Topconstr.explicitation * (bool * bool)) list; prg_notations : notations ; - prg_kind : definition_object_kind; + prg_kind : definition_kind; prg_hook : definition_hook; } @@ -161,21 +162,36 @@ let declare_definition prg = my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); with _ -> ()); + let (local, boxed, kind) = prg.prg_kind in let ce = { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = false; - const_entry_boxed = false} - in - let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition prg.prg_kind) + const_entry_boxed = boxed} in - let gr = ConstRef c in - if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; - print_message (Subtac_utils.definition_message c); - prg.prg_hook c; - c + (Command.get_declare_definition_hook ()) ce; + match local with + | Local when Lib.sections_are_opened () -> + let c = + SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in + let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in + print_message (Subtac_utils.definition_message prg.prg_name); + if Pfedit.refining () then + Flags.if_verbose msg_warning + (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ + str" is not visible from current goals"); + VarRef prg.prg_name + | (Global|Local) -> + let c = + Declare.declare_constant + prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) + in + let gr = ConstRef c in + if Impargs.is_implicit_args () || prg.prg_implicits <> [] then + Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; + print_message (Subtac_utils.definition_message prg.prg_name); + prg.prg_hook gr; + gr open Pp open Ppconstr @@ -241,7 +257,7 @@ let declare_obligation obl body = let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) in - print_message (Subtac_utils.definition_message constant); + print_message (Subtac_utils.definition_message obl.obl_name); { obl with obl_body = Some (mkConst constant) } let try_tactics obls = @@ -298,7 +314,7 @@ let update_state s = type progress = | Remain of int | Dependent - | Defined of constant + | Defined of global_reference let obligations_message rem = if rem > 0 then @@ -328,7 +344,7 @@ let update_obls prg obls rem = from_prg := List.fold_left (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs; - Defined kn) + Defined (ConstRef kn)) else Dependent); in update_state (!from_prg, !default_tactic_expr); @@ -473,7 +489,7 @@ let show_term n = msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls = +let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] None [] obls implicits kind hook in let obls,_ = prg.prg_obligations in @@ -491,7 +507,7 @@ let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?(kind=Definition) notations fixkind = +let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left (fun acc (n, b, t, imps, obls) -> diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 997c2479d..6d13e3bd3 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,5 +1,6 @@ open Names open Util +open Libnames type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array (* ident, type, location, opaque or transparent, dependencies *) @@ -7,7 +8,7 @@ type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) a type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) - | Defined of constant (* Defined as id *) + | Defined of global_reference (* Defined as id *) val set_default_tactic : Tacexpr.glob_tactic_expr -> unit val default_tactic : unit -> Proof_type.tactic @@ -15,11 +16,11 @@ val default_tactic : unit -> Proof_type.tactic val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) val get_proofs_transparency : unit -> bool -type definition_hook = constant -> unit +type definition_hook = global_reference -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> - ?kind:Decl_kinds.definition_object_kind -> + ?kind:Decl_kinds.definition_kind -> ?hook:definition_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -27,7 +28,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> - ?kind:Decl_kinds.definition_object_kind -> + ?kind:Decl_kinds.definition_kind -> notations -> Command.fixpoint_kind -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index ec5af37fe..2118dfbdd 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -136,8 +136,8 @@ let subtac_process env isevars id bl c tycon = open Subtac_obligations -let subtac_proof env isevars id bl c tycon = +let subtac_proof kind env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in - add_definition id def ty ~implicits:imps evars + add_definition id def ty ~implicits:imps ~kind:kind evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli index 4af37043f..1d8eb2507 100644 --- a/contrib/subtac/subtac_pretyping.mli +++ b/contrib/subtac/subtac_pretyping.mli @@ -19,5 +19,5 @@ val interp : val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list -val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list -> +val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 4af18f52d..bae2731aa 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -350,7 +350,7 @@ let id_of_name = function | Anonymous -> raise (Invalid_argument "id_of_name") let definition_message id = - Printer.pr_constant (Global.env ()) id ++ str " is defined" + Nameops.pr_id id ++ str " is defined" let recursive_message v = match Array.length v with diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 1bd5bb970..493352114 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -115,7 +115,7 @@ val destruct_ex : constr -> constr -> constr list val id_of_name : name -> identifier -val definition_message : constant -> std_ppcmds +val definition_message : identifier -> std_ppcmds val recursive_message : constant array -> std_ppcmds val print_message : std_ppcmds -> unit diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 7e3a1bd41..3c4b01f5b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -487,7 +487,10 @@ let kind_of_constant kn = | DK.IsDefinition DK.Instance -> Pp.warning "Instance not supported in dtd (used Definition instead)"; "DEFINITION","Definition" - | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> + | DK.IsDefinition DK.Method -> + Pp.warning "Method not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> Pp.warning "Unsupported theorem kind (used Theorem instead)"; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dedaf6af4..c922503aa 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -726,7 +726,7 @@ let rec extern inctx scopes vars r = | Some x -> Some (dummy_loc, out_name (List.nth ids x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - (fi, (n, ro), bl, extern_typ scopes vars0 ty, + ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) @@ -736,7 +736,7 @@ let rec extern inctx scopes vars r = let (ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in - (fi,bl,extern_typ scopes vars0 tyv.(i), + ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 65efc1f67..283dc269d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -44,8 +44,6 @@ let for_grammar f x = interning_grammar := false; a -let variables_bind = ref false - (**********************************************************************) (* Internalisation errors *) @@ -144,6 +142,56 @@ let coqdoc_unfreeze (lt,tn,lp) = token_number := tn; last_pos := lp +open Decl_kinds + +let type_of_logical_kind = function + | IsDefinition def -> + (match def with + | Definition -> "def" + | Coercion -> "coe" + | SubClass -> "subclass" + | CanonicalStructure -> "canonstruc" + | Example -> "ex" + | Fixpoint -> "def" + | CoFixpoint -> "def" + | Scheme -> "scheme" + | StructureComponent -> "proj" + | IdentityCoercion -> "coe" + | Instance -> "inst" + | Method -> "meth") + | IsAssumption a -> + (match a with + | Definitional -> "def" + | Logical -> "prf" + | Conjectural -> "prf") + | IsProof th -> + (match th with + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -> "thm") + +let type_of_global_ref gr = + if Typeclasses.is_class gr then + "class" + else + match gr with + | ConstRef cst -> + type_of_logical_kind (Decls.constant_kind cst) + | VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | IndRef ind -> + let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in + if mib.Declarations.mind_record then + if mib.Declarations.mind_finite then "rec" + else "corec" + else if mib.Declarations.mind_finite then "ind" + else "coind" + | ConstructRef _ -> "constr" + let add_glob loc ref = let sp = Nametab.sp_of_global ref in let lib_dp = Lib.library_part ref in @@ -151,8 +199,25 @@ let add_glob loc ref = let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in let filepath = string_of_dirpath lib_dp in let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in - dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) + let ty = type_of_global_ref ref in + dump_string (Printf.sprintf "R%d %s %s %s\n" + (fst (unloc loc)) filepath fullname ty) + +let add_glob loc ref = + if !Flags.dump && loc <> dummy_loc then add_glob loc ref +let add_glob_kn loc kn = + let sp = Nametab.sp_of_syntactic_definition kn in + let dp, id = repr_path sp in + let fullname = string_of_id id in + let filepath = string_of_dirpath dp in + dump_string (Printf.sprintf "R%d %s %s syndef\n" (fst (unloc loc)) filepath fullname) + +let add_glob_kn loc ref = + if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref + +let dump_binding loc id = () + let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) else snd (unloc (f (List.hd args))) @@ -171,8 +236,8 @@ let dump_notation_location pos ((path,df),sc) = let loc = next (pos >= !last_pos) in last_pos := pos; let path = string_of_dirpath path in - let sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) + let _sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -383,9 +448,10 @@ let check_no_explicitation l = let intern_qualid loc qid intern env args = try match Nametab.extended_locate qid with | TrueGlobal ref -> - if !dump then add_glob loc ref; + add_glob loc ref; RRef (loc, ref), args | SyntacticDef sp -> + add_glob_kn loc sp; let (ids,c) = Syntax_def.search_syntactic_definition loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; @@ -615,7 +681,7 @@ let find_constructor ref f aliases pats scopes = let v = Environ.constant_value (Global.env()) cst in unf (global_of_constr v) | ConstructRef cstr -> - if !dump then add_glob loc r; + add_glob loc r; cstr, [], pats | _ -> raise Not_found in unf r @@ -731,20 +797,28 @@ let push_name_env lvar (ids,tmpsc,scopes as env) = function check_hidden_implicit_parameters id lvar; (Idset.add id ids,tmpsc,scopes) -let intern_typeclass_binders intern_type env bl = +let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function + | Anonymous -> env + | Name id -> + check_hidden_implicit_parameters id lvar; + dump_binding loc id; + (Idset.add id ids,tmpsc,scopes) + +let intern_typeclass_binders intern_type lvar env bl = List.fold_left (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) -> + let env = push_loc_name_env lvar env loc na in let ty = locate_if_isevar loc na (intern_type env ty) in - ((name_fold Idset.add na ids,ts,sc), (na,bk,None,ty)::bl)) + (env, (na,bk,None,ty)::bl)) env bl -let intern_typeclass_binder intern_type (env,bl) na b ty = +let intern_typeclass_binder intern_type lvar (env,bl) na b ty = let ctx = (na, b, ty) in let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in - let env, ifvs = intern_typeclass_binders intern_type (env,bl) fvs in - intern_typeclass_binders intern_type (env,ifvs) bind + let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in + intern_typeclass_binders intern_type lvar (env,ifvs) bind -let intern_local_binder_aux intern intern_type ((ids,ts,sc as env),bl) = function +let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function | LocalRawAssum(nal,bk,ty) -> (match bk with | Default k -> @@ -756,7 +830,7 @@ let intern_local_binder_aux intern intern_type ((ids,ts,sc as env),bl) = functio ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl)) (env,bl) nal | TypeClass b -> - intern_typeclass_binder intern_type (env,bl) (List.hd nal) b ty) + intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty) | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,ts,sc), (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) @@ -840,7 +914,7 @@ let internalise sigma globalenv env allow_patvar lvar c = | [] -> c | l -> RApp (constr_loc x, c, l)) | CFix (loc, (locid,iddef), dl) -> - let lf = List.map (fun (id,_,_,_,_) -> id) dl in + let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = try list_index0 iddef lf @@ -886,7 +960,7 @@ let internalise sigma globalenv env allow_patvar lvar c = Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) | CCoFix (loc, (locid,iddef), dl) -> - let lf = List.map (fun (id,_,_,_) -> id) dl in + let lf = List.map (fun ((_, id),_,_,_) -> id) dl in let dl = Array.of_list dl in let n = try list_index0 iddef lf @@ -916,9 +990,9 @@ let internalise sigma globalenv env allow_patvar lvar c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,(_,na),c1,c2) -> + | CLetIn (loc,(loc1,na),c1,c2) -> RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_name_env lvar env na) c2) + intern (push_loc_name_env lvar env loc1 na) c2) | CNotation (loc,"- _",[CPrim (_,Numeral p)]) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) @@ -999,7 +1073,7 @@ let internalise sigma globalenv env allow_patvar lvar c = and intern_type env = intern (set_type_scope env) and intern_local_binder env bind = - intern_local_binder_aux intern intern_type env bind + intern_local_binder_aux intern intern_type lvar env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern scopes n (loc,pl) = @@ -1064,7 +1138,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let rec default env bk = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_name_env lvar env na) bk nal in + let body = default (push_loc_name_env lvar env loc1 na) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body @@ -1072,7 +1146,8 @@ let internalise sigma globalenv env allow_patvar lvar c = match bk with | Default b -> default env b nal | TypeClass b -> - let env, ibind = intern_typeclass_binder intern_type (env, []) (List.hd nal) b ty in + let env, ibind = intern_typeclass_binder intern_type lvar + (env, []) (List.hd nal) b ty in let body = intern_type env body in it_mkRProd ibind body @@ -1080,14 +1155,15 @@ let internalise sigma globalenv env allow_patvar lvar c = let rec default env bk = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_name_env lvar env na) bk nal in + let body = default (push_loc_name_env lvar env loc1 na) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body in match bk with | Default b -> default env b nal - | TypeClass b -> - let env, ibind = intern_typeclass_binder intern_type (env, []) (List.hd nal) b ty in + | TypeClass b -> + let env, ibind = intern_typeclass_binder intern_type lvar + (env, []) (List.hd nal) b ty in let body = intern env body in it_mkRLambda ibind body @@ -1151,9 +1227,9 @@ let intern_gen isarity sigma env c = let tmp_scope = if isarity then Some Notation.type_scope else None in - internalise sigma env (extract_ids env, tmp_scope,[]) - allow_patvar (ltacvars,Environ.named_context env, [], impls) c - + internalise sigma env (extract_ids env, tmp_scope,[]) + allow_patvar (ltacvars,Environ.named_context env, [], impls) c + let intern_constr sigma env c = intern_gen false sigma env c let intern_type sigma env c = intern_gen true sigma env c @@ -1282,15 +1358,16 @@ let interp_binder_evars evdref env na t = open Environ open Term -let my_intern_constr sigma env acc c = - internalise sigma env acc false (([],[]),Environ.named_context env, [], ([], [])) c +let my_intern_constr sigma env lvar acc c = + internalise sigma env acc false lvar c -let my_intern_type sigma env acc c = my_intern_constr sigma env (set_type_scope acc) c +let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c let intern_context sigma env params = - snd (List.fold_left - (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env)) - ((extract_ids env,None,[]), []) params) + let lvar = (([],[]),Environ.named_context env, [], ([], [])) in + snd (List.fold_left + (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) + ((extract_ids env,None,[]), []) params) let interp_context_gen understand_type understand_judgment env bl = let (env, par, _, impls) = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index fb69460c4..d3b8da8f9 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -149,3 +149,5 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b type coqdoc_state val coqdoc_freeze : unit -> coqdoc_state val coqdoc_unfreeze : coqdoc_state -> unit + +val add_glob : Util.loc -> global_reference -> unit diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 35b8f075a..cef1b9391 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -634,7 +634,7 @@ type constr_expr = | CDynamic of loc * Dyn.t and fixpoint_expr = - identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr + identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr and local_binder = | LocalRawDef of name located * constr_expr @@ -645,7 +645,7 @@ and typeclass_constraint = name located * binding_kind * constr_expr and typeclass_context = typeclass_constraint list and cofixpoint_expr = - identifier * local_binder list * constr_expr * constr_expr + identifier located * local_binder list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -794,7 +794,7 @@ let fold_constr_expr_with_binders g f n acc = function let acc = f n (f n (f n acc b1) b2) c in Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po | CFix (loc,_,l) -> - let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in + let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc @@ -909,14 +909,14 @@ let map_constr_expr_with_binders g f e = function let (e',bl') = map_local_binders f g e bl in let t' = f e' t in (* Note: fix names should be inserted before the arguments... *) - let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in + let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,n,bl',t',d')) dl) | CCoFix (loc,id,dl) -> CCoFix (loc,id,List.map (fun (id,bl,t,d) -> let (e',bl') = map_local_binders f g e bl in let t' = f e' t in - let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in + let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 155ac9ca8..6790e400f 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -139,10 +139,10 @@ type constr_expr = | CDynamic of loc * Dyn.t and fixpoint_expr = - identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr + identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr and cofixpoint_expr = - identifier * local_binder list * constr_expr * constr_expr + identifier located * local_binder list * constr_expr * constr_expr and recursion_order_expr = | CStructRec diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 20808f1e6..735a8fb07 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -40,6 +40,7 @@ type definition_object_kind = | StructureComponent | IdentityCoercion | Instance + | Method type assumption_object_kind = Definitional | Logical | Conjectural @@ -97,7 +98,9 @@ let string_of_definition_kind (l,boxed,d) = | Global, Example -> "Example" | Local, (CanonicalStructure|Example) -> anomaly "Unsupported local definition kind" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Instance) + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> anomaly "Internal definition kind" (* Strength *) diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 2ee454442..7aa1df0c9 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -40,6 +40,7 @@ type definition_object_kind = | StructureComponent | IdentityCoercion | Instance + | Method type assumption_object_kind = Definitional | Logical | Conjectural diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3b32cfd47..6b6b4871c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in - (snd id,(n,ro),bl,ty,body) + (id,(n,ro),bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> @@ -65,7 +65,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in - (snd id,bl,ty,body) + (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = if kw then diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 437ef58fd..33826c9f1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -258,7 +258,7 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident; + [ [ id = identref; bl = binders_let_fixannot; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> @@ -282,7 +282,7 @@ GEXTEND Gram ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = ident; bl = binders_let; ty = type_cstr; ":="; + [ [ id = identref; bl = binders_let; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -808,7 +808,7 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (local,(op,modl),p,sc) - | IDENT "Notation"; local = locality; id = ident; idl = LIST0 ident; + | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> VernacSyntacticDefinition (id,(idl,c),local,b) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 44aabc2cb..0f0c38adc 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -393,7 +393,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c -let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = +let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) = let annot = match ro with CStructRec -> @@ -407,7 +407,7 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = in pr_recursive_decl pr prd dangling_with_for id bl annot t c -let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) = +let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c31defe09..c4b5c2d3e 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -584,7 +584,7 @@ let rec pr_vernac = function | LocalRawAssum (nal,_,_) -> nal | LocalRawDef (_,_) -> [] in let pr_onerec = function - | (id,(n,ro),bl,type_,def),ntn -> + | ((loc,id),(n,ro),bl,type_,def),ntn -> let (bl',def,type_) = if Flags.do_translate() then extract_def_binders def type_ else ([],def,type_) in @@ -616,7 +616,7 @@ let rec pr_vernac = function prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) | VernacCoFixpoint (corecs,b) -> - let pr_onecorec ((id,bl,c,def),ntn) = + let pr_onecorec (((loc,id),bl,c,def),ntn) = let (bl',def,c) = if Flags.do_translate() then extract_def_binders def c else ([],def,c) in @@ -815,7 +815,7 @@ let rec pr_vernac = function pr_hints local dbnames h pr_constr pr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> hov 2 - (str"Notation " ++ pr_locality local ++ pr_id id ++ + (str"Notation " ++ pr_locality local ++ pr_lident id ++ prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (local,q,None) -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a1b07cb9f..ee385430c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -42,7 +42,7 @@ type typeclass = { cl_props : named_context; (* The method implementaions as projections. *) - cl_projs : constant list; + cl_projs : (identifier * constant) list; } type typeclasses = (global_reference, typeclass) Gmap.t @@ -144,7 +144,7 @@ let subst (_,subst,(cl,m,inst)) = (na, Option.smartmap do_subst b, do_subst t))) ctx in - let do_subst_projs projs = list_smartmap do_subst_con projs in + let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in let subst_class k cl classes = let k = do_subst_gr k in let cl' = { cl with cl_impl = k; @@ -175,7 +175,7 @@ let discharge (_,(cl,m,inst)) = let subst_class cl = { cl with cl_impl = Lib.discharge_global cl.cl_impl; cl_context = list_smartmap discharge_named cl.cl_context; - cl_projs = list_smartmap Lib.discharge_con cl.cl_projs } + cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs } in let classes = Gmap.map subst_class cl in let subst_inst insts = @@ -219,7 +219,7 @@ let update () = let add_class c = classes := Gmap.add c.cl_impl c !classes; - methods := List.fold_left (fun acc x -> Gmap.add x c.cl_impl acc) !methods c.cl_projs; + methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs; update () let class_info c = @@ -306,6 +306,20 @@ let method_typeclass ref = let is_class gr = Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false +let is_method c = + Gmap.mem c !methods + +let is_instance = function + | ConstRef c -> + (match Decls.constant_kind c with + | IsDefinition Instance -> true + | _ -> false) + | VarRef v -> + (match Decls.variable_kind v with + | IsDefinition Instance -> true + | _ -> false) + | _ -> false + let is_implicit_arg k = match k with ImplicitArg (ref, (n, id)) -> true diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 43ae592d5..e3c780402 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -38,7 +38,7 @@ type typeclass = { cl_props : named_context; (* The methods implementations of the typeclass as projections. *) - cl_projs : constant list; + cl_projs : (identifier * constant) list; } type instance @@ -60,6 +60,9 @@ val is_class : global_reference -> bool val class_of_constr : constr -> typeclass option val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *) +val is_instance : global_reference -> bool +val is_method : constant -> bool + (* Returns the term and type for the given instance of the parameters and fields of the type class. *) val instance_constructor : typeclass -> constr list -> constr * types diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 5bd8f9f6f..38fd3ab63 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -434,7 +434,7 @@ END (** Typeclass-based rewriting. *) -let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs)) +let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_projs))) let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 2c07b9fc8..d8cc33336 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -8,20 +8,20 @@ \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{coqdoc}[2002/02/11] -% Headings -\usepackage{fancyhdr} -\newcommand{\coqdocleftpageheader}{\thepage\ -- \today} -\newcommand{\coqdocrightpageheader}{\today\ -- \thepage} -\pagestyle{fancyplain} +% % Headings +% \usepackage{fancyhdr} +% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today} +% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage} +% \pagestyle{fancyplain} -%BEGIN LATEX -\headsep 8mm -\renewcommand{\plainheadrulewidth}{0.4pt} -\renewcommand{\plainfootrulewidth}{0pt} -\lhead[\coqdocleftpageheader]{\leftmark} -\rhead[\leftmark]{\coqdocrightpageheader} -\cfoot{} -%END LATEX +% %BEGIN LATEX +% \headsep 8mm +% \renewcommand{\plainheadrulewidth}{0.4pt} +% \renewcommand{\plainfootrulewidth}{0pt} +% \lhead[\coqdocleftpageheader]{\leftmark} +% \rhead[\leftmark]{\coqdocrightpageheader} +% \cfoot{} +% %END LATEX % Hevea puts to much space with \medskip and \bigskip %HEVEA\renewcommand{\medskip}{} @@ -36,11 +36,20 @@ %END LATEX % macro for typesetting keywords -\newcommand{\coqdockw}[1]{\textsf{#1}} +\newcommand{\coqdockw}[1]{\texttt{#1}} -% macro for typesetting identifiers +% macro for typesetting variable identifiers \newcommand{\coqdocid}[1]{\textit{#1}} +% macro for typesetting constant identifiers +\newcommand{\coqdoccst}[1]{\textsf{#1}} + +% macro for typesetting inductive type identifiers +\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}} + +% macro for typesetting constructor identifiers +\newcommand{\coqdocconstr}[1]{\textsf{#1}} + % newline and indentation %BEGIN LATEX \newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} @@ -53,6 +62,52 @@ \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } +\usepackage{hyperref} +%\usepackage{color} +%\hypersetup{colorlinks=true,linkcolor=black} +%\usepackage{multind} +%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} + +\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}} +\newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}} + +\newcommand{\coqdocvar}[1]{{\textit{#1}}} +\newcommand{\coqdoctac}[1]{{\texttt{#1}}} + +\newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}} + +\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} + +\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}} +\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}} + +\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + %HEVEA\newcommand{\lnot}{\coqwkw{not}} %HEVEA\newcommand{\lor}{\coqwkw{or}} %HEVEA\newcommand{\land}{\&} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 1af394570..9f0c3d24a 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -19,13 +19,22 @@ type entry_type = | Inductive | Constructor | Lemma + | Record + | Projection + | Instance + | Class + | Method | Variable | Axiom | TacticDefinition + | Abbreviation + | Notation + +val type_name : entry_type -> string type index_entry = | Def of string * entry_type - | Ref of coq_module * string + | Ref of coq_module * string * entry_type | Mod of coq_module * string val find : coq_module -> loc -> index_entry @@ -42,7 +51,7 @@ val scan_file : string -> coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> unit +val read_glob : string -> coq_module (*s Indexes *) diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 9bb7bd400..fa619a943 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -25,13 +26,20 @@ type entry_type = | Inductive | Constructor | Lemma + | Record + | Projection + | Instance + | Class + | Method | Variable | Axiom | TacticDefinition + | Abbreviation + | Notation type index_entry = | Def of string * entry_type - | Ref of coq_module * string + | Ref of coq_module * string * entry_type | Mod of coq_module * string let current_type = ref Library @@ -43,13 +51,13 @@ let table = Hashtbl.create 97 let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty)) -let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id)) +let add_ref m loc m' id ty = + Hashtbl.add table (m, loc) (Ref (m', id, ty)) let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id)) let find m l = Hashtbl.find table (m, l) - (*s Manipulating path prefixes *) type stack = string list @@ -173,9 +181,16 @@ let type_name = function | Inductive -> "inductive" | Constructor -> "constructor" | Lemma -> "lemma" + | Record -> "record" + | Projection -> "projection" + | Instance -> "instance" + | Class -> "class" + | Method -> "method" | Variable -> "variable" | Axiom -> "axiom" | TacticDefinition -> "tactic" + | Abbreviation -> "abbreviation" + | Notation -> "notation" let all_entries () = let gl = ref [] in @@ -390,7 +405,26 @@ and module_refs = parse { () } { - + let type_of_string = function + | "def" | "coe" | "subclass" | "canonstruc" + | "ex" | "scheme" -> Definition + | "prf" | "thm" -> Lemma + | "ind" | "coind" -> Inductive + | "constr" -> Constructor + | "rec" | "corec" -> Record + | "proj" -> Projection + | "class" -> Class + | "meth" -> Method + | "inst" -> Instance + | "var" -> Variable + | "ax" -> Axiom + | "syndef" -> Abbreviation + | "not" -> Notation + | s -> raise (Invalid_argument ("type_of_string:" ^ s)) +(* | Library *) +(* | Module *) +(* | TacticDefinition *) + let read_glob f = let c = open_in f in let cur_mod = ref "" in @@ -401,22 +435,22 @@ and module_refs = parse if n > 0 then begin match s.[0] with | 'F' -> - cur_mod := String.sub s 1 (n - 1) + cur_mod := String.sub s 1 (n - 1); + current_library := !cur_mod | 'R' -> (try - let i = String.index s ' ' in - let j = String.index_from s (i+1) ' ' in - let loc = int_of_string (String.sub s 1 (i - 1)) in - let lib_dp = String.sub s (i + 1) (j - i - 1) in - let full_id = String.sub s (j + 1) (n - j - 1) in - add_ref !cur_mod loc lib_dp full_id - with Not_found -> - ()) - | _ -> () + Scanf.sscanf s "R%d %s %s %s" + (fun loc lib_dp full_id ty -> + add_ref !cur_mod loc lib_dp full_id (type_of_string ty)) + with _ -> ()) + | _ -> + try Scanf.sscanf s "%s %d %s" + (fun ty loc id -> add_def loc (type_of_string ty) id) + with Scanf.Scan_failure _ -> () end - done + done; assert false with End_of_file -> - close_in c + close_in c; !cur_mod let scan_file f m = init_stack (); current_library := m; diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 469db5367..7466a6ba1 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -408,14 +409,16 @@ let gen_mult_files l = end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) -let read_glob = function - | Vernac_file (f,m) -> - let glob = (Filename.chop_extension f) ^ ".glob" in - (try - Index.read_glob glob - with - _ -> eprintf "Warning: file %s cannot be opened; links will not be available\n" glob) - | Latex_file _ -> () +let read_glob x = + match x with + | Vernac_file (f,m) -> + let glob = (Filename.chop_extension f) ^ ".glob" in + (try + Vernac_file (f, Index.read_glob glob) + with _ -> + eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + x) + | Latex_file _ -> x let index_module = function | Vernac_file (f,m) -> @@ -426,14 +429,14 @@ let produce_document l = (if !target_language=HTML then let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in - copy src dst; - List.iter read_glob l); + copy src dst); (if !target_language=LaTeX then let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.sty" else "coqdoc.sty" in copy src dst); + let l = List.map read_glob l in List.iter index_module l; match !out_to with | StdOut -> diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index fd8768fdf..251fb2357 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -46,7 +47,7 @@ let is_keyword = "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Arguments"; - "Instance"; "Class"; "where"; "Instantiation"; + "Instance"; "Class"; "Instantiation"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; @@ -59,6 +60,15 @@ let is_keyword = "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=" ] +let is_tactic = + build_table + [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite"; + "destruct"; "induction"; "elim"; "dependent"; + "generalize"; "clear"; "rename"; "move"; "set"; "assert"; + "cut"; "assumption"; "exact"; + "unfold"; "red"; "compute"; "at"; "in"; "by"; + "reflexivity"; "symmetry"; "transitivity" ] + (*s Current Coq module *) let current_module = ref "" @@ -159,6 +169,12 @@ module Latex = struct | _ -> output_char c + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + let latex_char = output_char let latex_string = output_string @@ -168,6 +184,9 @@ module Latex = struct let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + let label_ident s = + for i = 0 to String.length s - 1 do label_char s.[i] done + let start_module () = if not !short then begin printf "\\coqdocmodule{"; @@ -198,11 +217,52 @@ module Latex = struct with Not_found -> f tok - let ident s _ = + let module_ref m s = + printf "\\moduleid{%s}{" m; raw_ident s; printf "}" + (*i + match find_module m with + | Local -> + printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" + | Coqlib | Unknown -> + raw_ident s + i*) + + let ident_ref m fid typ s = + match find_module m with + | Local -> + printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}" + | Coqlib when !externals -> + let _m = Filename.concat !coqlib m in + printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}" + | Coqlib | Unknown -> + raw_ident s + + let defref m id ty s = + printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" + end else if is_tactic s then begin + printf "\\coqdoctac{"; raw_ident s; printf "}" end else begin - printf "\\coqdocid{"; raw_ident s; printf "}" + begin + try + (match Index.find !current_module loc with + | Def (fullid,typ) -> + defref !current_module fullid typ s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid,typ) -> + ident_ref m fullid typ s + | Mod _ -> + printf "\\coqdocid{"; raw_ident s; printf "}") + with Not_found -> + printf "\\coqdocvar{"; raw_ident s; printf "}" + end end let ident s l = with_latex_printing (fun s -> ident s l) s @@ -387,7 +447,7 @@ module Html = struct printf "<a name=\"%s\"></a>" fullid; raw_ident s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid) -> + | Ref (m,fullid,ty) -> ident_ref m fullid s | Mod _ -> raw_ident s) @@ -456,17 +516,6 @@ module Html = struct let rule () = printf "<hr/>\n" - let entry_type = function - | Library -> "library" - | Module -> "module" - | Definition -> "definition" - | Inductive -> "inductive" - | Constructor -> "constructor" - | Lemma -> "lemma" - | Variable -> "variable" - | Axiom -> "axiom" - | TacticDefinition -> "tactic definition" - (* make a HTML index from a list of triples (name,text,link) *) let index_ref i c = let idxc = sprintf "%s_%c" i.idx_name c in @@ -492,7 +541,7 @@ module Html = struct if t = Library then "[library]", m ^ ".html" else - sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m , + sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m , sprintf "%s.html#%s" m s) let format_bytype_index = function diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 8774d9d2e..2e0f46795 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -173,6 +173,7 @@ let firstchar = (* utf-8 latin 1 supplement *) '\195' ['\128'-'\191'] | (* utf-8 letterlike symbols *) + '\206' ['\177'-'\183'] | '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) let identchar = firstchar | ['\'' '0'-'9' '@' ] @@ -188,6 +189,7 @@ let symbolchar_no_brackets = (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ let symbolchar = symbolchar_no_brackets | '[' | ']' +let token_no_brackets = symbolchar_no_brackets+ let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' let printing_token = (token | id)+ @@ -608,7 +610,7 @@ and body = parse | eof { false } | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true } | '.' space+ { Output.char '.'; Output.char ' '; false } - | '"' { Output.char '"'; notation lexbuf; body lexbuf } + | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf } | "(*" { let eol = comment lexbuf in if eol then begin Output.line_break(); body_bol lexbuf end @@ -617,7 +619,7 @@ and body = parse { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); body lexbuf } - | printing_token + | token_no_brackets { let s = lexeme lexbuf in Output.symbol s; body lexbuf } | _ { let c = lexeme_char lexbuf 0 in @@ -659,7 +661,6 @@ and printing_token_body = parse let coq_file f m = reset (); - Index.scan_file f m; Output.start_module (); let c = open_in f in let lb = from_channel c in 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 |