From 8018e923c75eb5504310864f821972f794b7d554 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Wed, 13 Feb 2019 20:40:51 -0500 Subject: New upstream version 8.8.0+1.gbp069dc3b --- coq.ml | 611 ----------------------------------------------------------------- 1 file changed, 611 deletions(-) delete mode 100755 coq.ml (limited to 'coq.ml') diff --git a/coq.ml b/coq.ml deleted file mode 100755 index eb4b5f1..0000000 --- a/coq.ml +++ /dev/null @@ -1,611 +0,0 @@ -(***************************************************************************) -(* 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 -open Sigma.Notations -open Context.Rel.Declaration - -(* 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 = - Universes.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 = - { Locus.onhyps = Some []; - Locus.concl_occs = Locus.NoOccurrences - } - -let retype c gl = - let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in - Refiner.tclEVARS sigma gl - -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 = (Proofview.V82.of_tactic (Tactics.letin_tac None (Name name) c None nowhere)) in - Tacticals.tclTHENLIST [retype c; 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 evar_map = Sigma.Unsafe.of_evar_map evar_map in - let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in - let em = Sigma.to_evar_map em 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 -> CErrors.anomaly (Pp.str "Cannot resolve a typeclass : please report") - | Some x -> CErrors.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 evar_map = Sigma.Unsafe.of_evar_map evar_map in - let Sigma (x,em,_) = Evarutil.new_evar env evar_map x in - let em = Sigma.to_evar_map em 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 evar_map = Sigma.Unsafe.of_evar_map evar_map in - let Sigma (x,em,_) = Evarutil.new_evar env evar_map ty in - let em = Sigma.to_evar_map em 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 evar_map = Sigma.Unsafe.of_evar_map evar_map in - let Sigma (r, em, _) = Evarutil.new_evar env evar_map ty in - let em = Sigma.to_evar_map em 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 = Sigma.Unsafe.of_evar_map em in - let Sigma (r, em, _) = Evarutil.new_evar env em ty in - let em = Sigma.to_evar_map em 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 that the term - remains typable*) -let match_as_equation ?(context = Context.Rel.empty) 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.unsafe_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 _ = Feedback.msg_notice (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in - r - -let tclDEBUG msg tac = fun gl -> - let _ = Feedback.msg_debug (Pp.str msg) in - tac gl - -let tclPRINT tac = fun gl -> - let _ = Feedback.msg_notice (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 = - CErrors.anomaly ~label:"[aac_tactics]" (Pp.str msg) - -let user_error msg = - CErrors.error ("[aac_tactics] " ^ msg) - -let warning msg = - Feedback.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 : Context.Rel.t; (** 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_unsafe_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 -> f (get_type (Context.Rel.lookup i rel_context)) - | _ -> 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 : Context.Rel.t) - (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 - | 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 -> - let em = Sigma.Unsafe.of_evar_map em in - let Sigma (r, em, _) = Evarutil.new_evar env em (Vars.substl acc (get_type t)) in - let em = Sigma.to_evar_map em in - (em, r) - 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 : Context.Rel.t) - (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 = map_type Termops.pop 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 (Vars.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 - Proofview.V82.of_tactic begin - Equality.general_rewrite_bindings - hypinfo.l2r - Locus.AllOccurrences - true (* tell if existing evars must be frozen for instantiation *) - false - (rew,Misctypes.NoBindings) - true - end - else - Tacticals.tclIDTAC - in k tac - ) - - -end - -include Std -- cgit v1.2.3