From f8ae73357fd7650bc2409b9eddb5816d4025747e Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 5 Mar 2019 12:27:33 +0100
Subject: compilation of ImpIOOracles

---
 Makefile.extr                                     |  2 +-
 mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml  | 11 ++++++++---
 mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli |  1 -
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/Makefile.extr b/Makefile.extr
index 3d54f61f..d6a94d2e 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -43,7 +43,7 @@ cparser/pre_parser_messages.ml:
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight debug mppa_k1c/unittest
+  exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml
index e5ec8e87..0e5cf434 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml
@@ -6,8 +6,10 @@ These oracles assumes the following extraction directives:
 *)
 
 open ImpPrelude
+(*
 open BinNums
 open Datatypes
+*)
 
 (* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *)
 exception Overflow
@@ -52,12 +54,13 @@ let memo_int2pos: int -> int -> BinNums.positive
           pi
      in find;;
            
-  
+(* 
 let string_coq2caml: char list -> string
   = fun l ->
     let buf = Buffer.create (List.length l) in
     List.iter (fun c -> Buffer.add_char buf c) l;
     Buffer.contents buf;;
+*)
 
 let new_exit_observer: (unit -> unit) -> (unit -> unit) ref
   = fun f ->
@@ -120,16 +123,18 @@ let zTr: BinNums.coq_Z -> int
 let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH)))
 
 let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring
-= let (q,r) = BinIntDef.Z.pos_div_eucl p ten in       
+= let (q,r) = BinInt.Z.pos_div_eucl p ten in       
   let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in    
   match q with
   | BinNums.Z0 -> acc0
   | BinNums.Zpos p0 -> string_of_pos p0 acc0
   | _ -> assert false
 
+(*
 let string_of_Z_debug: BinNums.coq_Z -> pstring
 = fun p -> CamlStr (string_of_int (zTr p))
-
+*)
+     
 let string_of_Z: BinNums.coq_Z -> pstring
 = function
   | BinNums.Z0 -> CamlStr "0"
diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli
index 29db881b..6064286a 100644
--- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli
+++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli
@@ -1,5 +1,4 @@
 open ImpPrelude
-open Datatypes
 
 
 (* 
-- 
cgit