From 7940ef63c654be26b41ce20162207f3c67d0b10a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sun, 28 Oct 2018 00:30:23 +0200 Subject: New files SmtBtype.ml(i) for module formerly in SmtAtom --- src/trace/smtAtom.mli | 43 +++---------------------------------------- 1 file changed, 3 insertions(+), 40 deletions(-) (limited to 'src/trace/smtAtom.mli') diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index e6a3c47..8e69265 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -13,44 +13,7 @@ (* *) (**************************************************************************) - -type indexed_type - -val dummy_indexed_type: int -> indexed_type -val indexed_type_index : indexed_type -> int - -type btype = - | TZ - | Tbool - | Tpositive - | Tindex of indexed_type - -module Btype : - sig - - val equal : btype -> btype -> bool - - val to_coq : btype -> Term.constr - - val to_smt : Format.formatter -> btype -> unit - - type reify_tbl - - val create : unit -> reify_tbl - - val declare : reify_tbl -> Term.constr -> Term.constr -> btype - - val of_coq : reify_tbl -> Term.constr -> btype - - val interp_tbl : reify_tbl -> Term.constr - - val to_list : reify_tbl -> (int * indexed_type) list - - val interp_to_coq : reify_tbl -> btype -> Term.constr - - val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list - - end +open SmtBtype (** Operators *) @@ -142,7 +105,7 @@ module Atom : val get : reify_tbl -> atom -> hatom (** Given a coq term, build the corresponding atom *) - val of_coq : Btype.reify_tbl -> Op.reify_tbl -> + val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl -> reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -178,5 +141,5 @@ module Trace : sig end -val make_t_i : Btype.reify_tbl -> Term.constr +val make_t_i : SmtBtype.reify_tbl -> Term.constr val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr -- cgit