From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 14 Feb 2019 20:09:40 +0100 Subject: V8.7 (#36) Port SMTCoq to Coq-8.7 --- src/trace/smtAtom.ml | 41 +++++++++++++++++++---------------------- 1 file changed, 19 insertions(+), 22 deletions(-) (limited to 'src/trace/smtAtom.ml') diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index fd9f2bd..330884b 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -12,9 +12,6 @@ open SmtMisc open CoqTerms -open Entries -open Declare -open Decl_kinds open SmtBtype @@ -229,8 +226,8 @@ module Op = | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te)) - let interp_ieq t_i t = - mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] + (* let interp_ieq t_i t = + * mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] *) (* let veval_t te = let env = Global.env () in @@ -246,30 +243,30 @@ module Op = let interp_eqarray t_i ti te = mklApp cequalarray - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; - SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i te |] let interp_select t_i ti te = mklApp cselect - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.inh_interp t_i te|] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.inh_interp t_i te|] let interp_diff t_i ti te = mklApp cdiff - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; - SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; + SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |] let interp_store t_i ti te = mklApp cstore - SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; - SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; - SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |] + [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te; + SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti; + SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |] let interp_eq t_i = function @@ -1022,7 +1019,7 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom h = + let rec mk_hatom (h : Term.constr) = let c, args = Term.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args @@ -1064,9 +1061,9 @@ module Atom = | CCselect -> mk_bop_select args | CCdiff -> mk_bop_diff args | CCstore -> mk_top_store args - | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) + | CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h) | CCunknown_deps gobble -> - mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble + mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble and mk_cop op args = match op, args with -- cgit