diff options
Diffstat (limited to 'src/trace/smtAtom.ml')
| -rw-r--r-- | src/trace/smtAtom.ml | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 06e1472..9697882 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -85,7 +85,7 @@ type nop = type op_def = { tparams : SmtBtype.btype array; tres : SmtBtype.btype; - op_val : Structures.constr } + op_val : CoqInterface.constr } type index = Index of int | Rel_name of string @@ -97,14 +97,14 @@ let destruct s (i, hval) = match i with | Rel_name _ -> failwith s let dummy_indexed_op i dom codom = - (i, {tparams = dom; tres = codom; op_val = Structures.mkProp}) + (i, {tparams = dom; tres = codom; op_val = CoqInterface.mkProp}) let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in index let debruijn_indexed_op i ty = - (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i}) + (Index i, {tparams = [||]; tres = ty; op_val = CoqInterface.mkRel i}) module Op = struct @@ -357,7 +357,7 @@ module Op = (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Structures.constr, indexed_op) Hashtbl.t + tbl : (CoqInterface.constr, indexed_op) Hashtbl.t } let create () = @@ -385,7 +385,7 @@ module Op = let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in Hashtbl.iter set reify.tbl; - Structures.mkArray (tval, t) + CoqInterface.mkArray (tval, t) let to_list reify = let set _ op acc = @@ -713,7 +713,7 @@ module Atom = to_smt_atom (atom h) and to_smt_atom = function - | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv + | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv | Acop _ as a -> to_smt_int fmt (compute_int a) | Auop (op,h) -> to_smt_uop op h | Abop (op,h1,h2) -> to_smt_bop op h1 h2 @@ -740,7 +740,7 @@ module Atom = Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta; Format.fprintf fmt ") ( "; SmtBtype.to_smt fmt bt; - Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t)) + Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (CoqInterface.pr_constr t)) and to_smt_uop op h = match op with @@ -1107,8 +1107,8 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom (h : Structures.constr) = - let c, args = Structures.decompose_app h in + let rec mk_hatom (h : CoqInterface.constr) = + let c, args = CoqInterface.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args | CCZ0 -> mk_cop CCZ0 args @@ -1150,9 +1150,9 @@ module Atom = | CCselect -> mk_bop_select args | CCdiff -> mk_bop_diff args | CCstore -> mk_top_store args - | CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h) + | CCunknown -> mk_unknown c args (CoqInterface.retyping_get_type_of env sigma h) | CCunknown_deps gobble -> - mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble + mk_unknown_deps c args (CoqInterface.retyping_get_type_of env sigma h) gobble and mk_cop op args = match op, args with @@ -1346,10 +1346,10 @@ module Atom = let (l1, l2) = collect_types xs in match l1 with | [] -> - let ty = Structures.retyping_get_type_of env sigma x in + let ty = CoqInterface.retyping_get_type_of env sigma x in if Constr.iskind ty || - let c, _ = Structures.decompose_app ty in - Structures.eq_constr c (Lazy.force cCompDec) + let c, _ = CoqInterface.decompose_app ty in + CoqInterface.eq_constr c (Lazy.force cCompDec) then ([x], xs) else @@ -1368,10 +1368,10 @@ module Atom = with | Not_found -> let targs = Array.map type_of hargs in let tres = SmtBtype.of_coq rt known_logic ty in - let os = if Structures.isRel c then - let i = Structures.destRel c in - let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in - Some (Structures.string_of_name n) + let os = if CoqInterface.isRel c then + let i = CoqInterface.destRel c in + let n, _ = CoqInterface.destruct_rel_decl (Environ.lookup_rel i env) in + Some (CoqInterface.string_of_name n) else if Vars.closed0 c then None else @@ -1394,7 +1394,7 @@ module Atom = [gobble] *) and mk_unknown_deps c args ty gobble = let deps, args = split_list_at gobble args in - let c = Structures.mkApp (c, Array.of_list deps) in + let c = CoqInterface.mkApp (c, Array.of_list deps) in mk_unknown c args ty in @@ -1435,7 +1435,7 @@ module Atom = let interp_tbl reify = let t = to_array reify (Lazy.force dft_atom) a_to_coq in - Structures.mkArray (Lazy.force catom, t) + CoqInterface.mkArray (Lazy.force catom, t) (** Producing a Coq term corresponding to the interpretation of an atom *) @@ -1447,12 +1447,12 @@ module Atom = let pc = match atom a with | Acop c -> Op.interp_cop c - | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Auop (op,h) -> CoqInterface.mkApp (Op.interp_uop op, [|interp_atom h|]) | Abop (op,h1,h2) -> - Structures.mkApp (Op.interp_bop t_i op, + CoqInterface.mkApp (Op.interp_bop t_i op, [|interp_atom h1; interp_atom h2|]) | Atop (op,h1,h2,h3) -> - Structures.mkApp (Op.interp_top t_i op, + CoqInterface.mkApp (Op.interp_top t_i op, [|interp_atom h1; interp_atom h2; interp_atom h3|]) | Anop (NO_distinct ty as op,ha) -> let cop = Op.interp_nop t_i op in @@ -1460,9 +1460,9 @@ module Atom = let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Structures.mkApp (cop,[|cargs|]) + CoqInterface.mkApp (cop,[|cargs|]) | Aapp (op,t) -> - Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in + CoqInterface.mkApp ((snd op).op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a |