From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- plugins/cc/ccproof.mli | 1 - plugins/cc/cctac.ml | 20 +- plugins/decl_mode/decl_expr.mli | 32 +- plugins/decl_mode/decl_mode.ml | 26 +- plugins/decl_mode/decl_mode.mli | 4 +- plugins/decl_mode/decl_proof_instr.ml | 39 +- plugins/decl_mode/g_decl_mode.ml4 | 57 ++- plugins/decl_mode/ppdecl_proof.ml | 169 ++++---- plugins/decl_mode/ppdecl_proof.mli | 14 +- plugins/derive/derive.ml | 4 +- plugins/extraction/ExtrHaskellBasic.v | 15 + plugins/extraction/ExtrOcamlNatInt.v | 1 + plugins/extraction/common.ml | 3 +- plugins/extraction/extract_env.ml | 6 +- plugins/extraction/extraction_plugin.mllib | 1 + plugins/extraction/g_extraction.ml4 | 2 + plugins/extraction/haskell.ml | 36 +- plugins/extraction/json.ml | 278 +++++++++++++ plugins/extraction/json.mli | 1 + plugins/extraction/miniml.mli | 1 + plugins/extraction/ocaml.ml | 15 +- plugins/extraction/scheme.ml | 3 +- plugins/extraction/table.ml | 2 +- plugins/extraction/table.mli | 2 +- plugins/extraction/vo.itarget | 1 + plugins/firstorder/formula.mli | 1 - plugins/firstorder/instances.ml | 32 +- plugins/firstorder/sequent.ml | 2 +- plugins/fourier/fourierR.ml | 1 - plugins/funind/functional_principles_proofs.ml | 123 +++--- plugins/funind/functional_principles_proofs.mli | 1 + plugins/funind/functional_principles_types.ml | 143 +++---- plugins/funind/functional_principles_types.mli | 6 +- plugins/funind/g_indfun.ml4 | 6 +- plugins/funind/glob_term_to_relation.ml | 54 ++- plugins/funind/glob_term_to_relation.mli | 7 +- plugins/funind/indfun.ml | 221 ++++++---- plugins/funind/indfun_common.ml | 6 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/invfun.ml | 517 ++++++------------------ plugins/funind/recdef.ml | 118 +++--- plugins/micromega/MExtraction.v | 2 +- plugins/omega/Omega.v | 8 +- plugins/omega/OmegaPlugin.v | 6 + plugins/omega/OmegaTactic.v | 15 + plugins/omega/vo.itarget | 1 + plugins/quote/quote.ml | 4 +- 47 files changed, 1132 insertions(+), 877 deletions(-) create mode 100644 plugins/extraction/ExtrHaskellBasic.v create mode 100644 plugins/extraction/json.ml create mode 100644 plugins/extraction/json.mli create mode 100644 plugins/omega/OmegaTactic.v (limited to 'plugins') diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 0e0eb6d2..2ff2bd38 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,6 @@ (************************************************************************) open Ccalgo -open Names open Term type rule= diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7110e5b2..8884aef1 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,7 +23,7 @@ open Pp open Errors open Util -let reference dir s = Coqlib.gen_reference "CC" dir s +let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) let _f_equal = reference ["Init";"Logic"] "f_equal" let _eq_rect = reference ["Init";"Logic"] "eq_rect" @@ -91,7 +91,7 @@ let atom_of_constr env sigma term = let kot = kind_of_term wh in match kot with App (f,args)-> - if is_global _eq f && Int.equal (Array.length args) 3 + if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -126,7 +126,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp (whd_delta env term) with DestKO -> raise Not_found in - if is_global _eq f && Int.equal (Array.length args) 3 + if is_global (Lazy.force _eq) f && Int.equal (Array.length args) 3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) and patt2,rels2 = pattern_of_constr env sigma args.(2) in @@ -147,7 +147,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with Prod (id,atom,ff) -> - if is_global _False ff then + if is_global (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -159,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with | Prod (id,atom,ff) -> - if is_global _False ff then + if is_global (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -246,10 +246,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls= let _M =mkMeta let app_global f args k = - Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) let new_app_global f args k = - Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) let new_refine c = Proofview.V82.tactic (refine c) @@ -375,9 +375,9 @@ let discriminate_tac (cstr,u as cstru) p = let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) - let identity = Universes.constr_of_global _I in + let identity = Universes.constr_of_global (Lazy.force _I) in (* let trivial=pf_type_of gls identity in *) - let trivial = Universes.constr_of_global _True in + let trivial = Universes.constr_of_global (Lazy.force _True) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in @@ -493,7 +493,7 @@ let f_equal = in Proofview.tclORELSE begin match kind_of_term concl with - | App (r,[|_;t;t'|]) when Globnames.is_global _eq r -> + | App (r,[|_;t;t'|]) when Globnames.is_global (Lazy.force _eq) r -> begin match kind_of_term t, kind_of_term t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 7467604a..3c4cacbc 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -46,23 +46,23 @@ type ('constr,'tac) casee = Real of 'constr | Virtual of ('constr statement,'constr,'tac) cut -type ('hyp,'constr,'pat,'tac) bare_proof_instr = - | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr - | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr +type ('var,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr + | Phence of ('var,'constr,'pat,'tac) bare_proof_instr | Pcut of ('constr or_thesis statement,'constr,'tac) cut | Prew of side * ('constr statement,'constr,'tac) cut - | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut - | Passume of ('hyp,'constr) hyp list - | Plet of ('hyp,'constr) hyp list - | Pgiven of ('hyp,'constr) hyp list - | Pconsider of 'constr*('hyp,'constr) hyp list + | Psuffices of ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut + | Passume of ('var,'constr) hyp list + | Plet of ('var,'constr) hyp list + | Pgiven of ('var,'constr) hyp list + | Pconsider of 'constr*('var,'constr) hyp list | Pclaim of 'constr statement | Pfocus of 'constr statement - | Pdefine of Id.t * 'hyp list * 'constr + | Pdefine of Id.t * 'var list * 'constr | Pcast of Id.t or_thesis * 'constr - | Psuppose of ('hyp,'constr) hyp list - | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Psuppose of ('var,'constr) hyp list + | Pcase of 'var list*'pat*(('var,'constr or_thesis) hyp list) | Ptake of 'constr list | Pper of elim_type * ('constr,'tac) casee | Pend of block_type @@ -70,19 +70,19 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = type emphasis = int -type ('hyp,'constr,'pat,'tac) gen_proof_instr= +type ('var,'constr,'pat,'tac) gen_proof_instr= {emph: emphasis; - instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + instr: ('var,'constr,'pat,'tac) bare_proof_instr } type raw_proof_instr = - ((Id.t*(Constrexpr.constr_expr option)) Loc.located, + ((Id.t * (Constrexpr.constr_expr option)) Loc.located, Constrexpr.constr_expr, Constrexpr.cases_pattern_expr, raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located, + ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located, Tacexpr.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index d169dc13..774c20c9 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -89,25 +89,22 @@ let get_info sigma gl= let try_get_info sigma gl = Store.get (Goal.V82.extra sigma gl) info -let get_stack pts = +let get_goal_stack pts = let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let info = get_info sigma (List.hd goals) in info.pm_stack let proof_focus = Proof.new_focus_kind () -let proof_cond = Proof.no_cond proof_focus +let proof_cond = Proof.done_cond proof_focus let focus p = - let inf = get_stack p in + let inf = get_goal_stack p in Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) let unfocus () = Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus () = - Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) - let get_top_stack pts = try Proof.get_at_focus proof_focus pts @@ -116,7 +113,24 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack +let get_stack pts = Proof.get_at_focus proof_focus pts + let get_last env = match Environ.named_context env with | (id,_,_)::_ -> id | [] -> error "no previous statement to use" + +let get_end_command pts = + match get_top_stack pts with + | [] -> "\"end proof\"" + | Claim::_ -> "\"end claim\"" + | Focus_claim::_-> "\"end focus\"" + | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ -> + begin + match et with + Decl_expr.ET_Case_analysis -> + "\"end cases\" or start a new case" + | Decl_expr.ET_Induction -> + "\"end induction\" or start a new case" + end + | _ -> anomaly (Pp.str"lonely suppose") diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 2864ba18..fd7e15c1 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -72,8 +72,8 @@ val get_last: Environ.env -> Id.t (** [get_last] raises a [UserError] when it cannot find a previous statement in the environment. *) +val get_end_command : Proof.proof -> string + val focus : Proof.proof -> unit val unfocus : unit -> unit - -val maximal_unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9d25681d..9d0b7f34 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -131,12 +131,13 @@ let daimon_tac gls = (* post-instruction focus management *) -(* spiwack: This used to fail if there was no focusing command - above, but I don't think it ever happened. I hope it doesn't mess - things up*) let goto_current_focus () = - Decl_mode.maximal_unfocus () + Decl_mode.unfocus () +(* spiwack: used to catch errors indicating lack of "focusing command" + in the proof tree. In the current implementation, however, entering + the declarative mode puts a focus first, there should, therefore, + never be exception raised here. *) let goto_current_focus_or_top () = goto_current_focus () @@ -1444,27 +1445,35 @@ let rec postprocess pts instr = Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end - | Pend _ -> - goto_current_focus_or_top () + | Pend (B_elim ET_Case_analysis) -> goto_current_focus () + | Pend B_proof -> Proof_global.set_proof_mode "Classic" + | Pend _ -> () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in - begin + (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the + current proof (and, actually so does [do_instr] later one, so + it's ok to do the same here. Ideally the proof should be properly + threaded through the commands here, but since the are interleaved + with actions on the proof mode, which is attached to the global + proof environment, it is not possible without heavy lifting. *) + let pts = Proof_global.give_me_the_proof () in + let pts = if has_tactic then let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in + let ist = {ltacvars = Id.Set.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) env sigma glob_instr in - ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) - else () end; - postprocess pts raw_instr.instr; - (* spiwack: this should restore a compatible semantics with - v8.3 where we never stayed focused on 0 goal. *) - Proof_global.set_proof_mode "Declarative" ; - Decl_mode.maximal_unfocus () + let (pts',_) = Proof.run_tactic (Global.env()) + (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in + pts' + else pts + in + Proof_global.simple_with_current_proof (fun _ _ -> pts); + postprocess pts raw_instr.instr let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 03929b3b..d598e7c3 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic +open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in @@ -35,22 +36,20 @@ let pr_goal gs = str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () -(* arnaud: rebrancher ça ? -let pr_open_subgoals () = - let p = Proof_global.give_me_the_proof () in - let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in - let close_cmd = Decl_mode.get_end_command p in - pr_subgoals close_cmd sigma goals -*) - -let pr_raw_proof_instr _ _ _ instr = - Errors.anomaly (Pp.str "Cannot print a proof_instr") - (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller - dans cette direction - Ppdecl_proof.pr_proof_instr (Global.env()) instr - *) -let pr_proof_instr _ _ _ instr = Empty.abort instr -let pr_glob_proof_instr _ _ _ instr = Empty.abort instr +let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = + match gll with + | [goal] when pr_first -> + pr_goal { Evd.it = goal ; sigma = sigma } + | _ -> + (* spiwack: it's not very nice to have to call proof global + here, a more robust solution would be to add a hook for + [Printer.pr_open_subgoals] in proof modes, in order to + compute the end command. Yet a more robust solution would be + to have focuses give explanations of their unfocusing + behaviour. *) + let p = Proof_global.give_me_the_proof () in + let close_cmd = Decl_mode.get_end_command p in + str "Subproof completed, now type " ++ str close_cmd ++ str "." let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr @@ -65,23 +64,18 @@ let vernac_decl_proof () = else begin Decl_proof_instr.go_to_proof_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end (* spiwack: some bureaucracy is not performed here *) let vernac_return () = begin Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end let vernac_proof_instr instr = - begin - Decl_proof_instr.proof_instr instr; - Vernacentries.print_subgoals () - end + Decl_proof_instr.proof_instr instr (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare @@ -92,7 +86,7 @@ let vernac_proof_instr instr = (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = +let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = Genarg.make0 None "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode @@ -106,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry = let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr -let classify_proof_instr _ = VtProofStep false, VtLater +let classify_proof_instr = function + | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow + | _ -> VtProofStep false, VtLater (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. The "-" indicates that the rule does not start with a distinguished string. *) -VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr - [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] +VERNAC proof_mode EXTEND ProofInstr + [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ] END (* It is useful to use GEXTEND directly to call grammar entries that have been @@ -143,7 +139,8 @@ let _ = (* We substitute the goal printer, by the one we built for the proof mode. *) Printer.set_printer_pr { Printer.default_printer_pr with - Printer.pr_goal = pr_goal } + Printer.pr_goal = pr_goal; + pr_subgoals = pr_subgoals; } end ; (* function [reset] goes back to No Proof Mode from Declarative Proof Mode *) @@ -160,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof [ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END VERNAC COMMAND EXTEND DeclReturn -[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] +[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ] END let none_is_empty = function diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 27308666..b3198dbf 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -12,41 +12,35 @@ open Decl_expr open Names open Nameops -let pr_constr = Printer.pr_constr_env -let pr_tac = Pptactic.pr_glob_tactic -let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr - let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () -let pr_constr env c = pr_constr env Evd.empty c - -let pr_justification_items env = function +let pr_justification_items pr_constr = function Some [] -> mt () | Some (_::_ as l) -> spc () ++ str "by" ++ spc () ++ - prlist_with_sep (fun () -> str ",") (pr_constr env) l + prlist_with_sep (fun () -> str ",") pr_constr l | None -> spc () ++ str "by *" -let pr_justification_method env = function +let pr_justification_method pr_tac = function None -> mt () | Some tac -> - spc () ++ str "using" ++ spc () ++ pr_tac env tac + spc () ++ str "using" ++ spc () ++ pr_tac tac -let pr_statement pr_it env st = - pr_label st.st_label ++ pr_it env st.st_it +let pr_statement pr_constr st = + pr_label st.st_label ++ pr_constr st.st_it -let pr_or_thesis pr_this env = function +let pr_or_thesis pr_this = function Thesis Plain -> str "thesis" | Thesis (For id) -> str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id - | This c -> pr_this env c + | This c -> pr_this c -let pr_cut pr_it env c = - hov 1 (pr_it env c.cut_stat) ++ - pr_justification_items env c.cut_by ++ - pr_justification_method env c.cut_using +let pr_cut pr_constr pr_tac pr_it c = + hov 1 (pr_it c.cut_stat) ++ + pr_justification_items pr_constr c.cut_by ++ + pr_justification_method pr_tac c.cut_using let type_or_thesis = function Thesis _ -> Term.mkProp @@ -54,128 +48,127 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env sep _be _have hyps = +let rec pr_hyps pr_var pr_constr gtyp sep _be _have hyps = let pr_sep = if sep then str "and" ++ spc () else mt () in match hyps with (Hvar _ ::_) as rest -> spc () ++ pr_sep ++ str _have ++ - print_vars pconstr gtyp env false _be _have rest + pr_vars pr_var pr_constr gtyp false _be _have rest | Hprop st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> env - | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ pr_sep ++ pr_statement pconstr env st ++ - print_hyps pconstr gtyp nenv true _be _have rest + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) + spc() ++ pr_sep ++ pr_statement pr_constr st ++ + pr_hyps pr_var pr_constr gtyp true _be _have rest end | [] -> mt () -and print_vars pconstr gtyp env sep _be _have vars = +and pr_vars pr_var pr_constr gtyp sep _be _have vars = match vars with Hvar st :: rest -> begin - let nenv = - match st.st_label with - Anonymous -> anomaly (Pp.str "anonymous variable") - | Name id -> Environ.push_named (id,None,st.st_it) env in + (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*) let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ - pr_statement pr_constr env st ++ - print_vars pconstr gtyp nenv true _be _have rest + pr_var st ++ + pr_vars pr_var pr_constr gtyp true _be _have rest end | (Hprop _ :: _) as rest -> let _st = if _be then str "be such that" else str "such that" in - spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest + spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest | [] -> mt () -let pr_suffices_clause env (hyps,c) = - print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ - str "to show" ++ spc () ++ pr_or_thesis pr_constr env c +let pr_suffices_clause pr_var pr_constr (hyps,c) = + pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++ + str "to show" ++ spc () ++ pr_or_thesis pr_constr c let pr_elim_type = function ET_Case_analysis -> str "cases" | ET_Induction -> str "induction" -let pr_casee env =function - Real c -> str "on" ++ spc () ++ pr_constr env c - | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut +let pr_block_type = function + B_elim et -> pr_elim_type et + | B_proof -> str "proof" + | B_claim -> str "claim" + | B_focus -> str "focus" + +let pr_casee pr_constr pr_tac =function + Real c -> str "on" ++ spc () ++ pr_constr c + | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut let pr_side = function Lhs -> str "=~" | Rhs -> str "~=" -let rec pr_bare_proof_instr _then _thus env = function +let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr true _thus env i - | Pthus i -> pr_bare_proof_instr _then true env i - | Phence i -> pr_bare_proof_instr true true env i + | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i + | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i + | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i | Pcut c -> begin match _then,_thus with false,false -> str "have" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | false,true -> str "thus" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,false -> str "then" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c | true,true -> str "hence" ++ spc () ++ - pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c end | Psuffices c -> - str "suffices" ++ pr_cut pr_suffices_clause env c + str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ - pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c + pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c | Passume hyps -> - str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps + str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps | Plet hyps -> - str "let" ++ print_vars pr_constr _I env false true "let" hyps + str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps | Pclaim st -> - str "claim" ++ spc () ++ pr_statement pr_constr env st + str "claim" ++ spc () ++ pr_statement pr_constr st | Pfocus st -> - str "focus on" ++ spc () ++ pr_statement pr_constr env st + str "focus on" ++ spc () ++ pr_statement pr_constr st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr env id + str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr id | Pgiven hyps -> - str "given" ++ print_vars pr_constr _I env false false "given" hyps + str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ - prlist_with_sep pr_comma (pr_constr env) witl + prlist_with_sep pr_comma pr_constr witl | Pdefine (id,args,body) -> str "define" ++ spc () ++ pr_id id ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr env body) + pr_var st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr body) | Pcast (id,typ) -> str "reconsider" ++ spc () ++ - pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr env typ) + pr_or_thesis pr_id id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr typ) | Psuppose hyps -> str "suppose" ++ - print_hyps pr_constr _I env false false "we have" hyps + pr_hyps pr_var pr_constr _I false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ (if params = [] then mt () else (spc () ++ str "with" ++ spc () ++ prlist_with_sep spc (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") params ++ spc ())) + pr_var st ++ str ")") params ++ spc ())) ++ (if hyps = [] then mt () else (spc () ++ str "and" ++ - print_hyps (pr_or_thesis pr_constr) type_or_thesis - env false false "we have" hyps)) - | Pper (et,c) -> + pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis + false false "we have" hyps)) + | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ - pr_casee env c - | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly (Pp.str "unprintable instruction") + pr_casee pr_constr pr_tac c + | Pend blk -> str "end" ++ spc () ++ pr_block_type blk let pr_emph = function 0 -> str " " @@ -184,7 +177,39 @@ let pr_emph = function | 3 -> str "*** " | _ -> anomaly (Pp.str "unknown emphasis") -let pr_proof_instr env instr = +let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr = pr_emph instr.emph ++ spc () ++ - pr_bare_proof_instr false false env instr.instr + pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr + + +let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")" + ) + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) = + pr_gen_proof_instr + (fun (_,(id,otyp)) -> + match otyp with + None -> pr_id id + | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")") + pconstr2 + Ppconstr.pr_cases_pattern_expr + (ptac Pptactic.ltop) + instr + +let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) = + pr_gen_proof_instr + (fun st -> pr_statement pconstr1 st) + pconstr2 + (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr) + (ptac Pptactic.ltop) + instr diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli index fd6fb663..678fc076 100644 --- a/plugins/decl_mode/ppdecl_proof.mli +++ b/plugins/decl_mode/ppdecl_proof.mli @@ -1,2 +1,14 @@ -val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds +open Decl_expr +open Pptactic + +val pr_gen_proof_instr : + ('var -> Pp.std_ppcmds) -> + ('constr -> Pp.std_ppcmds) -> + ('pat -> Pp.std_ppcmds) -> + ('tac -> Pp.std_ppcmds) -> + ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds + +val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer +val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer +val pr_proof_instr : proof_instr extra_genarg_printer diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 439b1a5c..c232ae31 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -49,13 +49,13 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted -> Errors.error"Admitted isn't supported in Derive." + | Admitted _ -> Errors.error"Admitted isn't supported in Derive." | Proved (_,Some _,_) -> Errors.error"Cannot save a proof of Derive with an explicit name." | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque , f_def , lemma_def + opaque <> Vernacexpr.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v new file mode 100644 index 00000000..294d6102 --- /dev/null +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -0,0 +1,15 @@ +(** Extraction to Haskell : use of basic Haskell types *) + +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. + +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. + +Extract Inlined Constant andb => "(Prelude.&&)". +Extract Inlined Constant orb => "(Prelude.||)". +Extract Inlined Constant negb => "Prelude.not". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 5f653ee1..a0930f15 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare => "fun n m -> if n=m then Eq else if n "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". +Extract Inlined Constant Compare_dec.lt_dec => "(<)". Extract Constant Compare_dec.lt_eq_lt_dec => "fun n m -> if n>m then None else Some (n unquote s (* no modular Scheme extraction... *) + | JSON -> dottify (List.map unquote rls) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) @@ -628,7 +629,7 @@ let check_extract_ascii () = try let char_type = match lang () with | Ocaml -> "char" - | Haskell -> "Char" + | Haskell -> "Prelude.Char" | _ -> raise Not_found in String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 42e69d34..0f846013 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp - | MEwith(me',WithDef(idl,c))-> + | MEwith(me',WithDef(idl,(c,ctx)))-> let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in let mt = extract_mexpr_spec env mp1 (me_struct,me') in (match extract_with_type env' c with (* cb may contain some kn *) @@ -410,6 +410,7 @@ let descr () = match lang () with | Ocaml -> Ocaml.ocaml_descr | Haskell -> Haskell.haskell_descr | Scheme -> Scheme.scheme_descr + | JSON -> Json.json_descr (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" Works similarly for the other languages. *) @@ -440,7 +441,8 @@ let mono_filename f = let module_filename mp = let f = file_of_modfile mp in let d = descr () in - Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f + let p = d.file_naming mp ^ d.file_suffix in + Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f (*s Extraction of one decl to stdout. *) diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib index b7f45861..ad321243 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mllib @@ -6,6 +6,7 @@ Common Ocaml Haskell Scheme +Json Extract_env G_extraction Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 3caa558f..3fe5a8c0 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -41,12 +41,14 @@ let pr_language = function | Ocaml -> str "Ocaml" | Haskell -> str "Haskell" | Scheme -> str "Scheme" + | JSON -> str "JSON" VERNAC ARGUMENT EXTEND language PRINTED BY pr_language | [ "Ocaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] +| [ "JSON" ] -> [ JSON ] END (* Extraction commands *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 5e08fef5..37b41420 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id)) let keywords = List.fold_right (fun s -> Id.Set.add (Id.of_string s)) - [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; + [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] @@ -38,7 +38,7 @@ let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" let preamble mod_name comment used_modules usf = let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") in - (if not usf.magic then mt () + (if not (usf.magic || usf.tunknown) then mt () else str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++ str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}") @@ -52,17 +52,34 @@ let preamble mod_name comment used_modules usf = str "import qualified Prelude" ++ fnl () ++ prlist pp_import used_modules ++ fnl () ++ (if List.is_empty used_modules then mt () else fnl ()) ++ - (if not usf.magic then mt () + (if not (usf.magic || usf.tunknown) then mt () else str "\ \n#ifdef __GLASGOW_HASKELL__\ \nimport qualified GHC.Base\ +\nimport qualified GHC.Prim\ +\n#else\ +\n-- HUGS\ +\nimport qualified IOExts\ +\n#endif" ++ fnl2 ()) + ++ + (if not usf.magic then mt () + else str "\ +\n#ifdef __GLASGOW_HASKELL__\ \nunsafeCoerce :: a -> b\ \nunsafeCoerce = GHC.Base.unsafeCoerce#\ \n#else\ \n-- HUGS\ -\nimport qualified IOExts\ \nunsafeCoerce :: a -> b\ \nunsafeCoerce = IOExts.unsafeCoerce\ +\n#endif" ++ fnl2 ()) + ++ + (if not usf.tunknown then mt () + else str "\ +\n#ifdef __GLASGOW_HASKELL__\ +\ntype Any = GHC.Prim.Any\ +\n#else\ +\n-- HUGS\ +\ntype Any = ()\ \n#endif" ++ fnl2 ()) ++ (if not usf.mldummy then mt () @@ -102,7 +119,7 @@ let rec pp_type par vl t = pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy _ -> str "()" - | Tunknown -> str "()" + | Tunknown -> str "Any" | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" in hov 0 (pp_rec par t) @@ -243,12 +260,12 @@ let pp_logical_ind packet = prvect_with_sep spc pr_id packet.ip_consnames) let pp_singleton kn packet = + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - let l' = List.rev l in - hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc pr_id l ++ (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ - pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) @@ -346,7 +363,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = @@ -360,6 +377,7 @@ let pp_struct = let haskell_descr = { keywords = keywords; file_suffix = ".hs"; + file_naming = string_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = None; diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml new file mode 100644 index 00000000..125dc86b --- /dev/null +++ b/plugins/extraction/json.ml @@ -0,0 +1,278 @@ +open Pp +open Errors +open Util +open Names +open Nameops +open Globnames +open Table +open Miniml +open Mlutil +open Common + +let json_str s = + qs s + +let json_int i = + int i + +let json_bool b = + if b then str "true" else str "false" + +let json_null = + str "null" + +let json_global typ ref = + json_str (Common.pp_global typ ref) + +let json_id id = + json_str (Id.to_string id) + +let json_dict_one (k, v) = + json_str k ++ str (": ") ++ v + +let json_dict_open l = + str ("{") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l) + +let json_dict l = + json_dict_open l ++ fnl () ++ + str ("}") + +let json_list l = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++ + str ("]") + +let json_listarr a = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++ + str ("]") + + +let preamble mod_name comment used_modules usf = + (match comment with + | None -> mt () + | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++ + json_dict_open [ + ("what", json_str "module"); + ("name", json_id mod_name); + ("need_magic", json_bool (usf.magic)); + ("need_dummy", json_bool (usf.mldummy)); + ("used_modules", json_list + (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules)) + ] + + +(*s Pretty-printing of types. *) + +let rec json_type vl = function + | Tmeta _ | Tvar' _ -> assert false + | Tvar i -> (try + let varid = List.nth vl (pred i) in json_dict [ + ("what", json_str "type:var"); + ("name", json_id varid) + ] + with Failure _ -> json_dict [ + ("what", json_str "type:varidx"); + ("name", json_int i) + ]) + | Tglob (r, l) -> json_dict [ + ("what", json_str "type:glob"); + ("name", json_global Type r); + ("args", json_list (List.map (json_type vl) l)) + ] + | Tarr (t1,t2) -> json_dict [ + ("what", json_str "type:arrow"); + ("left", json_type vl t1); + ("right", json_type vl t2) + ] + | Tdummy _ -> json_dict [("what", json_str "type:dummy")] + | Tunknown -> json_dict [("what", json_str "type:unknown")] + | Taxiom -> json_dict [("what", json_str "type:axiom")] + + +(*s Pretty-printing of expressions. *) + +let rec json_expr env = function + | MLrel n -> json_dict [ + ("what", json_str "expr:rel"); + ("name", json_id (get_db_name n env)) + ] + | MLapp (f, args) -> json_dict [ + ("what", json_str "expr:apply"); + ("func", json_expr env f); + ("args", json_list (List.map (json_expr env) args)) + ] + | MLlam _ as a -> + let fl, a' = collect_lams a in + let fl, env' = push_vars (List.map id_of_mlid fl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev fl))); + ("body", json_expr env' a') + ] + | MLletin (id, a1, a2) -> + let i, env' = push_vars [id_of_mlid id] env in + json_dict [ + ("what", json_str "expr:let"); + ("name", json_id (List.hd i)); + ("nameval", json_expr env a1); + ("body", json_expr env' a2) + ] + | MLglob r -> json_dict [ + ("what", json_str "expr:global"); + ("name", json_global Term r) + ] + | MLcons (_, r, a) -> json_dict [ + ("what", json_str "expr:constructor"); + ("name", json_global Cons r); + ("args", json_list (List.map (json_expr env) a)) + ] + | MLtuple l -> json_dict [ + ("what", json_str "expr:tuple"); + ("items", json_list (List.map (json_expr env) l)) + ] + | MLcase (typ, t, pv) -> json_dict [ + ("what", json_str "expr:case"); + ("expr", json_expr env t); + ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv)) + ] + | MLfix (i, ids, defs) -> + let ids', env' = push_vars (List.rev (Array.to_list ids)) env in + let ids' = Array.of_list (List.rev ids') in + json_dict [ + ("what", json_str "expr:fix"); + ("funcs", json_listarr (Array.map (fun (fi, ti) -> + json_dict [ + ("what", json_str "fix:item"); + ("name", json_id fi); + ("body", json_function env' ti) + ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ] + | MLexn s -> json_dict [ + ("what", json_str "expr:exception"); + ("msg", json_str s) + ] + | MLdummy -> json_dict [("what", json_str "expr:dummy")] + | MLmagic a -> json_dict [ + ("what", json_str "expr:coerce"); + ("value", json_expr env a) + ] + | MLaxiom -> json_dict [("what", json_str "expr:axiom")] + +and json_one_pat env (ids,p,t) = + let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ + ("what", json_str "case"); + ("pat", json_gen_pat (List.rev ids') env' p); + ("body", json_expr env' t) + ] + +and json_gen_pat ids env = function + | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l) + | Pusual r -> json_cons_pat r (List.map json_id ids) + | Ptuple l -> json_dict [ + ("what", json_str "pat:tuple"); + ("items", json_list (List.map (json_gen_pat ids env) l)) + ] + | Pwild -> json_dict [("what", json_str "pat:wild")] + | Prel n -> json_dict [ + ("what", json_str "pat:rel"); + ("name", json_id (get_db_name n env)) + ] + +and json_cons_pat r ppl = json_dict [ + ("what", json_str "pat:constructor"); + ("name", json_global Cons r); + ("argnames", json_list ppl) + ] + +and json_function env t = + let bl, t' = collect_lams t in + let bl, env' = push_vars (List.map id_of_mlid bl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev bl))); + ("body", json_expr env' t') + ] + + +(*s Pretty-printing of inductive types declaration. *) + +let json_ind ip pl cv = json_dict [ + ("what", json_str "decl:ind"); + ("name", json_global Type (IndRef ip)); + ("argnames", json_list (List.map json_id pl)); + ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ + ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("argtypes", json_list (List.map (json_type pl) c)) + ]) cv)) + ] + + +(*s Pretty-printing of a declaration. *) + +let pp_decl = function + | Dind (kn, defs) -> prvecti_with_sep pr_comma + (fun i p -> if p.ip_logical then str "" + else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets + | Dtype (r, l, t) -> json_dict [ + ("what", json_str "decl:type"); + ("name", json_global Type r); + ("argnames", json_list (List.map json_id l)); + ("value", json_type l t) + ] + | Dfix (rv, defs, typs) -> json_dict [ + ("what", json_str "decl:fixgroup"); + ("fixlist", json_listarr (Array.mapi (fun i r -> + json_dict [ + ("what", json_str "fixgroup:item"); + ("name", json_global Term rv.(i)); + ("type", json_type [] typs.(i)); + ("value", json_function (empty_env ()) defs.(i)) + ]) rv)) + ] + | Dterm (r, a, t) -> json_dict [ + ("what", json_str "decl:term"); + ("name", json_global Term r); + ("type", json_type [] t); + ("value", json_function (empty_env ()) a) + ] + +let rec pp_structure_elem = function + | (l,SEdecl d) -> [ pp_decl d ] + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> [] + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel) + | MEfunctor _ -> [] + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) + +let pp_struct mls = + let pp_sel (mp,sel) = + push_visible mp []; + let p = prlist_with_sep pr_comma identity + (List.concat (List.map pp_structure_elem sel)) in + pop_visible (); p + in + str "," ++ fnl () ++ + str " " ++ qs "declarations" ++ str ": [" ++ fnl () ++ + str " " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++ + str " ]" ++ fnl () ++ + str "}" ++ fnl () + + +let json_descr = { + keywords = Id.Set.empty; + file_suffix = ".json"; + file_naming = file_of_modfile; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli new file mode 100644 index 00000000..3ba240a1 --- /dev/null +++ b/plugins/extraction/json.mli @@ -0,0 +1 @@ +val json_descr : Miniml.language_descr diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 1e491d36..b7dee6cb 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -197,6 +197,7 @@ type language_descr = { (* Concerning the source file *) file_suffix : string; + file_naming : module_path -> string; (* the second argument is a comment to add to the preamble *) preamble : Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 30ac3d3f..8c482b4b 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -634,7 +634,12 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let l = List.map pp_specif sign in + let try_pp_specif l x = + try pp_specif x :: l with Failure "empty phrase" -> l + in + (* We cannot use fold_right here due to side effects in pp_specif *) + let l = List.fold_left try_pp_specif [] sign in + let l = List.rev l in pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -707,7 +712,12 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let l = List.map pp_structure_elem sel in + let try_pp_structure_elem l x = + try pp_structure_elem x :: l with Failure "empty phrase" -> l + in + (* We cannot use fold_right here due to side effects in pp_structure_elem *) + let l = List.fold_left try_pp_structure_elem [] sel in + let l = List.rev l in pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -736,6 +746,7 @@ let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt () let ocaml_descr = { keywords = keywords; file_suffix = ".ml"; + file_naming = file_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = Some ".mli"; diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 69dea25a..cc8b6d8e 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -212,7 +212,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = @@ -225,6 +225,7 @@ let pp_struct = let scheme_descr = { keywords = keywords; file_suffix = ".scm"; + file_naming = file_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = None; diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 44d760cc..a57c39ee 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -554,7 +554,7 @@ let _ = declare_string_option (*s Extraction Lang *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 1acbe355..648f2321 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -142,7 +142,7 @@ val file_comment : unit -> string (*s Target language. *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON val lang : unit -> lang (*s Extraction modes: modular or monolithic, library or minimal ? diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget index 1fe09f6f..f0489048 100644 --- a/plugins/extraction/vo.itarget +++ b/plugins/extraction/vo.itarget @@ -1,3 +1,4 @@ +ExtrHaskellBasic.vo ExtrOcamlBasic.vo ExtrOcamlIntConv.vo ExtrOcamlBigIntConv.vo diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 29ea1e77..6c7b0938 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Context open Globnames diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a88778c7..5912f0a0 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t= Name id -> id | Anonymous -> dummy_bvid in let revt=substl (List.init m (fun i->mkRel (m-i))) t in - let rec aux n avoid= - if Int.equal n 0 then [] else + let rec aux n avoid env evmap decls = + if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in - (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in - let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] env evmap nt in - let rec raux n t= - if Int.equal n 0 then t else - match t with - GLambda(loc,name,k,_,t0)-> - let t1=raux (n-1) t0 in - GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1) - | _-> anomaly (Pp.str "can't happen") in - let ntt=try - fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*) - with e when Errors.noncritical e -> - error "Untypable instance, maybe higher-order non-prenex quantification" in - decompose_lam_n_assum m ntt + let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let decl = (Name nid,None,c) in + aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in + let evmap, decls = aux m [] env evmap [] in + evmap, decls, revt (* tactics *) @@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq= if m>0 then pf_constr_of_global id (fun idc -> fun gl-> - let (rc,ot) = mk_open_instance id idc gl m t in + let evmap,rc,ot = mk_open_instance id idc gl m t in let gt= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in - generalize [gt] gl) + let evmap, _ = + try Typing.e_type_of (pf_env gl) evmap gt + with e when Errors.noncritical e -> + error "Untypable instance, maybe higher-order non-prenex quantification" in + tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) else pf_constr_of_global id (fun idc -> generalize [mkApp(idc,[|t|])]) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2f7f21e4..7d034db5 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -209,7 +209,7 @@ open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = - match p_a_t.code with + match repr_auto_tactic p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8006a3e1..7a56cd66 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -16,7 +16,6 @@ open Term open Tactics open Names open Globnames -open Tacticals open Tacmach open Fourier open Contradiction diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8214ada..4a832435 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -7,7 +7,6 @@ open Context open Namegen open Names open Declarations -open Declareops open Pp open Tacmach open Proof_type @@ -16,7 +15,6 @@ open Tactics open Indfun_common open Libnames open Globnames -open Misctypes (* let msgnl = Pp.msgnl *) @@ -46,18 +44,20 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g let debug_queue = Stack.create () -let rec print_debug_queue b e = +let rec print_debug_queue e = if not (Stack.is_empty debug_queue) then begin let lmsg,goal = Stack.pop debug_queue in - if b then - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) - else - begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); - end; - print_debug_queue false e; + let _ = + match e with + | Some e -> + Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + | None -> + begin + Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + end in + print_debug_queue None ; end let observe strm = @@ -70,13 +70,13 @@ let do_observe_tac s tac g = let lmsg = (str "observation : ") ++ s in Stack.push (lmsg,goal) debug_queue; try - let v = tac g in + let v = tac g in ignore(Stack.pop debug_queue); v with reraise -> let reraise = Errors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); + then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise))); iraise reraise let observe_tac_stream s tac g = @@ -943,13 +943,13 @@ let revert idl = (generalize (List.map mkVar idl)) (thin idl) -let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = +let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "nb_args := " ++ str (string_of_int nb_args)); *) (* observe (str "nb_params := " ++ str (string_of_int nb_params)); *) (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = Option.get (Global.body_of_constant_body f_def)in + let f_body = Option.get (Global.body_of_constant_body f_def) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in let fnames_with_params = @@ -962,41 +962,48 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in -(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) - let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) - (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in + (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) + let (type_ctxt,type_of_f),evd = + let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f + in + decompose_prod_n_assum + (nb_params + nb_args) t,evd + in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in + (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *) let f_id = Label.to_id (con_label (fst (destConst f))) in let prove_replacement = tclTHENSEQ [ tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro); - (* observe_tac "" *) (fun g -> + observe_tac "" (fun g -> let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ - [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); + [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); + observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); (Proofview.V82.of_tactic intros_reflexivity)] g ) ] in + (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) Lemmas.start_proof (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) - Evd.empty + (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) + evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.Proved(false,None)) + Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); + evd -let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = +let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in @@ -1007,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = Ensures by: obvious i*) let equation_lemma_id = (mk_equation_id f_id) in - generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; + evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with | Option.IsNone -> @@ -1020,9 +1027,16 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = ) } | _ -> () - in - Constrintern.construct_reference (pf_hyps g) equation_lemma_id + (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) + let evd',res = + Evd.fresh_global + (Global.env ()) !evd + (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) + in + let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in + evd:=evd'; + res in let nb_intro_to_do = nb_prod (pf_concl g) in tclTHEN @@ -1031,13 +1045,17 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = fun g' -> let just_introduced = nLastDecls nb_intro_to_do g' in let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in - tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g' + tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) + (revert just_introduced_id) g' ) g -let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic = +let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic = fun g -> - let princ_type = pf_concl g in + let princ_type = pf_concl g in + (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *) + (* Pp.msgnl (str "all_funs "); *) + (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *) let princ_info = compute_elim_sig princ_type in let fresh_id = let avoid = ref (pf_ids_of_hyps g) in @@ -1101,17 +1119,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : f_body ) in -(* observe (str "full_params := " ++ *) -(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *) -(* full_params *) -(* ); *) -(* observe (str "princ_params := " ++ *) -(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *) -(* princ_params *) -(* ); *) -(* observe (str "fbody_with_full_params := " ++ *) -(* pr_lconstr fbody_with_full_params *) -(* ); *) + observe (str "full_params := " ++ + prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + full_params + ); + observe (str "princ_params := " ++ + prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + princ_params + ); + observe (str "fbody_with_full_params := " ++ + pr_lconstr fbody_with_full_params + ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs in @@ -1191,7 +1209,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : (List.rev princ_info.predicates) in pte_to_fix,List.rev rev_info - | _ -> Id.Map.empty,[] + | _ -> + Id.Map.empty,[] in let mk_fixes : tactic = let pre_info,infos = list_chop fun_num infos in @@ -1205,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in if List.is_empty other_fix_infos then - (* observe_tac ("h_fix") *) (fix (Some this_fix_info.name) (this_fix_info.idx +1)) + if this_fix_info.idx + 1 = 0 + then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) + else + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1)) else Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0 @@ -1213,10 +1235,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ - [ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)); - (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)); - (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)); - (* observe_tac "building fixes" *) mk_fixes; + [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params))); + observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates))); + observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches))); + observe_tac "building fixes" mk_fixes; ] in let intros_after_fixes : tactic = @@ -1250,8 +1272,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in tclTHENSEQ [ -(* observe_tac "do_replace" *) - (do_replace + observe_tac "do_replace" + (do_replace evd full_params (fix_info.idx + List.length princ_params) (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params)) @@ -1259,9 +1281,6 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : fix_info.num_in_block all_funs ); -(* observe_tac "do_replace" *) -(* (do_replace princ_info.params fix_info.idx args_id *) -(* (List.hd (List.rev pte_args)) fix_body); *) let do_prove = build_proof interactive_proof diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index ff98f2b9..61fce267 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -2,6 +2,7 @@ open Names open Term val prove_princ_for_struct : + Evd.evar_map ref -> bool -> int -> constant array -> constr array -> int -> Tacmach.tactic diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 545f8931..45e5aaf5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -6,7 +6,6 @@ open Vars open Context open Namegen open Names -open Declareops open Pp open Entries open Tactics @@ -106,7 +105,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in -(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) + observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = @@ -116,7 +115,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin try match Environ.lookup_rel n env with | _,_,t when is_dom t -> raise Toberemoved - | _ -> pre_princ,[] with Not_found -> assert false + | _ -> pre_princ,[] + with Not_found -> assert false end | Prod(x,t,b) -> compute_new_princ_type_for_binder remove mkProd env x t b @@ -234,7 +234,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = -let change_property_sort toSort princ princName = +let change_property_sort evd toSort princ princName = let princ_info = compute_elim_sig princ in let change_sort_in_predicate (x,v,t) = (x,None, @@ -244,46 +244,48 @@ let change_property_sort toSort princ princName = compose_prod args (mkSort toSort) ) in - let princName_as_constr = Constrintern.global_reference princName in + let evd,princName_as_constr = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in mkApp(princName_as_constr, Array.init nargs (fun i -> mkRel (nargs - i ))) in - it_mkLambda_or_LetIn + evd, it_mkLambda_or_LetIn (it_mkLambda_or_LetIn init (List.map change_sort_in_predicate princ_info.predicates) ) princ_info.params -let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in (* let time1 = System.get_time () in *) let new_principle_type = compute_new_princ_type_from_rel - (Array.map mkConst funs) + (Array.map mkConstU funs) sorts old_princ_type in (* let time2 = System.get_time () in *) (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) - observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in + let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty - new_principle_type + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + !evd + new_principle_type hook - ; + ; (* let _tim1 = System.get_time () in *) - ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams))); + ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams))); (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) @@ -294,7 +296,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro -let generate_functional_principle +let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof old_princ_type sorts new_princ_name funs i proof_tac = @@ -311,20 +313,23 @@ let generate_functional_principle match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = Label.to_id (con_label f) in + let id_of_f = Label.to_id (con_label (fst f)) in id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in - let hook new_principle_type _ _ = + let evd' = !evd in + let hook = + fun new_principle_type _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let s = Universes.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - let value = change_property_sort s new_principle_type new_princ_name in - (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *) + let evd',value = change_property_sort evd' s new_principle_type new_princ_name in + let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in ignore( Declare.declare_constant name @@ -338,7 +343,7 @@ let generate_functional_principle register_with_sort InSet in let ((id,(entry,g_kind)),hook) = - build_functional_principle interactive_proof old_princ_type new_sorts funs i + build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in (* Pr 1278 : @@ -441,39 +446,37 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list = - let env = Global.env () - and sigma = Evd.empty in +let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = + let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in - - - let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in let first_fun_kn = try - fst (find_Function_infos first_fun).graph_ind + fst (find_Function_infos (fst first_fun)).graph_ind with Not_found -> raise No_graph_found in - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in - let this_block_funs = Array.map fst this_block_funs_indexes in + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in + let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.map - (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes) + (function cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes) funs in let ind_list = List.map (fun (idx) -> let ind = first_fun_kn,idx in - (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort + (ind,snd first_fun),true,prop_sort ) funs_indexes in let sigma, schemes = - Indrec.build_mutual_induction_scheme env sigma ind_list + Indrec.build_mutual_induction_scheme env !evd ind_list in + let _ = evd := sigma in let l_schemes = List.map (Typing.type_of env sigma) schemes in @@ -484,6 +487,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis ) fas in + evd:=sigma; (* We create the first priciple by tactic *) let first_type,other_princ_types = match l_schemes with @@ -492,34 +496,34 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis in let ((_,(const,_)),_) = try - build_functional_principle false + build_functional_principle evd false first_type (Array.of_list sorts) this_block_funs 0 - (prove_princ_for_struct false 0 (Array.of_list funs)) + (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ _ -> ()) - with e when Errors.noncritical e -> - begin - begin - try - let id = Pfedit.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () - else () - else () - with e when Errors.noncritical e -> () - end; - raise (Defining_principle e) - end + with e when Errors.noncritical e -> + begin + begin + try + let id = Pfedit.get_current_proof_name () in + let s = Id.to_string id in + let n = String.length "___________princ_________" in + if String.length s >= n + then if String.equal (String.sub s 0 n) "___________princ_________" + then Pfedit.delete_current_proof () + else () + else () + with e when Errors.noncritical e -> () + end; + raise (Defining_principle e) + end in incr i; let opacity = - let finfos = find_Function_infos this_block_funs.(0) in + let finfos = find_Function_infos (fst first_fun) in try let equation = Option.get finfos.equation_lemma in Declareops.is_opaque (Global.lookup_constant equation) @@ -533,7 +537,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis [const] else let other_fun_princ_types = - let funs = Array.map mkConst this_block_funs in + let funs = Array.map mkConstU this_block_funs in let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in @@ -566,12 +570,13 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis *) let ((_,(const,_)),_) = build_functional_principle + evd false (List.nth other_princ_types (!i - 1)) (Array.of_list sorts) this_block_funs !i - (prove_princ_for_struct false !i (Array.of_list funs)) + (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ _ -> ()) in const @@ -589,24 +594,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis in const::other_result + let build_scheme fas = Dumpglob.pause (); - let bodies_types = - make_scheme - (List.map + let evd = (ref Evd.empty) in + let pconstants = (List.map (fun (_,f,sort) -> let f_as_constant = try - match Smartlocate.global_with_alias f with - | Globnames.ConstRef c -> c - | _ -> Errors.error "Functional Scheme can only be used with functions" + Smartlocate.global_with_alias f with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f) in - (f_as_constant,sort) + let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in + let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in + let _ = evd := evd' in + (destConst f,sort) ) fas - ) + ) in + let bodies_types = + make_scheme evd pconstants in List.iter2 (fun (princ_id,_,_) def_entry -> @@ -633,14 +641,10 @@ let build_case_scheme fa = with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in - let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in - - - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in - let this_block_funs = Array.map fst this_block_funs_indexes in + let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in @@ -666,12 +670,15 @@ let build_case_scheme fa = ); *) generate_functional_principle + (ref Evd.empty) false scheme_type (Some ([|sorts|])) (Some princ_name) this_block_funs 0 - (prove_princ_for_struct false 0 [|fst (destConst funs)|]) + (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|]) in () + + diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index a16b834f..f6e5578d 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -3,6 +3,7 @@ open Term open Misctypes val generate_functional_principle : + Evd.evar_map ref -> (* do we accept interactive proving *) bool -> (* induction principle on rel *) @@ -12,7 +13,7 @@ val generate_functional_principle : (* Name of the new principle *) (Id.t) option -> (* the compute functions to use *) - constant array -> + pconstant array -> (* We prove the nth- principle *) int -> (* The tactic to use to make the proof w.r @@ -27,7 +28,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found -val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list +val make_scheme : Evd.evar_map ref -> + (pconstant*glob_sort) list -> Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index fd48ab59..043d4328 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -217,7 +217,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme begin make_graph (Smartlocate.global_with_alias fun_name) end - ; + ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Errors.error ("Cannot generate induction principle(s)") @@ -386,7 +386,9 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) (nexttac:Proof_type.tactic) g = let test = match oid with | Some id -> - let idconstr = mkConst (const_of_id id) in + let idref = const_of_id id in + (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *) + let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in (fun u -> constr_head_match u idconstr) (* select only id *) | None -> (fun u -> isApp u) in (* select calls to any function *) let info_list = find_fapp test g in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index a2577e2b..9e3f3986 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -252,7 +252,7 @@ let coq_False_ref = (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with - (the list of expresions on which we will do the matching) + (the list of expressions on which we will do the matching) *) let make_discr_match_el = List.map (fun e -> (e,(Anonymous,None))) @@ -674,7 +674,7 @@ and build_entry_lc_from_case env funname make_discr match el with brl end we first compute the list of lists corresponding to [el] and combine them . - Then for each elemeent of the combinations, + Then for each element of the combinations, we compute the result we compute one list per branch in [brl] and finally we just concatenate those list *) @@ -720,9 +720,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve match brl with | [] -> (* computed_branches *) {result = [];to_avoid = avoid} | br::brl' -> - (* alpha convertion to prevent name clashes *) + (* alpha conversion to prevent name clashes *) let _,idl,patl,return = alpha_br avoid br in - let new_avoid = idl@avoid in (* for now we can no more use idl as an indentifier *) + let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *) (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) *) @@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGApp(mkGVar relname,args@[rt]),Id.Set.empty -(* debuging wrapper *) +(* debugging wrapper *) let rebuild_cons env nb_args relname args crossed_types rt = (* observennl (str "rebuild_cons : rt := "++ pr_glob_constr rt ++ *) (* str "nb_args := " ++ str (string_of_int nb_args)); *) @@ -1163,7 +1163,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = (* naive implementation of parameter detection. A parameter is an argument which is only preceded by parameters and whose - calls are all syntaxically equal. + calls are all syntactically equal. TODO: Find a valid way to deal with implicit arguments here! *) @@ -1178,7 +1178,7 @@ let rec compute_cst_params relnames params = function compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be - discriminitation ones *) + discrimination ones *) | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> @@ -1233,11 +1233,11 @@ let rec rebuild_return_type rt = let do_build_inductive - mp_dp - funnames (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in + let funnames = List.map (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c)))) funconstants in (* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in let funnames = Array.of_list funnames in @@ -1252,27 +1252,25 @@ let do_build_inductive let relnames = Array.map mk_rel_id funnames in let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in (* Construction of the pseudo constructors *) - let env = - Array.fold_right - (fun id env -> - let c = - match mp_dp with - | None -> (Constrintern.global_reference id) - | Some(mp,dp) -> mkConst (make_con mp dp (Label.of_id id)) - in - Environ.push_named (id,None, - try - Typing.type_of env Evd.empty c - with Not_found -> - raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) - ) env + let evd,env = + Array.fold_right2 + (fun id c (evd,env) -> + let evd,t = Typing.e_type_of env evd (mkConstU c) in + evd, + Environ.push_named (id,None,t) + (* try *) + (* Typing.e_type_of env evd (mkConstU c) *) + (* with Not_found -> *) + (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *) + env ) funnames - (Global.env ()) + (Array.of_list funconstants) + (evd,Global.env ()) in let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = - let rel_arity i funargs = (* Reduilding arities (with parameters) *) + let rel_arity i funargs = (* Rebuilding arities (with parameters) *) let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = funargs in @@ -1426,7 +1424,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1461,9 +1459,9 @@ let do_build_inductive -let build_inductive mp_dp funnames funsargs returned_types rtl = +let build_inductive evd funconstants funsargs returned_types rtl = try - do_build_inductive mp_dp funnames funsargs returned_types rtl + do_build_inductive evd funconstants funsargs returned_types rtl with e when Errors.noncritical e -> raise (Building_graph e) diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index b0a05ec3..5bb1376e 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -7,8 +7,11 @@ open Names *) val build_inductive : - (ModPath.t * DirPath.t) option -> - Id.t list -> (* The list of function name *) +(* (ModPath.t * DirPath.t) option -> + Id.t list -> (* The list of function name *) + *) + Evd.evar_map -> + Term.pconstant list -> (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6dbd61cf..e211b688 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,7 +8,6 @@ open Libnames open Globnames open Glob_term open Declarations -open Declareops open Misctypes open Decl_kinds @@ -29,48 +28,55 @@ let choose_dest_or_ind scheme_info = let functional_induction with_clean c princl pat = Dumpglob.pause (); - let res = let f,args = decompose_app c in - fun g -> - let princ,bindings, princ_type = - match princl with - | None -> (* No principle is given let's find the good one *) - begin - match kind_of_term f with - | Const (c',u) -> - let princ_option = - let finfo = (* we first try to find out a graph on f *) - try find_Function_infos c' - with Not_found -> - errorlabstrm "" (str "Cannot find induction information on "++ - Printer.pr_lconstr (mkConst c') ) - in - match Tacticals.elimination_sort_of_goal g with - | InProp -> finfo.prop_lemma - | InSet -> finfo.rec_lemma - | InType -> finfo.rect_lemma - in - let princ = (* then we get the principle *) - try mkConst (Option.get princ_option ) - with Option.IsNone -> - (*i If there is not default lemma defined then, + let res = + let f,args = decompose_app c in + fun g -> + let princ,bindings, princ_type,g' = + match princl with + | None -> (* No principle is given let's find the good one *) + begin + match kind_of_term f with + | Const (c',u) -> + let princ_option = + let finfo = (* we first try to find out a graph on f *) + try find_Function_infos c' + with Not_found -> + errorlabstrm "" (str "Cannot find induction information on "++ + Printer.pr_lconstr (mkConst c') ) + in + match Tacticals.elimination_sort_of_goal g with + | InProp -> finfo.prop_lemma + | InSet -> finfo.rec_lemma + | InType -> finfo.rect_lemma + in + let princ,g' = (* then we get the principle *) + try + let g',princ = + Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in + princ,g' + with Option.IsNone -> + (*i If there is not default lemma defined then, we cross our finger and try to find a lemma named f_ind (or f_rec, f_rect) i*) - let princ_name = - Indrec.make_elimination_ident - (Label.to_id (con_label c')) - (Tacticals.elimination_sort_of_goal g) - in - try - mkConst(const_of_id princ_name ) - with Not_found -> (* This one is neither defined ! *) - errorlabstrm "" (str "Cannot find induction principle for " - ++Printer.pr_lconstr (mkConst c') ) - in - (princ,NoBindings, Tacmach.pf_type_of g princ) - | _ -> raise (UserError("",str "functional induction must be used with a function" )) - end - | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_type_of g princ + let princ_name = + Indrec.make_elimination_ident + (Label.to_id (con_label c')) + (Tacticals.elimination_sort_of_goal g) + in + try + let princ_ref = const_of_id princ_name in + let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in + (b,a) + (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) + with Not_found -> (* This one is neither defined ! *) + errorlabstrm "" (str "Cannot find induction principle for " + ++Printer.pr_lconstr (mkConst c') ) + in + (princ,NoBindings, Tacmach.pf_type_of g' princ,g') + | _ -> raise (UserError("",str "functional induction must be used with a function" )) + end + | Some ((princ,binding)) -> + princ,binding,Tacmach.pf_type_of g princ,g in let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = @@ -116,7 +122,7 @@ let functional_induction with_clean c princl pat = princ_infos (args_as_induction_constr,princ'))) subst_and_reduce - g + g' in Dumpglob.continue (); res @@ -222,34 +228,54 @@ let process_vernac_interp_error e = let derive_inversion fix_names = try + let evd' = Evd.empty in (* we first transform the fix_names identifier into their corresponding constant *) - let fix_names_as_constant = - List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names + let evd',fix_names_as_constant = + List.fold_right + (fun id (evd,l) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in + evd, destConst c::l + ) + fix_names + (evd',[]) in (* Then we check that the graphs have been defined If one of the graphs haven't been defined we do nothing *) - List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ; + List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ; try + let evd', lind = + List.fold_right + (fun id (evd,l) -> + let evd,id = + Evd.fresh_global + (Global.env ()) evd + (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) + in + evd,(fst (destInd id))::l + ) + fix_names + (evd',[]) + in Invfun.derive_correctness Functional_principles_types.make_scheme functional_induction fix_names_as_constant - (*i The next call to mk_rel_id is valid since we have just construct the graph - Ensures by : register_built - i*) - (List.map - (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id)))) - fix_names - ) - with e when Errors.noncritical e -> + lind; + with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) - with e when Errors.noncritical e -> () + with e when Errors.noncritical e -> + let e' = process_vernac_interp_error e in + msg_warning + (str "Cannot build inversion information (early)" ++ + if do_observe () then (fnl() ++ Errors.print e') else mt ()) let warning_error names e = let e = process_vernac_interp_error e in @@ -293,7 +319,7 @@ let error_error names e = e_explain e) | _ -> raise e -let generate_principle mp_dp on_error +let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = @@ -303,7 +329,7 @@ let generate_principle mp_dp on_error let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in try (* We then register the Inductive graphs of the functions *) - Glob_term_to_relation.build_inductive mp_dp names funs_args funs_types recdefs; + Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; if do_built then begin @@ -328,14 +354,18 @@ let generate_principle mp_dp on_error let _ = List.map_i (fun i x -> - let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in - let princ_type = Global.type_of_global_unsafe princ in - Functional_principles_types.generate_functional_principle + let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in + let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in + let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in + let _ = evd := evd' in + Functional_principles_types.generate_functional_principle + evd interactive_proof princ_type None None - funs_kn + (Array.of_list pconstants) + (* funs_kn *) i (continue_proof 0 [|funs_kn.(i)|]) ) @@ -352,10 +382,37 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in - Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition) - bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())) + Command.do_definition + fname + (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) + bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); + let evd,rev_pconstants = + List.fold_left + (fun (evd,l) (((_,fname),_,_,_,_),_) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + evd,((destConst c)::l) + ) + (Evd.empty,[]) + fixpoint_exprl + in + evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl + Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + let evd,rev_pconstants = + List.fold_left + (fun (evd,l) (((_,fname),_,_,_,_),_) -> + let evd,c = + Evd.fresh_global + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + evd,((destConst c)::l) + ) + (Evd.empty,[]) + fixpoint_exprl + in + evd,List.rev rev_pconstants + let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -400,10 +457,10 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in - let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type + let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try - pre_hook + pre_hook [fconst] (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); @@ -551,7 +608,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle mp_dp on_error register_built interactive_proof +let do_generate_principle pconstants on_error register_built interactive_proof (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let _is_struct = @@ -566,9 +623,10 @@ let do_generate_principle mp_dp on_error register_built interactive_proof let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let pre_hook = + let pre_hook pconstants = generate_principle - mp_dp + (ref (Evd.empty)) + pconstants on_error true register_built @@ -589,9 +647,10 @@ let do_generate_principle mp_dp on_error register_built interactive_proof let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in - let pre_hook = + let pre_hook pconstants = generate_principle - mp_dp + (ref Evd.empty) + pconstants on_error true register_built @@ -615,20 +674,26 @@ let do_generate_principle mp_dp on_error register_built interactive_proof let fix_names = List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl in - (* ok all the expressions are structural *) + (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - if register_built then register_struct is_rec fixpoint_exprl; + let evd,pconstants = + if register_built + then register_struct is_rec fixpoint_exprl + else (Evd.empty,pconstants) + in + let evd = ref evd in generate_principle - mp_dp + (ref !evd) + pconstants on_error false register_built fixpoint_exprl recdefs interactive_proof - (Functional_principles_proofs.prove_princ_for_struct interactive_proof); - if register_built then derive_inversion fix_names; + (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); + if register_built then begin derive_inversion fix_names; end; true; in () @@ -774,7 +839,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env Evd.empty body, Constrextern.extern_type false env Evd.empty - ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) + ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type) ) ) () @@ -812,13 +877,13 @@ let make_graph (f_ref:global_reference) = [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = repr_con c in - do_generate_principle (Some (mp,dp)) error_error false false expr_list; + do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) expr_list); Dumpglob.continue () -let do_generate_principle = do_generate_principle None warning_error true +let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 76f8c6d2..738ade8c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -108,7 +108,7 @@ let const_of_id id = let _,princ_ref = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in - try Nametab.locate_constant princ_ref + try Constrintern.locate_reference princ_ref with Not_found -> Errors.error ("cannot find "^ Id.to_string id) let def_of_const t = @@ -380,9 +380,9 @@ let find_Function_of_graph ind = Indmap.find ind !from_graph let update_Function finfo = -(* Pp.msgnl (pr_info finfo); *) + (* Pp.msgnl (pr_info finfo); *) Lib.add_anonymous_leaf (in_Function finfo) - + let add_Function is_general f = let f_id = Label.to_id (con_label f) in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 67ddf374..10daf6e8 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,7 +42,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val def_of_const : Term.constr -> Term.constr val eq : Term.constr Lazy.t val refl_equal : Term.constr Lazy.t -val const_of_id: Id.t -> constant +val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c7b0a0b..d10924f8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -45,7 +45,7 @@ let pr_with_bindings prc prlc (c,bl) = let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = pr_with_bindings prc prc (c,bl) -(* The local debuging mechanism *) +(* The local debugging mechanism *) (* let msgnl = Pp.msgnl *) let observe strm = @@ -70,7 +70,7 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - msgnl (str "observation "++ s++str " raised exception " ++ + observe (str "observation "++ s++str " raised exception " ++ Errors.iprint e ++ str " on goal " ++ goal ); iraise reraise;; @@ -92,13 +92,24 @@ let nf_zeta = Evd.empty -(* [id_to_constr id] finds the term associated to [id] in the global environment *) -let id_to_constr id = +(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *) +(* let id_to_constr id = *) +(* try *) +(* Constrintern.global_reference id *) +(* with Not_found -> *) +(* raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *) + + +let make_eq () = try - Constrintern.global_reference id - with Not_found -> - raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) + Universes.constr_of_global (Coqlib.build_coq_eq ()) + with _ -> assert false +let make_eq_refl () = + try + Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) + with _ -> assert false + (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. @@ -111,11 +122,13 @@ let id_to_constr id = res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion *) -let generate_type g_to_f f graph i = +let generate_type evd g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) - let gr,u = destInd graph in - let graph_arity = Inductive.type_of_inductive (Global.env()) - (Global.lookup_inductive gr, u) in + let evd',graph = + Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph))) + in + let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in + evd:=evd'; let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -141,11 +154,10 @@ let generate_type g_to_f f graph i = the hypothesis [res = fv] can then be computed We will need to lift it by one in order to use it as a conclusion i*) - let make_eq () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) + let make_eq = make_eq () in let res_eq_f_of_args = - mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|]) + mkApp(make_eq ,[|lift 2 res_type;mkRel 1;mkRel 2|]) in (*i The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed @@ -158,12 +170,12 @@ let generate_type g_to_f f graph i = \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) let pre_ctxt = - (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt + (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt in (*i and we can return the solution depending on which lemma type we are defining i*) if g_to_f - then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args) - else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied) + then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -171,7 +183,7 @@ let generate_type g_to_f f graph i = WARNING: while convertible, [type_of body] and [type] can be non equal *) -let find_induction_principle f = +let find_induction_principle evd f = let f_as_constant,u = match kind_of_term f with | Const c' -> c' | _ -> error "Must be used with a function" @@ -180,28 +192,10 @@ let find_induction_principle f = match infos.rect_lemma with | None -> raise Not_found | Some rect_lemma -> - let rect_lemma = mkConst rect_lemma in - let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in - rect_lemma,typ - - - -(* let fname = *) -(* match kind_of_term f with *) -(* | Const c' -> *) -(* Label.to_id (con_label c') *) -(* | _ -> error "Must be used with a function" *) -(* in *) - -(* let princ_name = *) -(* ( *) -(* Indrec.make_elimination_ident *) -(* fname *) -(* InType *) -(* ) *) -(* in *) -(* let c = (\* mkConst(mk_from_const (destConst f) princ_name ) in *\) failwith "" in *) -(* c,Typing.type_of (Global.env ()) Evd.empty c *) + let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in + let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in + evd:=evd'; + rect_lemma,typ let rec generate_fresh_id x avoid i = @@ -211,11 +205,6 @@ let rec generate_fresh_id x avoid i = let id = Namegen.next_ident_away_in_goal x avoid in id::(generate_fresh_id x (id::avoid) (pred i)) -let make_eq () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) -let make_eq_refl () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) - (* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. @@ -241,7 +230,7 @@ let make_eq_refl () = \end{enumerate} *) -let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = +let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -255,12 +244,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let f_principle,princ_type = schemes.(i) in let princ_type = nf_zeta princ_type in let princ_infos = Tactics.compute_elim_sig princ_type in - (* The number of args of the function is then easilly computable *) + (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (pf_concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in - (* Since we cannot ensure that the funcitonnal principle is defined in the - environement and due to the bug #1174, we will need to pose the principle + (* Since we cannot ensure that the functional principle is defined in the + environment and due to the bug #1174, we will need to pose the principle using a name *) let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in @@ -286,46 +275,6 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* The tactic to prove the ith branch of the principle *) let prove_branche i g = (* We get the identifiers of this branch *) - (* - let this_branche_ids = - List.fold_right - (fun (_,pat) acc -> - match pat with - | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly (Pp.str "Not an identifier") - ) - (List.nth intro_pats (pred i)) - Id.Set.empty - in - let pre_args g = - List.fold_right - (fun (id,b,t) pre_args -> - if Id.Set.mem id this_branche_ids - then - match b with - | None -> id::pre_args - | Some b -> pre_args - else pre_args - ) - (pf_hyps g) - ([]) - in - let pre_args g = List.rev (pre_args g) in - let pre_tac g = - List.fold_right - (fun (id,b,t) pre_tac -> - if Id.Set.mem id this_branche_ids - then - match b with - | None -> pre_tac - | Some b -> - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac - else pre_tac - ) - (pf_hyps g) - tclIDTAC - in -*) let pre_args = List.fold_right (fun (_,pat) acc -> @@ -345,7 +294,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem If [hid] has another type the corresponding argument of the constructor is [hid] *) let constructor_args g = - List.fold_right + List.fold_right (fun hid acc -> let type_of_hid = pf_type_of g (mkVar hid) in match kind_of_term type_of_hid with @@ -358,7 +307,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | App(eq,args), App(graph',_) when (eq_constr eq eq_ind) && - Array.exists (eq_constr graph') graphs_constr -> + Array.exists (Constr.eq_constr_nounivs graph') graphs_constr -> (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) ::acc) | _ -> mkVar hid :: acc @@ -395,7 +344,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem end in (* we can then build the final proof term *) - let app_constructor g = applist((mkConstruct(constructor)),constructor_args g) in + let app_constructor g = applist((mkConstructU(constructor,u)),constructor_args g) in (* an apply the tactic *) let res,hres = match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with @@ -428,7 +377,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) - observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (app_constructor g)) g) + observe_tac "exact" (fun g -> + Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) g @@ -436,13 +386,15 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* end of branche proof *) let lemmas = Array.map - (fun (_,(ctxt,concl)) -> + (fun ((_,(ctxt,concl))) -> match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::(x,_,t)::ctxt -> - Termops.it_mkLambda_or_LetIn - (Termops.it_mkProd_or_LetIn concl [hres;res]) - ((x,None,t)::ctxt) + let res = Termops.it_mkLambda_or_LetIn + (Termops.it_mkProd_or_LetIn concl [hres;res]) + ((x,None,t)::ctxt) + in + res ) lemmas_types_infos in @@ -457,7 +409,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (*(Loc.ghost,Glob_term.NamedHyp id,p)*)p::bindings,id::avoid + p::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -467,12 +419,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (*(Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))*) (nf_zeta p)::bindings,id::avoid) + (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) in - (* Glob_term.ExplicitBindings *) (params_bindings@lemmas_bindings) + (params_bindings@lemmas_bindings) in tclTHENSEQ [ @@ -484,10 +436,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) observe_tac "idtac" tclIDTAC; tclTHEN_i - (observe_tac "functional_induction" ( - (fun gl -> - let term = mkApp (mkVar principle_id,Array.of_list bindings) in - let gl', _ty = pf_eapply Typing.e_type_of gl term in + (observe_tac + "functional_induction" ( + (fun gl -> + let term = mkApp (mkVar principle_id,Array.of_list bindings) in + let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true) gl term in Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) @@ -495,230 +448,6 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem g -(* -let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = - fun g -> - (* first of all we recreate the lemmas types to be used as predicates of the induction principle - that is~: - \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\] - *) - let lemmas = - Array.map - (fun (_,(ctxt,concl)) -> - match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") - | hres::res::(x,_,t)::ctxt -> - Termops.it_mkLambda_or_LetIn - (Termops.it_mkProd_or_LetIn concl [hres;res]) - ((x,None,t)::ctxt) - ) - lemmas_types_infos - in - (* we the get the definition of the graphs block *) - let graph_ind = destInd graphs_constr.(i) in - let kn = fst graph_ind in - let mib,_ = Global.lookup_inductive graph_ind in - (* and the principle to use in this lemma in $\zeta$ normal form *) - let f_principle,princ_type = schemes.(i) in - let princ_type = nf_zeta princ_type in - let princ_infos = Tactics.compute_elim_sig princ_type in - (* The number of args of the function is then easilly computable *) - let nb_fun_args = nb_prod (pf_concl g) - 2 in - let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in - let ids = args_names@(pf_ids_of_hyps g) in - (* Since we cannot ensure that the funcitonnal principle is defined in the - environement and due to the bug #1174, we will need to pose the principle - using a name - *) - let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in - let ids = principle_id :: ids in - (* We get the branches of the principle *) - let branches = List.rev princ_infos.branches in - (* and built the intro pattern for each of them *) - let intro_pats = - List.map - (fun (_,_,br_type) -> - List.map - (fun id -> Loc.ghost, Genarg.IntroIdentifier id) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) - ) - branches - in - (* before building the full intro pattern for the principle *) - let pat = Some (Loc.ghost,Genarg.IntroOrAndPattern intro_pats) in - let eq_ind = Coqlib.build_coq_eq () in - let eq_construct = mkConstruct((destInd eq_ind),1) in - (* The next to referencies will be used to find out which constructor to apply in each branch *) - let ind_number = ref 0 - and min_constr_number = ref 0 in - (* The tactic to prove the ith branch of the principle *) - let prove_branche i g = - (* We get the identifiers of this branch *) - let this_branche_ids = - List.fold_right - (fun (_,pat) acc -> - match pat with - | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly (Pp.str "Not an identifier") - ) - (List.nth intro_pats (pred i)) - Id.Set.empty - in - (* and get the real args of the branch by unfolding the defined constant *) - let pre_args,pre_tac = - List.fold_right - (fun (id,b,t) (pre_args,pre_tac) -> - if Id.Set.mem id this_branche_ids - then - match b with - | None -> (id::pre_args,pre_tac) - | Some b -> - (pre_args, - tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac - ) - else (pre_args,pre_tac) - ) - (pf_hyps g) - ([],tclIDTAC) - in - (* - We can then recompute the arguments of the constructor. - For each [hid] introduced by this branch, if [hid] has type - $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are - [ fv (hid fv (refl_equal fv)) ]. - If [hid] has another type the corresponding argument of the constructor is [hid] - *) - let constructor_args = - List.fold_right - (fun hid acc -> - let type_of_hid = pf_type_of g (mkVar hid) in - match kind_of_term type_of_hid with - | Prod(_,_,t') -> - begin - match kind_of_term t' with - | Prod(_,t'',t''') -> - begin - match kind_of_term t'',kind_of_term t''' with - | App(eq,args), App(graph',_) - when - (eq_constr eq eq_ind) && - Array.exists (eq_constr graph') graphs_constr -> - ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) - ::args.(2)::acc) - | _ -> mkVar hid :: acc - end - | _ -> mkVar hid :: acc - end - | _ -> mkVar hid :: acc - ) pre_args [] - in - (* in fact we must also add the parameters to the constructor args *) - let constructor_args = - let params_id = fst (List.chop princ_infos.nparams args_names) in - (List.map mkVar params_id)@(List.rev constructor_args) - in - (* We then get the constructor corresponding to this branch and - modifies the references has needed i.e. - if the constructor is the last one of the current inductive then - add one the number of the inductive to take and add the number of constructor of the previous - graph to the minimal constructor number - *) - let constructor = - let constructor_num = i - !min_constr_number in - let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in - if constructor_num <= length - then - begin - (kn,!ind_number),constructor_num - end - else - begin - incr ind_number; - min_constr_number := !min_constr_number + length ; - (kn,!ind_number),1 - end - in - (* we can then build the final proof term *) - let app_constructor = applist((mkConstruct(constructor)),constructor_args) in - (* an apply the tactic *) - let res,hres = - match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with - | [res;hres] -> res,hres - | _ -> assert false - in - observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); - ( - tclTHENSEQ - [ - (* unfolding of all the defined variables introduced by this branch *) - observe_tac "unfolding" pre_tac; - (* $zeta$ normalizing of the conclusion *) - h_reduce - (Glob_term.Cbv - { Glob_term.all_flags with - Glob_term.rDelta = false ; - Glob_term.rConst = [] - } - ) - onConcl; - (* introducing the the result of the graph and the equality hypothesis *) - observe_tac "introducing" (tclMAP h_intro [res;hres]); - (* replacing [res] with its value *) - observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres)); - (* Conclusion *) - observe_tac "exact" (exact_check app_constructor) - ] - ) - g - in - (* end of branche proof *) - let param_names = fst (List.chop princ_infos.nparams args_names) in - let params = List.map mkVar param_names in - let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in - (* The bindings of the principle - that is the params of the principle and the different lemma types - *) - let bindings = - let params_bindings,avoid = - List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (Loc.ghost,Glob_term.NamedHyp id,p)::bindings,id::avoid - ) - ([],pf_ids_of_hyps g) - princ_infos.params - (List.rev params) - in - let lemmas_bindings = - List.rev (fst (List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (Loc.ghost,Glob_term.NamedHyp id,(nf_zeta p))::bindings,id::avoid) - ([],avoid) - princ_infos.predicates - (lemmas))) - in - Glob_term.ExplicitBindings (params_bindings@lemmas_bindings) - in - tclTHENSEQ - [ observe_tac "intro args_names" (tclMAP h_intro args_names); - observe_tac "principle" (assert_by - (Name principle_id) - princ_type - (exact_check f_principle)); - tclTHEN_i - (observe_tac "functional_induction" ( - fun g -> - observe - (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); - functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) - (Some (mkVar principle_id,bindings)) - pat g - )) - (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) - ] - g -*) (* [generalize_dependent_of x hyp g] @@ -735,12 +464,9 @@ let generalize_dependent_of x hyp g = g - - - - (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis +(* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) - *) + *) let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g and intros_with_rewrite_aux : tactic = @@ -1020,11 +746,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = g - - -let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) - - (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1032,21 +753,28 @@ let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) [functional_induction] is Indfun.functional_induction (same pb) *) -let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = +let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) = + assert (funs <> []); + assert (graphs <> []); let funs = Array.of_list funs and graphs = Array.of_list graphs in - let funs_constr = Array.map mkConst funs in - States.with_state_protection_on_exception (fun () -> - let graphs_constr = Array.map mkInd graphs in - let lemmas_types_infos = - Util.Array.map2_i - (fun i f_constr graph -> - let const_of_f,u = destConst f_constr in - let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = - generate_type false const_of_f graph i - in - let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in + let funs_constr = Array.map mkConstU funs in + States.with_state_protection_on_exception + (fun () -> + let evd = ref Evd.empty in + let graphs_constr = Array.map mkInd graphs in + let lemmas_types_infos = + Util.Array.map2_i + (fun i f_constr graph -> + (* let const_of_f,u = destConst f_constr in *) + let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = + generate_type evd false f_constr graph i + in + let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in + graphs_constr.(i) <- graph; + let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in + let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info ) funs_constr @@ -1055,65 +783,79 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let schemes = (* The functional induction schemes are computed and not saved if there is more that one function if the block contains only one function we can safely reuse [f_rect] - *) + *) try if not (Int.equal (Array.length funs_constr) 1) then raise Not_found; - [| find_induction_principle funs_constr.(0) |] + [| find_induction_principle evd funs_constr.(0) |] with Not_found -> + ( + Array.of_list (List.map (fun entry -> (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type ) ) - (make_scheme (Array.map_to_list (fun const -> const,GType []) funs)) + (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs)) ) + ) in let proving_tac = - prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos + prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (con_label f_as_constant) in + let f_id = Label.to_id (con_label (fst f_as_constant)) in (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious i*) let lem_id = mk_correct_id f_id in - Lemmas.start_proof lem_id - (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty - (fst lemmas_types_infos.(i)) + let (typ,_) = lemmas_types_infos.(i) in + Lemmas.start_proof + lem_id + (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) + !evd + typ (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by - (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i)))); - do_save (); - let finfo = find_Function_infos f_as_constant in - let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in - update_Function {finfo with correctness_lemma = Some lem_cst} + (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") + (proving_tac i)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + let finfo = find_Function_infos (fst f_as_constant) in + (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) + let _,lem_cst_constr = Evd.fresh_global + (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in + let (lem_cst,_) = destConst lem_cst_constr in + update_Function {finfo with correctness_lemma = Some lem_cst}; + ) funs; + (* let evd = ref Evd.empty in *) let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> - let const_of_f = fst (destConst f_constr) in - let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = - generate_type true const_of_f graph i - in - let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); - type_of_lemma,type_info + let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = + generate_type evd true f_constr graph i + in + let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in + graphs_constr.(i) <- graph; + let type_of_lemma = + Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt + in + let type_of_lemma = nf_zeta type_of_lemma in + observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); + type_of_lemma,type_info ) funs_constr graphs_constr in - let kn,_ as graph_ind = fst (destInd graphs_constr.(0)) in - let mib,mip = Global.lookup_inductive graph_ind in + + let (kn,_) as graph_ind,u = (destInd graphs_constr.(0)) in + let mib,mip = Global.lookup_inductive graph_ind in let sigma, scheme = - (Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty + (Indrec.build_mutual_induction_scheme (Global.env ()) !evd (Array.to_list (Array.mapi - (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType) + (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType) mib.Declarations.mind_packets ) ) @@ -1127,26 +869,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (con_label f_as_constant) in + let f_id = Label.to_id (con_label (fst f_as_constant)) in (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i)))); - do_save (); - let finfo = find_Function_infos f_as_constant in - let lem_cst,u = destConst (Constrintern.global_reference lem_id) in + (proving_tac i)))) ; + (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + let finfo = find_Function_infos (fst f_as_constant) in + let _,lem_cst_constr = Evd.fresh_global + (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in + let (lem_cst,_) = destConst lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) - () + () (***********************************************) @@ -1257,7 +1000,7 @@ let invfun qhyp f g = match f with | Some f -> invfun qhyp f g | None -> - Proofview.V82.of_tactic begin + Proofview.V82.of_tactic begin Tactics.try_intros_until (fun hid -> Proofview.V82.tactic begin fun g -> let hyp_typ = pf_type_of g (mkVar hid) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5558556e..0999b95d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = let ce = definition_entry ~univs:ctx value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None)) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = match (kind_of_term t) with @@ -217,7 +217,7 @@ let rec print_debug_queue b e = begin Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); end; - print_debug_queue false e; + (* print_debug_queue false e; *) end let observe strm = @@ -246,6 +246,18 @@ let observe_tac s tac g = then do_observe_tac s tac g else tac g + +let observe_tclTHENLIST s tacl = + if do_observe () + then + let rec aux n = function + | [] -> tclIDTAC + | [tac] -> observe_tac (s ++ spc () ++ int n) tac + | tac::tacl -> observe_tac (s ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl)) + in + aux 0 tacl + else tclTHENLIST tacl + (* Conclusion tactics *) (* The boolean value is_mes expresses that the termination is expressed @@ -256,11 +268,11 @@ let tclUSER tac is_mes l g = | None -> clear [] | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l) in - tclTHENLIST + observe_tclTHENLIST (str "tclUSER1") [ clear_tac; if is_mes - then tclTHENLIST + then observe_tclTHENLIST (str "tclUSER2") [ unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]; @@ -378,12 +390,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ) [] rev_context in let rev_ids = pf_get_new_ids (List.rev ids) g in let new_b = substl (List.map mkVar rev_ids) b in - tclTHENLIST + observe_tclTHENLIST (str "treat_case1") [ h_intros (List.rev rev_ids); Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> - tclTHENLIST[ + observe_tclTHENLIST (str "treat_case2")[ thin to_intros; h_intros to_intros; (fun g' -> @@ -508,14 +520,14 @@ let rec prove_lt hyple g = in let y = List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in - tclTHENLIST[ + observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) ] with Not_found -> ( ( - tclTHENLIST[ + observe_tclTHENLIST (str "prove_lt2")[ Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) ]) @@ -533,7 +545,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = let h' = next_ident_away_in_goal (h'_id) ids in let ids = h'::ids in let def = next_ident_away_in_goal def_id ids in - tclTHENLIST[ + observe_tclTHENLIST (str "destruct_bounds_aux1")[ Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); Proofview.V82.of_tactic (intro_then (fun id -> @@ -541,18 +553,18 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = observe_tac (str "destruct_bounds_aux") (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ - tclTHENLIST[Proofview.V82.of_tactic (intro_using h_id); + observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id); Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); Proofview.V82.of_tactic default_full_auto]; - tclTHENLIST[ + observe_tclTHENLIST (str "destruct_bounds_aux2")[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)]); - observe_tac (str "test" ) ( - tclTHENLIST[ + ( + observe_tclTHENLIST (str "test")[ list_rewrite true (List.fold_right (fun e acc -> (mkVar e,true)::acc) @@ -572,7 +584,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = )end)) ] g | (_,v_bound)::l -> - tclTHENLIST[ + observe_tclTHENLIST (str "destruct_bounds_aux3")[ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); clear [v_bound]; tclDO 2 (Proofview.V82.of_tactic intro); @@ -580,7 +592,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (fun p_hyp -> (onNthHypId 2 (fun p -> - tclTHENLIST[ + observe_tclTHENLIST (str "destruct_bounds_aux4")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -604,7 +616,7 @@ let destruct_bounds infos = let terminate_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app1")[ continuation_tac infos; observe_tac (str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); @@ -615,7 +627,7 @@ let terminate_app f_and_args expr_info continuation_tac infos = let terminate_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_others")[ continuation_tac infos; observe_tac (str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); @@ -671,17 +683,17 @@ let mkDestructEq : let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> - tclTHENLIST + observe_tclTHENLIST (str "mkDestructEq") [Simple.generalize new_hyps; (fun g2 -> Proofview.V82.of_tactic (change_in_concl None - (fun sigma -> + (fun patvars sigma -> pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = - let b = + let f_is_present = try check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a; false @@ -697,11 +709,11 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating case " ++ int (Array.length l) ++ spc () ++ Printer.pr_lconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_lconstr a') (try (tclTHENS destruct_tac - (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) + (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) with | UserError("Refiner.thensn_tac3",_) @@ -717,11 +729,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = try let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app_rec")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app_rec1")[ observe_tac (str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (str "destruct_bounds (3)") @@ -734,7 +746,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = observe_tac (str "terminate_app_rec not found") (tclTHENS (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) [ - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app_rec2")[ Proofview.V82.of_tactic (intro_using rec_res_id); Proofview.V82.of_tactic intro; onNthHypId 1 @@ -747,11 +759,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = (v,v_bound)::expr_info.values_and_bounds; args_assoc=(args,mkVar v)::expr_info.args_assoc } in - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app_rec3")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - tclTHENLIST[ + observe_tclTHENLIST (str "terminate_app_rec4")[ observe_tac (str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (str "destruct_bounds (2)") @@ -769,7 +781,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) [ observe_tac (str "assumption") (Proofview.V82.of_tactic assumption); - tclTHENLIST + observe_tclTHENLIST (str "terminate_app_rec5") [ tclTRY(list_rewrite true (List.map @@ -805,7 +817,7 @@ let prove_terminate = travel terminate_info (* Equation proof *) let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = - terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos + observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) let rec prove_le g = let x,z = @@ -826,7 +838,7 @@ let rec prove_le g = let _,args = decompose_app t in List.hd (List.tl args) in - tclTHENLIST[ + observe_tclTHENLIST (str "prove_le")[ Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); observe_tac (str "prove_le (rec)") (prove_le) ] @@ -856,7 +868,7 @@ let rec make_rewrite_list expr_info max = function (f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; - tclTHENLIST[ (* x < S max proof *) + observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); observe_tac (str "prove_le(2)") prove_le ] @@ -883,7 +895,7 @@ let make_rewrite expr_info l hp max = (f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) - (tclTHENLIST[ + (observe_tclTHENLIST (str "make_rewrite")[ simpl_iter Locusops.onConcl; observe_tac (str "unfold functional") (unfold_in_concl[(Locus.OnlyOccurrences [1], @@ -891,9 +903,12 @@ let make_rewrite expr_info l hp max = (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); - (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity))])) + (observe_tac (str "h_reflexivity") + (Proofview.V82.of_tactic intros_reflexivity) + ) + ])) ; - tclTHENLIST[ (* x < S (S max) proof *) + observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *) Proofview.V82.of_tactic (apply (delayed_force le_lt_SS)); observe_tac (str "prove_le (3)") prove_le ] @@ -904,7 +919,7 @@ let rec compute_max rew_tac max l = match l with | [] -> rew_tac max | (_,p,_)::l -> - tclTHENLIST[ + observe_tclTHENLIST (str "compute_max")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| max; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -924,7 +939,7 @@ let rec destruct_hex expr_info acc l = observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) end | (v,hex)::l -> - tclTHENLIST[ + observe_tclTHENLIST (str "destruct_hex")[ Proofview.V82.of_tactic (simplest_case (mkVar hex)); clear [hex]; tclDO 2 (Proofview.V82.of_tactic intro); @@ -939,7 +954,7 @@ let rec destruct_hex expr_info acc l = let rec intros_values_eq expr_info acc = tclORELSE( - tclTHENLIST[ + observe_tclTHENLIST (str "intros_values_eq")[ tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hex -> (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) @@ -952,14 +967,15 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - tclTHEN + observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_lconstr expr_info.info) + (tclTHEN (continuation_tac infos) - (intros_values_eq expr_info []) - else continuation_tac infos + (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_lconstr expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_lconstr expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch - then intros_values_eq expr_info [] + then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info []))) else continuation_tac infos let equation_app_rec (f,args) expr_info continuation_tac info = @@ -971,13 +987,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info = with Not_found -> if expr_info.is_final && expr_info.is_main_branch then - tclTHENLIST + observe_tclTHENLIST (str "equation_app_rec") [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info []) ] else - tclTHENLIST[ + observe_tclTHENLIST (str "equation_app_rec1")[ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) ] @@ -1089,7 +1105,7 @@ let termination_proof_header is_mes input_type ids args_id relation ] ; (* rest of the proof *) - tclTHENLIST + observe_tclTHENLIST (str "rest of proof") [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> @@ -1247,9 +1263,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> true - | Declarations.Undef _ -> true - | Declarations.Def _ -> false + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None + | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) @@ -1280,7 +1296,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp build_proof Evd.empty ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in - tclTHENLIST + observe_tclTHENLIST (str "") [ Simple.generalize [lemma]; Proofview.V82.of_tactic (Simple.intro hid); @@ -1340,7 +1356,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (tclFIRST (List.map (fun c -> - Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST + Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [intros; Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); Tacticals.New.tclCOMPLETE Auto.default_auto @@ -1402,13 +1418,13 @@ let start_equation (f:global_reference) (term_f:global_reference) let terminate_constr = constr_of_global term_f in let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in let x = n_x_id ids nargs in - tclTHENLIST [ + observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; observe_tac (str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); - observe_tac (str "prove_eq") (cont_tactic x)] g;; + observe_tac (str "prove_eq") (cont_tactic x)]) g;; let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 22ddd549..8b959c27 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -34,7 +34,7 @@ Extract Inductive sumor => option [ Some None ]. - rightmost choice (Inright) is (None) *) -(** To preserve its laziness, andb is normally expansed. +(** To preserve its laziness, andb is normally expanded. Let's rather use the ocaml && *) Extract Inlined Constant andb => "(&&)". diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 7400d462..a5f90dd6 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -13,10 +13,11 @@ (* *) (**************************************************************************) -(* We do not require [ZArith] anymore, but only what's necessary for Omega *) +(* We import what is necessary for Omega *) Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. + Declare ML Module "omega_plugin". Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l @@ -25,11 +26,6 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Require Export Zhints. -(* -(* The constant minus is required in coq_omega.ml *) -Require Minus. -*) - Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith. Hint Extern 10 (_ <= _) => abstract omega: zarith. Hint Extern 10 (_ < _) => abstract omega: zarith. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index 9e5c1484..9f101dbf 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -6,4 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* To strictly import the omega tactic *) + +Require ZArith_base. +Require OmegaLemmas. +Require PreOmega. + Declare ML Module "omega_plugin". diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v new file mode 100644 index 00000000..9f101dbf --- /dev/null +++ b/plugins/omega/OmegaTactic.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* - PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) in aux bodyi -- cgit v1.2.3