aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common3
-rw-r--r--contrib/subtac/subtac_classes.ml18
-rw-r--r--interp/constrintern.ml26
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/ppvernac.ml2
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/typeclasses_errors.ml3
-rw-r--r--pretyping/typeclasses_errors.mli3
-rw-r--r--tactics/class_tactics.ml4160
-rw-r--r--theories/Classes/EquivDec.v138
-rw-r--r--theories/Classes/Equivalence.v4
-rw-r--r--theories/Classes/Morphisms.v3
-rw-r--r--theories/Classes/RelationClasses.v35
-rw-r--r--theories/Classes/SetoidClass.v2
-rw-r--r--theories/Classes/SetoidDec.v2
-rw-r--r--toplevel/classes.ml12
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/himsg.ml5
-rw-r--r--toplevel/vernacexpr.ml2
19 files changed, 297 insertions, 131 deletions
diff --git a/Makefile.common b/Makefile.common
index 9c539952f..ddd13223e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -744,7 +744,8 @@ UNICODEVO:= theories/Unicode/Utf8.vo
CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \
theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
- theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo
+ theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/EquivDec.vo \
+ theories/Classes/SetoidDec.vo
THEORIESVO:=\
$(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0c99fe16e..d65243680 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -136,12 +136,12 @@ let new_instance ctx (instid, bk, cl) props pri =
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.rev_append gen_ctx ctx in
- let k, ctx', subst =
+ let k, ctx', imps, subst =
let c = Command.generalize_constr_expr tclass ctx in
- let c' = interp_type_evars isevars env c 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, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+ 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
@@ -194,11 +194,13 @@ let new_instance ctx (instid, bk, cl) props pri =
Evarutil.nf_isevar !isevars t
in
isevars := undefined_evars !isevars;
- let imps =
- Util.list_map_i
- (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
- 1 ctx'
- in
+(* let imps = *)
+(* Util.list_map_i *)
+(* (fun i binder -> *)
+(* match binder with *)
+(* ExplByPos (i, Some na), (true, true)) *)
+(* 1 ctx *)
+(* in *)
let hook cst =
let inst =
{ is_class = k;
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ee245450b..ce445c3f6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1187,25 +1187,31 @@ let interp_open_constr sigma env c =
let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
-let interp_constr_evars_gen_impls ?(evdref=ref Evd.empty_evar_defs)
+let interp_constr_evars_gen_impls ?evdref
env ?(impls=([],[])) kind c =
- let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
- let imps = implicits_of_rawterm c in
- Default.understand_tcc_evars evdref env kind c, imps
+ match evdref with
+ | None ->
+ let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
+ let imps = implicits_of_rawterm c in
+ Default.understand_gen kind Evd.empty env c, imps
+ | Some evdref ->
+ let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+ let imps = implicits_of_rawterm c in
+ Default.understand_tcc_evars evdref env kind c, imps
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
Default.understand_tcc_evars evdref env kind c
-let interp_casted_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs)
+let interp_casted_constr_evars_impls ?evdref
env ?(impls=([],[])) c typ =
- interp_constr_evars_gen_impls ~evdref env ~impls (OfType (Some typ)) c
+ interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
-let interp_type_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ~evdref env IsType ~impls c
+let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref env IsType ~impls c
-let interp_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ~evdref env (OfType None) ~impls c
+let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 40c6180f0..df29d5096 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -475,14 +475,14 @@ GEXTEND Gram
(* Type classes, new syntax without artificial sup. *)
| IDENT "Class"; qid = identref; pars = binders_let;
- s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
+ s = [ ":"; c = sort -> Some (loc, c) | -> None ];
props = typeclass_field_types ->
VernacClass (qid, pars, s, [], props)
(* Type classes *)
| IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ];
qid = identref; pars = binders_let;
- s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
+ s = [ ":"; c = sort -> Some (loc, c) | -> None ];
props = typeclass_field_types ->
VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 92d56e078..7ca1964ea 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -701,7 +701,7 @@ let rec pr_vernac = function
str"Class" ++ spc () ++ pr_lident id ++
(* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *)
pr_and_type_binders_arg par ++
- spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) ++
+ (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++
spc () ++ str"where" ++ spc () ++
prlist_with_sep (fun () -> str";" ++ spc())
(fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 980a5075f..f9fcdb7b6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -700,7 +700,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let evdref = ref (Evd.create_evar_defs sigma) in
let c = pretype_gen evdref env lvar kind c in
let evd,_ = consider_remaining_unif_problems env !evdref in
- if fail_evar then check_evars env Evd.empty evd c;
+ if fail_evar then
+ (let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~all:false env (evars_of evd) evd in
+ check_evars env Evd.empty evd c);
evd, c
(** Entry points of the high-level type synthesis algorithm *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 1648f667a..4db826108 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -28,6 +28,7 @@ type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * identifier located (* Class name, method *)
| NoInstance of identifier located * constr list
+ | UnsatisfiableConstraints of evar_map
| MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
exception TypeClassError of env * typeclass_error
@@ -40,4 +41,6 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
let no_instance env id args = typeclass_error env (NoInstance (id, args))
+let unsatisfiable_constraints env evm = typeclass_error env (UnsatisfiableConstraints evm)
+
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 82e37f41d..a697087d2 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -28,6 +28,7 @@ type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * identifier located (* Class name, method *)
| NoInstance of identifier located * constr list
+ | UnsatisfiableConstraints of evar_map
| MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
exception TypeClassError of env * typeclass_error
@@ -38,4 +39,6 @@ val unbound_method : env -> global_reference -> identifier located -> 'a
val no_instance : env -> identifier located -> constr list -> 'a
+val unsatisfiable_constraints : env -> evar_map -> 'a
+
val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index dd93d511c..8d9ee36e9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -79,7 +79,7 @@ let rec e_trivial_fail_db db_list local_db goal =
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
(Hint_db.add_list hintl local_db) g'))) ::
- (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+ (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) )
in
tclFIRST (List.map tclCOMPLETE tacl) goal
@@ -93,36 +93,32 @@ and e_my_find_search db_list local_db hdc concl =
in
let tac_of_hint =
fun {pri=b; pat = p; code=t} ->
- (b,
- let tac =
- match t with
- | Res_pf (term,cl) -> unify_resolve (term,cl)
- | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
- | Give_exact (c) -> e_give_exact c
- | Res_pf_THEN_trivial_fail (term,cl) ->
- tclTHEN (unify_e_resolve (term,cl))
- (e_trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_in_concl [[],c]
- | Extern tacast -> conclPattern concl
- (Option.get p) tacast
- in
- (tac,fmt_autotactic t))
+ let tac =
+ match t with
+ | Res_pf (term,cl) -> unify_resolve (term,cl)
+ | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+ | Give_exact (c) -> e_give_exact c
+ | Res_pf_THEN_trivial_fail (term,cl) ->
+ tclTHEN (unify_e_resolve (term,cl))
+ (e_trivial_fail_db db_list local_db)
+ | Unfold_nth c -> unfold_in_concl [[],c]
+ | Extern tacast -> conclPattern concl
+ (Option.get p) tacast
+ in
+ (tac,b,fmt_autotactic t)
in
List.map tac_of_hint hintl
and e_trivial_resolve db_list local_db gl =
try
- Auto.priority
- (e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ e_my_find_search db_list local_db
+ (List.hd (head_constr_bound gl [])) gl
with Bound | Not_found -> []
let e_possible_resolve db_list local_db gl =
try
- List.map snd
- (List.sort (fun (b, _) (b', _) -> b - b')
- (e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl))
+ e_my_find_search db_list local_db
+ (List.hd (head_constr_bound gl [])) gl
with Bound | Not_found -> []
let find_first_goal gls =
@@ -132,6 +128,7 @@ let find_first_goal gls =
type search_state = {
depth : int; (*r depth of search before failing *)
tacres : goal list sigma * validation;
+ pri : int;
last_tactic : std_ppcmds;
custom_tactic : tactic;
dblist : Auto.Hint_db.t list;
@@ -152,24 +149,24 @@ module SearchProblem = struct
prlist (pr_ev evars) (sig_it gls)
let filter_tactics (glls,v) l =
-(* if !debug then *)
-(* (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
-(* let evars = Evarutil.nf_evars (Refiner.project glls) in *)
- (* msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *)
+ if !debug then
+ (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in
+ let evars = Evarutil.nf_evars (Refiner.project glls) in
+ msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"));
let rec aux = function
| [] -> []
- | (tac,pptac) :: tacl ->
+ | (tac,pri,pptac) :: tacl ->
try
- (* if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *)
+ if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n");
let (lgls,ptl) = apply_tac_list tac glls in
let v' p = v (ptl p) in
- (* if !debug then *)
- (* begin *)
- (* let evars = Evarutil.nf_evars (Refiner.project glls) in *)
- (* msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
- (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
- (* end; *)
- ((lgls,v'),pptac) :: aux tacl
+ if !debug then
+ begin
+ let evars = Evarutil.nf_evars (Refiner.project glls) in
+ msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n");
+ msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n"))
+ end;
+ ((lgls,v'),pri,pptac) :: aux tacl
with e when Logic.catchable_exception e ->
(* if !debug then msg (str"failed\n"); *)
aux tacl
@@ -179,14 +176,17 @@ module SearchProblem = struct
Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
(* Ordering of states is lexicographic on depth (greatest first) then
- number of remaining goals. *)
+ priority (lowest pri means higher priority), then number of remaining goals. *)
let compare s s' =
let d = s'.depth - s.depth in
let nbgoals s =
List.length (sig_it (fst s.tacres)) +
nb_empty_evars (sig_sig (fst s.tacres))
in
- if d <> 0 then d else nbgoals s - nbgoals s'
+ if d <> 0 then d else
+ let pri = s.pri - s'.pri in
+ if pri <> 0 then pri
+ else nbgoals s - nbgoals s'
let branching s =
if s.depth = 0 then
@@ -200,16 +200,16 @@ module SearchProblem = struct
let l =
filter_tactics s.tacres
(List.map
- (fun id -> (Eauto.e_give_exact_constr (mkVar id),
+ (fun id -> (Eauto.e_give_exact_constr (mkVar id), 0,
(str "exact" ++ spc () ++ pr_id id)))
- (pf_ids_of_hyps g))
+ (pf_ids_of_hyps g))
in
- List.map (fun (res,pp) -> { s with tacres = res;
+ List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0;
last_tactic = pp; localdb = List.tl s.localdb }) l
in
let intro_tac =
List.map
- (fun ((lgls,_) as res,pp) ->
+ (fun ((lgls,_) as res,pri,pp) ->
let g' = first_goal lgls in
let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
@@ -217,18 +217,19 @@ module SearchProblem = struct
let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in
{ s with tacres = res;
last_tactic = pp;
+ pri = pri;
localdb = ldb :: List.tl s.localdb })
- (filter_tactics s.tacres [Tactics.intro,(str "intro")])
+ (filter_tactics s.tacres [Tactics.intro,1,(str "intro")])
in
- let possible_resolve ((lgls,_) as res, pp) =
+ let possible_resolve ((lgls,_) as res, pri, pp) =
let nbgl' = List.length (sig_it lgls) in
if nbgl' < nbgl then
- { s with tacres = res; last_tactic = pp;
+ { s with tacres = res; last_tactic = pp; pri = pri;
localdb = List.tl s.localdb }
else
{ s with
depth = pred s.depth; tacres = res;
- last_tactic = pp;
+ last_tactic = pp; pri = pri;
localdb =
list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }
in
@@ -255,6 +256,7 @@ module Search = Explore.Make(SearchProblem)
let make_initial_state n gls ~(tac:tactic) dblist localdbs =
{ depth = n;
tacres = gls;
+ pri = 0;
last_tactic = (mt ());
custom_tactic = tac;
dblist = dblist;
@@ -341,13 +343,18 @@ let has_undefined p evd =
(evi.evar_body = Evar_empty && p ev evi))
(Evd.evars_of evd) false
-let rec resolve_all_evars ~(tac:tactic) debug m env p evd =
- let rec aux n evd =
- if has_undefined p evd && n > 0 then
- let evd' = resolve_all_evars_once ~tac debug m env p evd in
- aux (pred n) evd'
+let rec resolve_all_evars ~(tac:tactic) debug m env p oevd =
+(* let evd = resolve_all_evars_once ~tac debug m env p evd in *)
+(* if has_undefined p evd then raise Not_found *)
+(* else evd *)
+ let rec aux n evd =
+ if has_undefined p evd then
+ if n > 0 then
+ let evd' = resolve_all_evars_once ~tac debug m env p evd in
+ aux (pred n) evd'
+ else raise Not_found
else evd
- in aux 3 evd
+ in aux 3 oevd
(** Handling of the state of unfolded constants. *)
@@ -449,7 +456,11 @@ let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "s
let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive")
let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity")
-let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse")
+let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" *)
+ ["Program"; "Basics"] "flip")
+
+let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
+
let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement")
let pointwise_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "pointwise_relation")
@@ -506,19 +517,22 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a optio
| Some x -> f x
in
let rec aux t l =
- let t = Reductionops.whd_betadelta env (Evd.evars_of !isevars) t in
+ let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) t in
match kind_of_term t, l with
| Prod (na, ty, b), obj :: cstrs ->
- let (arg, evars) = aux b cstrs in
+ let (b, arg, evars) = aux b cstrs in
+ let ty = Reductionops.nf_betaiota ty in
let relty = mk_relty ty obj in
let arg' = mkApp (Lazy.force respectful, [| ty ; b ; relty ; arg |]) in
- arg', (ty, relty) :: evars
- | _, _ ->
+ mkProd(na, ty, b), arg', (ty, relty) :: evars
+ | _, obj :: _ -> anomaly "build_signature: not enough products"
+ | _, [] ->
(match finalcstr with
None ->
+ let t = Reductionops.nf_betaiota t in
let rel = mk_relty t None in
- rel, [t, rel]
- | Some (t, rel) -> rel, [t, rel])
+ t, rel, [t, rel]
+ | Some (t, rel) -> t, rel, [t, rel])
in aux m cstrs
let reflexivity_proof_evar env evars carrier relation x =
@@ -570,7 +584,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
let appm = mkApp(m, morphargs) in
let appmtype = Typing.type_of env sigma appm in
let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in
- let signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a, r) -> r) in
+ let appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a, r) -> r) in
let cl_args = [| appmtype ; signature ; appm |] in
let app = mkApp (Lazy.force morphism_type, cl_args) in
let morph = Evarutil.e_new_evar evars env app in
@@ -704,7 +718,7 @@ let unify_eqn env sigma hypinfo t =
else
try (mkApp (symmetric_proof env car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
with Not_found ->
- (prf, (car, mkApp (Lazy.force inverse, [| car ; rel |]), c2, c1))
+ (prf, (car, inverse car rel, c2, c1))
in Some (env', res)
with _ -> None
@@ -759,7 +773,7 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
with Not_found -> None)
in res, occ
- | Prod (_, x, b) ->
+ | Prod (_, x, b) when not (dependent (mkRel 1) b) ->
let x', occ = aux env x occ None in
let b', occ = aux env b occ None in
let res =
@@ -791,9 +805,9 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
| _ -> None, occ
in aux env concl 1 cstr
-let resolve_all_typeclasses env evd =
- resolve_all_evars false (true, 15) env
- (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
+(* let resolve_all_typeclasses env evd = *)
+(* resolve_all_evars false (true, 15) env *)
+(* (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd *)
let resolve_argument_typeclasses ?(tac=tclIDTAC) d p env evd onlyargs all =
let pred =
@@ -805,9 +819,15 @@ let resolve_argument_typeclasses ?(tac=tclIDTAC) d p env evd onlyargs all =
in
try
resolve_all_evars ~tac d p env pred evd
- with e ->
- if all then raise e else evd
-
+ with
+ | Not_found ->
+ if all then
+ (* Unable to satisfy the constraints. *)
+ Typeclasses_errors.unsatisfiable_constraints env (Evd.evars_of evd)
+ else evd
+ | e ->
+ if all then raise e else evd
+
let cl_rewrite_tactic = lazy (Tacinterp.interp <:tactic<setoid_rewrite_tac>>)
let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
@@ -818,7 +838,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
in
let cstr =
match is_hyp with
- None -> (mkProp, mkApp (Lazy.force inverse, [| mkProp; Lazy.force impl |]))
+ None -> (mkProp, inverse mkProp (Lazy.force impl))
| Some _ -> (mkProp, Lazy.force impl)
in
let evars = ref (Evd.create_evar_defs Evd.empty) in
@@ -1147,7 +1167,7 @@ let build_morphism_signature m =
| _ -> []
in aux t
in
- let sig_, evars = build_signature isevars env t cstrs None snd in
+ let t', sig_, evars = build_signature isevars env t cstrs None snd in
let _ = List.iter
(fun (ty, rel) ->
let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
@@ -1165,7 +1185,7 @@ let default_morphism sign m =
let env = Global.env () in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
let t = Typing.type_of env Evd.empty m in
- let sign, evars =
+ let _, sign, evars =
build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
in
let morph =
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
new file mode 100644
index 000000000..085023720
--- /dev/null
+++ b/theories/Classes/EquivDec.v
@@ -0,0 +1,138 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* Decidable equivalences.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ * 91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Export notations. *)
+
+Require Export Coq.Classes.Equivalence.
+
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
+ classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Open Scope equiv_scope.
+
+Class [ Equivalence A ] => DecidableEquivalence :=
+ setoid_decidable : forall x y : A, decidable (x === y).
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
+Class [ Equivalence A ] => EqDec :=
+ equiv_dec : forall x y : A, { x === y } + { x =/= y }.
+
+(** We define the [==] overloaded notation for deciding equality. It does not take precedence
+ of [==] defined in the type scope, hence we can have both at the same time. *)
+
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
+ match x with
+ | left H => @right _ _ H
+ | right H => @left _ _ H
+ end.
+
+Require Import Coq.Program.Program.
+
+Open Local Scope program_scope.
+
+(** Invert the branches. *)
+
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
+
+(** Overloaded notation for inequality. *)
+
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
+
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+ if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+ negb (equiv_decb x y).
+
+Infix "==b" := equiv_decb (no associativity, at level 70).
+Infix "<>b" := nequiv_decb (no associativity, at level 70).
+
+(** Decidable leibniz equality instances. *)
+
+Require Import Coq.Arith.Peano_dec.
+
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance nat_eq_eqdec : ! EqDec nat eq :=
+ equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : ! EqDec bool eq :=
+ equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : ! EqDec unit eq :=
+ equiv_dec x y := in_left.
+
+ Next Obligation.
+ Proof.
+ destruct x ; destruct y.
+ reflexivity.
+ Qed.
+
+Program Instance [ EqDec A eq, EqDec B eq ] =>
+ prod_eqdec : ! EqDec (prod A B) eq :=
+ equiv_dec x y :=
+ dest x as (x1, x2) in
+ dest y as (y1, y2) in
+ if x1 == y1 then
+ if x2 == y2 then in_left
+ else in_right
+ else in_right.
+
+ Solve Obligations using unfold complement, equiv ; program_simpl.
+
+Program Instance [ EqDec A eq, EqDec B eq ] =>
+ sum_eqdec : ! EqDec (sum A B) eq :=
+ equiv_dec x y :=
+ match x, y with
+ | inl a, inl b => if a == b then in_left else in_right
+ | inr a, inr b => if a == b then in_left else in_right
+ | inl _, inr _ | inr _, inl _ => in_right
+ end.
+
+ Solve Obligations using unfold complement, equiv ; program_simpl.
+
+(** Objects of function spaces with countable domains like bool have decidable equality. *)
+
+Require Import Coq.Program.FunctionalExtensionality.
+
+Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq :=
+ equiv_dec f g :=
+ if f true == g true then
+ if f false == g false then in_left
+ else in_right
+ else in_right.
+
+ Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+
+ Next Obligation.
+ Proof.
+ red.
+ extensionality x.
+ destruct x ; auto.
+ Qed.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 00519ecf4..a4c97fc82 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -109,8 +109,8 @@ Ltac equiv_simplify := repeat equiv_simplify_one.
Ltac equivify_tac :=
match goal with
- | [ s : Equivalence ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
- | [ s : Equivalence ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+ | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+ | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
end.
Ltac equivify := repeat equivify_tac.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index eda2aecaa..b4b217e38 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -453,8 +453,7 @@ Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : r
inverse (R ==> R') ==rel (inverse R ==> inverse R').
Proof.
intros.
- unfold inverse, flip.
- unfold respectful.
+ unfold flip, respectful.
split ; intros ; intuition.
Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0ca074589..009ee1e86 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -36,7 +36,9 @@ Definition default_relation [ DefaultRelation A R ] : relation A := R.
Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
-Definition inverse {A} : relation A -> relation A := flip.
+Notation "'inverse' R" := (flip (R:relation _) : relation _) (at level 0).
+
+(* Definition inverse {A} : relation A -> relation A := flip. *)
Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
@@ -93,26 +95,6 @@ Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
-(** Have to do it again for Prop. *)
-
-Program Instance [ Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
- reflexivity := reflexivity (R:=R).
-
-Program Instance [ Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
- irreflexivity := irreflexivity (R:=R).
-
-Program Instance [ Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
-
- Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
-
-Program Instance [ Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
-
- Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
-
-Program Instance [ Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
-
- Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
-
Program Instance [ Reflexive A (R : relation A) ] =>
Reflexive_complement_Irreflexive : Irreflexive (complement R).
@@ -148,7 +130,7 @@ Tactic Notation "apply" "*" constr(t) :=
refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
Ltac simpl_relation :=
- unfold inverse, flip, impl, arrow ; try reduce ; program_simpl ;
+ unfold flip, impl, arrow ; try reduce ; program_simpl ;
try ( solve [ intuition ]).
Ltac obligations_tactic ::= simpl_relation.
@@ -213,12 +195,11 @@ Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) :=
Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] =>
flip_antiSymmetric : Antisymmetric eq (flip R).
-Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq (R : relation A) ] =>
- inverse_antiSymmetric : Antisymmetric eq (inverse R).
-
-(** Leibinz equality [eq] is an equivalence relation. *)
+(** Leibinz equality [eq] is an equivalence relation.
+ The instance has low priority as it is always applicable
+ if only the type is constrained. *)
-Program Instance eq_equivalence : Equivalence A (@eq A).
+Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
(** Logical equivalence [iff] is an equivalence relation. *)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d4da4b8df..d370ffa44 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
Existing Instance setoid_morphism.
Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
- Reflexive_partial_app_morphism.
+ Reflexive_partial_app_morphism x.
Existing Instance setoid_partial_app_morphism.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 26e1ab244..835294ce3 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -40,8 +40,6 @@ Class [ Setoid A ] => EqDec :=
Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
-(** Use program to solve some obligations. *)
-
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
match x with
| left H => @right _ _ H
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9a0a0981e..eda8760a9 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -253,6 +253,10 @@ let new_class id par ar sup props =
(* Interpret the arity *)
let arity_imps, fullarity =
+ let ar =
+ match ar with
+ Some ar -> ar | None -> (dummy_loc, Rawterm.RType None)
+ in
let arity = CSort (fst ar, snd ar) in
let term = prod_constr_expr (prod_constr_expr arity par) sup in
interp_type_evars isevars env0 term
@@ -278,11 +282,15 @@ let new_class id par ar sup props =
List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
match fields with
[(Name proj_name, _, field)] ->
- let class_type = it_mkProd_or_LetIn arity params in
let class_body = it_mkLambda_or_LetIn field params in
+ let class_type =
+ match ar with
+ Some _ -> Some (it_mkProd_or_LetIn arity params)
+ | None -> None
+ in
let class_entry =
{ const_entry_body = class_body;
- const_entry_type = Some class_type;
+ const_entry_type = class_type;
const_entry_opaque = false;
const_entry_boxed = false }
in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 973845d9c..da00044d9 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -35,7 +35,7 @@ val infer_super_instances : env -> constr list ->
*)
val new_class : identifier located ->
local_binder list ->
- Vernacexpr.sort_expr located ->
+ Vernacexpr.sort_expr located option ->
local_binder list ->
binder_list -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 70441e50d..4adfaf6aa 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -488,6 +488,10 @@ let explain_no_instance env (_,id) l =
str "applied to arguments" ++ spc () ++
prlist_with_sep pr_spc (pr_lconstr_env env) l
+let explain_unsatisfiable_constraints env evm =
+ str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
+ Evd.pr_evar_map evm
+
let explain_mismatched_contexts env c i j =
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++
@@ -498,6 +502,7 @@ let explain_typeclass_error env err =
| NotAClass c -> explain_not_a_class env c
| UnboundMethod (cid, id) -> explain_unbound_method env cid id
| NoInstance (id, l) -> explain_no_instance env id l
+ | UnsatisfiableConstraints evm -> explain_unsatisfiable_constraints env evm
| MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
(* Refiner errors *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ee0c42aa2..4579d43a6 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -228,7 +228,7 @@ type vernac_expr =
| VernacClass of
lident * (* name *)
local_binder list * (* params *)
- sort_expr located * (* arity *)
+ sort_expr located option * (* arity *)
local_binder list * (* constraints *)
(lident * bool * constr_expr) list (* props, with substructure hints *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:53:45 +0000