Commit 4303825c authored by Mário Pereira's avatar Mário Pereira
Browse files

ocaml_printer : compatible code with OCaml versions previous to 4.04

parent 0060ceb9
......@@ -55,7 +55,7 @@ module Print = struct
let print_qident ~sanitizer info fmt id =
try
let lp, m, q =
let _, _, q =
try Pmodule.restore_path id
with Not_found -> Theory.restore_path id in
let s = String.concat "__" q in
......@@ -67,7 +67,7 @@ module Print = struct
false info.info_current_mo
then fprintf fmt "%s" s
else
let fname = if lp = [] then info.info_fname else None in
(* let fname = if lp = [] then info.info_fname else None in *)
let m = Strings.capitalize "m" in
fprintf fmt "%s.%s" m s
with Not_found ->
......@@ -311,16 +311,22 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
print_list nothing (Print.print_decl info) fmt mdecls;
fprintf fmt "@."
(*
let fg ?fname m =
let mod_name = m.Pmodule.mod_theory.Theory.th_name.id_string in
match fname with
| None -> mod_name ^ ".ml"
| Some f -> (Filename.remove_extension f) ^ "__" ^ mod_name ^ ".ml"
| Some f ->
(* TODO: replace with Filename.remove_extension
* after migration to OCaml 4.04+ *)
let remove_extension s =
try Filename.chop_extension s
with Invalid_argument _ -> s
in
(remove_extension f) ^ "__" ^ mod_name ^ ".ml"
let () = Pdriver.register_printer "ocaml"
~desc:"printer for OCaml code" fg extract_module
*)
(*
* Local Variables:
......
module M
use import int.Int
(* use import seq.Seq *)
use import seq.Seq
(* let function f (y: int) (x: int) : int *)
(* requires { x >= 0 } *)
(* ensures { result >= 0 } *)
(* = x *)
let function f (y: int) (x: int) : int
requires { x >= 0 }
ensures { result >= 0 }
= x
(* let g (ghost z: int) (x: int) : int *)
(* requires { x > 0 } *)
(* ensures { result > 0 } *)
(* = let y = x in *)
(* y *)
let g (ghost z: int) (x: int) : int
requires { x > 0 }
ensures { result > 0 }
= let y = x in
y
(* type t 'a 'b 'c 'd *)
type t 'a 'b 'c 'd
(* type list 'a = Nil | Cons 'a (list 'a) *)
type list 'a = Nil | Cons 'a (list 'a)
(* type btree 'a = E | N (btree 'a) 'a (btree 'a) *)
type btree 'a = E | N (btree 'a) 'a (btree 'a)
(* type ntree 'a = Empty | Node 'a (list 'a) *)
type ntree 'a = Empty | Node 'a (list 'a)
(* type list_int = list int *)
type list_int = list int
(* type cursor 'a = { *)
(* collection : list 'a; *)
(* index : int; *)
(* mutable index2 : int; *)
(* ghost mutable v : seq 'a; *)
(* } *)
type cursor 'a = {
collection : list 'a;
index : int;
mutable index2 : int;
ghost mutable v : seq 'a;
}
(* use import ref.Ref *)
use import ref.Ref
(* let update (c: cursor int) : int *)
(* = c.index *)
let update (c: cursor int) : int
= c.index
(* exception Empty (list int, int) *)
(* exception Out_of_bounds int *)
exception Empty (list int, int)
exception Out_of_bounds int
(* let rec length (l: list 'a) : int *)
(* variant { l } *)
(* = match l with *)
(* | Nil -> 0 *)
(* | Cons _ r -> 1 + length r *)
(* end *)
let rec length (l: list 'a) : int
variant { l }
= match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
(* let t (x:int) : int *)
(* requires { false } *)
(* = absurd *)
let t (x:int) : int
requires { false }
= absurd
(* let a () : unit *)
(* = assert { true } *)
let a () : unit
= assert { true }
(* let singleton (x: int) (l: list int) : list int = *)
(* let x = Nil in x *)
let singleton (x: int) (l: list int) : list int =
let x = Nil in x
(* use import int.Int *)
use import int.Int
(* let test (x: int) : int = *)
(* let y = *)
(* let z = x in *)
(* (ghost z) + 1 *)
(* in 42 *)
let test (x: int) : int =
let y =
let z = x in
(ghost z) + 1
in 42
type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)
......@@ -72,13 +72,6 @@ module M
| Cons2 _ _ n -> Cons2 x l (n+1)
end
type t = { c: int; ghost c2: (int, bool, int) }
let ghost f (x: t) : int =
match x.c2 with
| (n, b, m) -> m
end
let ggg () : int = 42
let call (x:int) : int =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment