From 4be43131e2b3dc60a530de5b3a8f23cd93564ad7 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 23 Sep 2016 16:01:42 +0200 Subject: More modularity on the format of traces depending on the version of coq --- src/Trace.v | 14 +++++---- src/configure.sh | 2 ++ src/trace/smtTrace.ml | 48 ++++++++++++++--------------- src/versions/native/Make | 3 +- src/versions/native/Makefile | 5 +-- src/versions/native/Structures_native.v | 39 +++++++++++++++++++++++ src/versions/native/structures.ml | 28 +++++++++++++++++ src/versions/standard/Make | 1 + src/versions/standard/Makefile | 15 +++++---- src/versions/standard/Structures_standard.v | 35 +++++++++++++++++++++ src/versions/standard/structures.ml | 15 +++++++++ 11 files changed, 166 insertions(+), 39 deletions(-) create mode 100644 src/versions/native/Structures_native.v create mode 100644 src/versions/standard/Structures_standard.v 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 ## ## "$@" || ( 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 -- cgit