diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-23 16:01:42 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-23 16:01:42 +0200 |
commit | 4be43131e2b3dc60a530de5b3a8f23cd93564ad7 (patch) | |
tree | 7743e1fbae5ee7b7ae72b16d35ea7fa38a9e46f2 /src/versions/standard | |
parent | fa9d33eea03bb59d55ee4dccf4fecb8b1520e69d (diff) | |
download | smtcoq-4be43131e2b3dc60a530de5b3a8f23cd93564ad7.tar.gz smtcoq-4be43131e2b3dc60a530de5b3a8f23cd93564ad7.zip |
More modularity on the format of traces depending on the version of coq
Diffstat (limited to 'src/versions/standard')
-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 |
4 files changed, 60 insertions, 6 deletions
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 |