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

11 files changed, 166 insertions, 39 deletions

diff --git a/src/Trace.v b/src/Trace.v
index 9566c47..0446dae 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -15,6 +15,7 @@
 
 
 Require Import Bool Int63 PArray.
+Require Structures.
 Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators Assumptions.
 
 Local Open Scope array_scope.
@@ -35,8 +36,7 @@ Section trace.
 
   Variable rho : Valuation.t.
 
-  (* We use [array array step] to allow bigger trace *)
-  Definition _trace_ := array (array step).
+  Definition _trace_ := Structures.trace step.
 
   (* A checker for such a trace *)
 
@@ -44,7 +44,8 @@ Section trace.
   Hypothesis is_false_correct : forall c, is_false c -> ~ C.interp rho c.
 
   Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool :=
-    let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in
+    let s' := Structures.trace_fold check_step s t in
+    (* let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in *)
     is_false (S.get s' confl).
   (* Register _checker_ as PrimInline. *)
 
@@ -82,9 +83,10 @@ Section trace.
     intros s t' cid Hf Hv.
     apply (is_false_correct Hf).
     apply S.valid_get.
-    apply PArray.fold_left_ind; auto.
-    intros a i _ Ha;apply PArray.fold_left_ind;trivial.
-    intros a0 i0 _ H1;auto.
+    apply Structures.trace_fold_ind; auto.
+    (* apply PArray.fold_left_ind; auto. *)
+    (* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *)
+    (* intros a0 i0 _ H1;auto. *)
   Qed.
  
 End trace.
diff --git a/src/configure.sh b/src/configure.sh
index dfa86ab..d83e20a 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -5,6 +5,7 @@ set -e
 if [ $@ -a $@ = -native ]; then
     cp versions/native/Makefile Makefile
     cp versions/native/smtcoq_plugin_native.ml4 smtcoq_plugin.ml4
+    cp versions/native/Structures_native.v versions/native/Structures.v
 else
     cp versions/standard/Makefile Makefile
     cp versions/standard/smtcoq_plugin_standard.ml4 smtcoq_plugin.ml4
@@ -17,4 +18,5 @@ else
     cp versions/standard/Int63/Int63Axioms_standard.v versions/standard/Int63/Int63Axioms.v
     cp versions/standard/Int63/Int63Properties_standard.v versions/standard/Int63/Int63Properties.v
     cp versions/standard/Array/PArray_standard.v versions/standard/Array/PArray.v
+    cp versions/standard/Structures_standard.v versions/standard/Structures.v
 fi
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b3248ef..74d3170 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -352,31 +352,31 @@ let to_coq to_lit interp (cstep,
   let nc = ref 0 in
   while not (isRoot !r.kind) do r := prev !r; incr nc done;
   let last_root = !r in
-  let size = !nc in
-  let max = Structures.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 (Structures.mkArray (step, [|def_step|])) in
-  for j = 0 to q - 1 do
-    let tracej = Array.make Structures.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) <- Structures.mkArray (step, tracej)
-  done;
-  if r1 <> 0 then begin
-    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) <- Structures.mkArray (step, traceq)
-  end;
 
-  (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts)
+  (* let size = !nc in *)
+  (* let max = Structures.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 (Structures.mkArray (step, [|def_step|])) in *)
+  (* for j = 0 to q - 1 do *)
+  (*   let tracej = Array.make Structures.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) <- Structures.mkArray (step, tracej) *)
+  (* done; *)
+  (* if r1 <> 0 then begin *)
+  (*   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) <- Structures.mkArray (step, traceq) *)
+  (* end; *)
+  (* (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) *)
+  (Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r, last_root, !cuts)
 
 
 
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
 
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index c833f4d..46faa49 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -58,6 +58,7 @@ versions/standard/Int63/Int63Axioms.v
 versions/standard/Int63/Int63Properties.v
 versions/standard/Array/PArray.v
 
+versions/standard/Structures.v
 versions/standard/structures.ml
 
 trace/coqTerms.ml
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index da82e43..21c0d54 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.5pl1     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.5pl2     ##
 #############################################################################
 
 # WARNING
@@ -71,6 +71,8 @@ COQLIBS?=\
   -I "versions/standard"\
   -I "versions/standard/Int63"\
   -I "versions/standard/Array"
+COQCHKLIBS?=\
+  -R "." SMTCoq
 COQDOCLIBS?=\
   -R "." SMTCoq
 
@@ -175,6 +177,7 @@ VFILES:=versions/standard/Int63/Int63.v\
   versions/standard/Int63/Int63Axioms.v\
   versions/standard/Int63/Int63Properties.v\
   versions/standard/Array/PArray.v\
+  versions/standard/Structures.v\
   cnf/Cnf.v\
   euf/Euf.v\
   lia/Lia.v\
@@ -326,7 +329,7 @@ all-gal.pdf: $(VFILES)
 	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
 
 validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
+	$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
 
 beautify: $(VFILES:=.beautified)
 	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
@@ -529,13 +532,13 @@ $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
 	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<
 
 $(VOFILES): %.vo: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(GLOBFILES): %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
-	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*
+	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
 
 $(GFILES): %.g: %.v
 	$(GALLINA) $<
@@ -556,7 +559,7 @@ $(addsuffix .d,$(VFILES)): %.v.d: %.v
 	$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 $(addsuffix .beautified,$(VFILES)): %.v.beautified:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
 
 # WARNING
 #
diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v
new file mode 100644
index 0000000..04b396f
--- /dev/null
+++ b/src/versions/standard/Structures_standard.v
@@ -0,0 +1,35 @@
+Require Import Int63.
+
+Require Import List.
+
+
+Section Trace.
+
+  Definition trace (step:Type) := ((list step) * step)%type.
+
+  Definition trace_length {step:Type} (t:trace step) : int :=
+    let (t,_) := t in
+    List.fold_left (fun i _ => (i+1)%int) t 0%int.
+
+  Fixpoint trace_get_aux {step:Type} (t:list step) (def:step) (i:int) : step :=
+    match t with
+    | nil => def
+    | s::ss =>
+      if (i == 0)%int then
+        s
+      else
+        trace_get_aux ss def (i-1)
+    end.
+  Definition trace_get {step:Type} (t:trace step) : int -> step :=
+    let (t,def) := t in trace_get_aux t def.
+
+  Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
+    let (t,_) := t in
+    List.fold_left transition t s0.
+
+  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)%int = true -> P s0 -> P (transition s0 (trace_get t i))) :
+      forall s0 : state, P s0 -> P (trace_fold transition s0 t).
+  Admitted.
+
+End Trace.
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 6921593..bf53f41 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -43,6 +43,7 @@ let mkInt : int -> Term.constr = fun i ->
 
 let cint = gen_constant int31_module "int31"
 
+
 (* PArray *)
 let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
 
@@ -63,6 +64,20 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
                        ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a)
 
 
+(* Traces *)
+(* WARNING: side effect on r! *)
+let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
+  let rec mkTrace s =
+    if s = size then
+      mklApp cnil [|step|]
+    else (
+      r := next !r;
+      let st = step_to_coq !r in
+      mklApp ccons [|step; st; mkTrace (s+1)|]
+    ) in
+  mklApp cpair [|mklApp clist [|step|]; step; mkTrace 0; def_step|]
+
+
 (* Differences between the two versions of Coq *)
 type names_id_t = Names.Id.t