diff options
Diffstat (limited to 'coq.ml')
| -rwxr-xr-x | coq.ml | 65 |
1 files changed, 39 insertions, 26 deletions
@@ -12,6 +12,8 @@ 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" @@ -55,7 +57,9 @@ let goal_update (goal : goal_sigma) evar_map : goal_sigma= 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 env evar_map ty 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= @@ -73,8 +77,8 @@ let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr -> Proof_type try Typeclasses.resolve_one_typeclass env em t with Not_found -> begin match error with - | None -> Errors.anomaly (Pp.str "Cannot resolve a typeclass : please report") - | Some x -> Errors.error x + | 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 @@ -88,28 +92,36 @@ let nf_evar goal c : Term.constr= 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 env evar_map x 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 (em,x) = Evarutil.new_evar env evar_map ty 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 (em,r) = Evarutil.new_evar env evar_map ty 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,r) = Evarutil.new_evar env em ty 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 @@ -319,9 +331,9 @@ module Equivalence = struct end end (**[ match_as_equation goal eqt] see [eqt] as an equation. An - optionnal rel_context can be provided to ensure taht the term + optionnal rel-context can be provided to ensure that the term remains typable*) -let match_as_equation ?(context = Context.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option = +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 @@ -345,15 +357,15 @@ let match_as_equation ?(context = Context.empty_rel_context) goal equation : (co 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 _ = Feedback.msg_notice (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 _ = Feedback.msg_debug (Pp.str msg) in tac gl let tclPRINT tac = fun gl -> - let _ = Pp.msgnl (Printer.pr_constr (Tacmach.pf_concl gl)) in + let _ = Feedback.msg_notice (Printer.pr_constr (Tacmach.pf_concl gl)) in tac gl @@ -361,13 +373,13 @@ let tclPRINT tac = fun gl -> (* 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 = - Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg) + CErrors.anomaly ~label:"[aac_tactics]" (Pp.str msg) let user_error msg = - Errors.error ("[aac_tactics] " ^ msg) + CErrors.error ("[aac_tactics] " ^ msg) let warning msg = - Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) + Feedback.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) (** {1 Rewriting tactics used in aac_rewrite} *) @@ -384,7 +396,7 @@ type hypinfo = { hyp : Term.constr; (** the actual constr corresponding to the hypothese *) hyptype : Term.constr; (** the type of the hypothesis *) - context : Context.rel_context; (** the quantifications of the hypothese *) + 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 *) @@ -397,16 +409,14 @@ let get_hypinfo c ~l2r ?check_type (k : hypinfo -> Proof_type.tactic) : Proo 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 = Context.lookup_rel i rel_context - in f types + | 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"; + 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 @@ -443,7 +453,7 @@ 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 - (context : Context.rel_context) + (context : Context.Rel.t) (subst : (int * Term.constr) list) env em @@ -457,14 +467,17 @@ let recompose_prod match context with | [] -> env, em, acc - | ((name,c,ty) as t)::q -> + | 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 env em (Vars.substl acc ty) + 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 @@ -477,7 +490,7 @@ let recompose_prod application to handle non-instanciated variables. *) let recompose_prod' - (context : Context.rel_context) + (context : Context.Rel.t) (subst : (int *Term.constr) list) c = @@ -487,7 +500,7 @@ let recompose_prod' | [] -> [] | t::q -> pop t :: (popn pop (n-1) q) in - let pop_rel_decl (name,c,ty) = (name,c,Termops.pop ty) 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 |