extraction: fixed parentheses in driver and printer

parent 8eab207e
......@@ -6,7 +6,7 @@ printer "ocaml"
theory BuiltIn
syntax type int "Z.t"
syntax predicate (=) "(%1 = %2)"
syntax predicate (=) "%1 = %2"
end
import "ocaml-no-arith.drv"
......@@ -17,25 +17,25 @@ module int.Int
syntax constant zero "Z.zero"
syntax constant one "Z.one"
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 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 (+) "(Z.add %1 %2)"
syntax function (-) "(Z.sub %1 %2)"
syntax function ( * ) "(Z.mul %1 %2)"
syntax function (-_) "(Z.neg %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
syntax function abs "(Z.abs %1)"
syntax function abs "Z.abs %1"
end
theory int.MinMax
syntax function min "(Z.min %1 %2)"
syntax function max "(Z.max %1 %2)"
syntax function min "Z.min %1 %2"
syntax function max "Z.max %1 %2"
end
(* TODO
......@@ -47,18 +47,18 @@ end
*)
theory int.EuclideanDivision
syntax function div "(Z.ediv %1 %2)"
syntax function mod "(Z.erem %1 %2)"
syntax function div "Z.ediv %1 %2"
syntax function mod "Z.erem %1 %2"
end
theory int.ComputerDivision
syntax function div "(Z.div %1 %2)"
syntax function mod "(Z.rem %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
syntax function power "(Z.pow %1 %2)"
syntax function power "Z.pow %1 %2"
end
theory int.Fact
......@@ -75,7 +75,7 @@ end
(* WhyML *)
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax type t "%1 Stack.t"
syntax val create "Stack.create"
syntax val push "Stack.push"
syntax exception Empty "Stack.Empty"
......@@ -86,11 +86,11 @@ module stack.Stack
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "(Z.of_int (Stack.length %1))"
syntax val length "Z.of_int (Stack.length %1)"
end
module queue.Queue
syntax type t "(%1 Queue.t)"
syntax type t "%1 Queue.t"
syntax val create "Queue.create"
syntax val push "Queue.push"
syntax exception Empty "Queue.Empty"
......@@ -106,23 +106,23 @@ module queue.Queue
end
module array.Array
syntax type array "(%1 Array.t)"
syntax function ([]) "(Array.get %1 %2)"
syntax exception OutOfBounds "Why3__Array.OutOfBounds"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val defensive_get "Why3__Array.defensive_get"
syntax val defensive_set "Why3__Array.defensive_set"
syntax val make "Why3__Array.make"
syntax val append "Why3__Array.append"
syntax val sub "Why3__Array.sub"
syntax val copy "Why3__Array.copy"
syntax val fill "Why3__Array.fill"
syntax val blit "Why3__Array.blit"
syntax type array "%1 array"
syntax function ([]) "%1.(Z.to_int %2)"
(* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)
syntax val ([]) "%1.(Z.to_int %2)"
syntax val ([]<-) "%1.(Z.to_int %2) <- %3"
syntax val length "Z.of_int (Array.length %1)"
syntax val defensive_get "%1.(Z.to_int %2)"
syntax val defensive_set "%1.(Z.to_int %2) <- %3"
syntax val make "Array.make (Z.to_int %1) %2"
syntax val append "Array.append %1 %2"
syntax val sub "Array.sub %1 (Z.to_int %2) (Z.to_int %3)"
syntax val copy "Array.copy %1"
syntax val fill "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4"
syntax val blit "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)"
end
module matrix.Matrix
......
......@@ -10,9 +10,9 @@ end
*)
theory option.Option
syntax type option "(%1 option)"
syntax type option "%1 option"
syntax function None "None"
syntax function Some "(Some %1)"
syntax function Some "Some %1"
end
(* bool *)
......@@ -28,11 +28,11 @@ theory bool.Ite
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)"
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 *)
......@@ -40,37 +40,37 @@ end
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "(%1 :: %2)"
syntax function Cons "%1 :: %2"
end
theory list.Mem
syntax predicate mem "(List.mem %1 %2)"
syntax predicate mem "List.mem %1 %2"
end
theory list.Append
syntax function (++) "(List.append %1 %2)"
syntax function (++) "List.append %1 %2"
end
theory list.Reverse
syntax function reverse "(List.rev %1)"
syntax function reverse "List.rev %1"
end
theory list.RevAppend
syntax function rev_append "(List.rev_append %1 %2)"
syntax function rev_append "List.rev_append %1 %2"
end
theory list.Combine
syntax function combine "(List.combine %1 %2)"
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 %1"
syntax val (!_) "Pervasives.(!) %1"
syntax val (:=) "Pervasives.(:=) %1 %2"
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
(* FIXME: once we extract ref.Refint, this module
......
......@@ -73,19 +73,19 @@ module mach.int.Int63
syntax type int63 "int"
syntax constant min_int63 "min_int"
syntax constant max_int63 "max_int"
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 ( + ) "%1 + %2"
syntax val ( - ) "%1 - %2"
syntax val (-_) "- %1"
syntax val ( * ) "%1 * %2"
syntax val ( / ) "%1 / %2"
syntax val ( % ) "%1 mod %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)"*)
......
......@@ -124,7 +124,7 @@ module ML = struct
| Enot of expr
| Eblock of expr list
| Ewhile of expr * expr
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr (* Why3's type int *)
| Eraise of xsymbol * expr option
| Etry of expr * (xsymbol * pvsymbol list * expr) list
| Eabsurd
......
......@@ -116,13 +116,13 @@ module Print = struct
fprintf fmt "unit"
| Ttuple tl ->
fprintf fmt (protect_on paren "@[%a@]")
(print_list star (print_ty ~paren:false info)) tl
(print_list star (print_ty ~paren:true info)) tl
| Tapp (ts, [t1; t2]) when id_equal ts ts_func.ts_name ->
fprintf fmt (protect_on paren "@[%a ->@ %a@]")
(print_ty ~paren:true info) t1 (print_ty info) t2
| Tapp (ts, tl) ->
begin match query_syntax info.info_syn ts with
| Some s -> syntax_arguments s (print_ty info) fmt tl
| Some s -> syntax_arguments s (print_ty ~paren:true info) fmt tl
| None ->
begin match tl with
| [] ->
......@@ -217,7 +217,15 @@ module Print = struct
let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
let rec print_apply info fmt rs pvl =
let is_true e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_true
| _ -> false
let is_false e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_false
| _ -> false
let rec print_apply info rs fmt pvl =
let isfield =
match rs.rs_field with
| None -> false
......@@ -239,7 +247,7 @@ module Print = struct
| _ -> assert false in
syntax_arguments s print_constant fmt pvl
| _, Some s, _ ->
syntax_arguments s (print_expr info) fmt pvl
syntax_arguments s (print_expr ~paren:true info) fmt pvl
| _, _, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]"
(print_list comma (print_expr info)) tl
......@@ -265,7 +273,7 @@ module Print = struct
(print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
| _, _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident rs.rs_name (print_list space (print_expr info)) tl
print_ident rs.rs_name (print_list space (print_expr ~paren:true info)) tl
and print_let_def info fmt = function
| Lvar (pv, e) ->
......@@ -313,7 +321,8 @@ module Print = struct
fprintf fmt "@[<hov 1>%a %a@]"
(print_expr info) e1 (print_expr info) e2
| Eapp (s, pvl) ->
print_apply info fmt (Hrs.find_def ht_rs s s) pvl
fprintf fmt (protect_on paren "%a")
(print_apply info (Hrs.find_def ht_rs s s)) pvl
| Ematch (e, pl) ->
fprintf fmt "begin match @[%a@] with@\n@[<hov>%a@]@\nend"
(print_expr info) e (print_list newline (print_branch info)) pl
......@@ -329,6 +338,12 @@ module Print = struct
fprintf fmt
"@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]"
(print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) when is_true e2 ->
fprintf fmt
(protect_on paren "@[<hv>%a || %a@]") (print_expr info) e1 (print_expr info) e3
| Eif (e1, e2, e3) when is_false e3 ->
fprintf fmt
(protect_on paren "@[<hv>%a && %a@]") (print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) ->
fprintf fmt
"@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
......
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