OCaml realizations (in lib/ocaml/)

parent 427bf011
......@@ -2,7 +2,6 @@
printer "ocaml"
theory BuiltIn
syntax type int "Num.num"
syntax predicate (=) "(%1 = %2)"
end
......@@ -13,7 +12,7 @@ theory option.Option
end
theory Bool
syntax type bool "bool"
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
......@@ -32,38 +31,6 @@ theory list.List
syntax function Cons "(%1 :: %2)"
end
theory int.Int
(* TODO: make a for_num prelude function *)
syntax function zero "(Num.num_of_int 0)"
syntax function one "(Num.num_of_int 1)"
syntax function (+) "(Num.add_num %1 %2)"
syntax function (-) "(Num.sub_num %1 %2)"
syntax function (*) "(Num.mult_num %1 %2)"
syntax function (-_) "(Num.minus_num %1)"
syntax predicate (<=) "(Num.le_num %1 %2)"
syntax predicate (<) "(Num.lt_num %1 %2)"
syntax predicate (>=) "(Num.ge_num %1 %2)"
syntax predicate (>) "(Num.gt_num %1 %2)"
end
theory int.Abs
syntax function abs "(Num.abs_num %1)"
end
theory int.MinMax
syntax function min "(Num.min_num %1 %2)"
syntax function max "(Num.max_num %1 %2)"
end
(* Note: documentation for Num says ``Euclidean division'' but this is
rather a computer division *)
theory int.ComputerDivision
syntax function div "(Num.quo_num %1 %2)"
syntax function mod "(Num.mod_num %1 %2)"
end
(* WhyML *)
......
(* This file has been generated from Why3 module array.Array *)
type 'a pervasives_array = 'a array
type 'a array = 'a pervasives_array
let mixfix_lbrb (a: 'a array) (i: Why3__BuiltIn.int) : 'a =
a.(Num.int_of_num i)
let mixfix_lbrblsmn (a: 'a array) (i: Why3__BuiltIn.int) (v: 'a) : unit =
a.(Num.int_of_num i) <- v
let length (a: 'a array) : Why3__BuiltIn.int =
Num.num_of_int (Array.length a)
exception OutOfBounds
let defensive_get (a: 'a array) (i: Why3__BuiltIn.int) =
begin if let o = (let o1 = (length a) in
(Int__Int.infix_gteq i o1)) in
(Int__Int.infix_ls i (Why3__BuiltIn.int_constant "0") || (o = true))
then raise OutOfBounds
else (());
((mixfix_lbrb a) i) end
let defensive_set (a1: 'a array) (i1: Why3__BuiltIn.int) (v: 'a) =
begin if let o = (let o1 = (length a1) in
(Int__Int.infix_gteq i1 o1)) in
(Int__Int.infix_ls i1 (Why3__BuiltIn.int_constant "0") || (o = true))
then raise OutOfBounds
else (());
(((mixfix_lbrblsmn a1) i1) v) end
let make (n: Why3__BuiltIn.int) (v1: 'a) : 'a array =
Array.make (Num.int_of_num n) v1
let append (a11: 'a array) (a2: 'a array) : 'a array =
Array.append a11 a2
let sub (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
: 'a array =
Array.sub a2 (Num.int_of_num ofs) (Num.int_of_num len)
let copy (a2: 'a array) : 'a array =
Array.copy a2
let fill (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
(v1: 'a) =
let o = (Int__Int.infix_mn len (Why3__BuiltIn.int_constant "1")) in
let o1 = ((Why3__BuiltIn.int_constant "0")) in
(Int__Int.for_loop_to o1 o
(fun k -> let o2 = (Int__Int.infix_pl ofs k) in
(((mixfix_lbrblsmn a2) o2) v1)))
let blit (a11: 'a array) (ofs1: Why3__BuiltIn.int) (a21: 'a array) (ofs2:
Why3__BuiltIn.int) (len1: Why3__BuiltIn.int) : unit =
Array.blit a11 (Num.int_of_num ofs1)
a21 (Num.int_of_num ofs2) (Num.int_of_num len1)
(* This file has been generated from Why3 theory int.Abs *)
let abs = Num.abs_num
(* This file has been generated from Why3 theory int.ComputerDivision *)
(* Note: documentation for Num says ``Euclidean division'' but this is
rather a computer division *)
let div = Num.quo_num
let mod_renamed = Num.mod_num
(* This file has been generated from Why3 theory int.Int *)
let zero : Why3__BuiltIn.int = (Num.num_of_string "0")
let one : Why3__BuiltIn.int = (Num.num_of_string "1")
let infix_ls (x: Why3__BuiltIn.int) (x1: Why3__BuiltIn.int) : bool =
Num.lt_num x x1
let infix_gt (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
infix_ls y x
let infix_lseq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
infix_ls x y || (x = y)
let infix_pl (x: Why3__BuiltIn.int) (x1:
Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.add_num x x1
let prefix_mn (x: Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.minus_num x
let infix_as (x: Why3__BuiltIn.int) (x1:
Why3__BuiltIn.int) : Why3__BuiltIn.int =
Num.mult_num x x1
let infix_mn (x: Why3__BuiltIn.int) (y:
Why3__BuiltIn.int) : Why3__BuiltIn.int = infix_pl x (prefix_mn y)
let infix_gteq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
infix_lseq y x
let rec for_loop_to x1 x2 body =
if Num.le_num x1 x2 then begin
body x1;
for_loop_to (Num.succ_num x1) x2 body
end
let rec for_loop_downto x1 x2 body =
if Num.ge_num x1 x2 then begin
body x1;
for_loop_downto (Num.pred_num x1) x2 body
end
(* This file has been generated from Why3 theory int.Lex2 *)
let lt_nat (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
Int__Int.infix_lseq (Why3__BuiltIn.int_constant "0") y &&
Int__Int.infix_ls x y
let rec lex (x: (Why3__BuiltIn.int * Why3__BuiltIn.int)) (x1:
(Why3__BuiltIn.int * Why3__BuiltIn.int)) : bool =
let (fst1, snd1) = x in
let (fst2, snd2) = x1 in
Int__Int.infix_ls fst1 fst2 || fst1 = fst2 && Int__Int.infix_ls snd1 snd2
(* This file has been generated from Why3 theory int.MinMax *)
let min = Num.min_num
let max = Num.max_num
type int = Num.num
let infix_eq = Pervasives.(=)
let int_constant = Num.num_of_string
......@@ -164,6 +164,7 @@ operator:
| OPERATOR UNDERSCORE { prefix $1 }
| LEFTSQ RIGHTSQ { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
;
list1_string_list:
......
......@@ -52,7 +52,8 @@ let extract_filename ?fname th =
(modulename ?fname th) ^ ".ml"
let modulename path t =
String.capitalize ((String.concat "__" path) ^ "__" ^ t)
String.capitalize
(if path = [] then "why3__" ^ t else String.concat "__" path ^ "__" ^ t)
(** Driver *)
......@@ -62,24 +63,29 @@ let is_stdlib path id = Hashtbl.mem stdlib (path, id)
(** Printers *)
let ocaml_keywords =
["and"; "as"; "assert"; "asr"; "begin";
"class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
"exception"; "external"; "false"; "for"; "fun"; "function";
"functor"; "if"; "in"; "include"; "inherit"; "initializer";
"land"; "lazy"; "let"; "lor"; "lsl"; "lsr"; "lxor"; "match";
"method"; "mod"; "module"; "mutable"; "new"; "object"; "of";
"open"; "or"; "private"; "rec"; "sig"; "struct"; "then"; "to";
"true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
"raise";]
let is_ocaml_keyword =
let h = Hashtbl.create 17 in
List.iter (fun s -> Hashtbl.add h s ()) ocaml_keywords;
Hashtbl.mem h
let iprinter,aprinter,tprinter,pprinter =
let bl = (* OCaml keywords *)
["and"; "as"; "assert"; "asr"; "begin";
"class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
"exception"; "external"; "false"; "for"; "fun"; "function";
"functor"; "if"; "in"; "include"; "inherit"; "initializer";
"land"; "lazy"; "let"; "lor"; "lsl"; "lsr"; "lxor"; "match";
"method"; "mod"; "module"; "mutable"; "new"; "object"; "of";
"open"; "or"; "private"; "rec"; "sig"; "struct"; "then"; "to";
"true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
"raise";]
in
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:isanitize
create_ident_printer ocaml_keywords ~sanitizer:isanitize,
create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
create_ident_printer ocaml_keywords ~sanitizer:isanitize
let forget_tvs () =
forget_all aprinter
......@@ -143,10 +149,10 @@ let print_path = print_list dot pp_print_string
let print_qident ~sanitizer info fmt id =
try
let lp, t, p = Theory.restore_path id in
let lp = if lp <> [] then lp else [Util.def_option "Builtin" info.fname] in
let s = String.concat "__" p in
let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
let s = sanitizer s in
let s = if is_ocaml_keyword s then s ^ "_renamed" else s in
if Sid.mem id info.current_theory.th_local then
fprintf fmt "%s" s
else
......@@ -343,7 +349,8 @@ and is_exec_branch b =
let _, t = t_open_branch b in is_exec_term t
let print_const fmt = function
| ConstInt (IConstDecimal s) -> fprintf fmt "(Num.num_of_string \"%s\")" s
| ConstInt (IConstDecimal s) ->
fprintf fmt "(Why3__BuiltIn.int_constant \"%s\")" s
| ConstInt (IConstHexa s) -> fprintf fmt (tbi "0x%s") s
| ConstInt (IConstOctal s) -> fprintf fmt (tbi "0o%s") s
| ConstInt (IConstBinary s) -> fprintf fmt (tbi "0b%s") s
......@@ -717,12 +724,11 @@ and print_lexpr pri info fmt e =
| Eloop (_,_,e) ->
fprintf fmt "@[while true do@ %a@ done@]" (print_expr info) e
| Efor (pv,(pvfrom,dir,pvto),_,e) ->
(* TODO: avoid conversion to/from int *)
fprintf fmt "@[<hov 2>for@ %a =@ Num.int_of_num %a@ %s@ \
Num.int_of_num %a do@\nlet %a = Num.num_of_int %a in@ %a@]@\ndone"
(print_pv info) pv (print_pv info) pvfrom
(if dir = To then "to" else "downto") (print_pv info) pvto
(print_pv info) pv (print_pv info) pv (print_expr info) e
fprintf fmt
"@[<hov 2>(Int__Int.for_loop_%s %a %a@ (fun %a -> %a))@]"
(if dir = To then "to" else "downto")
(print_pv info) pvfrom (print_pv info) pvto
(print_pv info) pv (print_expr info) e
| Eraise (xs,e) ->
begin match query_syntax info.info_syn xs.xs_name with
| Some s -> syntax_arguments s (print_expr info) fmt [e]
......@@ -946,13 +952,15 @@ let print_pprojections info fmt (ts, _, _ as d) =
let pdecl info fmt pd = match pd.pd_node with
| PDtype ts ->
print_type_decl info fmt ts
print_type_decl info fmt ts;
fprintf fmt "@\n@\n"
| PDdata tl ->
print_list_next newline (print_pdata_decl info) fmt tl;
fprintf fmt "@\n@\n";
print_list nothing (print_pprojections info) fmt tl
| PDval lv ->
print_val_decl info fmt lv
print_val_decl info fmt lv;
fprintf fmt "@\n@\n"
| PDlet ld ->
print_let_decl info fmt ld
| PDrec { rec_defn = rdl; rec_letrec = lr } ->
......
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