Skip to content

GitLab

why3
why3
Commit e68cdad5 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

prefix et infix (cf prelude.why)

parent ca60211b
Hide whitespace changes
Inline Side-by-side
Showing with 102 additions and 77 deletions
lib/prelude/prelude.why
View file @ e68cdad5
......@@ -3,58 +3,58 @@
theory Int
logic (<) (int, int)
logic (<=)(int, int)
logic (>) (int, int)
logic (>=)(int, int)
logic (_< _) (int, int)
logic (_<=_)(int, int)
logic (_> _) (int, int)
logic (_>=_)(int, int)
logic (+) (int, int) : int
logic (-) (int, int) : int
logic (*) (int, int) : int
logic (/) (int, int) : int
logic (%) (int, int) : int
logic (_+_) (int, int) : int
logic (_-_) (int, int) : int
logic (_*_) (int, int) : int
logic (_/_) (int, int) : int
logic (_%_) (int, int) : int
logic neg(int) : int
logic (-_)(int) : int
(* ring structure *)
axiom Add_assoc: forall x,y,z:int. x+(y+z) = (x+y)+z
axiom Add_comm: forall x,y:int. x+y = y+x
axiom Zero_neutral: forall x:int. x+0 = x
axiom Neg: forall x:int. x+neg(x) = 0
axiom Mul_assoc: forall x,y,z:int. x*(y*z) = (x*y)*z
axiom Mul_distr: forall x,y,z:int. x*(y+z) = x*y + x*z
axiom Add_assoc: forall x,y,z:int. x + (y + z) = (x + y) + z
axiom Add_comm: forall x,y:int. x + y = y + x
axiom Zero_neutral: forall x:int. x + 0 = x
axiom Neg: forall x:int. x + -x = 0
axiom Mul_assoc: forall x,y,z:int. x * (y * z) = (x * y) * z
axiom Mul_distr: forall x,y,z:int. x * (y + z) = x * y + x * z
(* int is a unitary, communtative ring *)
axiom Mul_comm: forall x,y:int. x*y = y*x
axiom One_neutral: forall x:int. 1*x = x
axiom Mul_comm: forall x,y:int. x * y = y * x
axiom One_neutral: forall x:int. 1 * x = x
end
theory Real
logic (<) (real, real)
logic (<=)(real, real)
logic (>) (real, real)
logic (>=)(real, real)
logic (_< _) (real, real)
logic (_<=_)(real, real)
logic (_> _) (real, real)
logic (_>=_)(real, real)
logic (+) (real, real) : real
logic (-) (real, real) : real
logic (*) (real, real) : real
logic (/) (real, real) : real
logic (_+_) (real, real) : real
logic (_-_) (real, real) : real
logic (_*_) (real, real) : real
logic (_/_) (real, real) : real
logic neg(real) : real
logic (-_)(real) : real
logic inv(real) : real
(* field structure *)
axiom Add_assoc: forall x,y,z:real. x+(y+z) = (x+y)+z
axiom Add_comm: forall x,y:real. x+y = y+x
axiom Mul_comm: forall x,y:real. x*y = y*x
axiom Zero_neutral: forall x:real. x+0. = x
axiom Neg: forall x:real. x+neg(x) = 0.
axiom Mul_assoc: forall x,y,z:real. x*(y*z) = (x*y)*z
axiom Mul_distr: forall x,y,z:real. x*(y+z) = x*y + x*z
axiom One_neutral: forall x:real. 1.*x = x
axiom Inv: forall x:real. x*inv(x) = 1.
axiom Add_assoc: forall x,y,z:real. x + (y + z) = (x + y) + z
axiom Add_comm: forall x,y:real. x + y = y + x
axiom Mul_comm: forall x,y:real. x * y = y * x
axiom Zero_neutral: forall x:real. x + 0. = x
axiom Neg: forall x:real. x + -x = 0.
axiom Mul_assoc: forall x,y,z:real. x * (y * z) = (x * y) * z
axiom Mul_distr: forall x,y,z:real. x * (y + z) = x * y + x * z
axiom One_neutral: forall x:real. 1. * x = x
axiom Inv: forall x:real. x * inv(x) = 1.
end
......
src/core/term.ml
View file @ e68cdad5
......@@ -1178,11 +1178,11 @@ let f_any prT prF f =
let ps_equ =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "=") [v; v]
create_psymbol (id_fresh "infix =") [v; v]
let ps_neq =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "<>") [v; v]
create_psymbol (id_fresh "infix <>") [v; v]
(* FIXME: is it right to do so? *)
let f_app p tl =
......
src/parser/lexer.mll
View file @ e68cdad5
......@@ -174,8 +174,6 @@ rule token = parse
|(hexadigit+ as i) ("" as f))
['p' 'P'] (['-' '+']? digit+ as e)
{ FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
| "(*)"
{ LIDENT "*" }
| "(*"
{ comment lexbuf; token lexbuf }
| "'"
......@@ -201,13 +199,11 @@ rule token = parse
| "="
{ EQUAL }
| "<>" | "<" | "<=" | ">" | ">=" as s
{ INFIXOP0 s }
| "+"
{ INFIXOP2 "+" }
| "-"
{ MINUS }
{ OP0 s }
| "+" | "-" as c
{ OP2 (String.make 1 c) }
| "*" | "/" | "%" as c
{ INFIXOP3 (String.make 1 c) }
{ OP3 (String.make 1 c) }
| "@"
{ AT }
| "."
......
src/parser/parser.mly
View file @ e68cdad5
......@@ -36,6 +36,10 @@
let prefix_ppl loc p a = mk_ppl loc (PPprefix (p, a))
let prefix_pp p a = prefix_ppl (loc ()) p a
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
let postfix s = "postfix " ^ s
(***
let with_loc loc d = { pdesc = d; ploc = loc }
let locate d = with_loc (loc ()) d
......@@ -92,7 +96,7 @@
%token <string> LIDENT UIDENT
%token <string> INTEGER
%token <string> INFIXOP0 INFIXOP2 INFIXOP3
%token <string> OP0 OP1 OP2 OP3
%token <Ptree.real_constant> FLOAT
%token <string> STRING
%token ABSURD AMPAMP AND ARRAY ARROW AS ASSERT AT AXIOM
......@@ -103,12 +107,12 @@
%token FUN FUNCTION GOAL
%token IF IMPORT IN INCLUDE INDUCTIVE INVARIANT
%token LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA
%token LET LOGIC LRARROW MATCH MINUS
%token LET LOGIC LRARROW MATCH
%token NAMESPACE NOT OF OR PARAMETER PREDICATE PROP
%token QUOTE RAISE RAISES READS REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ
%token SEMICOLON SLASH
%token THEN THEORY TIMES TRUE TRY TYPE UNDERSCORE
%token SEMICOLON
%token THEN THEORY TRUE TRY TYPE UNDERSCORE
%token UNIT USE VARIANT VOID WHILE WITH WRITES
/* Precedences */
......@@ -136,10 +140,11 @@
%right AND AMPAMP
%right NOT
%right prec_if
%left EQUAL INFIXOP0
%left INFIXOP2 MINUS
%left INFIXOP3
%right uminus
%left EQUAL OP0
%left OP1
%left OP2
%left OP3
%right unary_op
%left prec_app
%left prec_ident
%left LEFTSQ
......@@ -177,22 +182,40 @@ list0_decl:
;
ident:
| LIDENT { { id = $1; id_loc = loc () } }
| UIDENT { { id = $1; id_loc = loc () } }
| lident_string { { id = $1; id_loc = loc () } }
| UIDENT { { id = $1; id_loc = loc () } }
;
lident:
| LIDENT { { id = $1; id_loc = loc () } }
| LEFTPAR lident_infix RIGHTPAR { { id = $2; id_loc = loc () } }
| lident_string
{ { id = $1; id_loc = loc () } }
;
lident_infix:
| INFIXOP0 { $1 }
| INFIXOP2 { $1 }
| INFIXOP3 { $1 }
| EQUAL { "=" }
| MINUS { "-" }
lident_string:
| LIDENT
{ $1 }
| LEFTPAR UNDERSCORE lident_op UNDERSCORE RIGHTPAR
{ infix $3 }
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
{ prefix $2 }
/*
| LEFTPAR UNDERSCORE lident_op RIGHTPAR
{ postfix $3 }
*/
;
lident_op:
| OP0 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| EQUAL { "=" }
;
any_op:
| OP0 { $1 }
| OP2 { $1 }
| OP3 { $1 }
;
uident:
| UIDENT { { id = $1; id_loc = loc () } }
......@@ -372,22 +395,28 @@ lexpr:
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
{ let id = { id = "="; id_loc = loc_i 2 } in
{ let id = { id = infix "="; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) }
| lexpr INFIXOP0 lexpr
{ let id = { id = $2; id_loc = loc_i 2 } in
| lexpr OP0 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) }
| lexpr MINUS lexpr
{ let id = { id = "-"; id_loc = loc_i 2 } in
| lexpr OP1 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) }
| lexpr INFIXOP2 lexpr
{ let id = { id = $2; id_loc = loc_i 2 } in
| lexpr OP2 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) }
| lexpr INFIXOP3 lexpr
{ let id = { id = $2; id_loc = loc_i 2 } in
| lexpr OP3 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) }
| MINUS lexpr %prec uminus
{ prefix_pp PPneg $2 }
| any_op lexpr %prec unary_op
{ let id = { id = prefix $1; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$2])) }
/*
| lexpr any_op %prec unary_op
{ let id = { id = postfix $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1])) }
*/
| qualid
{ mk_pp (PPvar $1) }
| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
......
src/parser/ptree.mli
View file @ e68cdad5
......@@ -30,7 +30,7 @@ type pp_infix =
| PPand | PPor | PPimplies | PPiff
type pp_prefix =
| PPneg | PPnot
| PPnot
type ident = { id : string; id_loc : loc }
......
src/parser/typing.ml
View file @ e68cdad5
......@@ -486,7 +486,7 @@ and dfmla env e = match e.pp_desc with
Fnamed (x, f1)
| PPvar _ ->
assert false (* TODO *)
| PPconst _ | PPprefix (PPneg, _) ->
| PPconst _ ->
error ~loc:e.pp_loc PredicateExpected
and dtype_args s loc env el tl =
......
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