Commit 38bc0e10 authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

Adding support in drivers for Zarith and the ocaml.mlw file
parent 0f26787c
......@@ -1674,10 +1674,9 @@ test-ocaml-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmx
######################################
test-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa
@mkdir -p tests/test-extraction-mario
@cd tests ; ../bin/why3extract.opt -D ../drivers/ocaml64.drv \
test_extraction_mario.mlw -o test-extraction-mario
@cd tests/test-extraction-mario/ ; \
$(OCAMLOPT) test_extraction_mario__M.ml
@bin/why3extract.opt -D drivers/ocaml64.drv \
tests/test_extraction_mario.mlw -o tests/test-extraction-mario/
@$(OCAMLOPT) -c -I lib/ocaml -I lib/why3 tests/test-extraction-mario/test_extraction_mario__M.ml
################
# documentation
......
......@@ -5,7 +5,7 @@
printer "ocaml"
theory BuiltIn
syntax type int "Why3extract.Why3__BigInt.t"
syntax type int "Z.t"
syntax predicate (=) "(%1 = %2)"
end
......@@ -13,54 +13,52 @@ import "ocaml-no-arith.drv"
(* int *)
theory int.Int
prelude "open Why3extract"
syntax constant zero "Why3__BigInt.zero"
syntax constant one "Why3__BigInt.one"
module int.Int
syntax constant zero "Z.zero"
syntax constant one "Z.one"
syntax predicate (<) "(Why3__BigInt.lt %1 %2)"
syntax predicate (<=) "(Why3__BigInt.le %1 %2)"
syntax predicate (>) "(Why3__BigInt.gt %1 %2)"
syntax predicate (>=) "(Why3__BigInt.ge %1 %2)"
syntax predicate (<) "(Z.lt %1 %2)"
syntax predicate (<=) "(Z.leq %1 %2)"
syntax predicate (>) "(Z.gt %1 %2)"
syntax predicate (>=) "(Z.geq %1 %2)"
syntax val (=) "(Z.equal %1 %2)"
syntax function (+) "(Why3__BigInt.add %1 %2)"
syntax function (-) "(Why3__BigInt.sub %1 %2)"
syntax function ( * ) "(Why3__BigInt.mul %1 %2)"
syntax function (-_) "(Why3__BigInt.minus %1)"
syntax function (+) "(Z.add %1 %2)"
syntax function (-) "(Z.sub %1 %2)"
syntax function ( * ) "(Z.mul %1 %2)"
syntax function (-_) "(Z.neg %1)"
end
theory int.Abs
prelude "open Why3extract"
syntax function abs "(Why3__BigInt.abs %1)"
syntax function abs "(Z.abs %1)"
end
theory int.MinMax
prelude "open Why3extract"
syntax function min "(Why3__BigInt.min %1 %2)"
syntax function max "(Why3__BigInt.max %1 %2)"
syntax function min "(Z.min %1 %2)"
syntax function max "(Z.max %1 %2)"
end
(* TODO
theory int.Lex2
prelude "open Why3extract"
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
*)
theory int.EuclideanDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
syntax function div "(Z.ediv %1 %2)"
syntax function mod "(Z.erem %1 %2)"
end
theory int.ComputerDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.computer_div %1 %2)"
syntax function mod "(Why3__BigInt.computer_mod %1 %2)"
syntax function div "(Z.div %1 %2)"
syntax function mod "(Z.rem %1 %2)"
end
(* TODO Z.pow has type t -> int -> t, not t -> t -> t
theory int.Power
prelude "open Why3extract"
syntax function power "(Why3__BigInt.power %1 %2)"
syntax function power "(Z.pow %1 %2)"
end
theory int.Fact
......@@ -72,13 +70,11 @@ theory int.Fibonacci
prelude "open Why3extract"
syntax function fib "(Why3__IntAux.fib %1)"
end
(* TODO number.Gcd *)
*)
(* WhyML *)
module stack.Stack
prelude "open Why3extract"
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
syntax val push "Stack.push"
......@@ -90,11 +86,10 @@ module stack.Stack
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "Why3__IntAux.stack_length"
syntax val length "(Z.of_int (Stack.length %1))"
end
module queue.Queue
prelude "open Why3extract"
syntax type t "(%1 Queue.t)"
syntax val create "Queue.create"
syntax val push "Queue.push"
......@@ -106,7 +101,7 @@ module queue.Queue
syntax val clear "Queue.clear"
syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty"
syntax val length "Why3__IntAux.queue_length"
syntax val length "(Z.of_int (Queue.length %1))"
syntax val transfer "Queue.transfer"
end
......@@ -150,9 +145,8 @@ module matrix.Matrix
end
module mach.int.Int
prelude "open Why3extract"
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
syntax val ( / ) "Z.div %1 %2"
syntax val ( % ) "Z.rem %1 %2"
end
module mach.int.Int31
......
......@@ -68,9 +68,9 @@ end
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.(:=)"
syntax val ref "Pervasives.ref %1"
syntax val (!_) "Pervasives.(!) %1"
syntax val (:=) "Pervasives.(:=) %1 %2"
end
module null.Null
......
......@@ -5,6 +5,7 @@ import "ocaml-gen.drv"
(** Machine arithmetic *)
(*
module mach.int.Int32
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
......@@ -61,6 +62,7 @@ module mach.int.UInt32
(Int64.to_int (Int64.logand r 0xFFFFFFFFL),Int64.to_int (Int64.shift_right_logical r 32)))"
end
*)
module mach.int.Int63
syntax val of_int "Why3extract.Why3__BigInt.to_int"
......@@ -69,26 +71,27 @@ module mach.int.Int63
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int63 "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 (>) "(>)"
syntax val ( + ) "( + ) %1 %2"
syntax val ( - ) "( - ) %1 %2"
syntax val (-_) "( ~- ) %1 %2"
syntax val ( * ) "( * ) %1 %2"
syntax val ( / ) "( / ) %1 %2"
syntax val ( % ) "(mod) %1 %2"
syntax val eq "(=) %1 %2"
syntax val ne "(<>) %1 %2"
syntax val (=) "(=) %1 %2"
syntax val (<=) "(<=) %1 %2"
syntax val (<) "(<) %1 %2"
syntax val (>=) "(>=) %1 %2"
syntax val (>) "(>) %1 %2"
(* syntax val to_bv "(fun x -> x)"
syntax val of_bv "(fun x -> x)"*)
end
module mach.int.Refint63
syntax val incr "Pervasives.incr"
syntax val decr "Pervasives.decr"
syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
syntax val incr "Pervasives.incr %1"
syntax val decr "Pervasives.decr %1"
syntax val (+=) "%1 := !%1 + %2" (*"(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"*)
syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
end
......@@ -97,6 +100,7 @@ module mach.int.MinMax63
syntax val max "Pervasives.max"
end
(*
module mach.int.Int64
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
......@@ -195,22 +199,24 @@ module mach.array.Array32
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
*)
module mach.array.Array63
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"
syntax val make "Array.make %1 %2"
syntax val ([]) "Array.get %1 %2"
syntax val ([]<-) "Array.set %1 %2 %3"
syntax val length "Array.length %1"
syntax val append "Array.append %1 %2"
syntax val sub "Array.sub %1 %2 %3"
syntax val copy "Array.copy %1"
syntax val fill "Array.fill %1 %2 %3 %4"
syntax val blit "Array.blit %1 %2 %3 %4 %5"
syntax val self_blit "Array.blit %1 %2 %1 %3 %4"
end
(*
module mach.matrix.Matrix63
syntax type matrix "(%1 array array)"
......@@ -227,3 +233,12 @@ module mach.matrix.Matrix63
syntax val make "Array.make_matrix"
syntax val copy "(Array.map Array.copy)"
end
*)
module ocaml.Sys
syntax val max_array_length "Sys.max_array_length"
end
module ocaml.Pervasives
syntax exception Exit "Pervasives.Exit"
end
\ No newline at end of file
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