diff options
Diffstat (limited to 'contrib/subtac')
29 files changed, 1438 insertions, 1434 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v deleted file mode 100644 index f047b729..00000000 --- a/contrib/subtac/FixSub.v +++ /dev/null @@ -1,147 +0,0 @@ -Require Import Wf. -Require Import Coq.subtac.Utils. - -(** Reformulation of the Wellfounded module using subsets where possible. *) - -Section Well_founded. - Variable A : Type. - Variable R : A -> A -> Prop. - Hypothesis Rwf : well_founded R. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := - F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) - (Acc_inv r (proj1_sig y) (proj2_sig y))). - - Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g. - - Lemma Fix_F_eq : - forall (x:A) (r:Acc R x), - F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r. - Proof. - destruct r using Acc_inv_dep; auto. - Qed. - - Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. - Proof. - intro x; induction (Rwf x); intros. - rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. - apply F_ext; auto. - intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. - Qed. - - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)). - Proof. - intro x; unfold Fix in |- *. - rewrite <- (Fix_F_eq ). - apply F_ext; intros. - apply Fix_F_inv. - Qed. - - Lemma fix_sub_eq : - forall x : A, - Fix_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun {y : A | R y x}=> Fix (`y)). - exact Fix_eq. - Qed. - - End FixPoint. - -End Well_founded. - -Extraction Inline Fix_F_sub Fix_sub. - -Require Import Wf_nat. -Require Import Lt. - -Section Well_founded_measure. - Variable A : Type. - Variable m : A -> nat. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. - - Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (m (proj1_sig y)) (proj2_sig y))). - - Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). - - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. - - Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)), - (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. - - Lemma Fix_measure_F_eq : - forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r. - Proof. - intros x. - set (y := m x). - unfold Fix_measure_F_sub. - intros r ; case r ; auto. - Qed. - - Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. - Proof. - intros x r s. - rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. - Qed. - - Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). - Proof. - intro x; unfold Fix_measure in |- *. - rewrite <- (Fix_measure_F_eq ). - apply F_ext; intros. - apply Fix_measure_F_inv. - Qed. - - Lemma fix_measure_sub_eq : - forall x : A, - Fix_measure_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun {y : A | m y < m x}=> Fix_measure (`y)). - exact Fix_measure_eq. - Qed. - - End FixPoint. - -End Well_founded_measure. - -Extraction Inline Fix_measure_F_sub Fix_measure_sub. diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v deleted file mode 100644 index 4610f346..00000000 --- a/contrib/subtac/FunctionalExtensionality.v +++ /dev/null @@ -1,47 +0,0 @@ -Lemma equal_f : forall A B : Type, forall (f g : A -> B), - f = g -> forall x, f x = g x. -Proof. - intros. - rewrite H. - auto. -Qed. - -Axiom fun_extensionality : forall A B (f g : A -> B), - (forall x, f x = g x) -> f = g. - -Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), - (forall x, f x = g x) -> f = g. - -Hint Resolve fun_extensionality fun_extensionality_dep : subtac. - -Require Import Coq.subtac.Utils. -Require Import Coq.subtac.FixSub. - -Lemma fix_sub_eq_ext : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) - (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x), - forall x : A, - Fix_sub A R Rwf P F_sub x = - F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)). -Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). - apply (fun_extensionality_dep _ _ _ _ H). - rewrite H0 ; auto. -Qed. - -Lemma fix_sub_measure_eq_ext : - forall (A : Type) (f : A -> nat) (P : A -> Type) - (F_sub : forall x : A, (forall {y : A | f y < f x}, P (`y)) -> P x), - forall x : A, - Fix_measure_sub A f P F_sub x = - F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)). -Proof. - intros ; apply Fix_measure_eq ; auto. - intros. - assert(f0 = g). - apply (fun_extensionality_dep _ _ _ _ H). - rewrite H0 ; auto. -Qed. diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v deleted file mode 100644 index f2b216d9..00000000 --- a/contrib/subtac/Heq.v +++ /dev/null @@ -1,34 +0,0 @@ -Require Export JMeq. - -(** Notation for heterogenous equality. *) - -Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). - -(** Do something on an heterogeneous equality appearing in the context. *) - -Ltac on_JMeq tac := - match goal with - | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H - end. - -(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) - -Ltac simpl_one_JMeq := - on_JMeq - ltac:(fun H => let H' := fresh "H" in - assert (H' := JMeq_eq H) ; clear H ; rename H' into H). - -(** Repeat it for every possible hypothesis. *) - -Ltac simpl_JMeq := repeat simpl_one_JMeq. - -(** Just simplify an h.eq. without clearing it. *) - -Ltac simpl_one_dep_JMeq := - on_JMeq - ltac:(fun H => let H' := fresh "H" in - assert (H' := JMeq_eq H)). - - - - diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v deleted file mode 100644 index 9912cd24..00000000 --- a/contrib/subtac/Subtac.v +++ /dev/null @@ -1,2 +0,0 @@ -Require Export Coq.subtac.Utils. -Require Export Coq.subtac.FixSub.
\ No newline at end of file diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v deleted file mode 100644 index a00234dd..00000000 --- a/contrib/subtac/SubtacTactics.v +++ /dev/null @@ -1,158 +0,0 @@ -Ltac induction_with_subterm c H := - let x := fresh "x" in - let y := fresh "y" in - (remember c as x ; rewrite <- y in H ; induction H ; subst). - -Ltac induction_on_subterm c := - let x := fresh "x" in - let y := fresh "y" in - (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; - clear y). - -Ltac induction_with_subterms c c' H := - let x := fresh "x" in - let y := fresh "y" in - let z := fresh "z" in - let w := fresh "w" in - (set(x := c) ; assert(y:x = c) by reflexivity ; - set(z := c') ; assert(w:z = c') by reflexivity ; - rewrite <- y in H ; rewrite <- w in H ; - induction H ; subst). - - -Ltac destruct_one_pair := - match goal with - | [H : (_ /\ _) |- _] => destruct H - | [H : prod _ _ |- _] => destruct H - end. - -Ltac destruct_pairs := repeat (destruct_one_pair). - -Ltac destruct_one_ex := - let tac H := let ph := fresh "H" in destruct H as [H ph] in - match goal with - | [H : (ex _) |- _] => tac H - | [H : (sig ?P) |- _ ] => tac H - | [H : (ex2 _) |- _] => tac H - end. - -Ltac destruct_exists := repeat (destruct_one_ex). - -Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. - -Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. - -Tactic Notation "contradiction" "by" constr(t) := - let H := fresh in assert t as H by auto with * ; contradiction. - -Ltac discriminates := - match goal with - | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity - | _ => discriminate - end. - -Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). - -Ltac on_last_hyp tac := - match goal with - [ H : _ |- _ ] => tac H - end. - -Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. - -Ltac revert_last := - match goal with - [ H : _ |- _ ] => revert H - end. - -Ltac reverse := repeat revert_last. - -Ltac on_call f tac := - match goal with - | H : ?T |- _ => - match T with - | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) - | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) - | context [f ?x ?y ?z ?w] => tac (f x y z w) - | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) - | context [f ?x] => tac (f x) - end - | |- ?T => - match T with - | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) - | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) - | context [f ?x ?y ?z ?w] => tac (f x y z w) - | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) - | context [f ?x] => tac (f x) - end - end. - -(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) -Ltac destruct_call f := - let tac t := destruct t in on_call f tac. - -Ltac destruct_call_as f l := - let tac t := destruct t as l in on_call f tac. - -Tactic Notation "destruct_call" constr(f) := destruct_call f. -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. - -Ltac myinjection := - let tac H := inversion H ; subst ; clear H in - match goal with - | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H - | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H - | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H - | _ => idtac - end. - -Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. - -Ltac bang := - match goal with - | |- ?x => - match x with - | context [False_rect _ ?p] => elim p - end - end. - -Require Import Eqdep. - -Ltac elim_eq_rect := - match goal with - | [ |- ?t ] => - match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; - try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; - try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. - -Ltac real_elim_eq_rect := - match goal with - | [ |- ?t ] => - match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. -
\ No newline at end of file diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v deleted file mode 100644 index 76f49dd3..00000000 --- a/contrib/subtac/Utils.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Export Coq.subtac.SubtacTactics. - -Set Implicit Arguments. - -(** Wrap a proposition inside a subset. *) - -Notation " {{ x }} " := (tt : { y : unit | x }). - -(** A simpler notation for subsets defined on a cartesian product. *) - -Notation "{ ( x , y ) : A | P }" := - (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident) : type_scope. - -(** Generates an obligation to prove False. *) - -Notation " ! " := (False_rect _ _). - -(** Abbreviation for first projection and hiding of proofs of subset objects. *) - -Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. - -(** Coerces objects to their support before comparing them. *) - -Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). - -(** Quantifying over subsets. *) - -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). - -Notation "'forall' { x : A | P } , Q" := - (forall x:{x:A|P}, Q) - (at level 200, x ident, right associativity). - -Require Import Coq.Bool.Sumbool. - -(** Construct a dependent disjunction from a boolean. *) - -Notation "'dec'" := (sumbool_of_bool) (at level 0). - -(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) - -Notation in_right := (@right _ _ _). -Notation in_left := (@left _ _ _). - -(** Default simplification tactic. *) - -Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; - try (solve [ red ; intros ; discriminate ]) ; auto with *. - -(** Extraction directives *) -Extraction Inline proj1_sig. -Extract Inductive unit => "unit" [ "()" ]. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) -(* Extract Inductive sigT => "prod" [ "" ]. *) - -Require Export ProofIrrelevance. -Require Export Coq.subtac.Heq. - -Delimit Scope program_scope with program. diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 2a84fdd0..9bfb33ea 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -14,17 +14,21 @@ open Util open Subtac_utils let trace s = - if !Options.debug then (msgnl s; msgerr s) + if !Flags.debug then (msgnl s; msgerr s) else () +let succfix (depth, fixrels) = + (succ depth, List.map succ fixrels) + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) let subst_evar_constr evs n t = let seen = ref Intset.empty in + let transparent = ref Idset.empty in let evar_info id = List.assoc id evs in - let rec substrec depth c = match kind_of_term c with + let rec substrec (depth, fixrels) c = match kind_of_term c with | Evar (k, args) -> - let (id, idstr), hyps, chop, _, _ = + let (id, idstr), hyps, chop, _, _, _ = try evar_info k with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") @@ -42,7 +46,7 @@ let subst_evar_constr evs n t = let rec aux hyps args acc = match hyps, args with ((_, None, _) :: tlh), (c :: tla) -> - aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc) + aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc @@ -53,11 +57,15 @@ let subst_evar_constr evs n t = int (List.length hyps) ++ str " hypotheses" ++ spc () ++ pp_list (fun x -> my_print_constr (Global.env ()) x) args); with _ -> ()); + if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then + transparent := Idset.add idstr !transparent; mkApp (mkVar idstr, Array.of_list args) - | _ -> map_constr_with_binders succ substrec depth c + | Fix _ -> + map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c + | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c in - let t' = substrec 0 t in - t', !seen + let t' = substrec (0, []) t in + t', !seen, !transparent (** Substitute variable references in t using De Bruijn indices, @@ -74,26 +82,29 @@ let subst_vars acc n t = to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. A little optimization: don't include unnecessary let-ins and their dependencies. -*) +*) let etype_of_evar evs hyps concl = let rec aux acc n = function (id, copt, t) :: tl -> - let t', s = subst_evar_constr evs n t in + let t', s, trans = subst_evar_constr evs n t in let t'' = subst_vars acc 0 t' in - let rest, s' = aux (id :: acc) (succ n) tl in + let rest, s', trans' = aux (id :: acc) (succ n) tl in let s' = Intset.union s s' in + let trans' = Idset.union trans trans' in (match copt with Some c -> - if noccurn 1 rest then lift (-1) rest, s' + if noccurn 1 rest then lift (-1) rest, s', trans' else - let c', s'' = subst_evar_constr evs n c in + let c', s'', trans'' = subst_evar_constr evs n c in let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s' + mkNamedProd_or_LetIn (id, Some c', t'') rest, + Intset.union s'' s', + Idset.union trans'' trans' | None -> - mkNamedProd_or_LetIn (id, None, t'') rest, s') + mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') | [] -> - let t', s = subst_evar_constr evs n concl in - subst_vars acc 0 t', s + let t', s, trans = subst_evar_constr evs n concl in + subst_vars acc 0 t', s, trans in aux [] 0 (rev hyps) @@ -110,12 +121,14 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let eterm_obligations name nclen isevars evm fs t tycon = +let eterm_obligations env name isevars evm fs t ty = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) trace (str " In eterm: isevars: " ++ my_print_evardefs isevars); trace (str "Term given to eterm" ++ spc () ++ Termops.print_constr_env (Global.env ()) t); + let nc = Environ.named_context env in + let nc_len = Sign.named_context_length nc in let evl = List.rev (to_list evm) in let evn = let i = ref (-1) in @@ -128,9 +141,9 @@ let eterm_obligations name nclen isevars evm fs t tycon = (* Remove existential variables in types and build the corresponding products *) fold_right (fun (id, (n, nstr), ev) l -> - let hyps = Environ.named_context_of_val ev.evar_hyps in - let hyps = trunc_named_context nclen hyps in - let evtyp, deps = etype_of_evar l hyps ev.evar_concl in + let hyps = Evd.evar_filtered_context ev in + let hyps = trunc_named_context nc_len hyps in + let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with Some t -> @@ -145,26 +158,28 @@ let eterm_obligations name nclen isevars evm fs t tycon = let loc, k = evar_source id isevars in let opacity = match k with QuestionMark o -> o | _ -> true in let opaque = if not opacity || chop <> fs then None else Some chop in - let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in + let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in y' :: l) evn [] in - let t', _ = (* Substitute evar refs in the term by variables *) + let t', _, transparent = (* Substitute evar refs in the term by variables *) subst_evar_constr evts 0 t in + let ty, _, _ = subst_evar_constr evts 0 ty in let evars = - List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts + List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> + name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts in (try trace (str "Term constructed in eterm" ++ spc () ++ Termops.print_constr_env (Global.env ()) t'); ignore(iter - (fun (name, typ, _, deps) -> + (fun (name, typ, _, _, deps) -> trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ Termops.print_constr_env (Global.env ()) typ)) evars); with _ -> ()); - Array.of_list (List.rev evars), t' + Array.of_list (List.rev evars), t', ty let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 76994c06..007e327c 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) - +(*i $Id: eterm.mli 10889 2008-05-06 14:05:20Z msozeau $ i*) +open Environ open Tacmach open Term open Evd @@ -18,10 +18,11 @@ val mkMetas : int -> constr list (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) -(* id, named context length, evars, number of - function prototypes to try to clear from evars contexts, object and optional type *) -val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> - (identifier * types * bool * Intset.t) array * constr - (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *) +(* env, id, evars, number of + function prototypes to try to clear from evars contexts, object and type *) +val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> + (identifier * types * loc * bool * Intset.t) array * constr * types + (* Obl. name, type as product, location of the original evar, + opacity (true = opaque) and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 43a3bec4..88243b60 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -6,15 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo" i*) + + (* Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -(* $Id: g_subtac.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *) -(*i camlp4deps: "parsing/grammar.cma" i*) -open Options +open Flags open Util open Names open Nameops @@ -41,17 +44,20 @@ struct let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt" end +open Rawterm open SubtacGram open Util open Pcoq - +open Prim +open Constr let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt; + GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt; subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g ] ] + [ [ g = Vernac.gallina -> loc, g + | g = Vernac.gallina_ext -> loc, g ] ] ; subtac_nameopt: @@ -60,31 +66,31 @@ GEXTEND Gram ; Constr.binder_let: - [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in - LocalRawAssum ([id], typ) + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [LocalRawAssum ([id], default_binder_kind, typ)] ] ]; Constr.binder: [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> - ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)])) + ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)])) | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> - ([id],c) + ([id],default_binder_kind, c) | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> - (id::lid,c) + (id::lid,default_binder_kind, c) ] ]; END -type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type +type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type -let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype), - (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr ) gallina_loc_argtype), - (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) = +let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), + (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), + (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = Genarg.create_arg "subtac_gallina_loc" -type 'a nameopt_argtype = (identifier option, 'a, 'a) Genarg.abstract_argument_type +type 'a nameopt_argtype = (identifier option, 'a) Genarg.abstract_argument_type let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype), (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype), @@ -133,10 +139,18 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ] +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ + Coqlib.check_required_library ["Coq";"Program";"Tactics"]; + Tacinterp.add_tacdef false + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] END + +VERNAC COMMAND EXTEND Subtac_Show_Preterm +| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ] +| [ "Preterm" ] -> [ Subtac_obligations.show_term None ] +END diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 8bc310d5..a59ad6f5 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *) open Global open Pp @@ -49,24 +49,41 @@ open Decl_kinds open Tacinterp open Tacexpr +let solve_tccs_in_type env id isevars evm c typ = + if not (evm = Evd.empty) then + let stmt_id = Nameops.add_suffix id "_stmt" in + let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in + (** Make all obligations transparent so that real dependencies can be sorted out by the user *) + let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in + match Subtac_obligations.add_definition stmt_id c' typ obls with + Subtac_obligations.Defined cst -> constant_value (Global.env()) + (match cst with ConstRef kn -> kn | _ -> assert false) + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") + else + let _ = Typeops.infer_type env c in c + + let start_proof_com env isevars sopt kind (bl,t) hook = let id = match sopt with - | Some id -> + | Some (loc,id) -> (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - errorlabstrm "start_proof" (pr_id id ++ str " already exists"); + user_err_loc (loc,"start_proof",pr_id id ++ str " already exists"); id | None -> next_global_ident_away false (id_of_string "Unnamed_thm") (Pfedit.get_all_proof_names ()) in - let evm, c, typ = + let evm, c, typ, _imps = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None in - let _ = Typeops.infer_type env c in - Command.start_proof id kind c hook + let c = solve_tccs_in_type env id isevars evm c typ in + Command.start_proof id kind c hook -let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () +let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; @@ -75,122 +92,157 @@ let start_proof_and_print env isevars idopt k t hook = let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) let assumption_message id = - Options.if_verbose message ((string_of_id id) ^ " is assumed") + Flags.if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption env isevars idl is_coe k bl c = - if not (Pfedit.refining ()) then - let evm, c, typ = - Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None +let declare_assumption env isevars idl is_coe k bl c nl = + if not (Pfedit.refining ()) then + let id = snd (List.hd idl) in + let evm, c, typ, imps = + Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in - List.iter (Command.declare_one_assumption is_coe k c) idl + let c = solve_tccs_in_type env id isevars evm c typ in + List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let vernac_assumption env isevars kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l +let dump_definition (loc, id) s = + Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id)) + +let dump_constraint ty ((loc, n), _, _) = + match n with + | Name id -> dump_definition (loc, id) ty + | Anonymous -> () +let dump_variable lid = () +let vernac_assumption env isevars kind l nl = + let global = fst kind = Global in + List.iter (fun (is_coe,(idl,c)) -> + if !Flags.dump then + List.iter (fun lid -> + if global then dump_definition lid "ax" + else dump_variable lid) idl; + declare_assumption env isevars idl is_coe kind [] c nl) l + +let check_fresh (loc,id) = + if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + user_err_loc (loc,"",pr_id id ++ str " already exists") + let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; -(* check_required_library ["Coq";"Logic";"JMeq"]; *) - require_library "Coq.subtac.FixSub"; - require_library "Coq.subtac.Utils"; - require_library "Coq.Logic.JMeq"; + check_required_library ["Coq";"Program";"Tactics"]; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try match command with - VernacDefinition (defkind, (locid, id), expr, hook) -> - (match expr with - ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None - | DefineBody (bl, _, c, tycon) -> - Subtac_pretyping.subtac_proof env isevars id bl c tycon) - | VernacFixpoint (l, b) -> - let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l b) - - | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) -> - if not(Pfedit.refining ()) then - if lettop then - errorlabstrm "Subtac_command.StartProof" - (str "Let declarations can only be used in proof editing mode"); + | VernacDefinition (defkind, (_, id as lid), expr, hook) -> + check_fresh lid; + dump_definition lid "def"; + (match expr with + | ProveBody (bl, t) -> if Lib.is_modtype () then errorlabstrm "Subtac_command.StartProof" (str "Proof editing mode not supported in module types"); - start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - - - | VernacAssumption (stre,l) -> - vernac_assumption env isevars stre l - - (*| VernacEndProof e -> - subtac_end_proof e*) - - | _ -> user_err_loc (loc,"", str ("Invalid Program command")) - with - | Typing_error e -> - msg_warning (str "Type error in Program tactic:"); - let cmds = - (match e with - | NonFunctionalApp (loc, x, mux, e) -> - str "non functional application of term " ++ - e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux - | NonSigma (loc, t) -> - str "Term is not of Sigma type: " ++ t - | NonConvertible (loc, x, y) -> - str "Unconvertible terms:" ++ spc () ++ - x ++ spc () ++ str "and" ++ spc () ++ y - | IllSorted (loc, t) -> - str "Term is ill-sorted:" ++ spc () ++ t - ) - in msg_warning cmds - - | Subtyping_error e -> - msg_warning (str "(Program tactic) Subtyping error:"); - let cmds = - match e with - | UncoercibleInferType (loc, x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - | UncoercibleInferTerm (loc, x, y, tx, ty) -> - str "Uncoercible terms:" ++ spc () - ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x - ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y - | UncoercibleRewrite (x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - in msg_warning cmds - - | Cases.PatternMatchingError (env, exn) as e -> - debug 2 (Himsg.explain_pattern_matching_error env exn); - raise e - - | Type_errors.TypeError (env, exn) as e -> - debug 2 (Himsg.explain_type_error env exn); - raise e - - | Pretype_errors.PretypeError (env, exn) as e -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e + start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) + (fun _ _ -> ()) + | DefineBody (bl, _, c, tycon) -> + ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon)) + | VernacFixpoint (l, b) -> + List.iter (fun ((lid, _, _, _, _), _) -> + check_fresh lid; + dump_definition lid "fix") l; + let _ = trace (str "Building fixpoint") in + ignore(Subtac_command.build_recursive l b) - | (Stdpp.Exc_located (loc, e')) as e -> - debug 2 (str "Parsing exception: "); - (match e' with - | Type_errors.TypeError (env, exn) -> - debug 2 (Himsg.explain_type_error env exn); - raise e - - | Pretype_errors.PretypeError (env, exn) -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e - - | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); - raise e) - - | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); - raise e - - + | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> + if !Flags.dump then dump_definition id "prf"; + if not(Pfedit.refining ()) then + if lettop then + errorlabstrm "Subtac_command.StartProof" + (str "Let declarations can only be used in proof editing mode"); + if Lib.is_modtype () then + errorlabstrm "Subtac_command.StartProof" + (str "Proof editing mode not supported in module types"); + check_fresh id; + start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook + + | VernacAssumption (stre,nl,l) -> + vernac_assumption env isevars stre l nl + + | VernacInstance (glob, sup, is, props, pri) -> + if !Flags.dump then dump_constraint "inst" is; + ignore(Subtac_classes.new_instance ~global:glob sup is props pri) + + | VernacCoFixpoint (l, b) -> + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + ignore(Subtac_command.build_corecursive l b) + + (*| VernacEndProof e -> + subtac_end_proof e*) + + | _ -> user_err_loc (loc,"", str ("Invalid Program command")) + with + | Typing_error e -> + msg_warning (str "Type error in Program tactic:"); + let cmds = + (match e with + | NonFunctionalApp (loc, x, mux, e) -> + str "non functional application of term " ++ + e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux + | NonSigma (loc, t) -> + str "Term is not of Sigma type: " ++ t + | NonConvertible (loc, x, y) -> + str "Unconvertible terms:" ++ spc () ++ + x ++ spc () ++ str "and" ++ spc () ++ y + | IllSorted (loc, t) -> + str "Term is ill-sorted:" ++ spc () ++ t + ) + in msg_warning cmds + + | Subtyping_error e -> + msg_warning (str "(Program tactic) Subtyping error:"); + let cmds = + match e with + | UncoercibleInferType (loc, x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + | UncoercibleInferTerm (loc, x, y, tx, ty) -> + str "Uncoercible terms:" ++ spc () + ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x + ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y + | UncoercibleRewrite (x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + in msg_warning cmds + + | Cases.PatternMatchingError (env, exn) as e -> + debug 2 (Himsg.explain_pattern_matching_error env exn); + raise e + + | Type_errors.TypeError (env, exn) as e -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) as e -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | (Stdpp.Exc_located (loc, e')) as e -> + debug 2 (str "Parsing exception: "); + (match e' with + | Type_errors.TypeError (env, exn) -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); + raise e) + + | e -> + msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); + raise e diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 04cad7c0..c7182bd2 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *) +(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *) open Cases open Util @@ -100,8 +101,7 @@ type equation = rhs : rhs; alias_stack : name list; eqn_loc : loc; - used : bool ref; - tag : pattern_source } + used : bool ref } type matrix = equation list @@ -242,6 +242,7 @@ type pattern_matching_problem = history : pattern_continuation; mat : matrix; caseloc : loc; + casestyle: case_style; typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment } (*--------------------------------------------------------------------------* @@ -386,7 +387,7 @@ let mkDeclTomatch na = function let map_tomatch_type f = function | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (option_map f c, f t) + | NotInd (c,t) -> NotInd (Option.map f c, f t) let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 @@ -423,25 +424,6 @@ let remove_current_pattern eqn = let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } (**********************************************************************) -(* Dealing with regular and default patterns *) -let is_regular eqn = eqn.tag = RegularPat - -let lower_pattern_status = function - | RegularPat -> DefaultPat 0 - | DefaultPat n -> DefaultPat (n+1) - -let pattern_status pats = - if array_exists ((=) RegularPat) pats then RegularPat - else - let min = - Array.fold_right - (fun pat n -> match pat with - | DefaultPat i when i<n -> i - | _ -> n) - pats 0 in - DefaultPat min - -(**********************************************************************) (* Well-formedness tests *) (* Partial check on patterns *) @@ -499,7 +481,7 @@ let extract_rhs pb = | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion()) | eqn::_ -> set_used_pattern eqn; - eqn.tag, eqn.rhs + eqn.rhs (**********************************************************************) (* Functions to deal with matrix factorization *) @@ -676,26 +658,6 @@ let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n let push_rels_eqn sign eqn = let sign = all_name sign in -(* trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign ++ str "end"); *) -(* str " branch is " ++ my_print_constr (fst eqn.rhs.c_orig) (snd eqn.rhs.c_orig)); *) -(* let rhs = eqn.rhs in *) -(* let l, c, s, e = *) -(* List.fold_right *) -(* (fun (na, c, t) (itlift, it, sign, env) -> *) -(* (try trace (str "Pushing decl: " ++ pr_rel_decl env (na, c, t) ++ *) -(* str " lift is " ++ int itlift); *) -(* with _ -> trace (str "error in push_rels_eqn")); *) -(* let env' = push_rel (na, c, t) env in *) -(* match sign with *) -(* [] -> (itlift, lift 1 it, sign, env') *) -(* | (na', c, t) :: sign' -> *) -(* if na' = na then *) -(* (pred itlift, it, sign', env') *) -(* else ( *) -(* trace (str "skipping it"); *) -(* (itlift, liftn 1 itlift it, sign, env'))) *) -(* sign (rhs.rhs_lift, rhs.c_it, eqn.rhs.rhs_sign, eqn.rhs.rhs_env) *) -(* in *) {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } } let push_rels_eqn_with_names sign eqn = @@ -1126,7 +1088,6 @@ let group_equations pb ind current cstrs mat = for i=1 to Array.length cstrs do let n = cstrs.(i-1).cs_nargs in let args = make_anonymous_patvars n in - let rest = {rest with tag = lower_pattern_status rest.tag } in brs.(i-1) <- (args, rest) :: brs.(i-1) done | PatCstr (loc,((_,i)),args,_) -> @@ -1148,22 +1109,22 @@ let rec generalize_problem pb = function let tomatch = regeneralize_index_tomatch (i+1) tomatch in { pb with tomatch = Abstract d :: tomatch; - pred = option_map (generalize_predicate i d) pb'.pred } + pred = Option.map (generalize_predicate i d) pb'.pred } (* No more patterns: typing the right-hand-side of equations *) let build_leaf pb = - let tag, rhs = extract_rhs pb in + let rhs = extract_rhs pb in let tycon = match pb.pred with | None -> anomaly "Predicate not found" | Some (PrCcl typ) -> mk_tycon typ | Some _ -> anomaly "not all parameters of pred have been consumed" in - tag, pb.typing_function tycon rhs.rhs_env rhs.it + pb.typing_function tycon rhs.rhs_env rhs.it (* Building the sub-problem when all patterns are variables *) let shift_problem (current,t) pb = {pb with tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = option_map (specialize_predicate_var (current,t)) pb.pred; + pred = Option.map (specialize_predicate_var (current,t)) pb.pred; history = push_history_pattern 0 AliasLeaf pb.history; mat = List.map remove_current_pattern pb.mat } @@ -1228,7 +1189,7 @@ let build_branch current deps pb eqns const_info = let cur_alias = lift (List.length sign) current in let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in let env' = push_rels sign pb.env in - let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in + let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in sign, { pb with env = env'; @@ -1279,33 +1240,30 @@ and match_current pb tomatch = let brs = array_map2 (compile_branch current deps pb) eqns cstrs in (* We build the (elementary) case analysis *) - let tags = Array.map (fun (t,_,_) -> t) brs in - let brvals = Array.map (fun (_,v,_) -> v) brs in - let brtyps = Array.map (fun (_,_,t) -> t) brs in + let brvals = Array.map (fun (v,_) -> v) brs in + let brtyps = Array.map (fun (_,t) -> t) brs in let (pred,typ,s) = find_predicate pb.caseloc pb.env pb.isevars pb.pred brtyps cstrs current indt pb.tomatch in - let ci = make_case_info pb.env mind RegularStyle tags in + let ci = make_case_info pb.env mind pb.casestyle in let case = mkCase (ci,nf_betaiota pred,current,brvals) in let inst = List.map mkRel deps in - pattern_status tags, { uj_val = applist (case, inst); uj_type = substl inst typ } and compile_branch current deps pb eqn cstr = let sign, pb = build_branch current deps pb eqn cstr in - let tag, j = compile pb in - (tag, it_mkLambda_or_LetIn j.uj_val sign, j.uj_type) + let j = compile pb in + (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type) and compile_generalization pb d rest = let pb = { pb with env = push_rel d pb.env; tomatch = rest; - pred = option_map ungeneralize_predicate pb.pred; + pred = Option.map ungeneralize_predicate pb.pred; mat = List.map (push_rels_eqn [d]) pb.mat } in - let patstat,j = compile pb in - patstat, + let j = compile pb in { uj_val = mkLambda_or_LetIn d j.uj_val; uj_type = mkProd_or_LetIn d j.uj_type } @@ -1328,11 +1286,10 @@ and compile_alias pb (deppat,nondeppat,d,t) rest = {pb with env = newenv; tomatch = tomatch; - pred = option_map (lift_predicate n) pb.pred; + pred = Option.map (lift_predicate n) pb.pred; history = history; mat = mat } in - let patstat,j = compile pb in - patstat, + let j = compile pb in List.fold_left mkSpecialLetInJudge j sign (* pour les alias des initiaux, enrichir les env de ce qu'il faut et @@ -1352,7 +1309,6 @@ let matx_of_eqns env eqns = it = rhs; } in { patterns = lpat; - tag = RegularPat; alias_stack = []; eqn_loc = loc; used = ref false; @@ -1421,9 +1377,9 @@ let set_arity_signature dep n arsign tomatchl pred x = let rec decomp_lam_force n avoid l p = if n = 0 then (List.rev l,p,avoid) else match p with - | RLambda (_,(Name id as na),_,c) -> + | RLambda (_,(Name id as na),k,_,c) -> decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c + | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c | _ -> let x = next_ident_away (id_of_string "x") avoid in decomp_lam_force (n-1) (x::avoid) (Name x :: l) @@ -1513,7 +1469,7 @@ let extract_arity_signature env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> [na,option_map (lift n) bo,lift n typ] + | None -> [na,Option.map (lift n) bo,lift n typ] | Some (loc,_,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) @@ -1612,7 +1568,8 @@ let eq_id avoid id = let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq typ x typ' y = + mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) let hole = RHole (dummy_loc, Evd.QuestionMark true) @@ -1626,18 +1583,14 @@ let context_of_arsign l = let constr_of_pat env isevars arsign pat avoid = let rec typ env (ty, realargs) pat avoid = - trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++ - print_env env ++ str" should have type: " ++ my_print_constr env ty); match pat with | PatVar (l,name) -> - trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); let name, avoid = match name with Name n -> name, avoid | Anonymous -> let previd, id = prime avoid (Name (id_of_string "wildcard")) in Name id, id :: avoid in - trace (str "Treated pattern variable " ++ str (string_of_id (id_of_name name))); PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid | PatCstr (l,((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -1665,11 +1618,8 @@ let constr_of_pat env isevars arsign pat avoid = let cstr = mkConstruct ci.cs_cstr in let app = applistc cstr (List.map (lift (List.length sign)) params) in let app = applistc app args in - trace (str "Getting type of app: " ++ my_print_constr env app); let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in - trace (str "Family and args of apptype: " ++ my_print_constr env apptype); let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in - trace (str "Got Family and args of apptype: " ++ my_print_constr env apptype); match alias with Anonymous -> pat', sign, app, apptype, realargs, n, avoid @@ -1680,8 +1630,6 @@ let constr_of_pat env isevars arsign pat avoid = try let env = push_rels sign env in isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; - trace (str "convertible types for alias : " ++ my_print_constr env (lift (succ m) ty) - ++ my_print_constr env (lift 1 apptype)); let eq_t = mk_eq (lift (succ m) ty) (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) @@ -1693,15 +1641,8 @@ let constr_of_pat env isevars arsign pat avoid = (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in -(* let tycon, arity = mk_tycon_from_sign env isevars arsign arity in *) let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in - let c = it_mkProd_or_LetIn patc sign in - trace (str "arity signature is : " ++ my_print_rel_context env arsign); - trace (str "signature is : " ++ my_print_rel_context env sign); - trace (str "patty, args are : " ++ my_print_constr env (applistc patty args)); - trace (str "Constr_of_pat gives: " ++ my_print_constr env c); - trace (str "with args: " ++ pp_list (my_print_constr (push_rels sign env)) args); - pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid + pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid (* shadows functional version *) @@ -1729,7 +1670,7 @@ let vars_of_ctx ctx = match na with Anonymous -> raise (Invalid_argument "vars_of_ctx") | Name n -> n, RVar (dummy_loc, n) :: vars) - ctx (id_of_string "vars_of_ctx: error", []) + ctx (id_of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = @@ -1740,14 +1681,17 @@ let rec is_included x y = if i = i' then List.for_all2 is_included args args' else false -(* liftsign is the current pattern's signature length *) +(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its + full signature. However prevpatterns are in the original one signature per pattern form. + *) let build_ineqs prevpatterns pats liftsign = let _tomatchs = List.length pats in let diffs = List.fold_left (fun c eqnpats -> - let acc = List.fold_left2 - (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) + let acc = List.fold_left2 + (* ppat is the pattern we are discriminating against, curpat is the current one. *) + (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> match acc with None -> None @@ -1757,21 +1701,16 @@ let build_ineqs prevpatterns pats liftsign = let lens = List.length ppat_sign in (* Accumulated length of previous pattern's signatures *) let len' = lens + len in - trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by " - ++ int len'); let acc = ((* Jump over previous prevpat signs *) lift_rel_context len ppat_sign @ sign, len', succ n, (* nth pattern *) mkApp (Lazy.force eq_ind, - [| lift (lens + liftsign) ppat_ty ; - liftn liftsign (succ lens) ppat_c ; + [| lift (len' + liftsign) curpat_ty; + liftn (len + liftsign) (succ lens) ppat_c ; lift len' curpat_c |]) :: - List.map - (fun t -> - liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *) - (lift lens t (* Jump over this prevpat signature *))) c) + List.map (lift lens (* Jump over this prevpat signature *)) c) in Some acc else None) (Some ([], 0, 0, [])) eqnpats pats @@ -1790,20 +1729,19 @@ let subst_rel_context k ctx subst = let (_, ctx') = List.fold_right (fun (n, b, t) (k, acc) -> - (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc)) + (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) ctx (k, []) in ctx' let lift_rel_contextn n k sign = let rec liftrec k = function | (na,c,t)::sign -> - (na,option_map (liftn n k) c,type_app (liftn n k) t) - ::(liftrec (k-1) sign) + (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) | [] -> [] in liftrec (rel_context_length sign + k) sign -let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs arity = +let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = let i = ref 0 in let (x, y, z) = List.fold_left @@ -1815,71 +1753,53 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari (idents, pat' :: newpatterns, cpat :: pats)) ([], [], []) eqn.patterns sign in - let newpatterns = List.rev newpatterns and pats = List.rev pats in + let newpatterns = List.rev newpatterns and opats = List.rev pats in let rhs_rels, pats, signlen = List.fold_left (fun (renv, pats, n) (sign,c, (s, args), p) -> (* Recombine signatures and terms of all of the row's patterns *) -(* trace (str "treating pattern:" ++ my_print_constr Environ.empty_env c); *) let sign' = lift_rel_context n sign in let len = List.length sign' in (sign' @ renv, (* lift to get outside of previous pattern's signatures. *) (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, len + n)) - ([], [], 0) pats in + ([], [], 0) opats in let pats, _ = List.fold_left (* lift to get outside of past patterns to get terms in the combined environment. *) (fun (pats, n) (sign, c, (s, args), p) -> let len = List.length sign in ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) - ([], 0) pats + ([], 0) pats in + let ineqs = build_ineqs prevpatterns pats signlen in let rhs_rels' = rels_of_patsign rhs_rels in let _signenv = push_rel_context rhs_rels' env in -(* trace (str "Env with signature is: " ++ my_print_env _signenv); *) - let ineqs = build_ineqs prevpatterns pats signlen in - let eqs_rels = - let eqs = (*List.concat (List.rev eqs)*) context_of_arsign eqs in + let arity = let args, nargs = List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> -(* trace (str "treating arg:" ++ my_print_constr Environ.empty_env c); *) (args @ c :: allargs, List.length args + succ n)) pats ([], 0) in let args = List.rev args in -(* trace (str " equalities " ++ my_print_rel_context Environ.empty_env eqs); *) -(* trace (str " args " ++ pp_list (my_print_constr _signenv) args); *) - (* Make room for substitution of prime arguments by constr patterns *) - let eqs' = lift_rel_contextn signlen nargs eqs in - let eqs'' = subst_rel_context 0 eqs' args in -(* trace (str " new equalities " ++ my_print_rel_context Environ.empty_env eqs'); *) -(* trace (str " subtituted equalities " ++ my_print_rel_context _signenv eqs''); *) - eqs'' + substl args (liftn signlen (succ nargs) arity) in - let rhs_rels', lift_ineqs = - match ineqs with - None -> eqs_rels @ rhs_rels', 0 - | Some ineqs -> - (* let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in *) - lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels'), 1 + let rhs_rels', tycon = + let neqs_rels, arity = + match ineqs with + | None -> [], arity + | Some ineqs -> + [Anonymous, None, ineqs], lift 1 arity + in + let eqs_rels, arity = decompose_prod_n_assum neqs arity in + eqs_rels @ neqs_rels @ rhs_rels', arity in let rhs_env = push_rels rhs_rels' env in -(* (try trace (str "branch env: " ++ print_env rhs_env) *) -(* with _ -> trace (str "error in print branch env")); *) - let tycon = lift_tycon (List.length eqs_rels + lift_ineqs + signlen) tycon in - - let j = typing_fun tycon rhs_env eqn.rhs.it in -(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) -(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) -(* with _ -> *) -(* trace (str "Error in typed branch pretty printing")); *) + let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in - (* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *) - (* with _ -> trace (str "Error in branch decl pp")); *) let branch = let bref = RVar (dummy_loc, branch_name) in match vars_of_ctx rhs_rels with @@ -1890,22 +1810,13 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari Some _ -> RApp (dummy_loc, branch, [ hole ]) | None -> branch in - (* let branch = *) - (* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) - (* in *) - (* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *) - (* with _ -> trace (str "Error in new branch pp")); *) - incr i; - let rhs = { eqn.rhs with it = branch } in - (branch_decl :: branches, - { eqn with patterns = newpatterns; rhs = rhs } :: eqns, - pats :: prevpatterns)) + incr i; + let rhs = { eqn.rhs with it = branch } in + (branch_decl :: branches, + { eqn with patterns = newpatterns; rhs = rhs } :: eqns, + opats :: prevpatterns)) ([], [], []) eqns in x, y - - -(* liftn_rel_declaration *) - (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive @@ -1920,11 +1831,6 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs ari let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = (* We extract the signature of the arity *) let arsign = extract_arity_signature env tomatchs sign in -(* (try List.iter *) -(* (fun arsign -> *) -(* trace (str "arity signature: " ++ my_print_rel_context env arsign)) *) -(* arsign; *) -(* with _ -> trace (str "error in arity signature printing")); *) let env = List.fold_right push_rels arsign env in let allnames = List.rev (List.map (List.map pi1) arsign) in match rtntyp with @@ -1984,15 +1890,10 @@ let build_dependent_signature env evars avoid tomatchs arsign = (* Build the arity signature following the names in matched terms as much as possible *) let argsign = List.tl arsign in (* arguments in inverse application order *) let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) -(* let _ = trace (str "Working on dependent arg: " ++ my_print_rel_context *) -(* (push_rel_context argsign env) [_appsign]) *) -(* in *) let argsign = List.rev argsign in (* arguments in application order *) let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> -(* trace (str "Matching indexes: " ++ my_print_constr env arg ++ *) -(* str " and " ++ my_print_rel_context env [(name,b,t)]); *) let argt = Retyping.get_type_of env evars arg in let eq, refl_arg = if Reductionops.is_conv env evars argt t then @@ -2001,7 +1902,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = (lift (nargeqs + nar) arg), mk_eq_refl argt arg) else - (mk_JMeq (lift (nargeqs + slift) appt) + (mk_JMeq (lift (nargeqs + slift) t) (mkRel (nargeqs + slift)) (lift (nargeqs + nar) argt) (lift (nargeqs + nar) arg), @@ -2022,10 +1923,6 @@ let build_dependent_signature env evars avoid tomatchs arsign = (Name id, b, t) :: argsign')) (env, 0, [], [], slift, []) args argsign in -(* trace (str "neqs: " ++ int neqs ++ spc () ++ *) -(* str "nargeqs: " ++ int nargeqs ++spc () ++ *) -(* str "slift: " ++ int slift ++spc () ++ *) -(* str "nar: " ++ int nar); *) let eq = mk_JMeq (lift (nargeqs + slift) appt) (mkRel (nargeqs + slift)) @@ -2045,15 +1942,10 @@ let build_dependent_signature env evars avoid tomatchs arsign = let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in let previd, id = make_prime avoid name in let arsign' = (Name id, b, typ) in -(* let _ = trace (str "Working on arg: " ++ my_print_rel_context *) -(* env [arsign']) *) -(* in *) let tomatch_ty = type_of_tomatch ty in let eq = mk_eq (lift nar tomatch_ty) (mkRel slift) (lift nar tm) -(* mk_eq (lift (neqs + nar) tomatch_ty) *) -(* (mkRel (neqs + slift)) (lift (neqs + nar) tm) *) in ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, (mk_eq_refl tomatch_ty tm) :: refl_args, @@ -2062,28 +1954,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = in let arsign'' = List.rev arsign' in assert(slift = 0); (* we must have folded over all elements of the arity signature *) -(* begin try *) -(* List.iter *) -(* (fun arsign -> *) -(* trace (str "old arity signature: " ++ my_print_rel_context env arsign)) *) -(* arsign; *) - List.iter - (fun c -> - trace (str "new arity signature: " ++ my_print_rel_context env c)) - (arsign''); -(* with _ -> trace (str "error in arity signature printing") *) -(* end; *) - let env' = push_rel_context (context_of_arsign arsign') env in - let _eqsenv = push_rel_context (context_of_arsign eqs) env' in - (try trace (str "Where env with eqs is: " ++ my_print_env _eqsenv); - trace (str "args: " ++ List.fold_left (fun acc x -> acc ++ my_print_constr env x) - (mt()) refls) - with _ -> trace (str "error in equalities signature printing")); - arsign'', allnames, nar, eqs, neqs, refls - -(* let len = List.length eqs in *) -(* it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len *) - + arsign'', allnames, nar, eqs, neqs, refls (**************************************************************************) (* Main entry of the matching compilation *) @@ -2091,8 +1962,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = let liftn_rel_context n k sign = let rec liftrec k = function | (na,c,t)::sign -> - (na,option_map (liftn n k) c,type_app (liftn n k) t) - ::(liftrec (k-1) sign) + (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) | [] -> [] in liftrec (k + rel_context_length sign) sign @@ -2101,73 +1971,109 @@ let nf_evars_env evar_defs (env : env) : env = let nf t = nf_isevar evar_defs t in let env0 : env = reset_context env in let f e (na, b, t) e' : env = - Environ.push_named (na, option_map nf b, nf t) e' + Environ.push_named (na, Option.map nf b, nf t) e' in let env' = Environ.fold_named_context f ~init:env0 env in - Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e') + Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e') ~init:env' env -let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = +(* We put the tycon inside the arity signature, possibly discovering dependencies. *) + +let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let subst, len = + List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> + let signlen = List.length sign in + match kind_of_term tm with + | Rel n when dependent tm c + && signlen = 1 (* The term to match is not of a dependent type itself *) -> + ((n, len) :: subst, len - signlen) + | Rel _ when not (dependent tm c) + && signlen > 1 (* The term is of a dependent type but does not appear in + the tycon, maybe some variable in its type does. *) -> + (match tmtype with + NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) + | IsInd (_, IndType(indf,realargs)) -> + List.fold_left + (fun (subst, len) arg -> + match kind_of_term arg with + | Rel n when dependent arg c -> + ((n, len) :: subst, pred len) + | _ -> (subst, pred len)) + (subst, len) realargs) + | _ -> (subst, len - signlen)) + ([], nar) tomatchs arsign + in + let rec predicate lift c = + match kind_of_term c with + | Rel n when n > lift -> + (try + (* Make the predicate dependent on the matched variable *) + let idx = List.assoc (n - lift) subst in + mkRel (idx + lift) + with Not_found -> + (* A variable that is not matched, lift over the arsign. *) + mkRel (n + nar)) + | _ -> + map_constr_with_binders succ predicate lift c + in + try + (* The tycon may be ill-typed after abstraction. *) + let pred = predicate 0 c in + let env' = push_rel_context (context_of_arsign arsign) env in + ignore(Typing.sort_of env' evm pred); pred + with _ -> lift nar c + +let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = + + let typing_fun tycon env = typing_fun tycon env isevars in + (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env eqns in (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in -(* isevars := nf_evar_defs !isevars; *) -(* let env = nf_evars_env !isevars (env : env) in *) -(* trace (str "Evars : " ++ my_print_evardefs !isevars); *) -(* trace (str "Env : " ++ my_print_env env); *) - - let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in - let tomatchs_len = List.length tomatchs_lets in - let tycon = lift_tycon tomatchs_len tycon in - let env = push_rel_context tomatchs_lets env in let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in if predopt = None then + let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in + let tomatchs_len = List.length tomatchs_lets in + let env = push_rel_context tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = (* The arity signature *) let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) - trace (str "Arity signatures : " ++ my_print_rel_context env (context_of_arsign arsign)); let avoid = [] in build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign in - let tycon_constr = + let tycon, arity = match valcon_of_tycon tycon with - | None -> mkExistential env isevars - | Some t -> t + | None -> let ev = mkExistential env isevars in ev, ev + | Some t -> + t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) + tomatchs sign (lift tomatchs_len t) + in + let arity = + it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs) in let lets, matx = (* Type the rhs under the assumption of equations *) - constrs_of_pats typing_fun tycon env isevars matx tomatchs sign neqs - (eqs : rel_context list) (lift (signlen + neqs) tycon_constr) in - + constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity + in let matx = List.rev matx in let _ = assert(len = List.length lets) in let env = push_rels lets env in let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in let args = List.rev_map (lift len) args in - let sign = List.map (lift_rel_context len) sign in - let pred = it_mkProd_wo_LetIn (lift (signlen + neqs) tycon_constr) - (context_of_arsign eqs) in + let pred = liftn len (succ signlen) arity in + let pred = build_initial_predicate true allnames pred in - let pred = liftn len (succ signlen) pred in -(* it_mkProd_wo_LetIn (lift (len + signlen + neqs) tycon_constr) (liftn_rel_context len signlen eqs) in*) - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let _signenv = List.fold_right push_rels sign env in -(* trace (str "Using predicate: " ++ my_print_constr signenv pred ++ str " in env: " ++ my_print_env signenv ++ str " len is " ++ int len); *) - - let pred = - (* prepare_predicate_from_tycon loc typing_fun isevars env tomatchs eqs allnames signlen sign tycon in *) - build_initial_predicate true allnames pred in - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in let pb = @@ -2178,17 +2084,17 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e history = start_history (List.length initial_pushed); mat = matx; caseloc = loc; + casestyle= style; typing_function = typing_fun } in - let _, j = compile pb in + let j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = lift (-tomatchs_len) (nf_isevar !isevars tycon_constr); } + uj_type = nf_isevar !isevars tycon; } in j -(* inh_conv_coerce_to_tycon loc env isevars j tycon0 *) else (* We build the elimination predicate if any and check its consistency *) (* with the type of arguments to match *) @@ -2207,12 +2113,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e history = start_history (List.length initial_pushed); mat = matx; caseloc = loc; + casestyle= style; typing_function = typing_fun } in - let _, j = compile pb in + let j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in inh_conv_coerce_to_tycon loc env isevars j tycon end diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli index 02fe016d..6b8a0981 100644 --- a/contrib/subtac/subtac_cases.mli +++ b/contrib/subtac/subtac_cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*) +(*i $Id: subtac_cases.mli 10739 2008-04-01 14:45:20Z herbelin $ i*) (*i*) open Util diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml new file mode 100644 index 00000000..15addb44 --- /dev/null +++ b/contrib/subtac/subtac_classes.ml @@ -0,0 +1,210 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*) + +open Pretyping +open Evd +open Environ +open Term +open Rawterm +open Topconstr +open Names +open Libnames +open Pp +open Vernacexpr +open Constrintern +open Subtac_command +open Typeclasses +open Typeclasses_errors +open Termops +open Decl_kinds +open Entries +open Util + +module SPretyping = Subtac_pretyping.Pretyping + +let interp_binder_evars evdref env na t = + let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in + SPretyping.understand_tcc_evars evdref env IsType t + +let interp_binders_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) ((loc, i), t) -> + let n = Name i in + let t' = interp_binder_evars isevars env n t in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_typeclass_context_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) (iid, bk, cl) -> + let t' = interp_binder_evars isevars env (snd iid) cl in + let i = match snd iid with + | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids + | Name id -> id + in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_constrs_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) t -> + let t' = interp_binder_evars isevars env Anonymous t in + let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in + let d = (id,None,t') in + (push_named d env, id :: ids, d::params)) + (env, avoid, []) l + +let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = + SPretyping.understand_tcc_evars evdref env kind + (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c) + +let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = + interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c + +let type_ctx_instance isevars env ctx inst subst = + List.fold_left2 + (fun (subst, instctx) (na, _, t) ce -> + let t' = replace_vars subst t in + let c = interp_casted_constr_evars isevars env ce t' in + let d = na, Some c, t' in + (na, c) :: subst, d :: instctx) + (subst, []) (List.rev ctx) inst + +(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*) + +let type_class_instance_params isevars env id n ctx inst subst = + List.fold_left2 + (fun (subst, instctx) (na, _, t) ce -> + let t' = replace_vars subst t in + let c = +(* if ce = superclass_ce then *) + (* (\* Control over the evars which are direct superclasses to avoid partial instanciations *) + (* in instance search. *\) *) + (* Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *) + (* else *) + interp_casted_constr_evars isevars env ce t' + in + let d = na, Some c, t' in + (na, c) :: subst, d :: instctx) + (subst, []) (List.rev ctx) inst + +let substitution_of_constrs ctx cstrs = + List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] + +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = + let env = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in + let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in + let tclass = + match bk with + | Implicit -> + let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in + let k = class_info (Nametab.global id) in + let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in + let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in + if needlen <> applen then + Classes.mismatched_params env (List.map fst par) (List.map snd k.cl_context); + let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) + (fun avoid (clname, (id, _, t)) -> + match clname with + Some (cl, b) -> + let t = + if b then + let _k = class_info cl in + CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *) + else CHole (Util.dummy_loc, None) + in t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + par (List.rev k.cl_context) + in Topconstr.CAppExpl (loc, (None, id), pars) + + | Explicit -> cl + in + let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in + let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in + let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in + on_free_vars (List.rev (gen_ids @ fvs)); + let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in + let ctx, avoid = Classes.name_typeclass_binders bound ctx in + let ctx = List.append ctx (List.rev gen_ctx) in + let k, ctx', imps, subst = + let c = Command.generalize_constr_expr tclass ctx in + let c', imps = interp_type_evars_impls ~evdref:isevars env c in + let ctx, c = Classes.decompose_named_assum c' in + let cl, args = Typeclasses.dest_class_app c in + cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) + in + let id = + match snd instid with + Name id -> + let sp = Lib.make_path id in + if Nametab.exists_cci sp then + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + id + | Anonymous -> + let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in + Termops.next_global_ident_away false i (Termops.ids_of_context env) + in + let env' = Classes.push_named_context ctx' env in + isevars := Evarutil.nf_evar_defs !isevars; + isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; + let sigma = Evd.evars_of !isevars in + let substctx = Typeclasses.nf_substitution sigma subst in + let subst, _propsctx = + let props = + List.map (fun (x, l, d) -> + x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l)) + props + in + if List.length props > List.length k.cl_props then + Classes.mismatched_props env' (List.map snd props) k.cl_props; + let props, rest = + List.fold_left + (fun (props, rest) (id,_,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); + c :: props, rest' + with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props substctx + in + let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in + isevars := Evarutil.nf_evar_defs !isevars; + let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx') + and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') + in + isevars := undefined_evars !isevars; + Evarutil.check_evars env Evd.empty !isevars termtype; +(* let imps = *) +(* Util.list_map_i *) +(* (fun i binder -> *) +(* match binder with *) +(* ExplByPos (i, Some na), (true, true)) *) +(* 1 ctx *) +(* in *) + let hook gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + let inst = Typeclasses.new_instance k pri global cst in + Impargs.declare_manual_implicits false gr false imps; + Typeclasses.add_instance inst + in + let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in + let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in + ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls); + id diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli new file mode 100644 index 00000000..43f00107 --- /dev/null +++ b/contrib/subtac/subtac_classes.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +open Typeclasses +open Implicit_quantifiers +open Classes +(*i*) + +val type_ctx_instance : Evd.evar_defs ref -> + Environ.env -> + (Names.identifier * 'a * Term.constr) list -> + Topconstr.constr_expr list -> + (Names.identifier * Term.constr) list -> + (Names.identifier * Term.constr) list * + (Names.identifier * Term.constr option * Term.constr) list + +val new_instance : + ?global:bool -> + Topconstr.local_binder list -> + typeclass_constraint -> + binder_def_list -> + ?on_free_vars:(identifier list -> unit) -> + int option -> + identifier diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index c764443f..b45e23d0 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -5,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *) open Util open Names @@ -129,34 +130,45 @@ module Coercion = struct with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in - let rec coerce_application typ c c' l l' = + let rec coerce_application typ typ' c c' l l' = let len = Array.length l in - let rec aux tele typ i co = + let rec aux tele typ typ' i co = +(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *) +(* str " to "++ my_print_constr env y *) +(* ++ str "in env:" ++ my_print_env env); *) +(* with _ -> ()); *) if i < len then let hdx = l.(i) and hdy = l'.(i) in try isevars := the_conv_x_leq env hdx hdy !isevars; let (n, eqT, restT) = destProd typ in - aux (hdx :: tele) (subst1 hdy restT) (succ i) co + let (n', eqT', restT') = destProd typ' in + aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co with Reduction.NotConvertible -> let (n, eqT, restT) = destProd typ in + let (n', eqT', restT') = destProd typ' in + let _ = + try isevars := the_conv_x_leq env eqT eqT' !isevars + with Reduction.NotConvertible -> raise NoSubtacCoercion + in + (* Disallow equalities on arities *) + if Reduction.is_arity env eqT then raise NoSubtacCoercion; let restargs = lift_args 1 (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) in let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in -(* let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *) - let evar = make_existential dummy_loc env isevars eq in + let evar = make_existential loc env isevars eq in let eq_app x = mkApp (Lazy.force eq_rect, [| eqT; hdx; pred; x; hdy; evar|]) in - trace (str"Inserting coercion at application"); - aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) - else co - in aux [] typ 0 (fun x -> x) + aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) + else Some co + in aux [] typ typ' 0 (fun x -> x) in -(* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y); *) -(* with _ -> ()); *) +(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *) +(* str " to "++ my_print_constr env y *) +(* ++ str "in env:" ++ my_print_env env); *) +(* with _ -> ()); *) match (kind_of_term x, kind_of_term y) with | Sort s, Sort s' -> (match s, s' with @@ -167,24 +179,35 @@ module Coercion = struct | Prod (name, a, b), Prod (name', a', b') -> let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in + +(* let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *) +(* let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *) +(* let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *) +(* let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *) +(* mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *) + let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in - let c2 = coerce_unify env' b b' in + (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) + let coec1 = app_opt c1 (mkRel 1) in + (* env, x : a' |- c1[x] : lift 1 a *) + let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in + (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) (match c1, c2 with None, None -> failwith "subtac.coerce': Should have detected equivalence earlier" | _, _ -> Some (fun f -> - mkLambda (name', a', - app_opt c2 - (mkApp (Term.lift 1 f, - [| app_opt c1 (mkRel 1) |]))))) + mkLambda (name', a', + app_opt c2 + (mkApp (Term.lift 1 f, [| coec1 |]))))) | App (c, l), App (c', l') -> (match kind_of_term c, kind_of_term c' with - Ind i, Ind i' -> (* Sigma types *) + Ind i, Ind i' -> (* Inductive types *) let len = Array.length l in let existS = Lazy.force existS in let prod = Lazy.force prod in + (* Sigma types *) if len = Array.length l' && len = 2 && i = i' && (i = Term.destInd existS.typ || i = Term.destInd prod.typ) then @@ -248,21 +271,22 @@ module Coercion = struct else if i = i' && len = Array.length l' then let evm = evars_of !isevars in - let typ = Typing.type_of env evm c in (try subco () - with NoSubtacCoercion -> - -(* if not (is_arity env evm typ) then *) - Some (coerce_application typ c c' l l')) -(* else subco () *) + with NoSubtacCoercion -> + let typ = Typing.type_of env evm c in + let typ' = Typing.type_of env evm c' in + (* if not (is_arity env evm typ) then *) + coerce_application typ typ' c c' l l') + (* else subco () *) else subco () | x, y when x = y -> if Array.length l = Array.length l' then let evm = evars_of !isevars in let lam_type = Typing.type_of env evm c in + let lam_type' = Typing.type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) - Some (coerce_application lam_type c c' l l') + coerce_application lam_type lam_type' c c' l l' (* ) else subco () *) else subco () | _ -> subco ()) @@ -284,7 +308,7 @@ module Coercion = struct Some (fun x -> let cx = app_opt c x in - let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |])) + let evar = make_existential loc env isevars (mkApp (p, [| cx |])) in (mkApp ((Lazy.force sig_).intro, @@ -298,7 +322,7 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, option_map (app_opt coercion) v, t + !evars, Option.map (app_opt coercion) v (* Taken from pretyping/coercion.ml *) @@ -360,7 +384,7 @@ module Coercion = struct match kind_of_term t with | Prod (_,_,_) -> (isevars,j) | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',t) = define_evar_as_arrow isevars ev in + let (isevars',t) = define_evar_as_product isevars ev in (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try @@ -400,11 +424,15 @@ module Coercion = struct uj_type = typ' } - let inh_coerce_to_fail env isevars c1 v t = + let inh_coerce_to_fail env evd rigidonly v t c1 = + if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) + then + raise NoCoercion + else let v', t' = try - let t1,i1 = class_of1 env (evars_of isevars) c1 in - let t2,i2 = class_of1 env (evars_of isevars) t in + let t1,i1 = class_of1 env (evars_of evd) c1 in + let t2,i2 = class_of1 env (evars_of evd) t in let p = lookup_path_between (i2,i1) in match v with Some v -> @@ -413,132 +441,88 @@ module Coercion = struct | None -> None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 isevars, v', t') + try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion - let rec inh_conv_coerce_to_fail loc env isevars v t c1 = -(* (try *) -(* debug 1 (str "inh_conv_coerce_to_fail called for " ++ *) -(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *) -(* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *) -(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) -(* Termops.print_env env); *) -(* with _ -> ()); *) - try (the_conv_x_leq env t c1 isevars, v, t) + + let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) with Reduction.NotConvertible -> - (try - inh_coerce_to_fail env isevars c1 v t - with NoCoercion -> - (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), - kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with - | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in - let (evd',b) = - match v' with - Some v' -> - (match kind_of_term v' with - | Lambda (x,v1,v2) -> - (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *) - with Reduction.NotConvertible -> (isevars, None)) - | _ -> (isevars, None)) - | None -> (isevars, None) - in - (match b with - Some (x, v1, v2) -> - let env1 = push_rel (x,None,v1) env in - let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' - (Some v2) t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', - mkProd (x, v1, t2')) - | None -> - (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) - (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) - (* has type (name:u1)u2 (with v' recursively obtained) *) - let name = (match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = push_rel (name,None,u1) env in - let (evd', v1', t1') = - inh_conv_coerce_to_fail loc env1 isevars - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) - in - let (evd'', v2', t2') = - let v2 = - match v with - Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' - | None -> None - and evd', t2 = - match v1' with - Some v1' -> evd', subst1 v1' t2 - | None -> - let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in - evd', subst1 ev t2 - in - inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 - in - (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', - mkProd (name, u1, t2'))) - | _ -> raise NoCoercion)) + try inh_coerce_to_fail env evd rigidonly v t c1 + with NoCoercion -> + match + kind_of_term (whd_betadeltaiota env (evars_of evd) t), + kind_of_term (whd_betadeltaiota env (evars_of evd) c1) + with + | Prod (name,t1,t2), Prod (_,u1,u2) -> + (* Conversion did not work, we may succeed with a coercion. *) + (* We eta-expand (hence possibly modifying the original term!) *) + (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) + (* has type forall (x:u1), u2 (with v' recursively obtained) *) + let name = match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name in + let env1 = push_rel (name,None,u1) env in + let (evd', v1) = + inh_conv_coerce_to_fail loc env1 evd rigidonly + (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in + let v1 = Option.get v1 in + let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in + let t2 = Termops.subst_term v1 t2 in + let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') + | _ -> raise NoCoercion - (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) = -(* (try *) -(* trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *) -(* Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *) -(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *) -(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) -(* Termops.print_env env); *) -(* with _ -> ()); *) + let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = + let evd = nf_evar_defs evd in match n with None -> - let (evd', val', type') = + let (evd', val') = try - inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail loc env evd rigidonly + (Some (nf_isevar evd cj.uj_val)) + (nf_isevar evd cj.uj_type) (nf_isevar evd t) with NoCoercion -> - let sigma = evars_of isevars in + let sigma = evars_of evd in try - coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> error_actual_type_loc loc env sigma cj t in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> - (isevars, cj) + (evd, cj) + + let inh_conv_coerce_to = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = -(* (try *) -(* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *) -(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *) -(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *) -(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) -(* Termops.print_env env); *) -(* with _ -> ()); *) - let nabsinit, nabs = + let nabsinit, nabs = match abs with None -> 0, 0 | Some (init, cur) -> init, cur in - (* a little more effort to get products is needed *) + (* a little more effort to get products is needed *) try let rels, rng = decompose_prod_n nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) if noccur_with_meta 0 (succ nabsinit) rng then ( (* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) - let env', t, t' = + let env', t, t' = let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in env', rng, lift nabs t' in - try - pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' + try + fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' with NoCoercion -> - coerce_itf loc env' isevars None t t') + coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> let sigma = evars_of isevars in error_cannot_coerce env' sigma (t, t')) - else isevars + else isevars with _ -> isevars - (* trace (str "decompose_prod_n failed"); *) - (* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) +(* trace (str "decompose_prod_n failed"); *) +(* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 86139039..5bff6ad1 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -39,6 +39,8 @@ open Tacticals open Tacinterp open Vernacexpr open Notation +open Evd +open Evarutil module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils @@ -53,22 +55,24 @@ let evar_nf isevars c = Evarutil.nf_isevar !isevars c let interp_gen kind isevars env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in -(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' - + let interp_constr isevars env c = interp_gen (OfType None) isevars env c -let interp_type isevars env ?(impls=([],[])) c = +let interp_type_evars isevars env ?(impls=([],[])) c = interp_gen IsType isevars env ~impls c let interp_casted_constr isevars env ?(impls=([],[])) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c +let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = + interp_gen (OfType (Some typ)) isevars env ~impls c + let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in @@ -92,26 +96,31 @@ let locate_if_isevar loc na = function let interp_binder sigma env na t = let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in - SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t) - - -let interp_context sigma env params = - List.fold_left - (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder sigma env na t in - let d = (na,None,t) in - (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> - let t = interp_type sigma env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@params) - | LocalRawDef ((_,na),c) -> - let c = interp_constr_judgment sigma env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params)) - (env,[]) params + SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) + +let interp_context_evars evdref env params = + let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in + let (env, par, _, impls) = + List.fold_left + (fun (env,params,n,impls) (na, k, b, t) -> + match b with + None -> + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t = SPretyping.understand_tcc_evars evdref env IsType t' in + let d = (na,None,t) in + let impls = + if k = Implicit then + let na = match na with Name n -> Some n | Anonymous -> None in + (ExplByPos (n, na), (true, true)) :: impls + else impls + in + (push_rel d env, d::params, succ n, impls) + | Some b -> + let c = SPretyping.understand_judgment_tcc evdref env b in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params, succ n, impls)) + (env,[],1,[]) (List.rev bl) + in (env, par), impls (* try to find non recursive definitions *) @@ -126,7 +135,7 @@ let collect_non_rec env = let i = list_try_find_i (fun i f -> - if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec + if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec then i else failwith "try_find_i") 0 lnamerec in @@ -152,14 +161,14 @@ let collect_non_rec env = let list_of_local_binders l = let rec aux acc = function Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl - | Topconstr.LocalRawAssum (nl, c) :: tl -> + | Topconstr.LocalRawAssum (nl, k, c) :: tl -> aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl | [] -> List.rev acc in aux [] l let lift_binders k n l = let rec aux n = function - | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl + | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl | [] -> [] in aux n l @@ -172,11 +181,10 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with | _ -> assert(false) let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = + Coqlib.check_required_library ["Coq";"Program";"Wf"]; let sigma = Evd.empty in let isevars = ref (Evd.create_evar_defs sigma) in let env = Global.env() in - let nc = named_context env in - let nc_len = named_context_length nc in let pr c = my_print_constr env c in let prr = Printer.pr_rel_context env in let _prn = Printer.pr_named_context env in @@ -188,8 +196,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* Ppconstr.pr_constr_expr body) *) (* with _ -> () *) (* in *) - let env', binders_rel = interp_context isevars env bl in - let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in + let (env', binders_rel), impls = interp_context_evars isevars env bl in + let after, ((argname, _, argtyp) as arg), before = + let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in + split_args idx binders_rel in let before_length, after_length = List.length before, List.length after in let argid = match argname with Name n -> n | _ -> assert(false) in let liftafter = lift_binders 1 after_length after in @@ -226,11 +236,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in - let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in - (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ()); let top_env = push_rel_context top_bl env in + let top_arity = interp_type_evars isevars top_env arityc in + let intern_bl = wfarg 1 :: arg :: before in let _intern_env = push_rel_context intern_bl env in - let top_arity = interp_type isevars top_env arityc in let proj = (Lazy.force sig_).Coqlib.proj1 in let projection = mkApp (proj, [| argtyp ; @@ -240,29 +249,21 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = |]) in let intern_arity = it_mkProd_or_LetIn top_arity after in - (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity); - trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ()); - (* Top arity is in top_env = after :: arg :: before *) -(* let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *) -(* (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *) -(* trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *) - let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *) - (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); -(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *) -(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *) + (* Intern arity is in top_env = arg :: before *) + let intern_arity = liftn 2 2 intern_arity in +(* trace (str "After lifting arity: " ++ *) +(* my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *) +(* intern_arity); *) + (* arity is now in something :: wfarg :: arg :: before + where what refered to arg now refers to something *) + let intern_arity = substl [projection] intern_arity in + (* substitute the projection of wfarg for something *) let intern_before_env = push_rel_context before env in -(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *) -(* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *) - (try trace (str "Intern arity: " ++ - my_print_constr _intern_env intern_arity) with _ -> ()); let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - (try trace (str "Intern fun arity product: " ++ - my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ()); let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in -(* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *) let fun_env = push_rel_context fun_bl intern_before_env in - let fun_arity = interp_type isevars fun_env arityc in + let fun_arity = interp_type_evars isevars fun_env arityc in let intern_body = interp_casted_constr isevars fun_env body fun_arity in let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in let _ = @@ -274,161 +275,177 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* str "Intern body " ++ pr intern_body_lam) *) with _ -> () in - let _impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits top_env top_arity - else [] - in let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in + (* Lift to get to constant arguments *) + let lift_cst = List.length after + 1 in let fix_def = match measure_fn with None -> - mkApp (constr_of_reference (Lazy.force fix_sub_ref), + mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; - prop ; - intern_body_lam |]) + make_existential dummy_loc ~opaque:false env isevars wf_proof ; + lift lift_cst prop ; + lift lift_cst intern_body_lam |]) | Some f -> - lift (succ after_length) - (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), - [| argtyp ; - f ; - prop ; - intern_body_lam |])) + mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), + [| lift lift_cst argtyp ; + lift lift_cst f ; + lift lift_cst prop ; + lift lift_cst intern_body_lam |]) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in let typ = it_mkProd_or_LetIn top_arity binders_rel in let fullcoqc = Evarutil.nf_isevar !isevars def in let fullctyp = Evarutil.nf_isevar !isevars typ in -(* let _ = try trace (str "After evar normalization: " ++ spc () ++ *) -(* str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *) -(* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) -(* with _ -> () *) -(* in *) let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in let evm = non_instanciated_map env isevars evm in - - (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in - (* (try trace (str "Generated obligations : "); *) -(* Array.iter *) - (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) - (* evars; *) - (* with _ -> ()); *) - Subtac_obligations.add_definition recname evars_def fullctyp evars + let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in + Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> - (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx + (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx -let build_mutrec l boxed = - let sigma = Evd.empty and env = Global.env () in - let nc = named_context env in - let nc_len = named_context_length nc in - let lnameargsardef = - (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*) - l - in - let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef - and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef +let interp_fix_context evdref env fix = + interp_context_evars evdref env fix.Command.fix_binders + +let interp_fix_ccl evdref (env,_) fix = + interp_type_evars evdref env fix.Command.fix_type + +let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = + let env = push_rel_context ctx env_rec in + let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in + it_mkLambda_or_LetIn body ctx + +let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx + +let prepare_recursive_declaration fixnames fixtypes fixdefs = + let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in + let names = List.map (fun id -> Name id) fixnames in + (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) + +let rel_index n ctx = + list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) + +let rec unfold f b = + match f b with + | Some (x, b') -> x :: unfold f b' + | None -> [] + +let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = + match n with + | Some (loc, n) -> [rel_index n fixctx] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let len = List.length fixctx in + unfold (function x when x = len -> None + | n -> Some (n, succ n)) 0 + +let push_named_context = List.fold_right push_named + +let interp_recursive fixkind l boxed = + let env = Global.env() in + let fixl, ntnl = List.split l in + let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in + + (* Interp arities allowing for unresolved types *) + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in + let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in + let rec_sign = + List.fold_left2 (fun env id t -> (id,None,t) :: env) + [] fixnames fixtypes in - (* Build the recursive context and notations for the recursive types *) - let (rec_sign,rec_env,rec_impls,arityl) = - List.fold_left - (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) -> - let isevars = ref (Evd.create_evar_defs sigma) in - let arityc = Command.generalize_constr_expr arityc bl in - let arity = interp_type isevars env arityc in - let impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits env arity - else [] in - let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in - ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)) - ([],env,[],[]) lnameargsardef in - let arityl = List.rev arityl in - let notations = - List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) - lnameargsardef [] in - - let recdef = - - (* Declare local notations *) - let fs = States.freeze() in + let env_rec = push_named_context rec_sign env in + + (* Get interpretation metadatas *) + let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let notations = List.fold_right Option.List.cons ntnl [] in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let fixdefs = + States.with_heavy_rollback (fun () -> + List.iter (Command.declare_interning_data impls) notations; + list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) + () in + + (* Instantiate evars and check all are resolved *) + let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in + let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in + let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in + + let recdefs = List.length rec_sign in +(* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *) +(* List.iter (check_evars env Evd.empty evd) fixtypes; *) +(* check_mutuality env kind (List.combine fixnames fixdefs); *) + + (* Russell-specific code *) + + (* Get the interesting evars, those that were not instanciated *) + let isevars = Evd.undefined_evars evd in + trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars); + let evm = Evd.evars_of isevars in + trace (str "got the evm, recdefs is " ++ int recdefs); + (* Solve remaining evars *) + let rec collect_evars id def typ imps = + let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in + (* Generalize by the recursive prototypes *) let def = - try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df rec_impls c None) notations; - List.map2 - (fun ((_,_,bl,_,def),_) (isevars, info, arity) -> - match info with - None -> - let def = abstract_constr_expr def bl in - isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls) - def arity - | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) -> - let rec_env = push_rel_context fun_bl rec_env in - let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls) - def intern_arity - in isevars, info, it_mkLambda_or_LetIn cstr fun_bl) - lnameargsardef arityl - with e -> - States.unfreeze fs; raise e in - States.unfreeze fs; def - in - let (lnonrec,(namerec,defrec,arrec,nvrec)) = - collect_non_rec env lrecnames recdef arityl nv in - let recdefs = Array.length defrec in - (* Solve remaining evars *) - let rec collect_evars i acc = - if i < recdefs then - let (isevars, info, def) = defrec.(i) in - (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *) - let def = evar_nf isevars def in - let x, y, typ = arrec.(i) in - let typ = evar_nf isevars typ in - arrec.(i) <- (x, y, typ); - let rec_sign = nf_evar_context !isevars rec_sign in - let isevars = Evd.undefined_evars !isevars in - (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *) - let evm = Evd.evars_of isevars in - let id = namerec.(i) in - (* Generalize by the recursive prototypes *) - let def = - Termops.it_mkNamedLambda_or_LetIn def rec_sign - and typ = - Termops.it_mkNamedProd_or_LetIn typ rec_sign - in - let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in - collect_evars (succ i) ((id, def, typ, evars) :: acc) - else acc + Termops.it_mkNamedLambda_or_LetIn def rec_sign + and typ = + Termops.it_mkNamedProd_or_LetIn typ rec_sign + in + let evm' = Subtac_utils.evars_of_term evm Evd.empty def in + let evm' = Subtac_utils.evars_of_term evm evm' typ in + let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in + (id, def, typ, imps, evars) in - let defs = collect_evars 0 [] in - Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec - + let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in + (match fixkind with + | Command.IsFixpoint wfl -> + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in + let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + Array.of_list fixtypes, + Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) + in + let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l + | Command.IsCoFixpoint -> ()); + Subtac_obligations.add_mutual_definitions defs notations fixkind + let out_n = function Some n -> n - | None -> 0 - -let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed = - match lnameargsardef with - | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> - build_wellfounded (id, out_n n, bl, typ, body) r false no boxed - | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> - build_wellfounded (id, out_n n, bl, typ, body) r true no boxed - | l -> - let lnameargsardef = - List.map (fun ((id, (n, ro), bl, typ, body), no) -> - match ro with - CStructRec -> (id, out_n n, bl, typ, body), no - | CWfRec _ | CMeasureRec _ -> - errorlabstrm "Subtac_command.build_recursive" - (str "Well-founded fixpoints not allowed in mutually recursive blocks")) - lnameargsardef - in build_mutrec lnameargsardef boxed - - - + | None -> raise Not_found + +let build_recursive l b = + let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + match g, l with + [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> + ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false) + + | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] -> + ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false) + + | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l + in interp_recursive (Command.IsFixpoint g) fixl b + | _, _ -> + errorlabstrm "Subtac_command.build_recursive" + (str "Well-founded fixpoints not allowed in mutually recursive blocks") + +let build_corecursive l b = + let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) + l in + interp_recursive Command.IsCoFixpoint fixl b diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 846e06cf..27520867 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -14,18 +14,18 @@ val interp_gen : evar_defs ref -> env -> ?impls:full_implicits_env -> - ?allow_soapp:bool -> + ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : evar_defs ref -> env -> constr_expr -> constr -val interp_type : +val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> constr_expr -> constr -val interp_casted_constr : +val interp_casted_constr_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> @@ -38,5 +38,12 @@ val interp_constr_judgment : constr_expr -> unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list +val interp_binder : Evd.evar_defs ref -> + Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr + + val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit + +val build_corecursive : + (cofixpoint_expr * decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d182f7cd..55cdc7c4 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,7 +1,7 @@ -(* -*- default-directory: "~/research/coq/trunk/" -*- *) open Printf open Pp open Subtac_utils +open Command open Term open Names @@ -12,8 +12,11 @@ open Entries open Decl_kinds open Util open Evd +open Declare -let pperror cmd = Util.errorlabstrm "Subtac" cmd +type definition_hook = global_reference -> unit + +let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) exception NoObligations of identifier option @@ -22,11 +25,12 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ str (string_of_id ident) | None -> str "No obligations remaining" -type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array +type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array type obligation = { obl_name : identifier; obl_type : types; + obl_location : loc; obl_body : constr option; obl_opaque : bool; obl_deps : Intset.t; @@ -34,27 +38,46 @@ type obligation = type obligations = (obligation array * int) +type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list + type program_info = { prg_name: identifier; prg_body: constr; prg_type: constr; prg_obligations: obligations; prg_deps : identifier list; - prg_nvrec : int array; + prg_fixkind : Command.fixpoint_kind option ; + prg_implicits : (Topconstr.explicitation * (bool * bool)) list; + prg_notations : notations ; + prg_kind : definition_kind; + prg_hook : definition_hook; } let assumption_message id = - Options.if_verbose message ((string_of_id id) ^ " is assumed") + Flags.if_verbose message ((string_of_id id) ^ " is assumed") let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t -let evar_of_obligation o = { evar_hyps = Global.named_context_val () ; - evar_concl = o.obl_type ; - evar_body = Evar_empty ; - evar_extra = None } +(* true = All transparent, false = Opaque if possible *) +let proofs_transparency = ref true + +let set_proofs_transparency = (:=) proofs_transparency +let get_proofs_transparency () = !proofs_transparency + +open Goptions + +let _ = + declare_bool_option + { optsync = true; + optname = "transparency of Program obligations"; + optkey = (SecondaryTable ("Transparent","Obligations")); + optread = get_proofs_transparency; + optwrite = set_proofs_transparency; } + +let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type let subst_deps obls deps t = Intset.fold @@ -62,7 +85,7 @@ let subst_deps obls deps t = let xobl = obls.(x) in debug 3 (str "Trying to get body of obligation " ++ int x); let oblb = - try out_some xobl.obl_body + try Option.get xobl.obl_body with _ -> debug 3 (str "Couldn't get body of obligation " ++ int x); assert(false) @@ -96,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty let freeze () = !from_prg, !default_tactic_expr let unfreeze (v, t) = from_prg := v; set_default_tactic t let init () = - from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []) + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" []) let _ = Summary.declare_summary "program-tcc-table" @@ -110,7 +133,7 @@ let progmap_union = ProgMap.fold ProgMap.add let cache (_, (infos, tac)) = from_prg := infos; - default_tactic_expr := tac + set_default_tactic tac let (input,output) = declare_object @@ -129,69 +152,112 @@ let rec intset_to = function let subst_body prg = let obls, _ = prg.prg_obligations in - subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body - + let ints = intset_to (pred (Array.length obls)) in + subst_deps obls ints prg.prg_body, + subst_deps obls ints (Termops.refresh_universes prg.prg_type) + let declare_definition prg = - let body = subst_body prg in + let body, typ = subst_body prg in (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); with _ -> ()); + let (local, boxed, kind) = prg.prg_kind in let ce = { const_entry_body = body; - const_entry_type = Some prg.prg_type; + const_entry_type = Some typ; const_entry_opaque = false; - const_entry_boxed = false} + const_entry_boxed = boxed} in - let _constant = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition Definition) - in - Subtac_utils.definition_message prg.prg_name + (Command.get_declare_definition_hook ()) ce; + match local with + | Local when Lib.sections_are_opened () -> + let c = + SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in + let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in + print_message (Subtac_utils.definition_message prg.prg_name); + if Pfedit.refining () then + Flags.if_verbose msg_warning + (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ + str" is not visible from current goals"); + VarRef prg.prg_name + | (Global|Local) -> + let c = + Declare.declare_constant + prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) + in + let gr = ConstRef c in + if Impargs.is_implicit_args () || prg.prg_implicits <> [] then + Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; + print_message (Subtac_utils.definition_message prg.prg_name); + prg.prg_hook gr; + gr open Pp open Ppconstr +let rec lam_index n t acc = + match kind_of_term t with + | Lambda (na, _, b) -> + if na = Name n then acc + else lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences (n,_) fixbody fixtype = + match n with + | Some (loc, n) -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = Term.nb_prod fixtype in + let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in + list_map_i (fun i _ -> i) 0 ctx + let declare_mutual_definition l = let len = List.length l in - let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in - let arrec = - Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) - in - let recvec = - Array.of_list + let fixdefs, fixtypes, fiximps = + list_split3 (List.map (fun x -> - let subs = (subst_body x) in - snd (decompose_lam_n len subs)) l) + let subs, typ = (subst_body x) in + snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) in - let nvrec = (List.hd l).prg_nvrec in - let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in - let rec declare i fi = - (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr (Global.env()) (recvec.(i))); - with _ -> ()); - let ce = - { const_entry_body = mkFix ((nvrec,i),recdecls); - const_entry_type = Some arrec.(i); - const_entry_opaque = false; - const_entry_boxed = true} in - let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) - in - ConstRef kn - in - let lrefrec = Array.mapi declare namerec in - Options.if_verbose ppnl (recursive_message lrefrec) - + let fixkind = Option.get (List.hd l).prg_fixkind in + let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in + let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in + let boxed = true (* TODO *) in + let fixnames = (List.hd l).prg_deps in + let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in + let indexes, fixdecls = + match fixkind with + | IsFixpoint wfl -> + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in + let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l + | IsCoFixpoint -> + None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l + in + (* Declare the recursive definitions *) + let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in + (* Declare notations *) + List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations; + Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames); + (match List.hd kns with ConstRef kn -> kn | _ -> assert false) + let declare_obligation obl body = let ce = { const_entry_body = body; const_entry_type = Some obl.obl_type; - const_entry_opaque = obl.obl_opaque; + const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque; const_entry_boxed = false} in let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) in - Subtac_utils.definition_message obl.obl_name; + print_message (Subtac_utils.definition_message obl.obl_name); { obl with obl_body = Some (mkConst constant) } let try_tactics obls = @@ -209,18 +275,19 @@ let try_tactics obls = let red = Reductionops.nf_betaiota -let init_prog_info n b t deps nvrec obls = +let init_prog_info n b t deps fixkind notations obls impls kind hook = let obls' = Array.mapi - (fun i (n, t, o, d) -> + (fun i (n, t, l, o, d) -> debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d)); { obl_name = n ; obl_body = None; - obl_type = red t; obl_opaque = o; + obl_location = l; obl_type = red t; obl_opaque = o; obl_deps = d }) obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); - prg_deps = deps; prg_nvrec = nvrec; } + prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; + prg_implicits = impls; prg_kind = kind; prg_hook = hook; } let get_prog name = let prg_infos = !from_prg in @@ -244,44 +311,63 @@ let update_state s = (* msgnl (str "Updating obligations info"); *) Lib.add_anonymous_leaf (input s) -let obligations_message rem = +type progress = + | Remain of int + | Dependent + | Defined of global_reference + +let obligations_message rem = if rem > 0 then if rem = 1 then - Options.if_verbose msgnl (int rem ++ str " obligation remaining") + Flags.if_verbose msgnl (int rem ++ str " obligation remaining") else - Options.if_verbose msgnl (int rem ++ str " obligations remaining") + Flags.if_verbose msgnl (int rem ++ str " obligations remaining") else - Options.if_verbose msgnl (str "No more obligations remaining") - + Flags.if_verbose msgnl (str "No more obligations remaining") + let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in from_prg := map_replace prg.prg_name prg' !from_prg; obligations_message rem; - if rem > 0 then () - else ( - match prg'.prg_deps with - [] -> - declare_definition prg'; - from_prg := ProgMap.remove prg.prg_name !from_prg - | l -> - let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - (declare_mutual_definition progs; - from_prg := List.fold_left - (fun acc x -> - ProgMap.remove x.prg_name acc) !from_prg progs)); - update_state (!from_prg, !default_tactic_expr); - rem + let res = + if rem > 0 then Remain rem + else ( + match prg'.prg_deps with + [] -> + let kn = declare_definition prg' in + from_prg := ProgMap.remove prg.prg_name !from_prg; + Defined kn + | l -> + let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in + if List.for_all (fun x -> obligations_solved x) progs then + (let kn = declare_mutual_definition progs in + from_prg := List.fold_left + (fun acc x -> + ProgMap.remove x.prg_name acc) !from_prg progs; + Defined (ConstRef kn)) + else Dependent); + in + update_state (!from_prg, !default_tactic_expr); + res let is_defined obls x = obls.(x).obl_body <> None let deps_remaining obls deps = - Intset.fold - (fun x acc -> - if is_defined obls x then acc - else x :: acc) - deps [] - + Intset.fold + (fun x acc -> + if is_defined obls x then acc + else x :: acc) + deps [] + +let has_dependencies obls n = + let res = ref false in + Array.iteri + (fun i obl -> + if i <> n && Intset.mem n obl.obl_deps then + res := true) + obls; + !res + let kind_of_opacity o = if o then Subtac_utils.goal_proof_kind else Subtac_utils.goal_kind @@ -293,6 +379,7 @@ let obligations_of_evars evars = (fun (n, t) -> { obl_name = n; obl_type = t; + obl_location = dummy_loc; obl_body = None; obl_opaque = false; obl_deps = Intset.empty; @@ -315,11 +402,15 @@ let rec solve_obligation prg num = let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in let obls = Array.copy obls in let _ = obls.(num) <- obl in - if update_obls prg obls (pred rem) <> 0 then - auto_solve_obligations (Some prg.prg_name)); + match update_obls prg obls (pred rem) with + | Remain n when n > 0 -> + if has_dependencies obls num then + ignore(auto_solve_obligations (Some prg.prg_name)) + | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by !default_tactic + Pfedit.by !default_tactic; + Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) @@ -341,7 +432,7 @@ and solve_obligation_by_tac prg obls i tac = Some _ -> false | None -> (try - if deps_remaining obls obl.obl_deps = [] then + if deps_remaining obls obl.obl_deps = [] then let obl = subst_deps_obl obls obl in let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in if obl.obl_opaque then @@ -349,8 +440,12 @@ and solve_obligation_by_tac prg obls i tac = else obls.(i) <- { obl with obl_body = Some t }; true - else false - with _ -> false) + else false + with + | Stdpp.Exc_located(_, Refiner.FailError (_, s)) + | Refiner.FailError (_, s) -> + user_err_loc (obl.obl_location, "solve_obligation", s) + | e -> false) and solve_prg_obligations prg tac = let obls, rem = prg.prg_obligations in @@ -381,35 +476,66 @@ and try_solve_obligation n prg tac = and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () -and auto_solve_obligations n : unit = - Options.if_verbose msgnl (str "Solving obligations automatically..."); - try_solve_obligations n !default_tactic +and auto_solve_obligations n : progress = + Flags.if_verbose msgnl (str "Solving obligations automatically..."); + try solve_obligations n !default_tactic with NoObligations _ -> Dependent -let add_definition n b t obls = - Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n b t [] (Array.make 0 0) obls in +open Pp +let show_obligations ?(msg=true) n = + let prg = get_prog_err n in + let n = prg.prg_name in + let obls, rem = prg.prg_obligations in + if msg then msgnl (int rem ++ str " obligation(s) remaining: "); + Array.iteri (fun i x -> + match x.obl_body with + None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ + my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) + | Some _ -> ()) + obls + +let show_term n = + let prg = get_prog_err n in + let n = prg.prg_name in + msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () + ++ my_print_constr (Global.env ()) prg.prg_body) + +let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls = + Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + let prg = init_prog_info n b t [] None [] obls implicits kind hook in let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( - Options.if_verbose ppnl (str "."); - declare_definition prg; - from_prg := ProgMap.remove prg.prg_name !from_prg) + Flags.if_verbose ppnl (str "."); + let cst = declare_definition prg in + from_prg := ProgMap.remove prg.prg_name !from_prg; + Defined cst) else ( let len = Array.length obls in - let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; - auto_solve_obligations (Some n)) + let res = auto_solve_obligations (Some n) in + match res with + | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | _ -> res) -let add_mutual_definitions l nvrec = - let deps = List.map (fun (n, b, t, obls) -> n) l in +let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = + let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left - (fun acc (n, b, t, obls) -> - let prg = init_prog_info n b t deps nvrec obls in - ProgMap.add n prg acc) + (fun acc (n, b, t, imps, obls) -> + let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in + ProgMap.add n prg acc) !from_prg l in from_prg := upd; - List.iter (fun x -> auto_solve_obligations (Some x)) deps - + let _defined = + List.fold_left (fun finished x -> + if finished then finished + else + match auto_solve_obligations (Some x) with + Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true + | _ -> false) + false deps + in () + let admit_obligations n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in @@ -417,7 +543,7 @@ let admit_obligations n = match x.obl_body with None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (mkConst kn) } | Some _ -> ()) @@ -438,18 +564,5 @@ let next_obligation n = array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls in solve_obligation prg i - -open Pp -let show_obligations n = - let prg = get_prog_err n in - let n = prg.prg_name in - let obls, rem = prg.prg_obligations in - msgnl (int rem ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) - | Some _ -> ()) - obls - + let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index f015b80b..6d13e3bd 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,22 +1,42 @@ +open Names open Util +open Libnames -type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array - (* ident, type, opaque or transparent, dependencies *) +type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array + (* ident, type, location, opaque or transparent, dependencies *) +type progress = (* Resolution status of a program *) + | Remain of int (* n obligations remaining *) + | Dependent (* Dependent on other definitions *) + | Defined of global_reference (* Defined as id *) + val set_default_tactic : Tacexpr.glob_tactic_expr -> unit val default_tactic : unit -> Proof_type.tactic +val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) +val get_proofs_transparency : unit -> bool + +type definition_hook = global_reference -> unit + val add_definition : Names.identifier -> Term.constr -> Term.types -> - obligation_info -> unit + ?implicits:(Topconstr.explicitation * (bool * bool)) list -> + ?kind:Decl_kinds.definition_kind -> + ?hook:definition_hook -> obligation_info -> progress + +type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit + (Names.identifier * Term.constr * Term.types * + (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?kind:Decl_kinds.definition_kind -> + notations -> + Command.fixpoint_kind -> unit val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> int +val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress (* Number of remaining obligations to be solved for this program *) val solve_all_obligations : Proof_type.tactic -> unit @@ -25,7 +45,9 @@ val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic - val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit -val show_obligations : Names.identifier option -> unit +val show_obligations : ?msg:bool -> Names.identifier option -> unit + +val show_term : Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index cce9a358..0e987cf2 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *) open Global open Pp @@ -70,7 +70,12 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in - let evm = evars_of !isevars in + let _ = isevars := Evarutil.nf_evar_defs !isevars in + let evd,_ = consider_remaining_unif_problems env !isevars in +(* let unevd = undefined_evars evd in *) + let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in + let evm = evars_of unevd' in + isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type let find_with_index x l = @@ -98,7 +103,7 @@ let env_with_binders env isevars l = let coqdef, deftyp = interp env isevars rawdef empty_tycon in let reldecl = (name, Some coqdef, deftyp) in aux (push_rel reldecl env, reldecl :: rels) tl - | Topconstr.LocalRawAssum (bl, typ) :: tl -> + | Topconstr.LocalRawAssum (bl, k, typ) :: tl -> let rawtyp = coqintern_type !isevars env typ in let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in let acc = @@ -111,46 +116,28 @@ let env_with_binders env isevars l = | [] -> acc in aux (env, []) l -let subtac_process env isevars id l c tycon = - let c = Command.abstract_constr_expr c l in -(* let env_binders, binders_rel = env_with_binders env isevars l in *) +let subtac_process env isevars id bl c tycon = +(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) + let c = Command.abstract_constr_expr c bl in let tycon = match tycon with None -> empty_tycon | Some t -> - let t = Command.generalize_constr_expr t l in + let t = Command.generalize_constr_expr t bl in let t = coqintern_type !isevars env t in let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt in let c = coqintern_constr !isevars env c in + let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in -(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *) -(* str "Coq type: " ++ my_print_constr env ctyp) *) -(* with _ -> () *) -(* in *) -(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *) - -(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *) -(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *) -(* in *) - let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in - let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in -(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *) -(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *) -(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *) -(* Evd.pr_evar_map evm) *) -(* with _ -> () *) -(* in *) let evm = non_instanciated_map env isevars (evars_of !isevars) in -(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - evm, fullcoqc, fullctyp + evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps open Subtac_obligations -let subtac_proof env isevars id l c tycon = - let nc = named_context env in - let nc_len = named_context_length nc in - let evm, coqc, coqt = subtac_process env isevars id l c tycon in - let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in - add_definition id def coqt evars +let subtac_proof kind env isevars id bl c tycon = + let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in + let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in + let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in + add_definition id def ty ~implicits:imps ~kind:kind evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli index b62a8766..1d8eb250 100644 --- a/contrib/subtac/subtac_pretyping.mli +++ b/contrib/subtac/subtac_pretyping.mli @@ -5,11 +5,19 @@ open Sign open Evd open Global open Topconstr +open Implicit_quantifiers +open Impargs module Pretyping : Pretyping.S +val interp : + Environ.env -> + Evd.evar_defs ref -> + Rawterm.rawconstr -> + Evarutil.type_constraint -> Term.constr * Term.constr + val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> evar_map * constr * types + constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list -val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> unit +val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list -> + constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 53eec0b6..afa5817f 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *) open Pp open Util @@ -67,8 +68,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let mt_evd = Evd.empty - let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) - (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) @@ -113,7 +112,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let id = strip_meta id in (* May happen in tactics defined by Grammar *) try let (n,typ) = lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = type_app (lift n) typ } + { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> try List.assoc id lvar @@ -202,11 +201,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt - | (na,None,ty)::bl -> + | (na,k,None,ty)::bl -> let ty' = pretype_type empty_valcon env isevars lvar ty in let dcl = (na,None,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,Some bd,ty)::bl -> + | (na,k,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env isevars lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in @@ -223,43 +222,47 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let names = Array.map (fun id -> Name id) names in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = push_rec_types (names,ftys,[||]) env in + let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in let vdefj = array_map2_i (fun i ctxt def -> - (* we lift nbfix times the type in tycon, because of - * the nbfix variables pushed to newenv *) - let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) - (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon ty) nenv isevars lvar def in - { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) + let fty = + let ty = ftys.(i) in + if i = fixi then ( + Option.iter (fun tycon -> + isevars := Coercion.inh_conv_coerces_to loc env !isevars ftys.(i) tycon) + tycon; + nf_isevar !isevars ty) + else ty + in + (* we lift nbfix times the type in tycon, because of + * the nbfix variables pushed to newenv *) + let (ctxt,ty) = + decompose_prod_n_assum (rel_context_length ctxt) + (lift nbfix fty) in + let nenv = push_rel_context ctxt newenv in + let j = pretype (mk_tycon ty) nenv isevars lvar def in + { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; + uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env isevars names ftys vdefj; let fixj = match fixkind with | RFix (vn,i) -> - let guard_indexes = Array.mapi + (* First, let's find the guard indexes. *) + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem worth the effort (except for huge mutual + fixpoints ?) *) + let possible_indexes = Array.to_list (Array.mapi (fun i (n,_) -> match n with - | Some n -> n - | None -> - (* Recursive argument was not given by the user : We - check that there is only one inductive argument *) - let ctx = ctxtv.(i) in - let isIndApp t = - isInd (fst (decompose_app (strip_head_cast t))) in - (* This could be more precise (e.g. do some delta) *) - let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in - try (list_unique_index true lb) - 1 - with Not_found -> - Util.user_err_loc - (loc,"pretype", - Pp.str "cannot guess decreasing argument of fix")) - vn - in - let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in - (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkFix fix) ftys.(i) + | Some n -> [n] + | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) + vn) + in + let fixdecls = (names,ftys,Array.map j_val vdefj) in + let indexes = search_guard loc env possible_indexes fixdecls in + make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> let cofix = (i,(names,ftys,Array.map j_val vdefj)) in (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); @@ -292,7 +295,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in let typ' = nf_isevar !isevars typ in let tycon = - option_map + Option.map (fun (abs, ty) -> match abs with None -> @@ -308,7 +311,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct apply_rec env (n+1) { uj_val = nf_isevar !isevars value; uj_type = nf_isevar !isevars typ' } - (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest + (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest | _ -> let hj = pretype empty_tycon env isevars lvar c in @@ -316,7 +319,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in + let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with @@ -328,7 +331,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon - | RLambda(loc,name,c1,c2) -> + | RLambda(loc,name,k,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env isevars lvar c1 in @@ -336,7 +339,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j' = pretype rng (push_rel var env) isevars lvar c2 in judge_of_abstraction env name j j' - | RProd(loc,name,c1,c2) -> + | RProd(loc,name,k,c1,c2) -> let j = pretype_type empty_valcon env isevars lvar c1 in let var = (name,j.utj_val) in let env' = push_rel_assum var env in @@ -397,7 +400,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in + let ci = make_case_info env mis LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -415,7 +418,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in + let ci = make_case_info env mis LetStyle in mkCase (ci, p, cj.uj_val,[|f|] ) in { uj_val = v; uj_type = ccl }) @@ -485,14 +488,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let b2 = f cstrs.(1) b2 in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env IfStyle mis in + let ci = make_case_info env mis IfStyle in mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc - ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) + | RCases (loc,sty,po,tml,eqns) -> + Cases.compile_cases loc sty + ((fun vtyc env isevars -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) | RCast(loc,c,k) -> @@ -552,15 +555,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_unexpected_type_loc (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v - let pretype_gen isevars env lvar kind c = + let pretype_gen_aux isevars env lvar kind c = let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in (pretype tycon env isevars lvar c).uj_val | IsType -> (pretype_type empty_valcon env isevars lvar c).utj_val in + let evd,_ = consider_remaining_unif_problems env !isevars in + isevars:=evd; nf_evar (evars_of !isevars) c' + let pretype_gen isevars env lvar kind c = + let c = pretype_gen_aux isevars env lvar kind c in + isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars; + nf_evar (evars_of !isevars) c + (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... @@ -587,11 +597,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let isevars = ref (Evd.create_evar_defs sigma) in let c = pretype_gen isevars env lvar kind c in - let isevars,_ = consider_remaining_unif_problems env !isevars in - let c = nf_evar (evars_of isevars) c in - if fail_evar then check_evars env sigma isevars c; - isevars, c - + let evd = !isevars in + if fail_evar then check_evars env Evd.empty evd c; + evd, c + (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = @@ -601,16 +610,23 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c) let understand_type sigma env c = - snd (ise_pretype_gen true sigma env ([],[]) IsType c) + snd (ise_pretype_gen false sigma env ([],[]) IsType c) let understand_ltac sigma env lvar kind c = ise_pretype_gen false sigma env lvar kind c - let understand_tcc_evars isevars env kind c = - pretype_gen isevars env ([],[]) kind c - - let understand_tcc sigma env ?expected_type:exptyp c = - let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in + let understand_tcc_evars evdref env kind c = + pretype_gen evdref env ([],[]) kind c + + let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = + let ev, t = + if resolve_classes then + ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c + else + let isevars = ref (Evd.create_evar_defs sigma) in + let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in + !isevars, c + in Evd.evars_of ev, t end diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 28fe6352..bae2731a 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -10,10 +10,10 @@ let ($) f x = f x (****************************************************************************) (* Library linking *) -let contrib_name = "subtac" +let contrib_name = "Program" let subtac_dir = [contrib_name] -let fix_sub_module = "FixSub" +let fix_sub_module = "Wf" let utils_module = "Utils" let fixsub_module = subtac_dir @ [fix_sub_module] let utils_module = subtac_dir @ [utils_module] @@ -28,8 +28,8 @@ let make_ref l s = lazy (init_reference l s) let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded" let acc_ref = make_ref ["Init";"Wf"] "Acc" let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv" -let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub" -let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub" +let fix_sub_ref = make_ref fixsub_module "Fix_sub" +let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub" let lt_ref = make_ref ["Init";"Peano"] "lt" let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf" let refl_ref = make_ref ["Init";"Logic"] "refl_equal" @@ -64,9 +64,15 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec") let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep") let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro") -let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq") -let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec") -let jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl") +let jmeq_ind = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq") +let jmeq_rec = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_rec") +let jmeq_refl = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_refl") let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") @@ -113,20 +119,20 @@ let debug_on = true let debug n s = if debug_on then - if !Options.debug && n >= debug_level then + if !Flags.debug && n >= debug_level then msgnl s else () else () let debug_msg n s = if debug_on then - if !Options.debug && n >= debug_level then s + if !Flags.debug && n >= debug_level then s else mt () else mt () let trace s = if debug_on then - if !Options.debug && debug_level > 0 then msgnl s + if !Flags.debug && debug_level > 0 then msgnl s else () else () @@ -163,7 +169,7 @@ let make_existential loc ?(opaque = true) env isevars c = let make_existential_expr loc env c = let key = Evarutil.new_untyped_evar () in - let evar = Topconstr.CEvar (loc, key) in + let evar = Topconstr.CEvar (loc, key, None) in debug 2 (str "Constructed evar " ++ int key); evar @@ -174,6 +180,8 @@ let string_of_hole_kind = function | CasesType -> "CasesType" | InternalHole -> "InternalHole" | TomatchTypeParameter _ -> "TomatchTypeParameter" + | GoalEvar -> "GoalEvar" + | ImpossibleCase -> "ImpossibleCase" let evars_of_term evc init c = let rec evrec acc c = @@ -194,7 +202,7 @@ let non_instanciated_map env evd evm = QuestionMark _ -> Evd.add evm key evi | _ -> debug 2 (str " and is an implicit"); - Pretype_errors.error_unsolvable_implicit loc env evm k) + Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None) Evd.empty (Evarutil.non_instantiated evm) let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition @@ -231,8 +239,8 @@ let build_dependent_sum l = (tclTHENS tac ([intros; (tclTHENSEQ - [constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n]); + [constructor_tac false (Some 1) 1 + (Rawterm.ImplicitBindings [inj_open (mkVar n)]); cont]); ]))) in @@ -342,29 +350,44 @@ let id_of_name = function | Anonymous -> raise (Invalid_argument "id_of_name") let definition_message id = - Options.if_verbose message ((string_of_id id) ^ " is defined") - + Nameops.pr_id id ++ str " is defined" + let recursive_message v = match Array.length v with | 0 -> error "no recursive definition" - | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ + | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined") + | _ -> hov 0 (prvect_with_sep pr_coma (Printer.pr_constant (Global.env ())) v ++ spc () ++ str "are recursively defined") +let print_message m = + Flags.if_verbose ppnl m + (* Solve an obligation using tactics, return the corresponding proof term *) let solve_by_tac evi t = - debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi); let id = id_of_string "H" in - try + try Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl (fun _ _ -> ()); - debug 2 (str "Started proof"); Pfedit.by (tclCOMPLETE t); - let _,(const,_,_) = Pfedit.cook_proof () in + let _,(const,_,_) = Pfedit.cook_proof ignore in Pfedit.delete_current_proof (); const.Entries.const_entry_body - with e -> + with e -> Pfedit.delete_current_proof(); - raise Exit + raise e + +(* let apply_tac t goal = t goal *) + +(* let solve_by_tac evi t = *) +(* let ev = 1 in *) +(* let evm = Evd.add Evd.empty ev evi in *) +(* let goal = {it = evi; sigma = evm } in *) +(* let (res, valid) = apply_tac t goal in *) +(* if res.it = [] then *) +(* let prooftree = valid [] in *) +(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) +(* if obls = [] then proofterm *) +(* else raise Exit *) +(* else raise Exit *) let rec string_of_list sep f = function [] -> "" @@ -395,7 +418,7 @@ let pr_meta_map evd = | (mv,Clval(na,b,_)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " := " ++ - print_constr b.rebus ++ fnl ()) + print_constr (fst b).rebus ++ fnl ()) in prlist pr_meta_binding ml @@ -440,11 +463,11 @@ let pr_evar_defs evd = str"METAS:"++brk(0,1)++pr_meta_map evd in v 0 (pp_evm ++ pp_met) -let subtac_utils_path = - make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"]) -let utils_tac s = - lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s)) +let contrib_tactics_path = + make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"]) +let tactics_tac s = + lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) -let utils_call tac args = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args)) +let tactics_call tac args = + TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 5a5dd427..49335211 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -89,11 +89,11 @@ val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map val global_kind : logical_kind -val goal_kind : locality_flag * goal_object_kind +val goal_kind : locality * goal_object_kind val global_proof_kind : logical_kind -val goal_proof_kind : locality_flag * goal_object_kind +val goal_proof_kind : locality * goal_object_kind val global_fix_kind : logical_kind -val goal_fix_kind : locality_flag * goal_object_kind +val goal_fix_kind : locality * goal_object_kind val mkSubset : name -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr @@ -115,8 +115,10 @@ val destruct_ex : constr -> constr -> constr list val id_of_name : name -> identifier -val definition_message : identifier -> unit -val recursive_message : global_reference array -> std_ppcmds +val definition_message : identifier -> std_ppcmds +val recursive_message : constant array -> std_ppcmds + +val print_message : std_ppcmds -> unit val solve_by_tac : evar_info -> Tacmach.tactic -> constr @@ -125,6 +127,6 @@ val string_of_intset : Intset.t -> string val pr_evar_defs : evar_defs -> Pp.std_ppcmds -val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr +val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v index 97cef9a5..da612c43 100644 --- a/contrib/subtac/test/ListDep.v +++ b/contrib/subtac/test/ListDep.v @@ -1,6 +1,6 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import List. -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Set Implicit Arguments. @@ -23,13 +23,13 @@ Section Map_DependentRecursor. Variable f : { x : U | In x l } -> V. Obligations Tactic := unfold sub_list in * ; - subtac_simpl ; intuition. + program_simpl ; intuition. Program Fixpoint map_rec ( l' : list U | sub_list l' l ) { measure length l' } : { r : list V | length r = length l' } := match l' with - nil => nil - | cons x tl => let tl' := map_rec tl in + | nil => nil + | cons x tl => let tl' := map_rec tl in f x :: tl' end. diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v index 0b40ef82..ac49ca96 100644 --- a/contrib/subtac/test/Mutind.v +++ b/contrib/subtac/test/Mutind.v @@ -1,13 +1,20 @@ -Program Fixpoint f (a : nat) : nat := +Require Import List. + +Program Fixpoint f a : { x : nat | x > 0 } := match a with - | 0 => 0 + | 0 => 1 | S a' => g a a' end -with g (a b : nat) { struct b } : nat := +with g a b : { x : nat | x > 0 } := match b with - | 0 => 0 + | 0 => 1 | S b' => f b' end. Check f. -Check g.
\ No newline at end of file +Check g. + + + + + diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index a5a8b85f..501aa798 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -1,20 +1,17 @@ -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Require Import Coq.Arith.Compare_dec. Notation "( x & y )" := (existS _ x y) : core_scope. +Require Import Omega. + Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} : { q : nat & { r : nat | a = b * q + r /\ r < b } } := if le_lt_dec b a then let (q', r) := euclid (a - b) b in (S q' & r) else (O & a). -Require Import Omega. - -Obligations. -Solve Obligations using subtac_simpl ; omega. - Next Obligation. - assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega. + assert(b * S q' = b * q' + b) by auto with arith ; omega. Defined. Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v index 4764037d..4f938f4f 100644 --- a/contrib/subtac/test/measure.v +++ b/contrib/subtac/test/measure.v @@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope. Unset Printing All. Require Import Coq.Arith.Compare_dec. -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Fixpoint size (a : nat) : nat := match a with @@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat := | S n => S (size n) end. -Program Fixpoint test_measure (a : nat) {measure a size} : nat := +Program Fixpoint test_measure (a : nat) {measure size a} : nat := match a with | S (S n) => S (test_measure n) - | x => x + | 0 | S 0 => a end. -subst. -unfold n0. -auto with arith. -Qed. Check test_measure. Print test_measure.
\ No newline at end of file diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v new file mode 100644 index 00000000..87ab47d6 --- /dev/null +++ b/contrib/subtac/test/take.v @@ -0,0 +1,38 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) +Require Import JMeq. +Require Import List. +Require Import Coq.subtac.Utils. + +Set Implicit Arguments. + +Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := + match n with + | 0 => nil + | S p => + match l with + | cons hd tl => let rest := take tl p in cons hd rest + | nil => ! + end + end. + +Require Import Omega. + +Next Obligation. + intros. + simpl in l0. + apply le_S_n ; exact l0. +Defined. + +Next Obligation. + intros. + destruct_call take ; subtac_simpl. +Defined. + +Next Obligation. + intros. + inversion l0. +Defined. + + + + |