diff options
Diffstat (limited to 'coq.ml')
| -rw-r--r-- | coq.ml | 592 |
1 files changed, 592 insertions, 0 deletions
@@ -0,0 +1,592 @@ +(***************************************************************************) +(* This is part of aac_tactics, it is distributed under the terms of the *) +(* GNU Lesser General Public License version 3 *) +(* (see file LICENSE for more details) *) +(* *) +(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) +(***************************************************************************) + +(** Interface with Coq *) +type constr = Term.constr + +open Term +open Names +open Coqlib + +(* The contrib name is used to locate errors when loading constrs *) +let contrib_name = "aac_tactics" + +(* Getting constrs (primitive Coq terms) from existing Coq + libraries. *) +let find_constant contrib dir s = + Libnames.constr_of_global (Coqlib.find_reference contrib dir s) + +let init_constant dir s = find_constant contrib_name dir s + +(* A clause specifying that the [let] should not try to fold anything + in the goal *) +let nowhere = + { Tacexpr.onhyps = Some []; + Tacexpr.concl_occs = Glob_term.no_occurrences_expr + } + +let cps_mk_letin + (name:string) + (c: constr) + (k : constr -> Proof_type.tactic) +: Proof_type.tactic = + fun goal -> + let name = (Names.id_of_string name) in + let name = Tactics.fresh_id [] name goal in + let letin = (Tactics.letin_tac None (Name name) c None nowhere) in + Tacticals.tclTHEN letin (k (mkVar name)) goal + +(** {2 General functions} *) + +type goal_sigma = Proof_type.goal Tacmach.sigma +let goal_update (goal : goal_sigma) evar_map : goal_sigma= + let it = Tacmach.sig_it goal in + Tacmach.re_sig it evar_map + +let fresh_evar goal ty : constr * goal_sigma = + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let (em,x) = Evarutil.new_evar evar_map env ty in + x,( goal_update goal em) + +let resolve_one_typeclass goal ty : constr*goal_sigma= + let env = Tacmach.pf_env goal in + let evar_map = Tacmach.project goal in + let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in + c, (goal_update goal em) + +let general_error = + "Cannot resolve a typeclass : please report" + +let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic = fun t k goal -> + Tacmach.pf_apply + (fun env em -> let em ,c = + try Typeclasses.resolve_one_typeclass env em t + with Not_found -> + begin match error with + | None -> Util.anomaly "Cannot resolve a typeclass : please report" + | Some x -> Util.error x + end + in + Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal + ) goal + + +let nf_evar goal c : Term.constr= + let evar_map = Tacmach.project goal in + Evarutil.nf_evar evar_map c + +let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let (em,x) = Evarutil.new_evar evar_map env x in + x,(goal_update gl em) + +let evar_binary (gl: goal_sigma) (x : constr) = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let ty = mkArrow x (mkArrow x x) in + let (em,x) = Evarutil.new_evar evar_map env ty in + x,( goal_update gl em) + +let evar_relation (gl: goal_sigma) (x: constr) = + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in + let (em,r) = Evarutil.new_evar evar_map env ty in + r,( goal_update gl em) + +let cps_evar_relation (x: constr) k = fun goal -> + Tacmach.pf_apply + (fun env em -> + let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in + let (em,r) = Evarutil.new_evar em env ty in + Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal + ) goal + +(* decomp_term : constr -> (constr, types) kind_of_term *) +let decomp_term c = kind_of_term (strip_outer_cast c) + +let lapp c v = mkApp (Lazy.force c, v) + +(** {2 Bindings with Coq' Standard Library} *) +module Std = struct +(* Here we package the module to be able to use List, later *) + +module Pair = struct + + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "prod") + let pair = lazy (init_constant path "pair") + let of_pair t1 t2 (x,y) = + mkApp (Lazy.force pair, [| t1; t2; x ; y|] ) +end + +module Bool = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "bool") + let ctrue = lazy (init_constant path "true") + let cfalse = lazy (init_constant path "false") + let of_bool b = + if b then Lazy.force ctrue else Lazy.force cfalse +end + +module Comparison = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "comparison") + let eq = lazy (init_constant path "Eq") + let lt = lazy (init_constant path "Lt") + let gt = lazy (init_constant path "Gt") +end + +module Leibniz = struct + let path = ["Coq"; "Init"; "Logic"] + let eq_refl = lazy (init_constant path "eq_refl") + let eq_refl ty x = lapp eq_refl [| ty;x|] +end + +module Option = struct + let path = ["Coq"; "Init"; "Datatypes"] + let typ = lazy (init_constant path "option") + let some = lazy (init_constant path "Some") + let none = lazy (init_constant path "None") + let some t x = mkApp (Lazy.force some, [| t ; x|]) + let none t = mkApp (Lazy.force none, [| t |]) + let of_option t x = match x with + | Some x -> some t x + | None -> none t +end + +module Pos = struct + + let path = ["Coq" ; "PArith"; "BinPos"] + let typ = lazy (init_constant path "positive") + let xI = lazy (init_constant path "xI") + let xO = lazy (init_constant path "xO") + let xH = lazy (init_constant path "xH") + + (* A coq positive from an int *) + let of_int n = + let rec aux n = + begin match n with + | n when n < 1 -> assert false + | 1 -> Lazy.force xH + | n -> mkApp + ( + (if n mod 2 = 0 + then Lazy.force xO + else Lazy.force xI + ), [| aux (n/2)|] + ) + end + in + aux n +end + +module Nat = struct + let path = ["Coq" ; "Init"; "Datatypes"] + let typ = lazy (init_constant path "nat") + let _S = lazy (init_constant path "S") + let _O = lazy (init_constant path "O") + (* A coq nat from an int *) + let of_int n = + let rec aux n = + begin match n with + | n when n < 0 -> assert false + | 0 -> Lazy.force _O + | n -> mkApp + ( + (Lazy.force _S + ), [| aux (n-1)|] + ) + end + in + aux n +end + +(** Lists from the standard library*) +module List = struct + let path = ["Coq"; "Lists"; "List"] + let typ = lazy (init_constant path "list") + let nil = lazy (init_constant path "nil") + let cons = lazy (init_constant path "cons") + let cons ty h t = + mkApp (Lazy.force cons, [| ty; h ; t |]) + let nil ty = + (mkApp (Lazy.force nil, [| ty |])) + let rec of_list ty = function + | [] -> nil ty + | t::q -> cons ty t (of_list ty q) + let type_of_list ty = + mkApp (Lazy.force typ, [|ty|]) +end + +(** Morphisms *) +module Classes = +struct + let classes_path = ["Coq";"Classes"; ] + let morphism = lazy (init_constant (classes_path@["Morphisms"]) "Proper") + let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence") + let reflexive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Reflexive") + let transitive = lazy (init_constant (classes_path@ ["RelationClasses"]) "Transitive") + + (** build the type [Equivalence ty rel] *) + let mk_equivalence ty rel = + mkApp (Lazy.force equivalence, [| ty; rel|]) + + + (** build the type [Reflexive ty rel] *) + let mk_reflexive ty rel = + mkApp (Lazy.force reflexive, [| ty; rel|]) + + (** build the type [Proper rel t] *) + let mk_morphism ty rel t = + mkApp (Lazy.force morphism, [| ty; rel; t|]) + + (** build the type [Transitive ty rel] *) + let mk_transitive ty rel = + mkApp (Lazy.force transitive, [| ty; rel|]) +end + +module Relation = struct + type t = + { + carrier : constr; + r : constr; + } + + let make ty r = {carrier = ty; r = r } + let split t = t.carrier, t.r +end + +module Transitive = struct + type t = + { + carrier : constr; + leq : constr; + transitive : constr; + } + let make ty leq transitive = {carrier = ty; leq = leq; transitive = transitive} + let infer goal ty leq = + let ask = Classes.mk_transitive ty leq in + let transitive , goal = resolve_one_typeclass goal ask in + make ty leq transitive, goal + let from_relation goal rlt = + infer goal (rlt.Relation.carrier) (rlt.Relation.r) + let cps_from_relation rlt k = + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_transitive ty r in + cps_resolve_one_typeclass ask + (fun trans -> k (make ty r trans) ) + let to_relation t = + {Relation.carrier = t.carrier; Relation.r = t.leq} + +end + +module Equivalence = struct + type t = + { + carrier : constr; + eq : constr; + equivalence : constr; + } + let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence} + let infer goal ty eq = + let ask = Classes.mk_equivalence ty eq in + let equivalence , goal = resolve_one_typeclass goal ask in + make ty eq equivalence, goal + let from_relation goal rlt = + infer goal (rlt.Relation.carrier) (rlt.Relation.r) + let cps_from_relation rlt k = + let ty =rlt.Relation.carrier in + let r = rlt.Relation.r in + let ask = Classes.mk_equivalence ty r in + cps_resolve_one_typeclass ask (fun equiv -> k (make ty r equiv) ) + let to_relation t = + {Relation.carrier = t.carrier; Relation.r = t.eq} + let split t = + t.carrier, t.eq, t.equivalence +end +end +(**[ match_as_equation goal eqt] see [eqt] as an equation. An + optionnal rel_context can be provided to ensure taht the term + remains typable*) +let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = + let env = Tacmach.pf_env goal in + let env = Environ.push_rel_context context env in + let evar_map = Tacmach.project goal in + begin + match decomp_term equation with + | App(c,ca) when Array.length ca >= 2 -> + let n = Array.length ca in + let left = ca.(n-2) in + let right = ca.(n-1) in + let r = (mkApp (c, Array.sub ca 0 (n - 2))) in + let carrier = Typing.type_of env evar_map left in + let rlt =Std.Relation.make carrier r + in + Some (left, right, rlt ) + | _ -> None + end + + +(** {1 Tacticals} *) + +let tclTIME msg tac = fun gl -> + let u = Sys.time () in + let r = tac gl in + let _ = Pp.msgnl (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in + r + +let tclDEBUG msg tac = fun gl -> + let _ = Pp.msgnl (Pp.str msg) in + tac gl + +let tclPRINT tac = fun gl -> + let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in + tac gl + + +(** {1 Error related mechanisms} *) +(* functions to handle the failures of our tactic. Some should be + reported [anomaly], some are on behalf of the user [user_error]*) +let anomaly msg = + Util.anomaly ("[aac_tactics] " ^ msg) + +let user_error msg = + Util.error ("[aac_tactics] " ^ msg) + +let warning msg = + Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) + + +(** {1 Rewriting tactics used in aac_rewrite} *) +module Rewrite = struct +(** Some informations about the hypothesis, with an (informal) + invariant: + - [typeof hyp = hyptype] + - [hyptype = forall context, body] + - [body = rel left right] + +*) + +type hypinfo = + { + hyp : Term.constr; (** the actual constr corresponding to the hypothese *) + hyptype : Term.constr; (** the type of the hypothesis *) + context : Term.rel_context; (** the quantifications of the hypothese *) + body : Term.constr; (** the body of the type of the hypothesis*) + rel : Std.Relation.t; (** the relation *) + left : Term.constr; (** left hand side *) + right : Term.constr; (** right hand side *) + l2r : bool; (** rewriting from left to right *) + } + +let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proof_type.tactic = fun goal -> + let ctype = Tacmach.pf_type_of goal c in + let (rel_context, body_type) = Term.decompose_prod_assum ctype in + let rec check f e = + match decomp_term e with + | Term.Rel i -> + let name, constr_option, types = Term.lookup_rel i rel_context + in f types + | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e + in + begin match check_type with + | None -> () + | Some f -> + if not (check f body_type) + then user_error "Unable to deal with higher-order or heterogeneous patterns"; + end; + begin + match match_as_equation ~context:rel_context goal body_type with + | None -> + user_error "The hypothesis is not an applied relation" + | Some (hleft,hright,hrlt) -> + k { + hyp = c; + hyptype = ctype; + body = body_type; + l2r = l2r; + context = rel_context; + rel = hrlt ; + left =hleft; + right = hright; + } + goal + end + + +(* The problem : Given a term to rewrite of type [H :forall xn ... x1, + t], we have to instanciate the subset of [xi] of type + [carrier]. [subst : (int * constr)] is the mapping the debruijn + indices in [t] to the [constrs]. We need to handle the rest of the + indexes. Two ways : + + - either using fresh evars and rewriting [H tn ?1 tn-2 ?2 ] + - either building a term like [fun 1 2 => H tn 1 tn-2 2] + + Both these terms have the same type. +*) + + +(* Fresh evars for everyone (should be the good way to do this + recompose in Coq v8.4) *) +let recompose_prod + (context : Term.rel_context) + (subst : (int * Term.constr) list) + env + em + : Evd.evar_map * Term.constr list = + (* the last index of rel relevant for the rewriting *) + let min_n = List.fold_left + (fun acc (x,_) -> min acc x) + (List.length context) subst in + let rec aux context acc em n = + let _ = Printf.printf "%i\n%!" n in + match context with + | [] -> + env, em, acc + | ((name,c,ty) as t)::q -> + let env, em, acc = aux q acc em (n+1) in + if n >= min_n + then + let em,x = + try em, List.assoc n subst + with | Not_found -> + Evarutil.new_evar em env (Term.substl acc ty) + in + (Environ.push_rel t env), em,x::acc + else + env,em,acc + in + let _,em,acc = aux context [] em 1 in + em, acc + +(* no fresh evars : instead, use a lambda abstraction around an + application to handle non-instanciated variables. *) + +let recompose_prod' + (context : Term.rel_context) + (subst : (int *Term.constr) list) + c + = + let rec popn pop n l = + if n <= 0 then l + else match l with + | [] -> [] + | t::q -> pop t :: (popn pop (n-1) q) + in + let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) in + let rec aux sign n next app ctxt = + match sign with + | [] -> List.rev app, List.rev ctxt + | decl::sign -> + try let term = (List.assoc n subst) in + aux sign (n+1) next (term::app) (None :: ctxt) + with + | Not_found -> + let term = Term.mkRel next in + aux sign (n+1) (next+1) (term::app) (Some decl :: ctxt) + in + let app,ctxt = aux context 1 1 [] [] in + (* substitutes in the context *) + let rec update ctxt app = + match ctxt,app with + | [],_ -> [] + | _,[] -> [] + | None :: sign, _ :: app -> + None :: update sign (List.map (Termops.pop) app) + | Some decl :: sign, _ :: app -> + Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) + in + let ctxt = update ctxt app in + (* updates the rel accordingly, taking some care not to go to far + beyond: it is important not to lift indexes homogeneously, we + have to update *) + let rec update ctxt res n = + match ctxt with + | [] -> List.rev res + | None :: sign -> + (update (sign) (popn pop_rel_decl n res) 0) + | Some decl :: sign -> + update sign (decl :: res) (n+1) + in + let ctxt = update ctxt [] 0 in + let c = Term.applistc c (List.rev app) in + let c = Term.it_mkLambda_or_LetIn c (ctxt) in + c + +(* Version de Matthieu +let subst_rel_context k cstr ctx = + let (_, ctx') = + List.fold_left (fun (k, ctx') (id, b, t) -> (succ k, (id, Option.map + (Term.substnl [cstr] k) b, Term.substnl [cstr] k t) :: ctx')) (k, []) + ctx in List.rev ctx' + +let recompose_prod' context subst c = + let len = List.length context in + let rec aux sign n next app ctxt = + match sign with + | [] -> List.rev app, List.rev ctxt + | decl::sign -> + try let term = (List.assoc n subst) in + aux (subst_rel_context 0 term sign) (pred n) (succ next) + (term::List.map (Term.lift (-1)) app) ctxt + with Not_found -> + let term = Term.mkRel (len - next) in + aux sign (pred n) (succ next) (term::app) (decl :: ctxt) + in + let app,ctxt = aux (List.rev context) len 0 [] [] in + Term.it_mkLambda_or_LetIn (Term.applistc c(app)) (List.rev ctxt) +*) + +let build + (h : hypinfo) + (subst : (int *Term.constr) list) + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic = fun goal -> + let c = recompose_prod' h.context subst h.hyp in + Tacticals.tclTHENLIST [k c] goal + +let build_with_evar + (h : hypinfo) + (subst : (int *Term.constr) list) + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic + = fun goal -> + Tacmach.pf_apply + (fun env em -> + let evar_map, acc = recompose_prod h.context subst env em in + let c = Term.applistc h.hyp (List.rev acc) in + Tacticals.tclTHENLIST [Refiner.tclEVARS evar_map; k c] goal + ) goal + + +let rewrite ?(abort=false)hypinfo subst k = + build hypinfo subst + (fun rew -> + let tac = + if not abort then + Equality.general_rewrite_bindings + hypinfo.l2r + Termops.all_occurrences + true (* tell if existing evars must be frozen for instantiation *) + false + (rew,Glob_term.NoBindings) + true + else + Tacticals.tclIDTAC + in k tac + ) + + +end + +include Std |