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/versions/native/structures.ml | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'src/versions/native/structures.ml') 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 -- cgit