From 1aa8b6f6a876af22f538c869f022bc4ca5986b40 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 29 Nov 2010 23:30:48 +0100 Subject: Imported Upstream version 0.1-r13244 --- theory.ml | 708 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 708 insertions(+) create mode 100644 theory.ml (limited to 'theory.ml') 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 + + + -- cgit v1.2.3