diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 17:31:47 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 17:31:47 +0100 |
| commit | 37f297b89f04155124237acf3d7f220a9dcd1544 (patch) | |
| tree | b5d89abd09f0093d070efdf7658b24d932d70986 /src/trace/smtAtom.ml | |
| parent | 607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2 (diff) | |
| download | smtcoq-37f297b89f04155124237acf3d7f220a9dcd1544.tar.gz smtcoq-37f297b89f04155124237acf3d7f220a9dcd1544.zip | |
Code refactoring
Diffstat (limited to 'src/trace/smtAtom.ml')
| -rw-r--r-- | src/trace/smtAtom.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 392ef2e..80c012f 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -746,3 +746,16 @@ module Atom = module Form = SmtForm.Make(Atom) module Trace = SmtTrace.MakeOpt(Form) + + +(* Interpretation tables *) + +let mk_ftype cod dom = + let typeb = Lazy.force ctype in + let typea = mklApp clist [|typeb|] in + let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in + let b = Btype.to_coq dom in + mklApp cpair [|typea;typeb;a;b|] + +let make_t_i rt = Btype.interp_tbl rt +let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro |