From 8ab748064ddeec8400859e210bf9963826cba631 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 1 Dec 2010 13:33:41 +0100 Subject: Imported Upstream version 0.2.1 --- AAC_coq.ml | 374 ++++++++++++++++++++++++++++++------------------------------- 1 file changed, 187 insertions(+), 187 deletions(-) (limited to 'AAC_coq.ml') diff --git a/AAC_coq.ml b/AAC_coq.ml index cbe4beb..b3ee180 100644 --- a/AAC_coq.ml +++ b/AAC_coq.ml @@ -14,7 +14,7 @@ open Names open Coqlib (* The contrib name is used to locate errors when loading constrs *) -let contrib_name = "aac_tactics" +let contrib_name = "aac_tactics" (* Getting constrs (primitive Coq terms) from existing Coq libraries. *) @@ -25,93 +25,93 @@ 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 = Rawterm.no_occurrences_expr +let nowhere = + { Tacexpr.onhyps = Some []; + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } -let cps_mk_letin +let cps_mk_letin (name:string) (c: constr) - (k : constr -> Proof_type.tactic) + (k : constr -> Proof_type.tactic) : Proof_type.tactic = - fun goal -> + 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 + 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 +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 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 + 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 + 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 +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 + in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal ) goal -let nf_evar goal c : Term.constr= - let evar_map = Tacmach.project goal in +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 +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 + +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 +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 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} *) @@ -119,7 +119,7 @@ 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") @@ -132,7 +132,7 @@ module Bool = struct 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 = + let of_bool b = if b then Lazy.force ctrue else Lazy.force cfalse end @@ -157,13 +157,13 @@ module Option = struct 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 + let of_option t x = match x with | Some x -> some t x | None -> none t -end +end module Pos = struct - + let path = ["Coq" ; "NArith"; "BinPos"] let typ = lazy (init_constant path "positive") let xI = lazy (init_constant path "xI") @@ -172,14 +172,14 @@ module Pos = struct (* A coq positive from an int *) let of_int n = - let rec aux n = - begin match n with + let rec aux n = + begin match n with | n when n < 1 -> assert false - | 1 -> Lazy.force xH - | n -> mkApp + | 1 -> Lazy.force xH + | n -> mkApp ( - (if n mod 2 = 0 - then Lazy.force xO + (if n mod 2 = 0 + then Lazy.force xO else Lazy.force xI ), [| aux (n/2)|] ) @@ -187,7 +187,7 @@ module Pos = struct in aux n end - + module Nat = struct let path = ["Coq" ; "Init"; "Datatypes"] let typ = lazy (init_constant path "nat") @@ -195,11 +195,11 @@ module Nat = struct 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 + let rec aux n = + begin match n with | n when n < 0 -> assert false | 0 -> Lazy.force _O - | n -> mkApp + | n -> mkApp ( (Lazy.force _S ), [| aux (n-1)|] @@ -208,24 +208,24 @@ module Nat = struct 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 = + 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 + 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 @@ -263,7 +263,7 @@ module Relation = struct let make ty r = {carrier = ty; r = r } let split t = t.carrier, t.r end - + module Transitive = struct type t = { @@ -272,19 +272,19 @@ module Transitive = struct 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 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 + 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 = + let to_relation t = {Relation.carrier = t.carrier; Relation.r = t.leq} end @@ -297,55 +297,55 @@ module Equivalence = struct 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 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 + 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 = + let to_relation t = {Relation.carrier = t.carrier; Relation.r = t.eq} let split t = t.carrier, t.eq, t.equivalence end -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 +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 + 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 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 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 + in Some (left, right, rlt ) | _ -> None - end + 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 + 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 + let _ = Pp.msgnl (Pp.str msg) in tac gl let tclPRINT tac = fun gl -> @@ -356,24 +356,24 @@ let tclPRINT tac = fun 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 = +let anomaly msg = Util.anomaly ("[aac_tactics] " ^ msg) -let user_error 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: + invariant: - [typeof hyp = hyptype] - [hyptype = forall context, body] - [body = rel left right] - + *) type hypinfo = @@ -389,24 +389,24 @@ type hypinfo = } 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 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 + | 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 + in + begin match check_type with | None -> () - | Some f -> - if not (check f body_type) + | Some f -> + if not (check f body_type) then user_error "Unable to deal with higher-order or heterogeneous patterns"; end; - begin + begin match match_as_equation ~context:rel_context goal body_type with - | None -> + | None -> user_error "The hypothesis is not an applied relation" | Some (hleft,hright,hrlt) -> k { @@ -417,11 +417,11 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo context = rel_context; rel = hrlt ; left =hleft; - right = hright; + 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 @@ -438,75 +438,75 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo (* Fresh evars for everyone (should be the good way to do this recompose in Coq v8.4) *) -let recompose_prod +let recompose_prod (context : Term.rel_context) - (subst : (int * Term.constr) list) + (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 + 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 -> + | ((name,c,ty) as t)::q -> let env, em, acc = aux q acc em (n+1) in - if n >= min_n + 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 + 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 + 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' + +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 + 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 + 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 + match sign with + | [] -> List.rev app, List.rev ctxt | decl::sign -> - try let term = (List.assoc n subst) in + 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 + | 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 + in + let app,ctxt = aux context 1 1 [] [] in (* substitutes in the context *) let rec update ctxt app = - match ctxt,app with + 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 + | 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 *) @@ -519,68 +519,68 @@ let recompose_prod' 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 + 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 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 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 + 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) + 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 + 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) +let build + (h : hypinfo) (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) + (k :Term.constr -> Proof_type.tactic) : Proof_type.tactic = fun goal -> - let c = recompose_prod' h.context subst h.hyp in + let c = recompose_prod' h.context subst h.hyp in Tacticals.tclTHENLIST [k c] goal -let build_with_evar - (h : hypinfo) +let build_with_evar + (h : hypinfo) (subst : (int *Term.constr) list) - (k :Term.constr -> Proof_type.tactic) - : Proof_type.tactic + (k :Term.constr -> Proof_type.tactic) + : Proof_type.tactic = fun goal -> - Tacmach.pf_apply - (fun env em -> + 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 + ) goal -let rewrite ?(abort=false)hypinfo subst k = - build hypinfo subst - (fun rew -> +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 + hypinfo.l2r + Termops.all_occurrences false (rew,Rawterm.NoBindings) true - else + else Tacticals.tclIDTAC in k tac ) -- cgit v1.2.3