diff options
Diffstat (limited to 'coq.ml')
| -rw-r--r-- | coq.ml | 212 |
1 files changed, 0 insertions, 212 deletions
@@ -1,212 +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 - - -(* The contrib name is used to locate errors when loading constrs *) -let contrib_name = "aac_tactics" - -(* Getting constrs (primitive Coq terms) from exisiting 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 = Rawterm.no_occurrences_expr - } - - -let mk_letin (name: string) (constr: constr) : constr * Proof_type.tactic = - let name = (Names.id_of_string name) in - let letin = - (Tactics.letin_tac - None - (Name name) - constr - None (* or Some ty *) - nowhere - ) in - mkVar name, letin - -let mk_letin' (name: string) (constr: constr) : constr * Proof_type.tactic - = - constr, Tacticals.tclIDTAC - - - -(** {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 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 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) (rlt : constr * 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 (fst rlt) in - x,(goal_update gl em) - -let evar_binary (gl: goal_sigma) (rlt: constr * constr) = - let env = Tacmach.pf_env gl in - let evar_map = Tacmach.project gl in - let x = fst rlt 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) - -(* decomp_term : constr -> (constr, types) kind_of_term *) -let decomp_term c = kind_of_term (strip_outer_cast c) - - -(** {2 Bindings with Coq' Standard Library} *) - -module Pair = struct - - let path = ["Coq"; "Init"; "Datatypes"] - let typ = lazy (init_constant path "prod") - let pair = lazy (init_constant path "pair") -end - -module Pos = struct - - let path = ["Coq" ; "NArith"; "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") - - (** build the constr [Proper rel t] *) - let mk_morphism ty rel t = - mkApp (Lazy.force morphism, [| ty; rel; t|]) - - let equivalence = lazy (init_constant (classes_path@ ["RelationClasses"]) "Equivalence") - - (** build the constr [Equivalence ty rel] *) - let mk_equivalence ty rel = - mkApp (Lazy.force equivalence, [| ty; rel|]) -end - -(** a [mset] is a ('a * pos) list *) -let mk_mset ty (l : (constr * int) list) = - let pos = Lazy.force Pos.typ in - let pair_ty = mkApp (Lazy.force Pair.typ , [| ty; pos|]) in - let pair (x : constr) (ar : int) = - mkApp (Lazy.force Pair.pair, [| ty ; pos ; x ; Pos.of_int ar|]) in - let rec aux = function - | [] -> List.nil pair_ty - | (t,ar)::q -> List.cons pair_ty (pair t ar) (aux q) - in - aux l - -(** x r *) -type reltype = Term.constr * Term.constr -(** x r e *) -type eqtype = reltype * Term.constr - - -(** {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 - |