summaryrefslogtreecommitdiff
path: root/theory.ml
diff options
context:
space:
mode:
Diffstat (limited to 'theory.ml')
-rw-r--r--theory.ml708
1 files changed, 708 insertions, 0 deletions
diff --git a/theory.ml b/theory.ml
new file mode 100644
index 0000000..45a76f1
--- /dev/null
+++ b/theory.ml
@@ -0,0 +1,708 @@
+(***************************************************************************)
+(* 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. *)
+(***************************************************************************)
+
+(** Constr from the theory of this particular development
+
+ The inner-working of this module is highly correlated with the
+ particular structure of {b AAC.v}, therefore, it should
+ be of little interest to most readers.
+*)
+
+
+open Term
+
+let ac_theory_path = ["AAC"]
+
+module Sigma = struct
+ let sigma = lazy (Coq.init_constant ac_theory_path "sigma")
+ let sigma_empty = lazy (Coq.init_constant ac_theory_path "sigma_empty")
+ let sigma_add = lazy (Coq.init_constant ac_theory_path "sigma_add")
+ let sigma_get = lazy (Coq.init_constant ac_theory_path "sigma_get")
+
+ let add ty n x map =
+ mkApp (Lazy.force sigma_add,[|ty; n; x ; map|])
+ let empty ty =
+ mkApp (Lazy.force sigma_empty,[|ty |])
+ let typ ty =
+ mkApp (Lazy.force sigma, [|ty|])
+
+ let to_fun ty null map =
+ mkApp (Lazy.force sigma_get, [|ty;null;map|])
+
+ let of_list ty null l =
+ let map =
+ List.fold_left
+ (fun acc (i,t) -> assert (i > 0); add ty (Coq.Pos.of_int i) t acc)
+ (empty ty)
+ l
+ in to_fun ty null map
+end
+
+
+module Sym = struct
+ type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr}
+
+ let path = ac_theory_path @ ["Sym"]
+ let typ = lazy (Coq.init_constant path "pack")
+ let mkPack = lazy (Coq.init_constant path "mkPack")
+ let typeof = lazy (Coq.init_constant path "type_of")
+ let relof = lazy (Coq.init_constant path "rel_of")
+ let value = lazy (Coq.init_constant path "value")
+ let null = lazy (Coq.init_constant path "null")
+ let mk_typeof : Coq.reltype -> int -> constr = fun (x,r) n ->
+ mkApp (Lazy.force typeof, [| x ; Coq.Nat.of_int n |])
+ let mk_relof : Coq.reltype -> int -> constr = fun (x,r) n ->
+ mkApp (Lazy.force relof, [| x;r ; Coq.Nat.of_int n |])
+ let mk_pack ((x,r): Coq.reltype) s =
+ mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|])
+ let null eqt witness =
+ let (x,r),e = eqt in
+ mkApp (Lazy.force null, [| x;r;e;witness |])
+
+end
+
+module Sum = struct
+ type pack = {plus: Term.constr; zero: Term.constr ; opac: Term.constr}
+
+ let path = ac_theory_path @ ["Sum"]
+ let typ = lazy (Coq.init_constant path "pack")
+ let mkPack = lazy (Coq.init_constant path "mkPack")
+ let cstr_zero = lazy (Coq.init_constant path "zero")
+ let cstr_plus = lazy (Coq.init_constant path "plus")
+
+ let mk_pack: Coq.reltype -> pack -> Term.constr = fun (x,r) s ->
+ mkApp (Lazy.force mkPack , [| x ; r; s.plus; s.zero; s.opac|])
+
+ let zero: Coq.reltype -> constr -> constr = fun (x,r) pack ->
+ mkApp (Lazy.force cstr_zero, [| x;r;pack|])
+ let plus: Coq.reltype -> constr -> constr = fun (x,r) pack ->
+ mkApp (Lazy.force cstr_plus, [| x;r;pack|])
+
+
+end
+
+module Prd = struct
+ type pack = {dot: Term.constr; one: Term.constr ; opa: Term.constr}
+
+ let path = ac_theory_path @ ["Prd"]
+ let typ = lazy (Coq.init_constant path "pack")
+ let mkPack = lazy (Coq.init_constant path "mkPack")
+ let cstr_one = lazy (Coq.init_constant path "one")
+ let cstr_dot = lazy (Coq.init_constant path "dot")
+
+ let mk_pack: Coq.reltype -> pack -> Term.constr = fun (x,r) s ->
+ mkApp (Lazy.force mkPack , [| x ; r; s.dot; s.one; s.opa|])
+ let one: Coq.reltype -> constr -> constr = fun (x,r) pack ->
+ mkApp (Lazy.force cstr_one, [| x;r;pack|])
+ let dot: Coq.reltype -> constr -> constr = fun (x,r) pack ->
+ mkApp (Lazy.force cstr_dot, [| x;r;pack|])
+
+
+end
+
+
+let op_ac = lazy (Coq.init_constant ac_theory_path "Op_AC")
+let op_a = lazy (Coq.init_constant ac_theory_path "Op_A")
+
+(** The constants from the inductive type *)
+let _Tty = lazy (Coq.init_constant ac_theory_path "T")
+let vTty = lazy (Coq.init_constant ac_theory_path "vT")
+
+let rsum = lazy (Coq.init_constant ac_theory_path "sum")
+let rprd = lazy (Coq.init_constant ac_theory_path "prd")
+let rsym = lazy (Coq.init_constant ac_theory_path "sym")
+let vnil = lazy (Coq.init_constant ac_theory_path "vnil")
+let vcons = lazy (Coq.init_constant ac_theory_path "vcons")
+let eval = lazy (Coq.init_constant ac_theory_path "eval")
+let decide_thm = lazy (Coq.init_constant ac_theory_path "decide")
+
+(** Rebuild an equality *)
+let mk_equal = fun (x,r) left right ->
+ mkApp (r, [| left; right|])
+
+
+let anomaly msg =
+ Util.anomaly ("aac_tactics: " ^ msg)
+
+let user_error msg =
+ Util.error ("aac_tactics: " ^ msg)
+
+
+module Trans = struct
+
+
+ (** {1 From Coq to Abstract Syntax Trees (AST)}
+
+ This module provides facilities to interpret a Coq term with
+ arbitrary operators as an abstract syntax tree. Considering an
+ application, we try to infer instances of our classes. We
+ consider that raw morphisms ([Sym]) are coarser than [A]
+ operators, which in turn are coarser than [AC] operators. We
+ need to treat the units first. Indeed, considering [S] as a
+ morphism is problematic because [S O] is a unit.
+
+ During this reification, we gather some informations that will
+ be used to rebuild Coq terms from AST ( type {!envs}) *)
+
+ type pack =
+ | AC of Sum.pack (* the opac pack *)
+ | A of Prd.pack (* the opa pack *)
+ | Sym of Sym.pack (* the sym pack *)
+
+ type head =
+ | Fun
+ | Plus
+ | Dot
+ | One
+ | Zero
+
+
+ (* discr is a map from {!Term.constr} to
+ (head * pack).
+
+ [None] means that it is not possible to instantiate this partial
+ application to an interesting class.
+
+ [Some x] means that we found something in the past. This means in
+ particular that a single constr cannot be two things at the same
+ time.
+
+ However, for the transitivity process, we do not need to remember
+ if the constr was the unit or the binary operation. We will use
+ the projections from the module's record.
+
+ The field [bloom] allows to give a unique number to each class we
+ found. *)
+ type envs =
+ {
+ discr : (constr , (head * pack) option) Hashtbl.t ;
+
+ bloom : (pack, int ) Hashtbl.t;
+ bloom_back : (int, pack ) Hashtbl.t;
+ bloom_next : int ref;
+ }
+
+ let empty_envs () =
+ {
+ discr = Hashtbl.create 17;
+
+ bloom = Hashtbl.create 17;
+ bloom_back = Hashtbl.create 17;
+ bloom_next = ref 1;
+ }
+
+ let add_bloom envs pack =
+ if Hashtbl.mem envs.bloom pack
+ then ()
+ else
+ let x = ! (envs.bloom_next) in
+ Hashtbl.add envs.bloom pack x;
+ Hashtbl.add envs.bloom_back x pack;
+ incr (envs.bloom_next)
+
+ let find_bloom envs pack =
+ try Hashtbl.find envs.bloom pack
+ with Not_found -> assert false
+
+
+ (** try to infer the kind of operator we are dealing with *)
+ let is_morphism rlt papp ar goal =
+ let typeof = Sym.mk_typeof rlt ar in
+ let relof = Sym.mk_relof rlt ar in
+ let env = Tacmach.pf_env goal in
+ let evar_map = Tacmach.project goal in
+ let m = Coq.Classes.mk_morphism typeof relof papp in
+ try
+ let _ = Tacmach.pf_check_type goal papp typeof in
+ let evar_map,m = Typeclasses.resolve_one_typeclass env evar_map m in
+ let pack = {Sym.ar = (Coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in
+ Some (Coq.goal_update goal evar_map, Fun , Sym pack)
+ with
+ | Not_found -> None
+ | _ -> None
+
+ (** gives back the class *)
+ let is_op gl (rlt: Coq.reltype) pack op null =
+ let (x,r) = rlt in
+ let ty = mkApp (pack ,[|x;r; op; null |]) in
+ let env = Tacmach.pf_env gl in
+ let evar_map = Tacmach.project gl in
+ try
+ let em,t = Typeclasses.resolve_one_typeclass env evar_map ty in
+ let op = Evarutil.nf_evar em op in
+ let null = Evarutil.nf_evar em null in
+ Some (Coq.goal_update gl em,t,op,null)
+ with Not_found -> None
+
+
+ let is_plus (rlt: Coq.reltype) plus goal=
+ let (zero,goal) = Coq.evar_unit goal rlt in
+ match is_op goal rlt (Lazy.force op_ac) plus zero
+ with
+ | None -> None
+ | Some (gl,s,plus,zero) ->
+ let pack = {Sum.plus=plus;Sum.zero=zero;Sum.opac=s} in
+ Some (gl, Plus , AC pack)
+
+ let is_dot rlt dot goal=
+ let (one,goal) = Coq.evar_unit goal rlt in
+ match is_op goal rlt (Lazy.force op_a) dot one
+ with
+ | None -> None
+ | Some (goal,s,dot,one) ->
+ let pack = {Prd.dot=dot;Prd.one=one;Prd.opa=s} in
+ Some (goal, Dot, A pack)
+
+ let is_zero rlt zero goal =
+ let (plus,goal) = Coq.evar_binary goal rlt in
+ match is_op goal rlt (Lazy.force op_ac) plus zero
+ with
+ | None -> None
+ | Some (goal,s,plus,zero) ->
+ let pack = {Sum.plus=plus;Sum.zero=zero;Sum.opac=s} in
+ Some (goal, Zero , AC pack)
+
+ let is_one rlt one goal =
+ let (dot,goal) = Coq.evar_binary goal rlt in
+ match is_op goal rlt (Lazy.force op_a) dot one
+ with
+ | None -> None
+ | Some (goal,s,dot,one)->
+ let pack = {Prd.dot=dot;Prd.one=one;Prd.opa=s} in
+ Some (goal, One, A pack)
+
+
+ let (>>) x y a =
+ match x a with | None -> y a | x -> x
+
+ let is_unit rlt papp =
+ (is_zero rlt papp )>> (is_one rlt papp)
+
+ let what_is_it rlt papp ar goal :
+ (Coq.goal_sigma * head * pack ) option =
+ match ar with
+ | 2 ->
+ begin
+ (
+ (is_plus rlt papp)>>
+ (is_dot rlt papp)>>
+ (is_morphism rlt papp ar)
+ ) goal
+ end
+ | _ ->
+ is_morphism rlt papp ar goal
+
+
+
+
+ (** [discriminates goal envs rlt t ca] infer :
+
+ - the nature of the application [t ca] (is the head symbol a
+ Plus, a Dot, so on),
+
+ - its {! pack } (is it an AC operator, or an A operator, or a
+ Symbol ?),
+
+ - the relevant partial application,
+
+ - the vector of the remaining arguments
+
+ We use an expansion to handle the special case of units, before
+ going back to the general discrimination procedure *)
+ let discriminate goal envs (rlt : Coq.reltype) t ca : Coq.goal_sigma * head * pack * constr * constr array =
+ let nb_params = Array.length ca in
+ let f cont x p_app ar =
+ assert (0 <= ar && ar <= nb_params);
+ match x with
+ | Some (goal, discr, pack) ->
+ Hashtbl.add envs.discr p_app (Some (discr, pack));
+ add_bloom envs pack;
+ (goal, discr, pack, p_app, Array.sub ca (nb_params-ar) ar)
+ | None ->
+ begin
+ (* to memoise the failures *)
+ Hashtbl.add envs.discr p_app None;
+ (* will terminate, since [const] is
+ capped, and it is easy to find an
+ instance of a constant *)
+ cont goal (ar-1)
+ end
+ in
+ let rec aux goal ar :Coq.goal_sigma * head * pack * constr * constr array =
+ assert (0 <= ar && ar <= nb_params);
+ let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in
+ begin
+ try
+ begin match Hashtbl.find envs.discr p_app with
+ | None -> aux goal (ar-1)
+ | Some (discr,sym) ->
+ goal,
+ discr,
+ sym,
+ p_app,
+ Array.sub ca (nb_params -ar ) ar
+ end
+ with
+ Not_found -> (* Could not find this constr *)
+ f aux (what_is_it rlt p_app ar goal) p_app ar
+ end
+ in
+ match is_unit rlt (mkApp (t,ca)) goal with
+ | None -> aux goal (nb_params)
+ | x -> f (fun _ -> assert false) x (mkApp (t,ca)) 0
+
+ let discriminate goal envs rlt x =
+ try
+ match Coq.decomp_term x with
+ | Var _ ->
+ discriminate goal envs rlt x [| |]
+ | App (t,ca) ->
+ discriminate goal envs rlt t ca
+ | Construct c ->
+ discriminate goal envs rlt x [| |]
+ | _ ->
+ assert false
+ with
+ (* TODO: is it the only source of invalid use that fall into
+ this catch_all ? *)
+ e -> user_error "cannot handle this kind of hypotheses (higher order function symbols, variables occuring under a non-morphism, etc)."
+
+
+ (** [t_of_constr goal rlt envs cstr] builds the abstract syntax
+ tree of the term [cstr]. Doing so, it modifies the environment
+ of known stuff [envs], and eventually creates fresh
+ evars. Therefore, we give back the goal updated accordingly *)
+ let t_of_constr goal (rlt: Coq.reltype ) envs : constr -> Matcher.Terms.t *Coq.goal_sigma =
+ let r_evar_map = ref (goal) in
+ let rec aux x =
+ match Coq.decomp_term x with
+ | Rel i -> Matcher.Terms.Var i
+ | _ ->
+ let goal, sym, pack , p_app, ca = discriminate (!r_evar_map) envs rlt x in
+ r_evar_map := goal;
+ let k = find_bloom envs pack
+ in
+ match sym with
+ | Plus ->
+ assert (Array.length ca = 2);
+ Matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1))
+ | Zero ->
+ assert (Array.length ca = 0);
+ Matcher.Terms.Zero ( k)
+ | Dot ->
+ assert (Array.length ca = 2);
+ Matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1))
+ | One ->
+ assert (Array.length ca = 0);
+ Matcher.Terms.One ( k)
+ | Fun ->
+ Matcher.Terms.Sym ( k, Array.map aux ca)
+ in
+ (
+ fun x -> let r = aux x in r, !r_evar_map
+ )
+
+ (** {1 From AST back to Coq }
+
+ The next functions allow one to map OCaml abstract syntax trees
+ to Coq terms *)
+
+ (** {2 Building raw, natural, terms} *)
+
+ (** [raw_constr_of_t] rebuilds a term in the raw representation *)
+ let raw_constr_of_t envs (rlt : Coq.reltype) (t : Matcher.Terms.t) : Term.constr =
+ let add_set,get =
+ let r = ref [] in
+ let rec add x = function
+ [ ] -> [x]
+ | t::q when t = x -> t::q
+ | t::q -> t:: (add x q)
+ in
+ (fun x -> r := add x !r),(fun () -> !r)
+ in
+ let rec aux t =
+ match t with
+ | Matcher.Terms.Plus (s,l,r) ->
+ begin match Hashtbl.find envs.bloom_back s with
+ | AC s ->
+ mkApp (s.Sum.plus , [|(aux l);(aux r)|])
+ | _ -> assert false
+ end
+ | Matcher.Terms.Dot (s,l,r) ->
+ begin match Hashtbl.find envs.bloom_back s with
+ | A s ->
+ mkApp (s.Prd.dot, [|(aux l);(aux r)|])
+ | _ -> assert false
+ end
+ | Matcher.Terms.Sym (s,t) ->
+ begin match Hashtbl.find envs.bloom_back s with
+ | Sym s ->
+ mkApp (s.Sym.value, Array.map aux t)
+ | _ -> assert false
+ end
+ | Matcher.Terms.One x ->
+ begin match Hashtbl.find envs.bloom_back x with
+ | A s ->
+ s.Prd.one
+ | _ -> assert false
+ end
+ | Matcher.Terms.Zero x ->
+ begin match Hashtbl.find envs.bloom_back x with
+ | AC s ->
+ s.Sum.zero
+ | _ -> assert false
+ end
+ | Matcher.Terms.Var i -> add_set i;
+ let i = (Names.id_of_string (Printf.sprintf "x%i" i)) in
+ mkVar (i)
+ in
+ let x = fst rlt in
+ let rec cap c = function [] -> c
+ | t::q -> let i = (Names.id_of_string (Printf.sprintf "x%i" t)) in
+ cap (mkNamedProd i x c) q
+ in
+ cap ((aux t)) (get ())
+ (* aux t is possible for printing only, but I wonder what
+ would be the status of such a term*)
+
+
+ (** {2 Building reified terms} *)
+
+ (* Some informations to be able to build the maps *)
+ type reif_params =
+ {
+ a_null : constr;
+ ac_null : constr;
+ sym_null : constr;
+ a_ty : constr;
+ ac_ty : constr;
+ sym_ty : constr;
+ }
+
+ type sigmas = {
+ env_sym : Term.constr;
+ env_sum : Term.constr;
+ env_prd : Term.constr;
+ }
+ (** A record containing the environments that will be needed by the
+ decision procedure, as a Coq constr. Contains also the functions
+ from the symbols (as ints) to indexes (as constr) *)
+ type sigma_maps = {
+ sym_to_pos : int -> Term.constr;
+ sum_to_pos : int -> Term.constr;
+ prd_to_pos : int -> Term.constr;
+ }
+
+ (* convert the [envs] into the [sigma_maps] *)
+ let envs_to_list rlt envs =
+ let add x y (n,l) = (n+1, (x, ( n, y))::l) in
+ let nil = 1,[]in
+ Hashtbl.fold
+ (fun int pack (sym,sum,prd) ->
+ match pack with
+ |AC s ->
+ let s = Sum.mk_pack rlt s in
+ sym, add (int) s sum, prd
+ |A s ->
+ let s = Prd.mk_pack rlt s in
+ sym, sum, add (int) s prd
+ | Sym s ->
+ let s = Sym.mk_pack rlt s in
+ add (int) s sym, sum, prd
+ )
+ envs.bloom_back
+ (nil,nil,nil)
+
+
+
+ (** infers some stuff that will be required when we will build
+ environments (our environments need a default case, so we need
+ an Op_AC, an Op_A, and a symbol) *)
+
+ (* Note : this function can fail if the user is using the wrong
+ relation, like proving a = b, while the classes are defined with
+ another relation (==)
+ *)
+ let build_reif_params goal eqt =
+ let rlt = fst eqt in
+ let plus,goal = Coq.evar_binary goal rlt in
+ let dot ,goal = Coq.evar_binary goal rlt in
+ let one ,goal = Coq.evar_unit goal rlt in
+ let zero,goal = Coq.evar_unit goal rlt in
+
+ let (x,r) = rlt in
+ let ty_ac = ( mkApp (Lazy.force op_ac, [| x;r;plus;zero|])) in
+ let ty_a = ( mkApp (Lazy.force op_a, [| x;r;dot;one|])) in
+ let a ,goal=
+ try Coq.resolve_one_typeclass goal ty_a
+ with Not_found -> user_error ("Unable to infer a default A operator.")
+ in
+ let ac ,goal=
+ try Coq.resolve_one_typeclass goal ty_ac
+ with Not_found -> user_error ("Unable to infer a default AC operator.")
+ in
+ let plus = Coq.nf_evar goal plus in
+ let dot = Coq.nf_evar goal dot in
+ let one = Coq.nf_evar goal one in
+ let zero = Coq.nf_evar goal zero in
+
+ let record =
+ {a_null = Prd.mk_pack rlt {Prd.dot=dot;Prd.one=one;Prd.opa=a};
+ ac_null= Sum.mk_pack rlt {Sum.plus=plus;Sum.zero=zero;Sum.opac=ac};
+ sym_null = Sym.null eqt zero;
+ a_ty = (mkApp (Lazy.force Prd.typ, [| x;r; |]));
+ ac_ty = ( mkApp (Lazy.force Sum.typ, [| x;r|]));
+ sym_ty = mkApp (Lazy.force Sym.typ, [|x;r|])
+ }
+ in
+ goal, record
+
+ (** [build_sigma_maps] given a envs and some reif_params, we are
+ able to build the sigmas *)
+ let build_sigma_maps goal eqt envs : sigmas * sigma_maps * Proof_type.goal Evd.sigma =
+ let rlt = fst eqt in
+ let goal,rp = build_reif_params goal eqt in
+ let ((_,sym), (_,sum),(_,prd)) = envs_to_list rlt envs in
+ let f = List.map (fun (x,(y,z)) -> (x,Coq.Pos.of_int y)) in
+ let g = List.map (fun (x,(y,z)) -> (y,z)) in
+ let sigmas =
+ {env_sym = Sigma.of_list rp.sym_ty rp.sym_null (g sym);
+ env_sum = Sigma.of_list rp.ac_ty rp.ac_null (g sum);
+ env_prd = Sigma.of_list rp.a_ty rp.a_null (g prd);
+ } in
+ let sigma_maps = {
+ sym_to_pos = (let sym = f sym in fun x -> (List.assoc x sym));
+ sum_to_pos = (let sum = f sum in fun x -> (List.assoc x sum));
+ prd_to_pos = (let prd = f prd in fun x -> (List.assoc x prd));
+ }
+ in
+ sigmas, sigma_maps , goal
+
+
+
+ (** builders for the reification *)
+ type reif_builders =
+ {
+ rsum: constr -> constr -> constr -> constr;
+ rprd: constr -> constr -> constr -> constr;
+ rzero: constr -> constr;
+ rone: constr -> constr;
+ rsym: constr -> constr array -> constr
+ }
+
+ (* donne moi une tactique, je rajoute ma part. Potentiellement, il
+ est possible d'utiliser la notation 'do' a la Haskell:
+ http://www.cas.mcmaster.ca/~carette/pa_monad/ *)
+ let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic =
+ fun (x,t) f ->
+ let b,t' = f x in
+ b, Tacticals.tclTHEN t t'
+
+ let return x = x, Tacticals.tclIDTAC
+
+ let mk_vect vnil vcons v =
+ let ar = Array.length v in
+ let rec aux = function
+ | 0 -> vnil
+ | n -> let n = n-1 in
+ mkApp( vcons,
+ [|
+ (Coq.Nat.of_int n);
+ v.(ar - 1 - n);
+ (aux (n))
+ |]
+ )
+ in aux ar
+
+ (* TODO: use a do notation *)
+ let mk_reif_builders (rlt: Coq.reltype) (env_sym:constr) :reif_builders*Proof_type.tactic =
+ let x,r = rlt in
+ let tty = mkApp (Lazy.force _Tty, [| x ; r ; env_sym|]) in
+ (Coq.mk_letin' "mk_rsum" (mkApp (Lazy.force rsum, [| x; r; env_sym|]))) >>
+ (fun rsum -> (Coq.mk_letin' "mk_rprd" (mkApp (Lazy.force rprd, [| x; r; env_sym|])))
+ >> fun rprd -> ( Coq.mk_letin' "mk_rsym" (mkApp (Lazy.force rsym, [| x;r; env_sym|])))
+ >> fun rsym -> (Coq.mk_letin' "mk_vnil" (mkApp (Lazy.force vnil, [| x;r; env_sym|])))
+ >> fun vnil -> Coq.mk_letin' "mk_vcons" (mkApp (Lazy.force vcons, [| x;r; env_sym|]))
+ >> fun vcons ->
+ return {
+ rsum =
+ begin fun idx l r ->
+ mkApp (rsum, [| idx ; Coq.mk_mset tty [l,1 ; r,1]|])
+ end;
+ rzero =
+ begin fun idx ->
+ mkApp (rsum, [| idx ; Coq.mk_mset tty []|])
+ end;
+ rprd =
+ begin fun idx l r ->
+ let lst = Coq.List.of_list tty [l;r] in
+ mkApp (rprd, [| idx; lst|])
+ end;
+ rone =
+ begin fun idx ->
+ let lst = Coq.List.of_list tty [] in
+ mkApp (rprd, [| idx; lst|]) end;
+ rsym =
+ begin fun idx v ->
+ let vect = mk_vect vnil vcons v in
+ mkApp (rsym, [| idx; vect|])
+ end;
+ }
+ )
+
+
+
+ type reifier = sigma_maps * reif_builders
+
+ let mk_reifier eqt envs goal : sigmas * reifier * Proof_type.tactic =
+ let s, sm, goal = build_sigma_maps goal eqt envs in
+ let env_sym, env_sym_letin = Coq.mk_letin "env_sym_name" (s.env_sym) in
+ let env_prd, env_prd_letin = Coq.mk_letin "env_prd_name" (s.env_prd) in
+ let env_sum, env_sum_letin = Coq.mk_letin "env_sum_name" (s.env_sum) in
+ let s = {env_sym = env_sym; env_prd = env_prd; env_sum = env_sum} in
+ let rb , tac = mk_reif_builders (fst eqt) (s.env_sym) in
+ let evar_map = Tacmach.project goal in
+ let tac = Tacticals.tclTHENLIST (
+ [ Refiner.tclEVARS evar_map;
+ env_prd_letin ;
+ env_sum_letin ;
+ env_sym_letin ;
+ tac
+ ]) in
+ s, (sm, rb), tac
+
+
+ (** [reif_constr_of_t reifier t] rebuilds the term [t] in the
+ reified form. We use the [reifier] to minimise the size of the
+ terms (we make as much lets as possible)*)
+ let reif_constr_of_t (sm,rb) (t:Matcher.Terms.t) : constr =
+ let rec aux = function
+ | Matcher.Terms.Plus (s,l,r) ->
+ let idx = sm.sum_to_pos s in
+ rb.rsum idx (aux l) (aux r)
+ | Matcher.Terms.Dot (s,l,r) ->
+ let idx = sm.prd_to_pos s in
+ rb.rprd idx (aux l) (aux r)
+ | Matcher.Terms.Sym (s,t) ->
+ let idx = sm.sym_to_pos s in
+ rb.rsym idx (Array.map aux t)
+ | Matcher.Terms.One s ->
+ let idx = sm.prd_to_pos s in
+ rb.rone idx
+ | Matcher.Terms.Zero s ->
+ let idx = sm.sum_to_pos s in
+ rb.rzero idx
+ | Matcher.Terms.Var i ->
+ anomaly "call to reif_constr_of_t on a term with variables."
+ in aux t
+
+
+end
+
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 15:52:43 +0000