new syntax 'constant ident:type [=expr]' to declare constants

note that 'function' is still allowed
parent a46349ca
* marks an incompatible change
o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
introduce constants, as an alternative to "function"
version 0.71, October 13, 2011
==============================
o [examples] a lot of new program examples in directory examples/programs
o [Why3replayer] new option -latex to output a proof session in LaTeX format
o [WhyML] significant improvement of the efficiency of the WP calculus
o [WhyIDE] better coloring and source positioning including from front-ends
o [WhyIDE] better coloring and source positioning including from front-ends
such as Krakatoa and Jessie plugin of Frama-C
o [WhyML] fixed labels and source locations in WPs
o [Session] during reload, new method for pairing old and new subgoals
......
\begin{syntax}
theory ::= "theory" uident label* decl* "end"
theory ::= "theory" uident label* decl* "end"
\
decl ::= "type" type-decl ("with" type-decl)* ;
| "constant" constant-decl ;
| "function" function-decl ("with" logic-decl)* ;
| "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
| "goal" ident ":" formula ;
| "use" imp-exp tqualid ("as" uident-opt)? ;
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "use" imp-exp tqualid ("as" uident-opt)? ;
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "namespace" "import"? uident-opt decl* "end" ;
\
type-decl ::= lident label* ("'" lident label*)* type-defn;
......@@ -26,6 +27,9 @@
logic-decl ::= function-decl ;
| predicate-decl
\
constant-decl ::= lident label* ":" type ;
| lident label* ":" type "=" term
\
function-decl ::= lident label* type-param* ":" type ;
| lident label* type-param* ":" type "=" term
\
......
......@@ -13,8 +13,8 @@ module M
[0 <= y2 <= x2]. The seven other cases can be easily
deduced by symmetry. *)
function x2: int
function y2: int
constant x2: int
constant y2: int
axiom first_octant: 0 <= y2 <= x2
(* The code.
......
......@@ -25,7 +25,7 @@ module M
type vertex
function v : S.set vertex
constant v : S.set vertex
function g_succ(vertex) : S.set vertex
......
......@@ -49,7 +49,7 @@ theory Mat22 "2x2 integer matrices"
type t = {| a11: int; a12: int; a21: int; a22: int |}
function id : t = {| a11 = 1; a12 = 0; a21 = 0; a22 = 1 |}
constant id : t = {| a11 = 1; a12 = 0; a21 = 0; a22 = 1 |}
function mult (x: t) (y: t) : t =
{|
......@@ -71,7 +71,7 @@ module FibonacciLogarithmic
use import int.EuclideanDivision
use import Mat22
function m1110 : t = {| a11 = 1; a12 = 1;
constant m1110 : t = {| a11 = 1; a12 = 1;
a21 = 1; a22 = 0 |}
(* computes ((1 1) (1 0))^n in O(log(n)) time
......
......@@ -12,8 +12,8 @@ module FIND
use import module array.Array
use import module array.ArrayPermut
function _N: int (* actually N in Hoare's notation *)
function f: int
constant _N: int (* actually N in Hoare's notation *)
constant f: int
axiom f_N_range: 1 <= f <= _N
......
......@@ -8,7 +8,7 @@ module M
(** Memory model and definition of is_list *)
type pointer
type next = map pointer pointer
function null : pointer
constant null : pointer
val value : ref (map pointer int)
val next : ref (next)
......@@ -191,7 +191,7 @@ module M2
axiom pointer_dec : forall p1:pointer, p2 : pointer. p1 = p2 \/ p1 <> p2
type next = map pointer pointer
function null : pointer
constant null : pointer
val value : ref (map pointer int)
val next : ref (next)
......
......@@ -23,7 +23,7 @@ theory Bitset "sets of small integers"
use import int.Int
function size : int (* elements belong to 0..size-1 *)
constant size : int (* elements belong to 0..size-1 *)
type set
......@@ -172,13 +172,13 @@ module MaxMatrixMemo
use import map.Map
use import module ref.Ref
function n : int
constant n : int
axiom n_nonneg: 0 <= n
use import Bitset
axiom integer_size: n <= size
function m : map int (map int int)
constant m : map int (map int int)
axiom m_pos: forall i j: int. 0 <= i < n -> 0 <= j < n -> 0 <= m[i][j]
predicate solution (s: map int int) (i: int) =
......
......@@ -65,14 +65,14 @@ module M
val x : array int
(* the number of digits of X *)
function n : int
constant n : int
(* the target digit sum *)
function y : int
constant y : int
axiom Hypotheses: n >= 0 /\ y > 0
function m : int = 1 + max n (div y 9)
constant m : int = 1 + max n (div y 9)
exception Success
......
......@@ -49,7 +49,7 @@ theory Solution
use export map.Map
(* the number of queens *)
function n : int
constant n : int
type solution = map int int
......
......@@ -12,7 +12,7 @@ module TortoiseAndHare
function f t : t
(* given some initial value x0 *)
function x0: t
constant x0: t
(* we can build the infinite sequence defined by x{i+1} = f(xi) *)
clone import int.Iter with type t = t, function f = f
......@@ -27,8 +27,8 @@ module TortoiseAndHare
(2) x{n+lambda} = x_n when n >= mu. *)
(* lambda and mu are skomlemized *)
function mu : int
function lambda : int
constant mu : int
constant lambda : int
(* they are axiomatized as follows *)
axiom mu_range: 0 <= mu
......
......@@ -17,10 +17,10 @@ theory GilbreathCardTrick
use export list.Reverse
use import list.Nth
function m: int
constant m: int
axiom m_positive: 0 < m
function n: int
constant n: int
axiom n_nonnegative: 0 <= n
(* c is a riffle shuffle of a and b *)
......
......@@ -40,7 +40,7 @@ back +-+-+-+-------------------+
(* invariant *)
function maxlen : int = 1000
constant maxlen : int = 1000
function length (a: sparse_array 'a) : int = A.length a.values
......@@ -109,10 +109,10 @@ module Harness
use import module SparseArray
type elt
function def : elt
constant def : elt
function c1 : elt
function c2 : elt
constant c1 : elt
constant c2 : elt
let harness () =
let a = create 10 def in
......
......@@ -11,7 +11,7 @@ module M
use import module ref.Ref
use import module array.Array
function n : int
constant n : int
axiom N_non_negative : n >= 0
let hull (a: array int) (b: array int) =
......
......@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
......
......@@ -149,6 +149,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>end</keyword>
<keyword>exception</keyword>
<keyword>export</keyword>
<keyword>constant</keyword>
<keyword>function</keyword>
<keyword>goal</keyword>
<keyword>import</keyword>
......
......@@ -31,7 +31,7 @@ let debug_print_labels = Debug.register_flag "print_labels"
let debug_print_locs = Debug.register_flag "print_locs"
let iprinter,aprinter,tprinter,pprinter =
let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
"axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
"namespace"; "import"; "export"; "end";
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
......@@ -329,7 +329,9 @@ let print_type_decl first fmt d =
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
let ls_kind ls = if ls.ls_value = None then "predicate" else "function"
let ls_kind ls =
if ls.ls_value = None then "predicate"
else if ls.ls_args = [] then "constant" else "function"
let print_logic_decl fst fmt (ls,ld) = match ld with
| Some ld ->
......
......@@ -44,6 +44,7 @@
"as", AS;
"axiom", AXIOM;
"clone", CLONE;
"constant", CONSTANT;
"else", ELSE;
"end", END;
"epsilon", EPSILON;
......
......@@ -194,7 +194,7 @@ end
/* keywords */
%token AS AXIOM CLONE
%token AS AXIOM CLONE CONSTANT
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
......@@ -320,6 +320,8 @@ namespace_name:
decl:
| TYPE list1_type_decl
{ TypeDecl $2 }
| CONSTANT logic_decl_constant
{ LogicDecl [$2] }
| FUNCTION list1_logic_decl_function
{ LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
......@@ -370,6 +372,7 @@ list1_comma_subst:
subst:
| NAMESPACE ns EQUAL ns { CSns ($2, $4) }
| TYPE qualid EQUAL qualid { CStsym ($2, $4) }
| CONSTANT qualid EQUAL qualid { CSfsym ($2, $4) }
| FUNCTION qualid EQUAL qualid { CSfsym ($2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2, $4) }
| LEMMA qualid { CSlemma $2 }
......@@ -469,6 +472,12 @@ list1_logic_decl:
| logic_decl WITH list1_logic_decl { $1 :: $3 }
;
logic_decl_constant:
| lident_rich labels COLON primitive_type logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = []; ld_type = Some $4; ld_def = $5 } }
;
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
......
theory TestConstant
constant a : int
constant b : int
constant c : int
function f : int
function g : int
predicate p
goal G: a=0 && p
end
theory TestCoq
use import list.List
use import list.Append
......@@ -31,8 +45,8 @@ theory Order
end
(*
Local Variables:
Local Variables:
compile-command: "make -C .. tests/test-jcf.gui"
End:
End:
*)
......@@ -22,7 +22,7 @@ end
theory Group
type t
function unit : t
constant unit : t
function op t t : t
function inv t : t
......@@ -47,13 +47,13 @@ end
theory Ring
type t
function zero : t
constant zero : t
function (+) t t : t
function (-_) t : t
function (*) t t : t
clone CommutativeGroup with type t = t,
function unit = zero,
constant unit = zero,
function op = (+),
function inv = (-_)
......@@ -72,7 +72,7 @@ end
theory UnitaryCommutativeRing
clone export CommutativeRing
function one : t
constant one : t
axiom Unitary : forall x:t. one * x = x
axiom NonTrivialRing : zero <> one
end
......
......@@ -4,7 +4,7 @@ theory Abs
type t
predicate ge t t
function neg t : t
function zero : t
constant zero : t
function abs t : t
......
......@@ -44,7 +44,7 @@ theory GenFloat
function round_error (x : t) : real = abs (value x - exact x)
function total_error (x : t) : real = abs (value x - model x)
function max : real
constant max : real
predicate no_overflow (m:mode) (x:real) = abs (round m x) <= max
......@@ -63,7 +63,7 @@ theory GenFloat
axiom Bounded_value :
forall x:t. abs (value x) <= max
function max_representable_integer : int
constant max_representable_integer : int
axiom Exact_rounding_for_integers:
forall m:mode,i:int.
......@@ -87,13 +87,13 @@ theory Single
type single
function max_single : real = 0x1.FFFFFEp127
function max_int : int = 16777216 (* 2^24 *)
constant max_single : real = 0x1.FFFFFEp127
constant max_int : int = 16777216 (* 2^24 *)
clone export GenFloat with
type t = single,
function max = max_single,
function max_representable_integer = max_int
constant max = max_single,
constant max_representable_integer = max_int
end
......@@ -103,13 +103,13 @@ theory Double
type double
function max_double : real = 0x1.FFFFFFFFFFFFFp1023
function max_int : int = 9007199254740992 (* 2^53 *)
constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
constant max_int : int = 9007199254740992 (* 2^53 *)
clone export GenFloat with
type t = double,
function max = max_double,
function max_representable_integer = max_int
constant max = max_double,
constant max_representable_integer = max_int
end
......@@ -188,13 +188,13 @@ theory SingleFull
type single
function max_single : real = 0x1.FFFFFEp127
function max_int : int = 16777216 (* 2^24 *)
constant max_single : real = 0x1.FFFFFEp127
constant max_int : int = 16777216 (* 2^24 *)
clone export GenFloatFull with
type t = single,
function max = max_single,
function max_representable_integer = max_int
constant max = max_single,
constant max_representable_integer = max_int
end
......@@ -204,12 +204,12 @@ theory DoubleFull
type double
function max_double : real = 0x1.FFFFFFFFFFFFFp1023
function max_int : int = 9007199254740992 (* 2^23 *)
constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
constant max_int : int = 9007199254740992 (* 2^23 *)
clone export GenFloatFull with
type t = double,
function max = max_double,
function max_representable_integer = max_int
constant max = max_double,
constant max_representable_integer = max_int
end
theory Int
function zero : int = 0
function one : int = 1
constant zero : int = 0
constant one : int = 1
predicate (< ) int int
predicate (> ) (x y : int) = y < x
predicate (<=) (x y : int) = x < y \/ x = y
clone export algebra.OrderedUnitaryCommutativeRing with type t = int,
function zero = zero, function one = one, predicate (<=) = (<=)
constant zero = zero, constant one = one, predicate (<=) = (<=)
end
......@@ -136,7 +136,7 @@ theory Exponentiation
use import Int
type t
function one : t
constant one : t
function (*) t t : t
function power t int : t
......@@ -160,7 +160,7 @@ theory Power
use import Int
clone export
Exponentiation with type t = int, function one = one, function (*) = (*)
Exponentiation with type t = int, constant one = one, function (*) = (*)
end
......@@ -288,7 +288,7 @@ theory Induction
(forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
forall n:int. 0 <= n -> p n
function bound : int
constant bound : int
lemma Induction_bound :
(forall n:int. bound <= n ->
......
......@@ -134,17 +134,17 @@ theory BitVector
use export bool.Bool
use import int.Int
function size : int
constant size : int
type bv
function nth bv int: bool
function bvzero : bv
constant bvzero : bv
axiom Nth_zero:
forall n:int. 0 <= n < size -> nth bvzero n = False
function bvone : bv
constant bvone : bv
axiom Nth_one:
forall n:int. 0 <= n < size -> nth bvone n = True
......@@ -188,9 +188,9 @@ end
theory BV32
function size : int = 32
constant size : int = 32
clone export BitVector with function size = size
clone export BitVector with constant size = size
end
......
theory Real
function zero : real = 0.0
function one : real = 1.0
constant zero : real = 0.0
constant one : real = 1.0
predicate (< ) real real
predicate (> ) (x y : real) = y < x
predicate (<=) (x y : real) = x < y \/ x = y
clone export algebra.OrderedField with type t = real,
function zero = zero, function one = one, predicate (<=) = (<=)
constant zero = zero, constant one = one, predicate (<=) = (<=)
(*
lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
......@@ -195,7 +195,7 @@ theory ExpLog
axiom Exp_zero : exp(0.0) = 1.0
axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
function e : real = exp 1.0
constant e : real = exp 1.0
function log real : real
axiom Log_one : log 1.0 = 0.0
......@@ -282,7 +282,7 @@ theory Trigonometry
axiom Cos_0: cos 0.0 = 1.0
axiom Sin_0: sin 0.0 = 0.0
function pi : real
constant pi : real
axiom Pi_interval:
3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
......
......@@ -19,7 +19,7 @@ theory Set
forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3
(* empty set *)
function empty : set 'a
constant empty : set 'a
predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)
......@@ -144,7 +144,7 @@ theory SetMap
predicate mem (x:'a) (s:set 'a) = s[x] = True
function empty : set 'a = const False
constant empty : set 'a = const False
predicate is_empty (s : set 'a) = forall x : 'a. not (mem x s)
......
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