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/native/structures.ml | |
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/native/structures.ml')
-rw-r--r-- | src/versions/native/structures.ml | 28 |
1 files changed, 28 insertions, 0 deletions
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 |