From 5aab6b96318d440f818fdf2f5bea69ad5dcda431 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 31 Dec 2007 13:11:55 +0000 Subject: Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/class_setoid.ml4 | 224 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 224 insertions(+) create mode 100644 tactics/class_setoid.ml4 (limited to 'tactics/class_setoid.ml4') diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 new file mode 100644 index 0000000000..0c8bdd2980 --- /dev/null +++ b/tactics/class_setoid.ml4 @@ -0,0 +1,224 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raise Not_found + | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; c + +let is_equiv env sigma t = + isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t + +let resolve_morphism env sigma direction oldt m args args' = + let evars = ref (Evd.create_evar_defs Evd.empty) in + let morph_instance, proj, subst, len, m', args, args' = + if is_equiv env sigma m then + let params, rest = array_chop 3 args in + let a, r, s = params.(0), params.(1), params.(2) in + let params', rest' = array_chop 3 args' in + let inst = mkApp (Lazy.force setoid_morphism, params) in + (* Equiv gives a binary morphism *) + let (cl, proj) = Lazy.force class_two in + let ctxargs = [ a; r; a; r; mkProp; Lazy.force iff; s; s; Lazy.force iff_setoid; ] in + let m' = mkApp (m, [| a; r; s |]) in + inst, proj, ctxargs, 6, m', rest, rest' + else + let cls = + match Array.length args with + 1 -> [Lazy.force class_one, 1] + | 2 -> [Lazy.force class_two, 2; Lazy.force class_one, 1] + | 3 -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1] + | n -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1] + in + try + List.iter (fun ((cl, proj), n) -> + evars := Evd.create_evar_defs Evd.empty; + let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] cl.cl_context in + let len = List.length ctxevs in + let superevs = substitution_of_named_context evars env cl.cl_name len ctxevs cl.cl_super in + let morphargs, morphobjs = array_chop (Array.length args - n) args in + let morphargs', morphobjs' = array_chop (Array.length args - n) args' in + let args = List.rev_map (fun (_, c) -> c) superevs in + let appm = mkApp(m, morphargs) in + let appmtype = Typing.type_of env sigma appm in + let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in + let mtype = replace_vars superevs (pi3 (List.hd cl.cl_params)) in + try + evars := Unification.w_unify true env CONV ~mod_delta:true appmtype mtype !evars; + evars := Evarutil.nf_evar_defs !evars; + let app = Evarutil.nf_isevar !evars app in + raise (Found (resolve_morphism_evd env evars app, proj, args, len, appm, morphobjs, morphobjs')) + with Not_found -> () + | Stdpp.Exc_located (_, Pretype_errors.PretypeError _) + | Pretype_errors.PretypeError _ -> ()) + cls; + raise Not_found + with Found x -> x + in + evars := Evarutil.nf_evar_defs !evars; + let evm = Evd.evars_of !evars in + let ctxargs = List.map (Reductionops.nf_evar evm) subst in + let ctx, sup = Util.list_chop len ctxargs in + let m' = Reductionops.nf_evar evm m' in + let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in + let projargs, respars, ressetoid, typeargs = + array_fold_left2 + (fun (acc, ctx, sup, typeargs') x y -> + let par, ctx = list_chop 2 ctx in + let setoid, sup = List.hd sup, List.tl sup in + match y with + None -> + let refl_proof = setoid_refl par setoid x in + [ refl_proof ; x ; x ] @ acc, ctx, sup, x :: typeargs' + | Some (p, (_, _, _, _, t')) -> + if direction then + [ p ; t'; x ] @ acc, ctx, sup, t' :: typeargs' + else [ p ; x; t' ] @ acc, ctx, sup, t' :: typeargs') + ([], ctx, sup, []) args args' + in + let proof = applistc appproj (List.rev projargs) in + let newt = applistc m' (List.rev typeargs) in + match respars, ressetoid with + [ a ; r ], [ s ] -> (proof, (a, r, s, oldt, newt)) + | _ -> assert(false) + +let build_new gl env setoid direction origt newt hyp hypinfo concl = + let rec aux t = + match kind_of_term t with + | _ when eq_constr t origt -> + Some (hyp, hypinfo) + | App (m, args) -> + let args' = Array.map aux args in + if array_for_all (fun x -> x = None) args' then None + else + (try Some (resolve_morphism env (project gl) direction t m args args') + with Not_found -> None) + | Prod (_, x, b) -> + let x', b' = aux x, aux b in + if x' = None && b' = None then None + else + (try Some (resolve_morphism env (project gl) direction t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |]) + with Not_found -> None) + + | _ -> None + in aux concl + +let decompose_setoid_eqhyp env sigma c dir t = + match kind_of_term t with + | App (equiv, [| a; r; s; x; y |]) -> + if dir then (c, (a, r, s, x, y)) + else (c, (a, r, s, y, x)) + | App (r, args) when Array.length args >= 2 -> + (try + let (p, (a, r, s, _, _)) = resolve_morphism env sigma dir t r args (Array.map (fun _ -> None) args) in + let _, args = array_chop (Array.length args - 2) args in + if dir then (c, (a, r, s, args.(0), args.(1))) + else (c, (a, r, s, args.(1), args.(0))) + with Not_found -> error "Not a (declared) setoid equality") + | _ -> error "Not a setoid equality" + +let cl_rewrite c left2right gl = + let env = pf_env gl in + let sigma = project gl in + let hyp = pf_type_of gl c in + let hypt, (typ, rel, setoid, origt, newt as hypinfo) = decompose_setoid_eqhyp env sigma c left2right hyp in + let concl = pf_concl gl in + let _concltyp = pf_type_of gl concl in + let eq = build_new gl env setoid left2right origt newt hypt hypinfo concl in + match eq with + Some (p, (_, _, _, _, t)) -> + let proj = + if left2right then + applistc (Lazy.force coq_proj2) + [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] + else + applistc (Lazy.force coq_proj1) + [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] + in + (Tactics.apply proj) gl + | None -> tclIDTAC gl + +open Extraargs + +TACTIC EXTEND class_rewrite +| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite c o ] +END -- cgit v1.2.3