preliminary driver to map Why3 type int to OCaml type int

this is of course unsafe, yet useful if you have proved absence of
overflows independently or if you are happy with a partial correctness
proof (that is, if there is no overflow then the postcondition holds)

this is work in progress; nothing plugged in yet
parent 0cf707a8
......@@ -9,37 +9,7 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
end
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
theory option.Option
syntax type option "(%1 option)"
syntax function None "None"
syntax function Some "(Some %1)"
end
(* bool *)
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "(%1 && %2)"
syntax function orb "(%1 || %2)"
syntax function xorb "(%1 <> %2)"
syntax function notb "(not %1)"
syntax function implb "(not %1 || %2)"
end
import "ocaml-no-arith.drv"
(* int *)
......@@ -96,44 +66,8 @@ end
(* TODO number.Gcd *)
(* list *)
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "(%1 :: %2)"
end
theory list.Mem
syntax predicate mem "(List.mem %1 %2)"
end
theory list.Append
syntax function (++) "(List.append %1 %2)"
end
theory list.Reverse
syntax function reverse "(List.rev %1)"
end
theory list.RevAppend
syntax function rev_append "(List.rev_append %1 %2)"
end
theory list.Combine
syntax function combine "(List.combine %1 %2)"
end
(* WhyML *)
module ref.Ref
syntax type ref "(%1 Pervasives.ref)"
syntax function contents "%1.Pervasives.contents"
syntax val ref "Pervasives.ref"
syntax val (!_) "Pervasives.(!)"
syntax val (:=) "Pervasives.(:=)"
end
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
......@@ -265,16 +199,6 @@ module io.StdIO
syntax val print_newline "Pervasives.print_newline"
end
module null.Null
syntax type t "%1"
syntax val create_null "(fun () -> Obj.magic (ref 0))"
syntax val eq_null "(==)"
syntax val create "(fun x -> x)"
syntax val get "(fun x -> x)"
end
module random.Random
syntax val random_int "Why3__BigInt.random_int"
......
(** Arithmetic-independent OCaml driver *)
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
theory option.Option
syntax type option "(%1 option)"
syntax function None "None"
syntax function Some "(Some %1)"
end
(* bool *)
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "(%1 && %2)"
syntax function orb "(%1 || %2)"
syntax function xorb "(%1 <> %2)"
syntax function notb "(not %1)"
syntax function implb "(not %1 || %2)"
end
(* list *)
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "(%1 :: %2)"
end
theory list.Mem
syntax predicate mem "(List.mem %1 %2)"
end
theory list.Append
syntax function (++) "(List.append %1 %2)"
end
theory list.Reverse
syntax function reverse "(List.rev %1)"
end
theory list.RevAppend
syntax function rev_append "(List.rev_append %1 %2)"
end
theory list.Combine
syntax function combine "(List.combine %1 %2)"
end
(* WhyML *)
module ref.Ref
syntax type ref "(%1 Pervasives.ref)"
syntax function contents "%1.Pervasives.contents"
syntax val ref "Pervasives.ref"
syntax val (!_) "Pervasives.(!)"
syntax val (:=) "Pervasives.(:=)"
end
module null.Null
syntax type t "%1"
syntax val create_null "(fun () -> Obj.magic (ref 0))"
syntax val eq_null "(==)"
syntax val create "(fun x -> x)"
syntax val get "(fun x -> x)"
end
(** OCaml driver with Why3 type int being mapped to OCaml type int.
This is of course unsafe, yet useful to run your code is you
have an independant argument regarding the absence of arithmetic
overflows. *)
printer "ocaml"
theory BuiltIn
syntax type int "int"
(* meta "ocaml arithmetic" "unsafe int" *)
syntax predicate (=) "(%1 = %2)"
end
import "ocaml-no-arith.drv"
(* int *)
theory int.Int
syntax constant zero "0"
syntax constant one "1"
syntax predicate (<) "(%1 < %2)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (>) "(%1 > %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (-_) "(- %1)"
end
theory int.ComputerDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 mod %2)"
end
(* FIXME: avoid Pervasives using a black list of reserved OCaml names *)
theory int.Abs
syntax function abs "(Pervasives.abs %1)"
end
theory int.MinMax
syntax function min "(Pervasives.min %1 %2)"
syntax function max "(Pervasives.max %1 %2)"
end
(* FIXME
theory int.Lex2
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
theory int.EuclideanDivision
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
end
theory int.Power
syntax function power "(Why3__BigInt.power %1 %2)"
end
theory int.Fact
syntax function fact "(Why3__IntAux.fact %1)"
end
theory int.Fibonacci
syntax function fib "(Why3__IntAux.fib %1)"
end
TODO number.Gcd
*)
(* WhyML *)
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
syntax val push "Stack.push"
syntax exception Empty "Stack.Empty"
syntax val pop "Stack.pop"
syntax val top "Stack.top"
syntax val safe_pop "Stack.pop"
syntax val safe_top "Stack.top"
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "Stack.length"
end
module queue.Queue
syntax type t "(%1 Queue.t)"
syntax val create "Queue.create"
syntax val push "Queue.push"
syntax exception Empty "Queue.Empty"
syntax val pop "Queue.pop"
syntax val peek "Queue.peek"
syntax val safe_pop "Queue.pop"
syntax val safe_peek "Queue.peek"
syntax val clear "Queue.clear"
syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty"
syntax val length "Queue.length"
syntax val transfer "Queue.transfer"
end
module array.Array
syntax type array "(%1 array)"
syntax function ([]) "(%1.(%2))"
syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
syntax val ([]) "Array.unsafe_get"
syntax val ([]<-) "Array.unsafe_set"
syntax val length "Array.length"
syntax val defensive_get "Array.get"
syntax val defensive_set "Array.set"
syntax val make "Array.make"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
end
module mach.int.Int31
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax function to_int "(%1)"
syntax type int31 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
(* TODO
other mach.int.XXX modules *)
module mach.array.Array31
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
(* TODO
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
syntax function uppercase "Char.uppercase"
syntax function lowercase "Char.lowercase"
end
module io.StdIO
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
syntax val random_int "Why3__BigInt.random_int"
end
*)
......@@ -1039,6 +1039,11 @@ end
let extract_filename ?fname th =
(modulename ?fname th.th_path th.th_name.Ident.id_string) ^ ".ml"
(*
let arith_meta = register_meta "ocaml arithmetic" [MTstring]
~desc:"Specify@ OCaml@ arithmetic:@ 32, 64, or unsafe"
*)
let extract_theory drv ?old ?fname fmt th =
ignore (old); ignore (fname);
let info = {
......
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