diff options
Diffstat (limited to 'theory.ml')
| -rw-r--r-- | theory.ml | 708 |
1 files changed, 0 insertions, 708 deletions
diff --git a/theory.ml b/theory.ml deleted file mode 100644 index 45a76f1..0000000 --- a/theory.ml +++ /dev/null @@ -1,708 +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. *) -(***************************************************************************) - -(** 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 - - - |