diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
commit | cfb4587e26623318f432c7e3e21711afc2b966e7 (patch) | |
tree | a90c6f372633458aa0766510bcfdc4682eaa8f6a /src/trace/smtMisc.ml | |
parent | 1e10dcc783b82269cc3fe3bb7419b9c1cc9e0fa7 (diff) | |
download | smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.tar.gz smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.zip |
Initial import of SMTCoq v1.2
Diffstat (limited to 'src/trace/smtMisc.ml')
-rw-r--r-- | src/trace/smtMisc.ml | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml new file mode 100644 index 0000000..02e5f26 --- /dev/null +++ b/src/trace/smtMisc.ml @@ -0,0 +1,47 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +(** Sharing of coq Int *) +let cInt_tbl = Hashtbl.create 17 + +let mkInt i = + try Hashtbl.find cInt_tbl i + with Not_found -> + let ci = Term.mkInt (Uint63.of_int i) in + Hashtbl.add cInt_tbl i ci; + ci + +(** Generic representation of shared object *) +type 'a gen_hashed = { index : int; hval : 'a } + +(** Functions over constr *) + +let mklApp f args = Term.mkApp (Lazy.force f, args) + +(* TODO : Set -> Type *) +let coqtype = lazy Term.mkSet + +let declare_new_type t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Pp.dummy_loc,t); + Term.mkVar t + +let declare_new_variable v constr_t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Pp.dummy_loc,v); + Term.mkVar v + +let mkName s = + let id = Names.id_of_string s in + Names.Name id |