Commit 6fb58a7a authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'ocaml_printer_precedences' into 'master'

Move the Ocaml printer to a precedence-based system

Closes #284

See merge request !104
parents 4508d668 81369020
......@@ -16,12 +16,6 @@ module ref.Ref
syntax val (:=) "%1 = %2" prec 14 13 14
end
module mach.int.Unsigned
syntax constant zero_unsigned "0"
end
module mach.int.Int32
syntax type int32 "int32_t"
......
......@@ -3,89 +3,82 @@
printer "ocaml"
theory BuiltIn
module BuiltIn
syntax type int "Z.t"
syntax predicate (=) "%1 = %2"
end
module HighOrd
syntax type (->) "%1 -> %2"
syntax val ( @ ) "%1 %2"
syntax val ( @ ) "%1 %2" prec 4 4 3
end
theory option.Option
module option.Option
syntax type option "%1 option"
syntax function None "None"
syntax function Some "Some %1"
syntax predicate is_none "%1 = None"
syntax val None "None"
syntax val Some "Some %1" prec 4 3
end
theory Bool
module Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax val True "true"
syntax val False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
module bool.Ite
syntax val ite "if %1 then %2 else %3" prec 16 15 15 15
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"
module bool.Bool
syntax val andb "%1 && %2" prec 12 11 12
syntax val orb "%1 || %2" prec 13 12 13
syntax val xorb "%1 <> %2" prec 11 11 10
syntax val notb "not %1" prec 4 3
syntax val implb "not %1 || %2" prec 13 3 13
end
theory list.List
module list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "%1 :: %2"
syntax predicate is_nil "%1 = []"
syntax val Nil "[]"
syntax val Cons "%1 :: %2" prec 9 8 9
end
theory list.Length
syntax function length "Z.of_int (List.length %1)"
module list.Length
syntax val length "Z.of_int (List.length %1)" prec 4 3
end
theory list.Mem
syntax predicate mem "List.mem %1 %2"
module list.Append
syntax val (++) "List.append %1 %2" prec 4 3 3
end
theory list.Append
syntax function (++) "List.append %1 %2"
module list.Reverse
syntax val reverse "List.rev %1" prec 4 3
end
theory list.Reverse
syntax function reverse "List.rev %1"
module list.RevAppend
syntax val rev_append "List.rev_append %1 %2" prec 4 3
end
theory list.RevAppend
syntax function rev_append "List.rev_append %1 %2"
end
theory list.Combine
syntax function combine "List.combine %1 %2"
module list.Combine
syntax val combine "List.combine %1 %2" prec 4 3 3
end
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
syntax val contents "!%1" prec 1 0
syntax val ref "ref %1" prec 4 3
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
syntax val (!_) "!%1" prec 1 0
syntax val (:=) "%1 := %2" prec 15 14 15
end
module ref.Refint
syntax val incr "%1 := Z.succ (!%1)"
syntax val decr "%1 := Z.pred (!%1)"
syntax val (+=) "%1 := Z.add (!%1) %2"
syntax val (-=) "%1 := Z.sub (!%1) %2"
syntax val ( *= ) "%1 := Z.mul (!%1) %2"
syntax val incr "%1 := Z.succ !%1" prec 15 0
syntax val decr "%1 := Z.pred !%1" prec 15 0
syntax val (+=) "%1 := Z.add !%1 %2" prec 15 0 0
syntax val (-=) "%1 := Z.sub !%1 %2" prec 15 0 0
syntax val ( *= ) "%1 := Z.mul !%1 %2" prec 15 0 0
end
module null.Null
......@@ -99,38 +92,38 @@ module null.Null
end
module int.Int
syntax constant zero "Z.zero"
syntax constant one "Z.one"
syntax val zero "Z.zero"
syntax val 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 val (<) "Z.lt %1 %2" prec 4 3 3
syntax val (<=) "Z.leq %1 %2" prec 4 3 3
syntax val (>) "Z.gt %1 %2" prec 4 3 3
syntax val (>=) "Z.geq %1 %2" prec 4 3 3
syntax val (=) "Z.equal %1 %2" prec 4 3 3
syntax function (+) "Z.add %1 %2"
syntax function (-) "Z.sub %1 %2"
syntax function ( * ) "Z.mul %1 %2"
syntax function (-_) "Z.neg %1"
syntax val (+) "Z.add %1 %2" prec 4 3 3
syntax val (-) "Z.sub %1 %2" prec 4 3 3
syntax val ( * ) "Z.mul %1 %2" prec 4 3 3
syntax val (-_) "Z.neg %1" prec 4 3
end
theory int.Abs
syntax function abs "Z.abs %1"
module int.Abs
syntax val abs "Z.abs %1" prec 4 3
end
theory int.MinMax
syntax function min "Z.min %1 %2"
syntax function max "Z.max %1 %2"
module int.MinMax
syntax val min "Z.min %1 %2" prec 4 3 3
syntax val max "Z.max %1 %2" prec 4 3 3
end
module int.EuclideanDivision
syntax val div "Z.ediv %1 %2"
syntax val mod "Z.erem %1 %2"
syntax val div "Z.ediv %1 %2" prec 4 3 3
syntax val mod "Z.erem %1 %2" prec 4 3 3
end
module int.ComputerDivision
syntax val div "Z.div %1 %2"
syntax val mod "Z.rem %1 %2"
syntax val div "Z.div %1 %2" prec 4 3 3
syntax val mod "Z.rem %1 %2" prec 4 3 3
end
module stack.Stack
......@@ -145,7 +138,7 @@ module stack.Stack
syntax val clear "Stack.clear"
syntax val copy "Stack.copy"
syntax val is_empty "Stack.is_empty"
syntax val length "Stack.length %1"
syntax val length "Stack.length %1" prec 4 3
end
module queue.Queue
......@@ -160,7 +153,7 @@ module queue.Queue
syntax val clear "Queue.clear"
syntax val copy "Queue.copy"
syntax val is_empty "Queue.is_empty"
syntax val length "Queue.length %1"
syntax val length "Queue.length %1" prec 4 3
syntax val transfer "Queue.transfer"
end
......@@ -169,21 +162,21 @@ module array.Array
(* 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)"
syntax val ([]) "%1.(Z.to_int %2)" prec 2 1 3
syntax val ([]<-) "%1.(Z.to_int %2) <- %3" prec 15 2 1 15
syntax val length "Z.of_int (Array.length %1)" prec 4 3
syntax val defensive_get "%1.(Z.to_int %2)" prec 2 1 3
syntax val defensive_set "%1.(Z.to_int %2) <- %3" prec 15 2 1 15
syntax val make "Array.make (Z.to_int %1) %2" prec 4 3 3
syntax val append "Array.append %1 %2" prec 4 3 3
syntax val sub "Array.sub %1 (Z.to_int %2) (Z.to_int %3)" prec 4 3 3 3
syntax val copy "Array.copy %1" prec 4 3
syntax val fill "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4" prec 4 3 3 3
syntax val blit "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)" prec 4
end
module array.Init
syntax val init "Array.init (Z.to_int %1) (fun i -> %2 (Z.of_int i))"
syntax val init "Array.init (Z.to_int %1) (fun i -> %2 (Z.of_int i))" prec 4 3 14
end
module matrix.Matrix
......@@ -191,19 +184,19 @@ module matrix.Matrix
(* syntax exception OutOfBounds "Why3__Matrix.OutOfBounds" *) (* FIXME *)
syntax val get "%1.(Z.to_int %2).(Z.to_int %3)"
syntax val set "%1.(Z.to_int %2).(Z.to_int %3) <- %4"
syntax val rows "Z.of_int (Array.length %1)"
syntax val columns "Z.of_int (Array.length %1.(0))"
syntax val defensive_get "%1.(Z.to_int %2).(Z.to_int %3)"
syntax val defensive_set "%1.(Z.to_int %2).(Z.to_int %3) <- %4"
syntax val make "Array.make_matrix (Z.to_int %1) (Z.to_int %2) %3"
syntax val copy "Array.map Array.copy %1"
syntax val get "%1.(Z.to_int %2).(Z.to_int %3)" prec 2 1 3 3
syntax val set "%1.(Z.to_int %2).(Z.to_int %3) <- %4" prec 15 1 3 3 14
syntax val rows "Z.of_int (Array.length %1)" prec 4 3
syntax val columns "Z.of_int (Array.length %1.(0))" prec 4 3
syntax val defensive_get "%1.(Z.to_int %2).(Z.to_int %3)" prec 2 1 3 3
syntax val defensive_set "%1.(Z.to_int %2).(Z.to_int %3) <- %4" prec 15 1 3 3 14
syntax val make "Array.make_matrix (Z.to_int %1) (Z.to_int %2) %3" prec 4 3 3 3
syntax val copy "Array.map Array.copy %1" prec 4 3
end
module mach.int.Int
syntax val ( / ) "Z.div %1 %2"
syntax val ( % ) "Z.rem %1 %2"
syntax val ( / ) "Z.div %1 %2" prec 4 3 3
syntax val ( % ) "Z.rem %1 %2" prec 4 3 3
end
module mach.int.Int32
......@@ -211,22 +204,22 @@ module mach.int.Int32
syntax literal int32 "%1"
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1"
syntax val of_int "Z.to_int %1" prec 4 3
syntax val to_int "Z.of_int %1" prec 4 3
syntax constant min_int32 "Z.of_int 0x7fff_ffff"
syntax constant max_int32 "Z.of_int (-0x8000_0000)"
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 (=) "%1 = %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val min_int32 "Z.of_int 0x7fff_ffff"
syntax val max_int32 "Z.of_int (-0x8000_0000)"
syntax val ( + ) "%1 + %2" prec 8 8 7
syntax val ( - ) "%1 - %2" prec 8 8 7
syntax val (-_) "- %1" prec 5 4
syntax val ( * ) "%1 * %2" prec 8 8 7
syntax val ( / ) "%1 / %2" prec 8 8 7
syntax val ( % ) "%1 mod %2" prec 8 8 7
syntax val (=) "%1 = %2" prec 11 11 10
syntax val (<=) "%1 <= %2" prec 11 11 10
syntax val (<) "%1 < %2" prec 11 11 10
syntax val (>=) "%1 >= %2" prec 11 11 10
syntax val (>) "%1 > %2" prec 11 11 10
end
module mach.int.Int63
......@@ -237,23 +230,23 @@ module mach.int.Int63
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1"
syntax constant min_int63 "Z.of_int min_int"
syntax constant max_int63 "Z.of_int max_int"
syntax constant min_int "min_int"
syntax constant max_int "max_int"
syntax constant zero "0"
syntax constant one "1"
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 (=) "%1 = %2"
syntax val (<=) "%1 <= %2"
syntax val (<) "%1 < %2"
syntax val (>=) "%1 >= %2"
syntax val (>) "%1 > %2"
syntax val min_int63 "Z.of_int min_int"
syntax val max_int63 "Z.of_int max_int"
syntax val min_int "min_int"
syntax val max_int "max_int"
syntax val zero "0"
syntax val one "1"
syntax val ( + ) "%1 + %2" prec 8 8 7
syntax val ( - ) "%1 - %2" prec 8 8 7
syntax val (-_) "- %1" prec 5 4
syntax val ( * ) "%1 * %2" prec 8 8 7
syntax val ( / ) "%1 / %2" prec 8 8 7
syntax val ( % ) "%1 mod %2" prec 8 8 7
syntax val (=) "%1 = %2" prec 11 11 10
syntax val (<=) "%1 <= %2" prec 11 11 10
syntax val (<) "%1 < %2" prec 11 11 10
syntax val (>=) "%1 >= %2" prec 11 11 10
syntax val (>) "%1 > %2" prec 11 11 10
(* syntax val to_bv "(fun x -> x)"
syntax val of_bv "(fun x -> x)"*)
......@@ -261,10 +254,10 @@ end
module mach.int.Random63
syntax val s "REMOVE"
syntax val init "Random.init %1"
syntax val self_init "Random.self_init %1"
syntax val random_bool "Random.bool %1"
syntax val random_int63 "Random.int %1"
syntax val init "Random.init %1" prec 4 3
syntax val self_init "Random.self_init %1" prec 4 3
syntax val random_bool "Random.bool %1" prec 4 3
syntax val random_int63 "Random.int %1" prec 4 3
end
module mach.int.State63
......@@ -280,131 +273,131 @@ end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int %1"
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1" prec 4 3
syntax val of_int "Z.to_int %1" prec 4 3
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 = %2"
syntax val ne "%1 <> %2"
syntax val neg "- %1"
syntax val abs "abs %1"
syntax val add "%1 + %2"
syntax val sub "%1 - %2"
syntax val mul "%1 * %2"
syntax val succ "%1 + 1" prec 8 8
syntax val pred "%1 - 1" prec 8 8
syntax val lt "%1 < %2" prec 11 11 10
syntax val le "%1 <= %2" prec 11 11 10
syntax val gt "%1 > %2" prec 11 11 10
syntax val ge "%1 >= %2" prec 11 11 10
syntax val eq "%1 = %2" prec 11 11 10
syntax val ne "%1 <> %2" prec 11 11 10
syntax val neg "- %1" prec 5 4
syntax val abs "abs %1" prec 4 3
syntax val add "%1 + %2" prec 8 8 7
syntax val sub "%1 - %2" prec 8 8 7
syntax val mul "%1 * %2" prec 7 7 6
end
module mach.peano.ComputerDivision
syntax val div "%1 / %2"
syntax val mod "%1 mod %2"
syntax val div "%1 / %2" prec 7 7 6
syntax val mod "%1 mod %2" prec 7 7 6
end
module mach.peano.MinMax
syntax val max "max %1 %2"
syntax val min "min %1 %2"
syntax val max "max %1 %2" prec 4 3 3
syntax val min "min %1 %2" prec 4 3 3
end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Z.of_int %1"
syntax val to_int "Z.of_int %1" prec 4 3
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 = %2"
syntax val ne "%1 <> %2"
syntax val succ "%1 + 1" prec 8 8
syntax val pred "%1 - 1" prec 8 8
syntax val lt "%1 < %2" prec 11 11 10
syntax val le "%1 <= %2" prec 11 11 10
syntax val gt "%1 > %2" prec 11 11 10
syntax val ge "%1 >= %2" prec 11 11 10
syntax val eq "%1 = %2" prec 11 11 10
syntax val ne "%1 <> %2" prec 11 11 10
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)"
syntax val neg "-%1" prec 5 4
syntax val abs "abs %1" prec 4 3
syntax val add "%1 + %2" prec 8 8 7
syntax val sub "%1 - %2" prec 8 8 7
syntax val split "(%1-%2, %2)" prec 0 13 13
end
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Char.chr (Z.to_int %1)"
syntax val code "Z.of_int (Char.code %1)"
syntax function uppercase "Char.uppercase %1"
syntax function lowercase "Char.lowercase %1"
syntax val chr "Char.chr (Z.to_int %1)" prec 4 3
syntax val code "Z.of_int (Char.code %1)" prec 4 3
syntax val uppercase "Char.uppercase %1" prec 4 3
syntax val lowercase "Char.lowercase %1" prec 4 3
end
module io.StdIO
syntax val print_char "Pervasives.print_char %1"
syntax val print_int "Pervasives.print_string (Z.to_string %1)"
syntax val print_newline "Pervasives.print_newline %1"
syntax val print_char "Pervasives.print_char %1" prec 4 3
syntax val print_int "Pervasives.print_string (Z.to_string %1)" prec 4 3
syntax val print_newline "Pervasives.print_newline %1" prec 4 3
end
module random.Random
syntax val random_int "Z.of_int (Random.int (Z.to_int %1))"
syntax val random_int "Z.of_int (Random.int (Z.to_int %1))" prec 4 3
end
module mach.int.Refint63
syntax val incr "incr %1"
syntax val decr "decr %1"
syntax val (+=) "%1 := !%1 + %2"
syntax val (-=) "%1 := !%1 - %2"
syntax val ( *= ) "%1 := !%1 * %2"
syntax val incr "incr %1" prec 4 3
syntax val decr "decr %1" prec 4 3
syntax val (+=) "%1 := !%1 + %2" prec 15 0 7
syntax val (-=) "%1 := !%1 - %2" prec 15 0 7
syntax val ( *= ) "%1 := !%1 * %2" prec 15 0 7
end
module mach.int.MinMax63
syntax val min "Pervasives.min %1 %2"
syntax val max "Pervasives.max %1 %2"
syntax val min "Pervasives.min %1 %2" prec 4 3 3
syntax val max "Pervasives.max %1 %2" prec 4 3 3
end
module mach.array.Array32
syntax type array "(%1 array)"
syntax exception OutOfBounds "Invalid_argument \"index out of bounds\""
syntax val make "Array.make %1 %2"
syntax val ([]) "%1.(%2)"
syntax val ([]<-) "%1.(%2) <- %3"
syntax val defensive_get "%1.(%2)"
syntax val defensive_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"
syntax val make "Array.make %1 %2" prec 4 3 3
syntax val ([]) "%1.(%2)" prec 2 1 18
syntax val ([]<-) "%1.(%2) <- %3" prec 15 1 18 15
syntax val defensive_get "%1.(%2)" prec 2 1 18
syntax val defensive_set "%1.(%2) <- %3" prec 15 1 18 15
syntax val length "Array.length %1" prec 4
syntax val append "Array.append %1 %2" prec 4
syntax val sub "Array.sub %1 %2 %3" prec 4
syntax val copy "Array.copy %1" prec 4
syntax val fill "Array.fill %1 %2 %3 %4" prec 4
syntax val blit "Array.blit %1 %2 %3 %4 %5" prec 4
syntax val self_blit "Array.blit %1 %2 %1 %3 %4" prec 4
end
module mach.array.Array63
syntax type array "(%1 array)"
syntax exception OutOfBounds "Invalid_argument \"index out of bounds\""
syntax val make "Array.make %1 %2"
syntax val ([]) "%1.(%2)"
syntax val ([]<-) "%1.(%2) <- %3"
syntax val defensive_get "%1.(%2)"
syntax val defensive_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"
syntax val init "Array.init %1 %2"
syntax val make "Array.make %1 %2" prec 4
syntax val ([]) "%1.(%2)" prec 2 1 18
syntax val ([]<-) "%1.(%2) <- %3" prec 15 1 18 15
syntax val defensive_get "%1.(%2)" prec 2 1 18
syntax val defensive_set "%1.(%2) <- %3" prec 15 1 18 15
syntax val length "Array.length %1" prec 4
syntax val append "Array.append %1 %2" prec 4
syntax val sub "Array.sub %1 %2 %3" prec 4
syntax val copy "Array.copy %1" prec 4
syntax val fill "Array.fill %1 %2 %3 %4" prec 4
syntax val blit "Array.blit %1 %2 %3 %4 %5" prec 4
syntax val self_blit "Array.blit %1 %2 %1 %3 %4" prec 4
syntax val init "Array.init %1 %2" prec 4
end
module mach.array.ArrayInt63
syntax type array63 "(int array)"
syntax val make "Array.make %1 %2"
syntax val ([]) "%1.(%2)"
syntax val ([]<-) "%1.(%2) <- %3"
syntax val length "Array.length %1"
syntax val copy "Array.copy %1"
syntax val make "Array.make %1 %2" prec 4
syntax val ([]) "%1.(%2)" prec 2 1 18
syntax val ([]<-) "%1.(%2) <- %3" prec 15 1 18 15
syntax val length "Array.length %1" prec 4
syntax val copy "Array.copy %1" prec 4
end
module mach.matrix.Matrix63
......@@ -412,16 +405,16 @@ module mach.matrix.Matrix63
(* syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")" *)
syntax function rows "Array.length %1"
syntax function columns "Array.length %1.(0)"
syntax val rows "Array.length %1"
syntax val columns "Array.length %1.(0)"
syntax val get "%1.(%2).(%3)"
syntax val set "%1.(%2).(%3) <- %4"
syntax val defensive_get "%1.(%2).(%3)"
syntax val defensive_set "%1.(%2).(%3) <- %4"
syntax val make "Array.make_matrix %1 %2 %3"
syntax val copy "Array.map Array.copy %1"
syntax val rows "Array.length %1" prec 4
syntax val columns "Array.length %1.(0)" prec 4 1
syntax val rows "Array.length %1" prec 4
syntax val columns "Array.length %1.(0)" prec 4 1
syntax val get "%1.(%2).(%3)" prec 2 1 18 18
syntax val set "%1.(%2).(%3) <- %4" prec 15 1 18 18 15
syntax val defensive_get "%1.(%2).(%3)" prec 2 1 18 18
syntax val defensive_set "%1.(%2).(%3) <- %4" prec 15 1 18 18 15
syntax val make "Array.make_matrix %1 %2 %3" prec 4
syntax val copy "Array.map Array.copy %1" prec 4
end
module ocaml.Sys
......@@ -432,8 +425,8 @@ module ocaml.Pervasives
syntax exception Exit "Pervasives.Exit"
syntax exception Not_found "Not_found"
syntax exception AssertFailure "REMOVE"
syntax val ocaml_assert "assert (%1)"
syntax val ocaml_assert "assert %1" prec 4
syntax exception Invalid_argument "Invalid_argument \"\""
syntax val succ "succ %1"
syntax val pred "pred %1"
syntax val succ "succ %1" prec 4
syntax val pred "pred %1" prec 4
end
......@@ -116,7 +116,7 @@ val gen_syntax_arguments_typed_prec :
val syntax_arguments_typed_prec :
string -> (int -> term Pp.pp) -> ty Pp.pp -> term -> int list -> term list Pp.pp
(** (syntax_arguments_typed templ print_arg prec_list fmt l) prints in the
(** (syntax_arguments_typed_prec templ print_arg prec_list fmt l) prints in the
formatter fmt the list l using the template templ, the printer print_arg
and the precedence list prec_list *)
......
......@@ -59,6 +59,7 @@ module C = struct
| Eindex of expr * expr (* Array access *)
| Edot of expr * string (* Field access with dot *)
| Earrow of expr * string (* Pointer access with arrow *)
| Esyntaxrename of string * expr list (* syntax val f "g" w/o params *)
| Esyntax of string * ty * (ty array) * (expr*ty) list * int list
(* template, type and type arguments of result, typed arguments, precedence level *)
......@@ -172,7 +173,9 @@ module C = struct
| Edot (e,i) -> Edot (propagate_in_expr id v e, i)
| Earrow (e,i) -> Earrow (propagate_in_expr id v e, i)
| Esyntax (s,t,ta,l,p) ->
Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l,p)
Esyntax (s,t,ta,List.map (fun (e,t) -> (propagate_in_expr id v e),t) l,p)
| Esyntaxrename (s, l) ->
Esyntaxrename (s, List.map (propagate_in_expr id v) l)
| Enothing -> Enothing
| Econst c -> Econst c
| Elikely e -> Elikely (propagate_in_expr id v e)
......@@ -400,6 +403,7 @@ module C = struct
| Esize_type _ -> true
| Eindex (_,_) | Edot (_,_) | Earrow (_,_) -> false
| Esyntax (_,_,_,_,_) -> false
| Esyntaxrename _ -> false
let rec get_const_expr (d,s) =
let fail () = raise (Unsupported "non-constant array size") in
......@@ -558,8 +562,8 @@ module Print = struct
| Ecast(ty, e) ->
fprintf fmt (protect_on (prec < 2) "(%a)%a")
(print_ty ~paren:false) ty (print_expr ~prec:2) e
| Ecall (Esyntax (s, _, _, [],_), l) ->
(* function defined in the prelude *)
| Esyntaxrename (s, l) ->
(* call to function defined in the prelude *)
fprintf fmt (protect_on (prec < 1) "%s(%a)")
s (print_list comma (print_expr ~prec:15)) l
| Ecall (e,l) ->
......@@ -988,29 +992,29 @@ module MLToC = struct
unboxed_params args in
match query_syntax info.syntax rs.rs_name with
| Some s ->
begin
try
let _ =
Str.search_forward
(Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0 in
let rty =