From 37f297b89f04155124237acf3d7f220a9dcd1544 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 2 Mar 2016 17:31:47 +0100 Subject: Code refactoring --- src/trace/smtAtom.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/trace/smtAtom.ml') 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 -- cgit