Commit 7166632d authored by Mário Pereira's avatar Mário Pereira

OneTime module added to ocaml64 driver

parent a621477b
......@@ -222,6 +222,30 @@ module mach.int.Int63
syntax val of_bv "(fun x -> x)"*)
end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Z.of_int %1"
syntax val zero "0"
syntax val one "1"
syntax val succ "%1 + 1"
syntax val pred "%1 - 1"
syntax val lt "%1 < %2"
syntax val le "%1 <= %2"
syntax val gt "%1 > %2"
syntax val ge "%1 >= %2"
syntax val eq "%1 =a %2"
syntax val ne "%1 <> %2"
syntax converter to_peano "%1"
syntax val transfer "%1"
syntax val neg "-%1"
syntax val abs "abs %1"
syntax val add "%1 + %2"
syntax val sub "%1 - %2"
syntax val split "(%1-%2, %2)"
end
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Char.chr (Z.to_int %1)"
......
......@@ -7,13 +7,19 @@ module OneTime
type t = abstract { v: int; mutable valid: bool }
val to_int (x: t) : int
val function to_int (x: t) : int
ensures { result = x.v }
meta coercion function to_int
val zero (): t
ensures { result.valid }
ensures { result.v = 0 }
val one () : t
ensures { result.valid }
ensures { result.v = 1 }
val succ (x: t) : t
requires { x.valid }
writes { x.valid }
......
......@@ -10,26 +10,9 @@
(********************************************************************)
(*
- option to extract into a single file
- no more why3extract.cma
use driver preludes instead
- 2 drivers for nums and zarith
- no delcaration at all for a module -> no file produced
(e.g. ref.Ref)
- suggest a command line to compile the extracted code
(for instance in a comment)
- drivers for val now may use %1, %2, etc. (though not mandatory)
Capp f x y
"..." -> "..." x y
"...%1..." -> "...x..." y
"..(*%1*)..." -> "...(*x*)..." y
"..%1..%3.." -> (fun z -> "..x..z..") (y ignored)
- extract file f.mlw into OCaml file f.ml, with sub-modules
- "use (im|ex)port" -> "open"
......@@ -38,33 +21,8 @@
- if a WhyML module M is extracted to something that is a signature,
then extract "module type B_sig = ..." (as well as "module B = ...")
- use a black list in printer to avoid clash with Pervasives symbols
(e.g. ref, (!), etc.)
*)
(*
Questions pour Jean-Christophe et Andreï :
- est-ce qu'il y a des utilisations particulières du champ
[itd_fields], vis-à-vis du champ [itd_constructors] ?
- comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
fait du sense pour vous d'utiliser des applications de la forme
[Eapp of ident * ident list] ?
- faire un module Erasure, pour y concentrer tout ce qui
appartient à l'éffacement du code fantôme ?
- comment est-ce qu'il marche la [mask] d'un [prog_pattern] ?
*)
(*
TODO: réfléchir sur l'affectation parallèle
*)
(** Abstract syntax of ML *)
open Ident
......
......@@ -170,11 +170,18 @@ let translate_module =
Ident.Hid.add memo name pm;
pm
let not_extractable_theories = ["why3"; "map";]
let is_not_extractable_theory =
let h = Hstr.create 16 in
List.iter (fun s -> Hstr.add h s ()) not_extractable_theories;
Hstr.mem h
let extract_to =
let memo = Ident.Hid.create 16 in
fun ?fname ?decl m ->
match m.mod_theory.Theory.th_path with
| ("why3" | "map")::_ -> ()
| t::_ when is_not_extractable_theory t -> ()
| _ -> let name = m.mod_theory.Theory.th_name in
if not (Ident.Hid.mem memo name) then begin
Ident.Hid.add memo name ();
......
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