diff options
Diffstat (limited to 'kvx/abstractbb/Impure/ocaml')
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml | 66 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli | 5 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml | 142 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli | 33 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml | 78 | ||||
| -rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli | 8 |
6 files changed, 0 insertions, 332 deletions
diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml deleted file mode 100644 index 2b66899b..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml +++ /dev/null @@ -1,66 +0,0 @@ -open ImpPrelude -open HConsingDefs - -let make_dict (type key) (p: key Dict.hash_params) = - let module MyHashedType = struct - type t = key - let equal = p.Dict.test_eq - let hash = p.Dict.hashing - end in - let module MyHashtbl = Hashtbl.Make(MyHashedType) in - let dict = MyHashtbl.create 1000 in - { - Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d); - Dict.get = (fun k -> MyHashtbl.find_opt dict k) - } - - -exception Stop;; - -let xhCons (type a) (hp:a hashP) = - (* We use a hash-table, but a hash-set would be sufficient ! *) - (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *) - (* Ideally, a parameter would allow to select between the weak or full version *) - let module MyHashedType = struct - type t = a hashinfo - let equal x y = hp.hash_eq x.hdata y.hdata - let hash x = Hashtbl.hash x.hcodes - end in - let module MyHashtbl = Hashtbl.Make(MyHashedType) in - let pick t = - let res = ref None in - try - MyHashtbl.iter (fun k d -> res:=Some (k,d); raise Stop) t; - None - with - | Stop -> !res - in - let t = MyHashtbl.create 1000 in - let logs = ref [] in - { - hC = (fun (k:a hashinfo) -> - match MyHashtbl.find_opt t k with - | Some d -> d - | None -> (*print_string "+";*) - let d = hp.set_hid k.hdata (MyHashtbl.length t) in - MyHashtbl.add t {k with hdata = d } d; d); - next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs)); - next_hid = (fun () -> MyHashtbl.length t); - remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x); - export = fun () -> - match pick t with - | None -> { get_info = (fun _ -> raise Not_found); iterall = (fun _ -> ()) } - | Some (k,_) -> - (* the state is fully copied at export ! *) - let logs = ref (List.rev_append (!logs) []) in - let rec step_log i = - match !logs with - | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i) - | _ -> [] - in let a = Array.make (MyHashtbl.length t) k in - MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t; - { - get_info = (fun i -> a.(i)); - iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a) - } - } diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli deleted file mode 100644 index 5075d176..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli +++ /dev/null @@ -1,5 +0,0 @@ -open ImpPrelude -open HConsingDefs - -val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t -val xhCons: 'a hashP -> 'a hashConsing diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml deleted file mode 100644 index 9e63c12d..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml +++ /dev/null @@ -1,142 +0,0 @@ -(* Warning - -These oracles assumes the following extraction directives: - "Require Import ExtrOcamlString." - -*) - -open ImpPrelude -(* -open BinNums -open Datatypes -*) - -(* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *) -exception Overflow - -let aux_add: ('a, 'b) Hashtbl.t -> 'b Queue.t -> 'a -> 'b -> unit - = fun t q i p -> - if i < 1 then (* protection against wrap around *) - raise Overflow; - Queue.add p q; - Hashtbl.add t i p - -let memo_int2pos: int -> int -> BinNums.positive - = fun n -> - (* init of the Hashtbl *) - let n = max n 1 in - let t = Hashtbl.create n in - let q = Queue.create () in - aux_add t q 1 BinNums.Coq_xH ; - for i = 1 to (n-1)/2 do - let last = Queue.take q in - let ni = 2*i in - aux_add t q ni (BinNums.Coq_xO last); - aux_add t q (ni+1) (BinNums.Coq_xI last) - done; - if n mod 2 = 0 then ( - let last = Queue.take q in - Hashtbl.add t n (BinNums.Coq_xO last) - ); - (* memoized translation of i *) - let rec find i = - try - (* Printf.printf "-> %d\n" i; *) - Hashtbl.find t i - with Not_found -> - (* Printf.printf "<- %d\n" i; *) - if i <= 0 then - invalid_arg "non-positive integer" - else - let p = find (i/2) in - let pi = if i mod 2 = 0 then BinNums.Coq_xO p else BinNums.Coq_xI p in - Hashtbl.add t i pi; - pi - in find;; - -let new_exit_observer: (unit -> unit) -> (unit -> unit) ref - = fun f -> - let o = ref f in - at_exit (fun () -> !o()); - o;; - -let set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit - = fun (r, f) -> r := f - -let rec print: pstring -> unit - = fun ps -> - match ps with - | Str l -> List.iter print_char l - | CamlStr s -> print_string s - | Concat(ps1,ps2) -> (print ps1; print ps2);; - -let println: pstring -> unit - = fun l -> print l; print_newline() - -let read_line () = - CamlStr (Stdlib.read_line());; - -exception ImpureFail of pstring;; - -let exn2string: exn -> pstring - = fun e -> CamlStr (Printexc.to_string e) - -let fail: pstring -> 'a - = fun s -> raise (ImpureFail s);; - -let try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a - = fun (k1, k2) -> - try - k1() - with - | (ImpureFail s) as e -> k2 s e - -let try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a - = fun (k1, k2) -> - try - k1() - with - | e -> k2 e - -(** MISC **) - -let rec posTr: BinNums.positive -> int -= function - | BinNums.Coq_xH -> 1 - | BinNums.Coq_xO p -> (posTr p)*2 - | BinNums.Coq_xI p -> (posTr p)*2+1;; - -let zTr: BinNums.coq_Z -> int -= function - | BinNums.Z0 -> 0 - | BinNums.Zpos p -> posTr p - | BinNums.Zneg p -> - (posTr p) - -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) = 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" - | BinNums.Zpos p -> string_of_pos p (CamlStr "") - | BinNums.Zneg p -> Concat (CamlStr "-", string_of_pos p (CamlStr "")) - -let timer ((f:'a -> 'b), (x:'a)) : 'b = - Gc.compact(); - let itime = (Unix.times()).Unix.tms_utime in - let r = f x in - let rt = (Unix.times()).Unix.tms_utime -. itime in - Printf.printf "time = %f\n" rt; - r diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli deleted file mode 100644 index 6064286a..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli +++ /dev/null @@ -1,33 +0,0 @@ -open ImpPrelude - - -(* -Memoized version of translation from int -> BinNums.positive. -The first arg is an indicative bound on the max int translated: -it pre-computes all positives lower or equal to this bound. -*) -val memo_int2pos: int -> int -> BinNums.positive - -val read_line: unit -> pstring - -val print: pstring -> unit - -val println: pstring -> unit - -val string_of_Z: BinNums.coq_Z -> pstring - -val timer : (('a -> 'b ) * 'a) -> 'b - -val new_exit_observer: (unit -> unit) -> (unit -> unit) ref - -val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit - -val exn2string: exn -> pstring - -val fail: pstring -> 'a - -exception ImpureFail of pstring;; - -val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a - -val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml deleted file mode 100644 index cb7625e5..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml +++ /dev/null @@ -1,78 +0,0 @@ -open ImpPrelude -open Datatypes - -(** GENERIC ITERATIVE LOOP **) - -(* a simple version of loop *) -let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - = fun (a0, f) -> - let rec iter: 'a -> 'b - = fun a -> - match f a with - | Coq_inl a' -> iter a' - | Coq_inr b -> b - in - iter a0;; - -(* loop from while *) -let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - = fun (a0, f) -> - let s = ref (f a0) in - while (match !s with Coq_inl _ -> true | _ -> false) do - match !s with - | Coq_inl a -> s:=f a - | _ -> assert false - done; - match !s with - | Coq_inr b -> b - | _ -> assert false;; - -let loop = simple_loop - - -(** GENERIC FIXPOINTS **) - -let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let rec f x = recf f x in - f - -let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let memo = Hashtbl.create 10 in - let rec f x = - try - Hashtbl.find memo x - with - Not_found -> - let r = recf f x in - Hashtbl.replace memo x r; - r - in f - -let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let fix = ref (fun x -> failwith "init") in - fix := (fun x -> recf !fix x); - !fix;; - -let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = - let memo = ref None in - let rec f x = - match !memo with - | Some y -> y - | None -> - let r = recf f x in - memo := Some r; - r - in f - -let xrec_mode = ref MemoRec - -let xrec_set_option : recMode -> unit -= fun m -> xrec_mode := m - -let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) - = fun recf -> - match !xrec_mode with - | StdRec -> std_rec recf - | MemoRec -> memo_rec recf - | BareRec -> bare_rec recf - | BuggyRec -> buggy_rec recf diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli deleted file mode 100644 index 194696a1..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli +++ /dev/null @@ -1,8 +0,0 @@ -open ImpPrelude -open Datatypes - -val loop: ('a * ('a -> ('a, 'b) sum)) -> 'b - -val xrec_set_option: recMode -> unit - -val xrec: (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) |