diff options
Diffstat (limited to 'coq.ml')
| -rwxr-xr-x[-rw-r--r--] | coq.ml | 60 |
1 files changed, 32 insertions, 28 deletions
@@ -19,17 +19,21 @@ 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) + 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 = - { Tacexpr.onhyps = Some []; - Tacexpr.concl_occs = Glob_term.no_occurrences_expr + { 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) @@ -38,20 +42,20 @@ let cps_mk_letin 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 + 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 + 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 (em,x) = Evarutil.new_evar env evar_map ty in x,( goal_update goal em) let resolve_one_typeclass goal ty : constr*goal_sigma= @@ -69,8 +73,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 -> Util.anomaly "Cannot resolve a typeclass : please report" - | Some x -> Util.error x + | None -> Errors.anomaly (Pp.str "Cannot resolve a typeclass : please report") + | Some x -> Errors.error x end in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal @@ -84,28 +88,28 @@ 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 evar_map env x in + let (em,x) = Evarutil.new_evar env evar_map 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 (em,x) = Evarutil.new_evar env evar_map 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 (em,r) = Evarutil.new_evar env evar_map 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 + let (em,r) = Evarutil.new_evar env em ty in Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal ) goal @@ -148,8 +152,6 @@ 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|] - let eq ty = Term.mkApp (init_constant path "eq", [| ty |]) - end module Option = struct @@ -319,7 +321,7 @@ 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 match_as_equation ?(context = Context.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 @@ -330,7 +332,7 @@ let match_as_equation ?(context = Term.empty_rel_context) goal equation : (const 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 carrier = Typing.unsafe_type_of env evar_map left in let rlt =Std.Relation.make carrier r in Some (left, right, rlt ) @@ -359,10 +361,10 @@ 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 = - Util.anomaly ("[aac_tactics] " ^ msg) + Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg) let user_error msg = - Util.error ("[aac_tactics] " ^ msg) + Errors.error ("[aac_tactics] " ^ msg) let warning msg = Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg)) @@ -382,7 +384,7 @@ 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 *) + context : Context.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 *) @@ -391,12 +393,12 @@ 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 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 -> - let name, constr_option, types = Term.lookup_rel i rel_context + let name, constr_option, types = Context.lookup_rel i rel_context in f types | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e in @@ -441,7 +443,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 : Term.rel_context) + (context : Context.rel_context) (subst : (int * Term.constr) list) env em @@ -462,7 +464,7 @@ let recompose_prod let em,x = try em, List.assoc n subst with | Not_found -> - Evarutil.new_evar em env (Term.substl acc ty) + Evarutil.new_evar env em (Vars.substl acc ty) in (Environ.push_rel t env), em,x::acc else @@ -475,7 +477,7 @@ let recompose_prod application to handle non-instanciated variables. *) let recompose_prod' - (context : Term.rel_context) + (context : Context.rel_context) (subst : (int *Term.constr) list) c = @@ -506,7 +508,7 @@ let recompose_prod' | 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) + 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 @@ -576,13 +578,15 @@ let rewrite ?(abort=false)hypinfo subst k = (fun rew -> let tac = if not abort then + Proofview.V82.of_tactic begin Equality.general_rewrite_bindings hypinfo.l2r - Termops.all_occurrences + Locus.AllOccurrences true (* tell if existing evars must be frozen for instantiation *) false - (rew,Glob_term.NoBindings) + (rew,Misctypes.NoBindings) true + end else Tacticals.tclIDTAC in k tac |