mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
119 lines
2.7 KiB
Plaintext
119 lines
2.7 KiB
Plaintext
|
|
(** CakeML driver *)
|
|
|
|
printer "cakeml"
|
|
|
|
module BuiltIn
|
|
syntax type int "int"
|
|
end
|
|
|
|
module HighOrd
|
|
syntax type (->) "%1 -> %2"
|
|
syntax val ( @ ) "%1 %2"
|
|
end
|
|
|
|
module option.Option
|
|
syntax type option "%1 option"
|
|
syntax val None "NONE"
|
|
syntax val Some "SOME %1"
|
|
end
|
|
|
|
module Bool
|
|
syntax type bool "bool"
|
|
syntax val True "true"
|
|
syntax val False "false"
|
|
end
|
|
|
|
module bool.Ite
|
|
syntax val ite "(if %1 then %2 else %3)"
|
|
end
|
|
|
|
module bool.Bool
|
|
syntax val andb "%1 andalso %2"
|
|
syntax val orb "%1 orelse %2"
|
|
syntax val xorb "%1 <> %2"
|
|
syntax val notb "not %1"
|
|
syntax val implb "not %1 orelse %2"
|
|
end
|
|
|
|
module list.List
|
|
syntax type list "%1 list"
|
|
syntax val Nil "[]"
|
|
syntax val Cons "%1 :: %2"
|
|
syntax val is_nil "%1 = []"
|
|
end
|
|
|
|
module list.Length
|
|
syntax val length "List.length %1"
|
|
end
|
|
|
|
module Ref
|
|
syntax type ref "%1 ref"
|
|
syntax val contents "!%1"
|
|
syntax val ref "ref %1"
|
|
end
|
|
|
|
module ref.Ref
|
|
syntax val (!_) "!%1"
|
|
syntax val (:=) "%1 := %2"
|
|
end
|
|
|
|
module ref.Refint
|
|
syntax val incr "%1 := !%1 + 1"
|
|
syntax val decr "%1 := !%1 - 1"
|
|
syntax val (+=) "%1 := !%1 + %2"
|
|
syntax val (-=) "%1 := !%1 - %2"
|
|
syntax val ( *= ) "%1 := !%1 * %2"
|
|
end
|
|
|
|
module int.Int
|
|
syntax val zero "0"
|
|
syntax val one "1"
|
|
|
|
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 * %2"
|
|
syntax val (-_) "~%1"
|
|
end
|
|
|
|
module int.EuclideanDivision
|
|
syntax val div "%1 div %2"
|
|
syntax val mod "%1 mod %2"
|
|
end
|
|
|
|
(* not implemented in CakeML *)
|
|
(* module int.ComputerDivision *)
|
|
(* syntax val div "quot (%1, %2)" *)
|
|
(* syntax val mod "%1 rem %2" *)
|
|
(* end *)
|
|
|
|
module array.Array
|
|
syntax type array "%1 array"
|
|
|
|
(* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)
|
|
|
|
syntax val ([]) "Array.sub %1 %2"
|
|
syntax val ([]<-) "Array.update %1 %2 %3"
|
|
syntax val length "Array.length %1"
|
|
syntax val defensive_get "Array.sub %1 %2"
|
|
syntax val defensive_set "Array.update %1 %2 %3"
|
|
syntax val make "Array.array %1 %2"
|
|
syntax val empty "Array.arrayEmpty %1"
|
|
(* 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 mach.int.Int *)
|
|
(* syntax val ( / ) "Z.div %1 %2" *)
|
|
(* syntax val ( % ) "Z.rem %1 %2" *)
|
|
(* end *)
|