diff options
Diffstat (limited to 'src/versions')
-rw-r--r-- | src/versions/native/Make | 3 | ||||
-rw-r--r-- | src/versions/native/Makefile | 5 | ||||
-rw-r--r-- | src/versions/native/Structures_native.v | 39 | ||||
-rw-r--r-- | src/versions/native/structures.ml | 28 | ||||
-rw-r--r-- | src/versions/standard/Make | 1 | ||||
-rw-r--r-- | src/versions/standard/Makefile | 15 | ||||
-rw-r--r-- | src/versions/standard/Structures_standard.v | 35 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 15 |
8 files changed, 132 insertions, 9 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 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 |