From e121b1de13ed893a37a73c852e4e9de933eef32a Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 10 Jun 2008 18:28:26 +0000 Subject: - Correct handling of DependentMorphism error, using tclFAIL instead of letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/class_tactics.ml4 | 198 ++++++++++++++++------------ test-suite/bugs/closed/shouldsucceed/1604.v | 2 +- theories/Classes/Morphisms.v | 40 ++++-- theories/Classes/RelationClasses.v | 21 +-- tools/coqdoc/pretty.mll | 5 +- 5 files changed, 154 insertions(+), 112 deletions(-) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index afefeabb3..bbeeb4e03 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -512,6 +512,8 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) +exception DependentMorphism + let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) = let new_evar isevars env t = Evarutil.e_new_evar isevars env @@ -528,8 +530,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy. let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> - if dependent (mkRel 1) ty then - raise (Invalid_argument "build_signature: cannot handle dependent morphisms"); + if dependent (mkRel 1) ty then raise DependentMorphism; let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in let ty = Reductionops.nf_betaiota ty in let relty = mk_relty ty obj in @@ -842,21 +843,34 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars = decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args)) in Some res, occ else rewrite_args occ - - | Prod (_, x, b) when not (dependent (mkRel 1) b) -> - let x', occ = aux env x occ None in - let b = subst1 mkProp b in - let b', occ = aux env b occ None in - let res = - if x' = None && b' = None then None - else - Some (resolve_morphism env sigma t - ~fnewt:unfold_impl - (arrow_morphism (Typing.type_of env sigma x) (Typing.type_of env sigma b)) - [| x ; b |] [| x' ; b' |] - cstr evars) - in res, occ + | Prod (n, x, b) when not (dependent (mkRel 1) b) -> + let x', occ = aux env x occ None in +(* if x' = None && flags.under_lambdas then *) +(* let lam = mkLambda (n, x, b) in *) +(* let lam', occ = aux env lam occ None in *) +(* let res = *) +(* match lam' with *) +(* | None -> None *) +(* | Some (prf, (car, rel, c1, c2)) -> *) +(* Some (resolve_morphism env sigma t *) +(* ~fnewt:unfold_all *) +(* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *) +(* cstr evars) *) +(* in res, occ *) +(* else *) + let b = subst1 mkProp b in + let b', occ = aux env b occ None in + let res = + if x' = None && b' = None then None + else + Some (resolve_morphism env sigma t + ~fnewt:unfold_impl + (arrow_morphism (Typing.type_of env sigma x) (Typing.type_of env sigma b)) + [| x ; b |] [| x' ; b' |] + cstr evars) + in res, occ + | Prod (n, ty, b) -> let lam = mkLambda (n, ty, b) in let lam', occ = aux env lam occ None in @@ -910,60 +924,65 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g let evars = ref (Evd.create_evar_defs Evd.empty) in let env = pf_env gl in let sigma = project gl in - let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in + let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars + in match eq with - Some (p, (_, _, oldt, newt)) -> - (try - evars := Typeclasses.resolve_typeclasses env ~fail:true !evars; - let p = Evarutil.nf_isevar !evars p in - let newt = Evarutil.nf_isevar !evars newt in - let undef = Evd.undefined_evars !evars in - let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x, - Evarutil.nf_isevar !evars y) !hypinfo.abs in - let rewtac = - match is_hyp with - | Some id -> - let term = - match abs with - None -> p - | Some (t, ty) -> - mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) - in - cut_replacing id newt - (fun x -> Tactics.refine (mkApp (term, [| mkVar id |]))) - | None -> - (match abs with - None -> - let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in - tclTHENLAST - (Tacmach.internal_cut_no_check name newt) - (tclTHEN (Tactics.revert [name]) (Tactics.refine p)) - | Some (t, ty) -> - Tactics.refine - (mkApp (mkLambda (Name (id_of_string "newt"), newt, - mkLambda (Name (id_of_string "lemma"), ty, - mkApp (p, [| mkRel 2 |]))), - [| mkMeta goal_meta; t |]))) - in - let evartac = - let evd = Evd.evars_of undef in - if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) - else tclIDTAC - in tclTHENLIST [evartac; rewtac] gl - with - | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) - | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> - tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." - ++ fnl () ++ Himsg.explain_typeclass_error env e) gl) -(* | Not_found -> *) -(* tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *) - | None -> - let {l2r=l2r; c1=x; c2=y} = !hypinfo in - raise (Pretype_errors.PretypeError - (pf_env gl, - Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp))) - (* tclFAIL 1 (str"setoid rewrite failed") gl *) + | Some (p, (_, _, oldt, newt)) -> + (try + evars := Typeclasses.resolve_typeclasses env ~fail:true !evars; + let p = Evarutil.nf_isevar !evars p in + let newt = Evarutil.nf_isevar !evars newt in + let undef = Evd.undefined_evars !evars in + let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar !evars x, + Evarutil.nf_isevar !evars y) !hypinfo.abs in + let rewtac = + match is_hyp with + | Some id -> + let term = + match abs with + | None -> p + | Some (t, ty) -> + mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) + in + cut_replacing id newt + (fun x -> Tactics.refine (mkApp (term, [| mkVar id |]))) + | None -> + (match abs with + | None -> + let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in + tclTHENLAST + (Tacmach.internal_cut_no_check name newt) + (tclTHEN (Tactics.revert [name]) (Tactics.refine p)) + | Some (t, ty) -> + Tactics.refine + (mkApp (mkLambda (Name (id_of_string "newt"), newt, + mkLambda (Name (id_of_string "lemma"), ty, + mkApp (p, [| mkRel 2 |]))), + [| mkMeta goal_meta; t |]))) + in + let evartac = + let evd = Evd.evars_of undef in + if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) + else tclIDTAC + in tclTHENLIST [evartac; rewtac] gl + with + | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) + | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> + tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." + ++ fnl () ++ Himsg.explain_typeclass_error env e) gl) + (* | Not_found -> *) + (* tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *) + | None -> + let {l2r=l2r; c1=x; c2=y} = !hypinfo in + raise (Pretype_errors.PretypeError + (pf_env gl, + Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp))) + (* tclFAIL 1 (str"setoid rewrite failed") gl *) +let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl = + try cl_rewrite_clause_aux ~flags hypinfo goal_meta occs clause gl + with DependentMorphism -> tclFAIL 0 (str " setoid rewrite failed: cannot handle dependent morphisms") gl + let cl_rewrite_clause c left2right occs clause gl = init_setoid (); let meta = Evarutil.new_meta() in @@ -1046,20 +1065,32 @@ VERNAC COMMAND EXTEND Typeclasses_Settings END TACTIC EXTEND typeclasses_eauto -| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl -> - let env = pf_env gl in - let sigma = project gl in - if Evd.dom sigma = [] then Refiner.tclIDTAC gl - else - let evd = Evd.create_evar_defs sigma in - let mode = match s with Some t -> t | None -> true in - let depth = match depth with Some i -> i | None -> default_eauto_depth in - match resolve_typeclass_evars d (mode, depth) env evd false with - | Some evd' -> Refiner.tclEVARS (Evd.evars_of evd') gl - | None -> tclIDTAC gl - ] +| [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ + let mode = match s with Some t -> t | None -> true in + let depth = match depth with Some i -> i | None -> default_eauto_depth in + fun gl -> + let gls = {it = [sig_it gl]; sigma = project gl} in + let vals v = List.hd v in + typeclasses_eauto d (mode, depth) [] (gls, vals) ] END + +(* fun gl -> *) +(* let env = pf_env gl in *) +(* let sigma = project gl in *) +(* let proj = sig_it gl in *) +(* let evd = Evd.create_evar_defs (Evd.add Evd.empty 1 proj) in *) +(* let mode = match s with Some t -> t | None -> true in *) +(* let depth = match depth with Some i -> i | None -> default_eauto_depth in *) +(* match resolve_typeclass_evars d (mode, depth) env evd false with *) +(* | Some evd' -> *) +(* let goal = Evd.find (Evd.evars_of evd') 1 in *) +(* (match goal.evar_body with *) +(* | Evar_empty -> tclIDTAC gl *) +(* | Evar_defined b -> refine b gl) *) +(* | None -> tclIDTAC gl *) +(* ] *) + let _ = Classes.refine_ref := Refine.refine @@ -1316,7 +1347,8 @@ let default_morphism sign m = let isevars = ref (Evd.create_evar_defs Evd.empty) in let t = Typing.type_of env Evd.empty m in let _, sign, evars = - build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel) + try build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel) + with DependentMorphism -> error "Cannot infer the signature of dependent morphisms" in let morph = mkApp (Lazy.force morphism_type, [| t; sign; m |]) @@ -1339,7 +1371,9 @@ let add_setoid binders a aeq t n = let add_morphism_infer m n = init_setoid (); let instance_id = add_suffix n "_Morphism" in - let instance = build_morphism_signature m in + let instance = try build_morphism_signature m + with DependentMorphism -> error "Cannot infer the signature of dependent morphisms" + in if Lib.is_modtype () then let cst = Declare.declare_internal_constant instance_id (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v index 2d0991cb1..22c3df824 100644 --- a/test-suite/bugs/closed/shouldsucceed/1604.v +++ b/test-suite/bugs/closed/shouldsucceed/1604.v @@ -3,5 +3,5 @@ Require Import Setoid. Parameter F : nat -> nat. Axiom F_id : forall n : nat, n = F n. Goal forall n : nat, F n = n. -intro n. setoid_rewrite F_id at 2. reflexivity. +intro n. setoid_rewrite F_id at 3. reflexivity. Qed. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 6885d0b29..0d464b84e 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -28,6 +28,21 @@ Unset Strict Implicit. We now turn to the definition of [Morphism] and declare standard instances. These will be used by the [setoid_rewrite] tactic later. *) +(** A morphism on a relation [R] is an object respecting the relation (in its kernel). + The relation [R] will be instantiated by [respectful] and [A] by an arrow type + for usual morphisms. *) + +Class Morphism A (R : relation A) (m : A) : Prop := + respect : R m m. + +(** We make the type implicit, it can be infered from the relations. *) + +Implicit Arguments Morphism [A]. + +(** We allow to unfold the [relation] definition while doing morphism search. *) + +Typeclasses unfold relation. + (** Respectful morphisms. *) (** The fully dependent version, not used yet. *) @@ -49,6 +64,7 @@ Definition respectful (A B : Type) (** Notations reminiscent of the old syntax for declaring morphisms. *) Delimit Scope signature_scope with signature. +Arguments Scope Morphism [type_scope signature_scope]. Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. @@ -63,22 +79,18 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop Open Local Scope signature_scope. -(** A morphism on a relation [R] is an object respecting the relation (in its kernel). - The relation [R] will be instantiated by [respectful] and [A] by an arrow type - for usual morphisms. *) - -Class Morphism A (R : relation A) (m : A) : Prop := - respect : R m m. - -Arguments Scope Morphism [type_scope signature_scope]. - -(** We make the type implicit, it can be infered from the relations. *) - -Implicit Arguments Morphism [A]. +(** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) -(** We allow to unfold the [relation] definition while doing morphism search. *) +Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : + PER (A -> B) (R ==> R'). -Typeclasses unfold relation. + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. (** Subrelations induce a morphism on the identity, not used for morphism search yet. *) diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 17a645c8f..044195f19 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -162,26 +162,19 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop := PER_Symmetric :> Symmetric pequiv ; PER_Transitive :> Transitive pequiv. -(** We can build a PER on the Coq function space if we have PERs on the domain and - codomain. *) - -Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B) - (fun f g => forall (x y : A), R x y -> R' (f x) (g y)). - - Next Obligation. - Proof with auto. - assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... - Qed. - -(** The [Equivalence] typeclass. *) +(** Equivalence relations. *) Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := Equivalence_Reflexive :> Reflexive equiv ; Equivalence_Symmetric :> Symmetric equiv ; Equivalence_Transitive :> Transitive equiv. +(** An Equivalence is a PER plus reflexivity. *) + +Instance Equivalence_PER [ Equivalence A R ] : PER A R := + PER_Symmetric := Equivalence_Symmetric ; + PER_Transitive := Equivalence_Transitive. + (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index a9ad92f4c..d5d8702bc 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -170,11 +170,14 @@ let firstchar = ['A'-'Z' 'a'-'z' '_' (* iso 8859-1 accents *) '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | + '\194' '\185' | (* utf-8 latin 1 supplement *) '\195' ['\128'-'\191'] | (* utf-8 letterlike symbols *) '\206' ['\177'-'\183'] | - '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) + '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) + | '\129' [ '\176'-'\187' ] (* superscripts *) + | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) let identchar = firstchar | ['\'' '0'-'9' '@' ] let id = firstchar identchar* -- cgit v1.2.3