More modularity on the format of traces depending on the version of coq

4 files changed, 72 insertions, 3 deletions

diff --git a/src/versions/native/Make b/src/versions/native/Make
index 2b81917..07ff232 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -42,10 +42,11 @@
 
 CMXA = smtcoq.cmxa
 CMXS = smtcoq_plugin.cmxs
-VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
+VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
+versions/native/Structures.v
 versions/native/structures.ml
 
 trace/coqTerms.ml
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 958b64f..bbeb95a 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -65,7 +65,7 @@ COQDOCLIBS?=-R . SMTCoq
 
 CAMLYACC=$(CAMLBIN)ocamlyacc
 CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
+VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
 CMXS=smtcoq_plugin.cmxs
 CMXA=smtcoq.cmxa
 
@@ -145,7 +145,8 @@ VFILES:=Trace.v\
   spl/Assumptions.v\
   lia/Lia.v\
   euf/Euf.v\
-  cnf/Cnf.v
+  cnf/Cnf.v\
+  versions/native/Structures.v
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
diff --git a/src/versions/native/Structures_native.v b/src/versions/native/Structures_native.v
new file mode 100644
index 0000000..950d7bd
--- /dev/null
+++ b/src/versions/native/Structures_native.v
@@ -0,0 +1,39 @@
+Require Import PArray.
+
+
+Section Trace.
+
+  (* We use [array array step] to allow bigger trace *)
+  Definition trace (step:Type) := array (array step).
+
+  Definition trace_length {step:Type} (t:trace step) : int :=
+    PArray.fold_left (fun l a => (l + (length a))%int63) 0%int63 t.
+
+  Definition trace_get {step:Type} (t:trace step) (i:int) : step :=
+    snd (PArray.fold_left (fun (jres:(option int) * step) a =>
+                        let (j,res) := jres in
+                        match j with
+                        | Some j' =>
+                          let l := length a in
+                          if (j' < l)%int63 then
+                            (None, get a j')
+                          else
+                            ((Some ((j' - l)%int63)),res)
+                        | None => (None,res)
+                        end
+                     ) (Some i, (get (get t 0) 0)) t).
+
+  Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
+    PArray.fold_left (PArray.fold_left transition) s0 t.
+
+  Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step)
+      (IH: forall (s0 : state) (i : int), (i < trace_length t)%int63 = true -> P s0 -> P (transition s0 (trace_get t i))) :
+      forall s0 : state, P s0 -> P (trace_fold transition s0 t).
+  Proof.
+    apply PArray.fold_left_ind.
+    intros a i Hi Ha.
+    apply PArray.fold_left_ind;trivial.
+    intros a0 i0 Hi0 Ha0.       (* IH applied to a0 and (sum of the lengths of the first i arrays + i0) *)
+  Admitted.
+
+End Trace.
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index a35d04b..60ea0e5 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -31,6 +31,7 @@ let mkInt : int -> Term.constr =
 
 let cint = gen_constant int63_modules "int"
 
+
 (* PArray *)
 let parray_modules = [["Coq";"Array";"PArray"]]
 
@@ -40,6 +41,33 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
   Term.mkArray
 
 
+(* Traces *)
+(* WARNING: side effect on r! *)
+let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
+  let max = max_array_size - 1 in
+  let q,r1 = size / max, size mod max in
+  let trace =
+    let len = if r1 = 0 then q + 1 else q + 2 in
+    Array.make len (mkArray (step, [|def_step|])) in
+  for j = 0 to q - 1 do
+    let tracej = Array.make max_array_size def_step in
+    for i = 0 to max - 1 do
+      r := next !r;
+      tracej.(i) <- step_to_coq !r;
+    done;
+    trace.(j) <- mkArray (step, tracej)
+  done;
+  if r1 <> 0 then (
+    let traceq = Array.make (r1 + 1) def_step in
+    for i = 0 to r1-1 do
+    r := next !r;
+    traceq.(i) <- step_to_coq !r;
+    done;
+    trace.(q) <- mkArray (step, traceq)
+  );
+  mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace)
+
+
 (* Differences between the two versions of Coq *)
 type names_id_t = Names.identifier