From fd19fbb3720f1f1d930dcd082ddcd021cb6e8b50 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 16:50:38 +0200 Subject: Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes QuicksortComplexity). --- pretyping/patternops.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 009b7323e4..9fb6ec9d11 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -171,7 +171,10 @@ let pattern_of_constr env sigma t = assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + | _ -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + remove := Evar.Set.union (evars_of_term ty) !remove; + PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; -- cgit v1.2.3 From b322c6131ab45be2d65ab2f6fcbcde7588314260 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 17:10:27 +0200 Subject: Strengthen minimization: it shouldn't set a universe u to a max if it has a strict upper bound. --- library/universes.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/universes.ml b/library/universes.ml index 51c2b4d851..9fddc7067b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -772,7 +772,7 @@ let minimize_univ_variables ctx us algs left right cstrs = else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs - with Option.IsNone -> assert false) + with Option.IsNone -> failwith "") cstrs dangling in (ctx', us, algs, insts, cstrs'), b @@ -784,7 +784,8 @@ let minimize_univ_variables ctx us algs left right cstrs = | None -> (* Nothing to do *) acc' (acc, (true, false, Universe.make u)) | Some lbound -> - acc' (instantiate_lbound lbound) + try acc' (instantiate_lbound lbound) + with Failure _ -> acc' (acc, (true, false, Universe.make u)) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u -- cgit v1.2.3 From f973052543cdd0f4c98366a7c2eefabeaf138afa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 17:32:36 +0200 Subject: Really fix constr_of_pattern and bugs #3590 and #4120 by removing all evars appearing in the constr (or their types, recursively) from the evar_map. --- pretyping/patternops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9fb6ec9d11..705e594af1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -167,13 +167,13 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (b,id) -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in ctx := (id,None,ty)::!ctx; - keep := Evar.Set.union (evars_of_term ty) !keep; + let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in - remove := Evar.Set.union (evars_of_term ty) !remove; + let () = ignore (pattern_of_constr env ty) in PMeta None) | Case (ci,p,a,br) -> let cip = -- cgit v1.2.3 From 968c8af13deaa3871aca7fc7086f1a5dc5769fde Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 17:34:09 +0200 Subject: Add test-suite file for bug #4120. --- test-suite/bugs/closed/4120.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/4120.v diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v new file mode 100644 index 0000000000..4164d86dc1 --- /dev/null +++ b/test-suite/bugs/closed/4120.v @@ -0,0 +1,6 @@ +Definition id {T} (x : T) := x. +Goal sigT (fun x => id x)%type. + change (fun x => ?f x) with f. + Unshelve. + exists Type. exact Set. +Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *) \ No newline at end of file -- cgit v1.2.3 From 6158ec51adc31814fde0293f54151c19a5f3b1e4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 17:49:42 +0200 Subject: Fix declarations of instances to perform restriction of universe instances as definitions and lemmas do (fixes bug# 4121). --- test-suite/bugs/closed/4121.v | 15 +++++++++++++++ toplevel/classes.ml | 9 +++++++-- toplevel/classes.mli | 2 +- 3 files changed, 23 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/4121.v diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v new file mode 100644 index 0000000000..5f8c411ca8 --- /dev/null +++ b/test-suite/bugs/closed/4121.v @@ -0,0 +1,15 @@ +(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) + +Set Universe Polymorphism. +Class Contr_internal (A : Type) := BuildContr { center : A }. +Arguments center A {_}. +Class Contr (A : Type) : Type := Contr_is_trunc : Contr_internal A. +Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances. +Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A |}. +Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}. +Check @contr_paths_contr0@{i}. +Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *) +(** It should have length 1, just like contr_paths_contr0 *) \ No newline at end of file diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 07f881721d..33891ad94c 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id poly uctx term termtype = let kind = IsDefinition Instance in + let uctx = + let levels = Univ.LSet.union (Universes.universes_of_constr termtype) + (Universes.universes_of_constr term) in + Universes.restrict_universe_context uctx levels + in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then - let ctx = Evd.universe_context evm in + let ctx = Evd.universe_context_set evm in declare_instance_constant k pri global imps ?hook id poly ctx (Option.get term) termtype else if !refine_instance || Option.is_empty term then begin diff --git a/toplevel/classes.mli b/toplevel/classes.mli index cb88ae564d..2b7e9e4fe2 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -32,7 +32,7 @@ val declare_instance_constant : ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) bool -> (* polymorphic *) - Univ.universe_context -> (* Universes *) + Univ.universe_context_set -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) Names.Id.t -- cgit v1.2.3 From 33650e275a4b3f00541ea87ee4b39892be5fdb2f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Apr 2015 18:33:07 +0200 Subject: Better test-suite files, removing reliance on admit. --- test-suite/bugs/closed/3590.v | 7 ++----- test-suite/bugs/closed/4120.v | 1 - 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v index 3440f0e806..3ef9270d40 100644 --- a/test-suite/bugs/closed/3590.v +++ b/test-suite/bugs/closed/3590.v @@ -1,13 +1,10 @@ -Require Import TestSuite.admit. -(* Set Primitive Projections. *) Set Implicit Arguments. Record prod A B := pair { fst : A ; snd : B }. Definition idS := Set. -Goal forall x y : prod Set Set, fst x = fst y. +Goal forall x y : prod Set Set, forall H : fst x = fst y, fst x = fst y. intros. change (@fst _ _ ?z) with (@fst Set idS z) at 2. - Unshelve. - admit. + apply H. Qed. (* Toplevel input, characters 20-58: diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v index 4164d86dc1..00db8f7f3c 100644 --- a/test-suite/bugs/closed/4120.v +++ b/test-suite/bugs/closed/4120.v @@ -1,6 +1,5 @@ Definition id {T} (x : T) := x. Goal sigT (fun x => id x)%type. change (fun x => ?f x) with f. - Unshelve. exists Type. exact Set. Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *) \ No newline at end of file -- cgit v1.2.3 From ba6f6500a948985b091cbf6a05d3631490465081 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 10 Apr 2015 15:13:37 +0200 Subject: Making the hints for the auto tactics private. They are all generated by the Hints module, and making them purely opaque is not worthwhile because we project them a lot. This ensures that they all get generated following a uniform process. --- tactics/hints.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/hints.mli b/tactics/hints.mli index 45cf562c05..42379b7c0c 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -40,7 +40,7 @@ type hints_path_atom = | PathHints of global_reference list | PathAny -type 'a gen_auto_tactic = { +type 'a gen_auto_tactic = private { pri : int; (** A number between 0 and 4, 4 = lower priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) -- cgit v1.2.3 From 9cd8bbc7808479c71e4413bc6f3555f494feda09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 10 Apr 2015 15:37:17 +0200 Subject: Eauto hints respect their priority. Fixes bug #3199. This patch changes the semantics of eauto w.r.t. to extern hints, so it may break some code out there. There is no compatibility flag because this is a real bug, and we do not really want the users to depend on this. Moreover, there are still some fishy parts in the current implementation that should be rewritten for the next release. --- tactics/eauto.ml4 | 40 +++++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 3d98bc6e19..1d89286af1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -184,7 +184,7 @@ and e_trivial_resolve db_list local_db gl = let e_possible_resolve db_list local_db gl = let hd = try Some (decompose_app_bound gl) with Bound -> None in - try List.map snd (e_my_find_search db_list local_db hd gl) + try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl) with Not_found -> [] let find_first_goal gls = @@ -194,6 +194,7 @@ let find_first_goal gls = exploration functor [Explore.Make]. *) type search_state = { + priority : int; depth : int; (*r depth of search before failing *) tacres : goal list sigma; last_tactic : std_ppcmds Lazy.t; @@ -221,12 +222,12 @@ module SearchProblem = struct (* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) let rec aux = function | [] -> [] - | (tac,pptac) :: tacl -> + | (tac, cost, pptac) :: tacl -> try let lgls = apply_tac_list tac glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) - (lgls,pptac) :: aux tacl + (lgls, cost, pptac) :: aux tacl with e when Errors.noncritical e -> let e = Errors.push e in Refiner.catch_failerror e; aux tacl @@ -236,8 +237,11 @@ module SearchProblem = struct number of remaining goals. *) let compare s s' = let d = s'.depth - s.depth in + let d' = Int.compare s.priority s'.priority in let nbgoals s = List.length (sig_it s.tacres) in - if not (Int.equal d 0) then d else nbgoals s - nbgoals s' + if not (Int.equal d' 0) then d' + else if not (Int.equal d 0) then d + else Int.compare (nbgoals s) (nbgoals s') let branching s = if Int.equal s.depth 0 then @@ -248,42 +252,39 @@ module SearchProblem = struct let nbgl = List.length (sig_it lg) in assert (nbgl > 0); let g = find_first_goal lg in + let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in let assumption_tacs = - let l = - filter_tactics s.tacres - (List.map - (fun id -> (e_give_exact (mkVar id), - lazy (str "exact" ++ spc () ++ pr_id id))) - (pf_ids_of_hyps g)) - in - List.map (fun (res,pp) -> { depth = s.depth; tacres = res; + let tacs = List.map map_assum (pf_ids_of_hyps g) in + let l = filter_tactics s.tacres tacs in + List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = List.tl s.localdb; prev = ps}) l in let intro_tac = + let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in List.map - (fun (lgls as res,pp) -> + (fun (lgls, cost, pp) -> let g' = first_goal lgls in let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in let ldb = Hint_db.add_list hintl (List.hd s.localdb) in - { depth = s.depth; tacres = res; + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) - (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")]) + l in let rec_tacs = let l = filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) in List.map - (fun (lgls as res, pp) -> + (fun (lgls, cost, pp) -> let nbgl' = List.length (sig_it lgls) in if nbgl' < nbgl then - { depth = s.depth; tacres = res; last_tactic = pp; prev = ps; - dblist = s.dblist; localdb = List.tl s.localdb } + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; + prev = ps; dblist = s.dblist; localdb = List.tl s.localdb } else let newlocal = let hyps = pf_hyps g in @@ -294,7 +295,7 @@ module SearchProblem = struct else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true []) (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) in - { depth = pred s.depth; tacres = res; + { depth = pred s.depth; priority = cost; tacres = lgls; dblist = s.dblist; last_tactic = pp; prev = ps; localdb = newlocal @ List.tl s.localdb }) l @@ -363,6 +364,7 @@ let pr_info dbg s = let make_initial_state dbg n gl dblist localdb = { depth = n; + priority = 0; tacres = tclIDTAC gl; last_tactic = lazy (mt()); dblist = dblist; -- cgit v1.2.3 From 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 10 Apr 2015 16:14:09 +0200 Subject: Test for bug #3199. --- test-suite/bugs/closed/3199.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test-suite/bugs/closed/3199.v diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v new file mode 100644 index 0000000000..08bf62493d --- /dev/null +++ b/test-suite/bugs/closed/3199.v @@ -0,0 +1,18 @@ +Axiom P : nat -> Prop. +Axiom admit : forall n : nat, P n -> P n -> n = S n. +Axiom foo : forall n, P n. + +Create HintDb bar. +Hint Extern 3 => symmetry : bar. +Hint Resolve admit : bar. +Hint Immediate foo : bar. + +Lemma qux : forall n : nat, n = S n. +Proof. +intros n. +eauto with bar. +Defined. + +Goal True. +pose (e := eq_refl (qux 0)); unfold qux in e. +match type of e with context [eq_sym] => fail 1 | _ => idtac end. -- cgit v1.2.3 From a86ae4d352cc8e4ac306f04d5536d7fff04d3303 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 10 Apr 2015 18:28:12 +0200 Subject: Fix #3590 for good this time, by changing the API, change's argument now takes a variable substitution for matched variables in the (lhs) pattern, and uses the existing ist structure to pretype the rhs correcly, without having to deal with the volatile evars. --- plugins/funind/recdef.ml | 2 +- tactics/equality.ml | 4 ++-- tactics/tacinterp.ml | 14 ++++++++++++-- tactics/tactics.ml | 19 ++++++++----------- tactics/tactics.mli | 3 ++- 5 files changed, 25 insertions(+), 17 deletions(-) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b1cbea51c8..86b5e414fe 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -675,7 +675,7 @@ let 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 diff --git a/tactics/equality.ml b/tactics/equality.ml index bcfd6657e0..7ab8d0c3ba 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1493,10 +1493,10 @@ let cutSubstInHyp l2r eqn id = tclTHENFIRST (tclTHENLIST [ (Proofview.Unsafe.tclEVARS sigma); - (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly)); + (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) - (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly)) + (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)) end let try_rewrite tac = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f894eb8fc4..5406832d2f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2119,7 +2119,12 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp sigma = + let c_interp patvars sigma = + let lfun' = Id.Map.fold (fun id c lfun -> + Id.Map.add id (Value.of_constr c) lfun) + patvars ist.lfun + in + let ist = { ist with lfun = lfun' } in if is_onhyps && is_onconcl then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c @@ -2139,7 +2144,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let env' = Environ.push_named_context sign env in - let c_interp sigma = + let c_interp patvars sigma = + let lfun' = Id.Map.fold (fun id c lfun -> + Id.Map.add id (Value.of_constr c) lfun) + patvars ist.lfun + in + let ist = { ist with lfun = lfun' } in try interp_constr ist env' sigma c with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b1559da33f..7484139c68 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -584,7 +584,10 @@ let e_change_in_hyp redfun (id,where) = (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)) convert_hyp -type change_arg = evar_map -> evar_map * constr +type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr + +let make_change_arg c = + fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c) let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -612,21 +615,15 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); sigma, t' -let change_and_check_subst cv_pb mayneedglobalcheck subst t env sigma c = - let t' sigma = - let sigma, t = t sigma in - sigma, replace_vars (Id.Map.bindings subst) t - in change_and_check cv_pb mayneedglobalcheck true t' env sigma c - (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb deep t where env sigma c = let mayneedglobalcheck = ref false in let sigma,c = match where with - | None -> change_and_check cv_pb mayneedglobalcheck deep t env sigma c + | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c | Some occl -> e_contextually false occl (fun subst -> - change_and_check_subst Reduction.CONV mayneedglobalcheck subst t) + change_and_check Reduction.CONV mayneedglobalcheck true (t subst)) env sigma c in if !mayneedglobalcheck then begin @@ -656,7 +653,7 @@ let change chg c cls gl = cls) gl let change_concl t = - change_in_concl None (fun sigma -> sigma, t) + change_in_concl None (make_change_arg t) (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl (red_product,REVERTcast) @@ -2769,7 +2766,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = if Int.equal i nparams then let t = applist (hd, params@args) in Tacticals.New.tclTHEN - (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly)) + (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly)) (tac avoid) else let c = List.nth argl (i-1) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eea4956214..0069d100b7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -125,8 +125,9 @@ val exact_proof : Constrexpr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr -type change_arg = evar_map -> evar_map * constr +type change_arg = patvar_map -> evar_map -> evar_map * constr +val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic -- cgit v1.2.3 From b3192497979a57a6078b2ecdb0d8b546cb100ffa Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 10 Apr 2015 19:22:12 +0200 Subject: Fix compilation broken by Matthieu's last commit. Btw, also unset the READABLE_ML4 option, which probably caused this issue. No, we normally do *not* want to see the internals of .ml generated out of a .ml4 (except during some specific debug sessions). It is *so* easy otherwise to edit the wrong .ml by mistake and forget to edit the original .ml4. --- Makefile.build | 2 +- tactics/eauto.ml4 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile.build b/Makefile.build index 57c22c6588..018471b684 100644 --- a/Makefile.build +++ b/Makefile.build @@ -59,7 +59,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES)) VERBOSE= NO_RECOMPILE_ML4= NO_RECALC_DEPS= -READABLE_ML4=true # non-empty means .ml of .ml4 will be ascii instead of binary +READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library VM= # is "-no-vm" to not use the vm" diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 1d89286af1..7af43e6062 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -568,7 +568,7 @@ let autounfold_one db cl = in if did then match cl with - | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp + | Some hyp -> change_in_hyp None (make_change_arg c') hyp | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end -- cgit v1.2.3 From 91172e9c3a1430c3be3ad1080d2da68b25d940aa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Apr 2015 21:13:51 +0200 Subject: Making the hint entry type opaque. --- tactics/hints.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tactics/hints.mli b/tactics/hints.mli index 42379b7c0c..9a781c722c 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -54,8 +54,7 @@ type search_entry (** The head may not be bound. *) -type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) gen_auto_tactic +type hint_entry type hints_path = | PathAtom of hints_path_atom -- cgit v1.2.3 From 914095183c54a35909c5c31b376e816859a594aa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 13 Apr 2015 08:48:20 +0200 Subject: Fixing bug #4186. --- plugins/extraction/ExtrOcamlNatInt.v | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 5f653ee109..a0930f15f4 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 searchtable_add (name, Hint_db.empty st b) | AddTransparency (grs, b) -> add_transparency name grs b | AddHints hints -> add_hint name hints @@ -793,7 +798,7 @@ let cache_autohint (_,(local,name,hints)) = | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m -let subst_autohint (subst,(local,name,hintlist as obj)) = +let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in let gr' = @@ -835,29 +840,30 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = in if k' == k && data' == data then hint else (k',data') in - match hintlist with - | CreateDB _ -> obj + let action = match obj.hint_action with + | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in - if grs==grs' then obj else (local, name, AddTransparency (grs', b)) + let grs' = List.smartmap (subst_evaluable_reference subst) grs in + if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in - if hintlist' == hintlist then obj else - (local,name,AddHints hintlist') + let hintlist' = List.smartmap subst_hint hintlist in + if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in - if grs==grs' then obj else (local, name, RemoveHints grs') + let grs' = List.smartmap (subst_global_reference subst) grs in + if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in - if path' == path then obj else (local, name, AddCut path') + if path' == path then obj.hint_action else AddCut path' | AddMode (l,m) -> let l' = subst_global_reference subst l in - (local, name, AddMode (l', m)) + if l' == l then obj.hint_action else AddMode (l', m) + in + if action == obj.hint_action then obj else { obj with hint_action = action } -let classify_autohint ((local,name,hintlist) as obj) = - match hintlist with +let classify_autohint obj = + match obj.hint_action with | AddHints [] -> Dispose - | _ -> if local then Dispose else Substitute obj + | _ -> if obj.hint_local then Dispose else Substitute obj let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with @@ -866,14 +872,22 @@ let inAutoHint : hint_obj -> obj = subst_function = subst_autohint; classify_function = classify_autohint; } +let make_hint ?(local = false) name action = { + hint_local = local; + hint_name = name; + hint_action = action; +} + let create_hint_db l n st b = - Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st))) + let hint = make_hint ~local:l n (CreateDB (b, st)) in + Lib.add_anonymous_leaf (inAutoHint hint) let remove_hints local dbnames grs = let dbnames = if List.is_empty dbnames then ["core"] else dbnames in List.iter (fun dbname -> - Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs))) + let hint = make_hint ~local dbname (RemoveHints grs) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames (**************************************************************************) @@ -882,37 +896,42 @@ let remove_hints local dbnames grs = let add_resolves env sigma clist local dbnames = List.iter (fun dbname -> - Lib.add_anonymous_leaf - (inAutoHint - (local,dbname, AddHints - (List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,Flags.is_verbose()) - pri poly ~name:path gr) clist))))) + let r = + List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> + make_resolves env sigma (true,hnf,Flags.is_verbose()) + pri poly ~name:path gr) clist) + in + let hint = make_hint ~local dbname (AddHints r) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_unfolds l local dbnames = List.iter - (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, AddHints (List.map make_unfold l)))) + (fun dbname -> + let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_cuts l local dbnames = List.iter - (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, AddCut l))) + (fun dbname -> + let hint = make_hint ~local dbname (AddCut l) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_mode l m local dbnames = List.iter - (fun dbname -> Lib.add_anonymous_leaf - (let m' = make_mode l m in - (inAutoHint (local,dbname, AddMode (l,m'))))) + (fun dbname -> + let m' = make_mode l m in + let hint = make_hint ~local dbname (AddMode (l, m')) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_transparency l b local dbnames = List.iter - (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, AddTransparency (l, b)))) + (fun dbname -> + let hint = make_hint ~local dbname (AddTransparency (l, b)) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_extern pri pat tacast local dbname = @@ -920,7 +939,7 @@ let add_extern pri pat tacast local dbname = | None -> None | Some (_, pat) -> Some pat in - let hint = local, dbname, AddHints [make_extern pri pat tacast] in + let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in Lib.add_anonymous_leaf (inAutoHint hint) let add_externs pri pat tacast local dbnames = @@ -929,9 +948,9 @@ let add_externs pri pat tacast local dbnames = let add_trivials env sigma l local dbnames = List.iter (fun dbname -> - Lib.add_anonymous_leaf ( - inAutoHint(local,dbname, - AddHints (List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l)))) + let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in + let hint = make_hint ~local dbname (AddHints l) in + Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let (forward_intern_tac, extern_intern_tac) = Hook.make () -- cgit v1.2.3 From 546e2454f244340694f8fca460598499359afe28 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Apr 2015 16:40:16 +0200 Subject: Remove declarations of matched variables in change as an extension of the context... overlooked by my last commit. Fixes relation-algebra. --- tactics/tacinterp.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5406832d2f..f29680e185 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2143,14 +2143,13 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.tactic begin fun gl -> let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let env' = Environ.push_named_context sign env in let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in - try interp_constr ist env' sigma c + try interp_constr ist env sigma c with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in -- cgit v1.2.3 From a3d686a3bd1ac4256279a77c291949a3b15abc18 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Apr 2015 16:44:22 +0200 Subject: Program: Do not reduce obligation types preemptively, only at definition time. The obligation tactic or user can still choose to do so. --- toplevel/obligations.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 456a6f9d0f..523134b50f 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -658,7 +658,7 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls Array.mapi (fun i (n, t, l, o, d, tac) -> { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; + obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in -- cgit v1.2.3 From 7f49f829260078f76c5b219472afb4fa1abce5f9 Mon Sep 17 00:00:00 2001 From: jforest Date: Mon, 13 Apr 2015 22:16:30 +0200 Subject: correction of a bug reported by Tristan Crolard --- plugins/funind/functional_principles_proofs.ml | 60 ++++++++++++++------------ 1 file changed, 33 insertions(+), 27 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 04347537f2..5ccc4b27aa 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -44,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 = @@ -68,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 = @@ -1099,17 +1101,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 @@ -1189,7 +1191,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 @@ -1203,7 +1206,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 @@ -1211,10 +1217,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 = -- cgit v1.2.3 From dc29a85d428d95fa3a3b1d30373f353436bf04a9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 13 Apr 2015 13:44:49 +0200 Subject: Opaque implementation of auto tactics. We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility. --- plugins/firstorder/sequent.ml | 2 +- tactics/auto.ml | 5 ++--- tactics/class_tactics.ml | 23 +++++++++++------------ tactics/eauto.ml4 | 22 +++++++++++----------- tactics/hints.ml | 13 +++++++++---- tactics/hints.mli | 15 ++++++++++++--- 6 files changed, 46 insertions(+), 34 deletions(-) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2f7f21e418..7d034db552 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/tactics/auto.ml b/tactics/auto.ml index 45052685df..46274f8329 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -359,8 +359,7 @@ and my_find_search_delta db_list local_db hdc concl = (local_db::db_list) and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) = - let tactic = - match t with + let tactic = function | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") | Give_exact (c, cl) -> exact poly (c, cl) @@ -378,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_autotactic t) tactic + tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic) and trivial_resolve dbg mod_delta db_list local_db cl = try diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 98266a4b6c..e11458c049 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -221,20 +221,19 @@ and e_my_find_search db_list local_db hdc complete sigma concl = in let tac_of_hint = fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> - let tac = - match t with - | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags) - | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags) - | Give_exact c -> e_give_exact flags poly c - | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) - (if complete then tclIDTAC else e_trivial_fail_db db_list local_db) - | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]) - | Extern tacast -> - Proofview.V82.of_tactic (conclPattern concl p tacast) + let tac = function + | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags)) + | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) + | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) + | Res_pf_THEN_trivial_fail (term,cl) -> + Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) + (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) + | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) + | Extern tacast -> conclPattern concl p tacast in + let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in let tac = if complete then tclCOMPLETE tac else tac in - match t with + match repr_auto_tactic t with | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) | _ -> (* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 7af43e6062..27c3569daf 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -162,18 +162,18 @@ and e_my_find_search db_list local_db hdc concl = let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> (b, - let tac = - match t with - | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl)) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> e_exact poly st (c,cl) - | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve poly st (term,cl)) - (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast) + let tac = function + | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl)) + | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl)) + | Res_pf_THEN_trivial_fail (term,cl) -> + Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl)) + (e_trivial_fail_db db_list local_db)) + | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) + | Extern tacast -> conclPattern concl p tacast in - (tac,lazy (pr_autotactic t))) + let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + (tac, lazy (pr_autotactic t))) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index bbd66dfd43..cf1754e381 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -68,7 +68,7 @@ let decompose_app_bound t = (* The Type of Constructions Autotactic Hints *) (************************************************************************) -type 'a auto_tactic = +type 'a auto_tactic_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -92,18 +92,23 @@ type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set +type 'a auto_tactic = 'a auto_tactic_ast + type 'a gen_auto_tactic = { pri : int; (* A number lower is higher priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) name : hints_path_atom; (* A potential name to refer to the hint *) - code : 'a auto_tactic (* the tactic to apply when the concl matches pat *) + code : 'a (* the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) gen_auto_tactic +type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) gen_auto_tactic + (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic + +let run_auto_tactic tac k = k tac +let repr_auto_tactic tac = tac let eq_hints_path_atom p1 p2 = match p1, p2 with | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 diff --git a/tactics/hints.mli b/tactics/hints.mli index 9a781c722c..958cca1c3b 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array (** Pre-created hint databases *) -type 'a auto_tactic = +type 'a auto_tactic_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -36,6 +36,8 @@ type 'a auto_tactic = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) +type 'a auto_tactic + type hints_path_atom = | PathHints of global_reference list | PathAny @@ -45,10 +47,10 @@ type 'a gen_auto_tactic = private { poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) name : hints_path_atom; (** A potential name to refer to the hint *) - code : 'a auto_tactic; (** the tactic to apply when the concl matches pat *) + code : 'a; (** the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) gen_auto_tactic +type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic type search_entry @@ -195,6 +197,13 @@ val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr -> hint_entry +val run_auto_tactic : 'a auto_tactic -> + ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic + +(** This function is for backward compatibility only, not to use in newly + written code. *) +val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast + val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t -- cgit v1.2.3 From b1970f8644b32ae3069d6ef539d51e4f4576dc36 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Apr 2015 09:12:53 +0200 Subject: Cleaning up the implementation of search entries in Hints. --- tactics/hints.ml | 99 ++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 60 insertions(+), 39 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index cf1754e381..dea47794ec 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -161,10 +161,19 @@ module Bounded_net = Btermdn.Make(struct let compare = pri_order_int end) -type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list - +type search_entry = { + sentry_nopat : stored_data list; + sentry_pat : stored_data list; + sentry_bnet : Bounded_net.t; + sentry_mode : bool array list; +} -let empty_se = ([],[],Bounded_net.create (),[]) +let empty_se = { + sentry_nopat = []; + sentry_pat = []; + sentry_bnet = Bounded_net.create (); + sentry_mode = []; +} let eq_pri_auto_tactic (_, x) (_, y) = if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then @@ -182,27 +191,29 @@ let eq_pri_auto_tactic (_, x) (_, y) = else false -let add_tac pat t st (l,l',dn,m) = +let add_tac pat t st se = match pat with | None -> - if not (List.exists (eq_pri_auto_tactic t) l) then (List.insert pri_order t l, l', dn, m) - else (l, l', dn, m) + if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se + else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat } | Some pat -> - if not (List.exists (eq_pri_auto_tactic t) l') - then (l, List.insert pri_order t l', Bounded_net.add st dn (pat,t), m) else (l, l', dn, m) + if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se + else { se with + sentry_pat = List.insert pri_order t se.sentry_pat; + sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); } -let rebuild_dn st ((l,l',dn,m) : search_entry) = +let rebuild_dn st se = let dn' = List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) - (Bounded_net.create ()) l' + (Bounded_net.create ()) se.sentry_pat in - (l, l', dn', m) + { se with sentry_bnet = dn' } -let lookup_tacs concl st (l,l',dn) = - let l' = Bounded_net.lookup st dn concl in +let lookup_tacs concl st se = + let l' = Bounded_net.lookup st se.sentry_bnet concl in let sl' = List.stable_sort pri_order_int l' in - List.merge pri_order_int l sl' + List.merge pri_order_int se.sentry_nopat sl' module Constr_map = Map.Make(RefOrdered) @@ -416,34 +427,38 @@ module Hint_db = struct if List.is_empty modes then true else List.exists (matches_mode args) modes + let merge_entry db nopat pat = + let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in + List.map realize_tac h + let map_none db = - List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) []) - + merge_entry db [] [] + let map_all k db = - let (l,l',_,_) = find k db in - List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l') + let se = find k db in + merge_entry db se.sentry_nopat se.sentry_pat (** Precondition: concl has no existentials *) let map_auto (k,args) concl db = - let (l,l',dn,m) = find k db in + let se = find k db in let st = if db.use_dn then (Some db.hintdb_state) else None in - let l' = lookup_tacs concl st (l,l',dn) in - List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l') + let pat = lookup_tacs concl st se in + merge_entry db [] pat let map_existential (k,args) concl db = - let (l,l',_,m) = find k db in - if matches_modes args m then - List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l') - else List.map realize_tac (List.map snd db.hintdb_nopat) + let se = find k db in + if matches_modes args se.sentry_mode then + merge_entry db se.sentry_nopat se.sentry_pat + else merge_entry db [] [] (* [c] contains an existential *) let map_eauto (k,args) concl db = - let (l,l',dn,m) = find k db in - if matches_modes args m then - let st = if db.use_dn then Some db.hintdb_state else None in - let l' = lookup_tacs concl st (l,l',dn) in - List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l') - else List.map realize_tac (List.map snd db.hintdb_nopat) + let se = find k db in + if matches_modes args se.sentry_mode then + let st = if db.use_dn then Some db.hintdb_state else None in + let pat = lookup_tacs concl st se in + merge_entry db [] pat + else merge_entry db [] [] let is_exact = function | Give_exact _ -> true @@ -501,10 +516,12 @@ module Hint_db = struct let add_list l db = List.fold_left (fun db k -> add_one k db) db l let remove_sdl p sdl = List.smartfilter p sdl - let remove_he st p (sl1, sl2, dn, m as he) = - let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in - if sl1' == sl1 && sl2' == sl2 then he - else rebuild_dn st (sl1', sl2', dn, m) + + let remove_he st p se = + let sl1' = remove_sdl p se.sentry_nopat in + let sl2' = remove_sdl p se.sentry_pat in + if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se + else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' } let remove_list grs db = let filter (_, h) = @@ -515,13 +532,16 @@ module Hint_db = struct let remove_one gr db = remove_list [gr] db + let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat) + let iter f db = + let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat); - Constr_map.iter (fun k (l,l',_,m) -> f (Some k) m (List.map realize_tac (l@l'))) db.hintdb_map + Constr_map.iter iter_se db.hintdb_map let fold f db accu = let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in - Constr_map.fold (fun k (l,l',_,m) -> f (Some k) m (List.map snd (l@l'))) db.hintdb_map accu + Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu let transparent_state db = db.hintdb_state @@ -533,8 +553,9 @@ module Hint_db = struct { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) } let add_mode gr m db = - let (l,l',dn,ms) = find gr db in - { db with hintdb_map = Constr_map.add gr (l,l',dn,m :: ms) db.hintdb_map } + let se = find gr db in + let se = { se with sentry_mode = m :: se.sentry_mode } in + { db with hintdb_map = Constr_map.add gr se db.hintdb_map } let cut db = db.hintdb_cut -- cgit v1.2.3 From efbc8eef69dd66c51d7f4b666d7b3ffeb99a35c7 Mon Sep 17 00:00:00 2001 From: jforest Date: Tue, 14 Apr 2015 20:50:31 +0200 Subject: better debug in recdef --- plugins/funind/recdef.ml | 108 +++++++++++++++++++++++++++-------------------- 1 file changed, 62 insertions(+), 46 deletions(-) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 86b5e414fe..0999b95d71 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -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,7 +683,7 @@ 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 @@ -681,7 +693,7 @@ let mkDestructEq : 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 -> @@ -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 -- cgit v1.2.3 From 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 Mon Sep 17 00:00:00 2001 From: jforest Date: Thu, 9 Apr 2015 22:19:31 +0200 Subject: Function now supports puniveres --- interp/constrintern.mli | 1 + plugins/funind/functional_principles_proofs.ml | 61 +-- plugins/funind/functional_principles_proofs.mli | 1 + plugins/funind/functional_principles_types.ml | 111 ++--- plugins/funind/functional_principles_types.mli | 6 +- plugins/funind/g_indfun.ml4 | 6 +- plugins/funind/glob_term_to_relation.ml | 38 +- plugins/funind/glob_term_to_relation.mli | 7 +- plugins/funind/indfun.ml | 220 ++++++---- plugins/funind/indfun_common.ml | 6 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/invfun.ml | 511 ++++++------------------ 12 files changed, 405 insertions(+), 565 deletions(-) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 792e6f6322..0d33d43345 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -174,6 +174,7 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) +val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool val construct_reference : named_context -> Id.t -> constr val global_reference : Id.t -> constr diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5ccc4b27aa..4a832435f8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -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(Transparent,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 @@ -1254,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)) @@ -1263,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 ff98f2b97f..61fce267a3 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 deaf603ef0..45e5aaf545 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -105,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) = @@ -115,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 @@ -233,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, @@ -243,47 +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 - let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in Lemmas.start_proof new_princ_name - (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - evd - 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 + 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,_ = KerName.repr (Constant.canonical 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,12 +496,12 @@ 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 @@ -519,7 +523,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis in incr i; let opacity = - let finfos = find_Function_infos first_fun 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 a16b834f89..f6e5578d2e 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 fd48ab59fb..043d4328c4 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 f6a543a1c6..9e3f398633 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -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,23 +1252,21 @@ 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 = @@ -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 b0a05ec322..5bb1376e26 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 2730fd421a..e211b68837 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -28,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 = @@ -115,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 @@ -221,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 @@ -292,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 = @@ -302,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 @@ -327,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)|]) ) @@ -351,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 @@ -399,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 ); @@ -550,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 = @@ -565,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 @@ -588,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 @@ -614,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 () @@ -773,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) ) ) () @@ -811,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 76f8c6d219..738ade8ca3 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 67ddf3741f..10daf6e848 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 0ee8877082..d9ae87ecc1 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -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~: @@ -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,9 @@ 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 -> + Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g)); + Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) g @@ -436,13 +387,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 +410,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,13 +420,14 @@ 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 + Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type); tclTHENSEQ [ observe_tac "principle" (Proofview.V82.of_tactic (assert_by @@ -484,10 +438,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 +450,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 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 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 - 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 +466,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 +748,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = g - - -let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,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 +755,28 @@ let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,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 +785,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 +871,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 +1002,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 -- cgit v1.2.3