Commit b78a1e58 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

- unify the syntax of infix/prefix symbols in WhyML and Why

- accept predicate symbols as functions to bool in programs
- get rid of *_bool comparisons in theories/programs.why
parent 38fd9d22
......@@ -233,16 +233,17 @@ let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)
let specialize_lsymbol p uc =
let s = find_lsymbol p uc in
s, specialize_lsymbol ~loc:(qloc p) s
let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
s,tl,ty
let specialize_fsymbol p uc =
let s, (tl, ty) = specialize_lsymbol p uc in
let s,tl,ty = specialize_lsymbol p uc in
match ty with
| None -> let loc = qloc p in error ~loc TermExpected
| Some ty -> s, tl, ty
let specialize_psymbol p uc =
let s, (tl, ty) = specialize_lsymbol p uc in
let s,tl,ty = specialize_lsymbol p uc in
match ty with
| None -> s, tl
| Some _ -> let loc = qloc p in error ~loc PredicateExpected
......
......@@ -40,6 +40,9 @@ val close_theory : theory Mnm.t -> Ptree.ident -> theory_uc -> theory Mnm.t
(** The following is exported for program typing (src/programs/pgm_typing.ml) *)
(******************************************************************************)
val specialize_lsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty option
val specialize_fsymbol :
Ptree.qualid -> theory_uc -> lsymbol * Denv.dty list * Denv.dty
......
......@@ -113,6 +113,16 @@ let int_literal =
decimal_literal | hex_literal | oct_literal | bin_literal
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
rule token = parse
| "#" space* ("\"" ([^ '\010' '\013' '"' ]* as file) "\"")?
space* (digit+ as line) space* (digit+ as char) space* "#"
......@@ -152,8 +162,6 @@ rule token = parse
{ COLON }
| ";"
{ SEMICOLON }
| "!"
{ BANG }
| ":="
{ COLONEQUAL }
| "->"
......@@ -161,19 +169,7 @@ rule token = parse
| "="
{ EQUAL }
| "<>"
{ OP0 "ne" }
| "<"
{ OP0 "lt" }
| "<="
{ OP0 "le" }
| ">"
{ OP0 "gt" }
| ">="
{ OP0 "ge" }
| "+" | "-" as c
{ OP2 (String.make 1 c) }
| "*" | "/" | "%" as c
{ OP3 (String.make 1 c) }
{ LTGT }
| "@"
{ AT }
| "."
......@@ -199,6 +195,16 @@ rule token = parse
{ BARBAR }
| "&&"
{ AMPAMP }
| op_char_pref op_char_4* as s
{ OPPREF s }
| op_char_1234* op_char_1 op_char_1234* as s
{ OP1 s }
| op_char_234* op_char_2 op_char_234* as s
{ OP2 s }
| op_char_34* op_char_3 op_char_34* as s
{ OP3 s }
| op_char_4+ as s
{ OP4 s }
| "\""
{ STRING (string lexbuf) }
| eof
......
......@@ -98,7 +98,7 @@
%token <string> LIDENT UIDENT
%token <string> INTEGER
%token <string> OP0 OP1 OP2 OP3
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Why.Ptree.real_constant> REAL
%token <string> STRING
%token <Lexing.position * string> LOGIC
......@@ -114,7 +114,7 @@
/* symbols */
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON
%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ BANG
%token COLONEQUAL ARROW EQUAL LTGT AT DOT LEFTSQ RIGHTSQ
%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP
%token EOF
......@@ -144,10 +144,10 @@
%right BARBAR
%right AMPAMP
%right prec_if
%left EQUAL OP0
%left OP1
%left EQUAL LTGT OP1
%left OP2
%left OP3
%left OP4
%nonassoc prefix_op
%right unary_op
%left prec_app
......@@ -225,9 +225,10 @@ ident:
;
any_op:
| OP0 { $1 }
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| OP4 { $1 }
;
qualid:
......@@ -248,16 +249,19 @@ uqualid:
expr:
| simple_expr %prec prec_simple
{ $1 }
| expr EQUAL expr
{ mk_binop $1 "eq_bool" $3 }
| expr OP0 expr
{ mk_binop $1 ($2 ^ "_bool") $3 }
| expr EQUAL expr
{ mk_infix $1 "=" $3 }
| expr LTGT expr
{ let t = mk_infix $1 "=" $3 in
mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [t]) }
| expr OP1 expr
{ mk_infix $1 $2 $3 }
| expr OP2 expr
{ mk_infix $1 $2 $3 }
| expr OP3 expr
{ mk_infix $1 $2 $3 }
| expr OP4 expr
{ mk_infix $1 $2 $3 }
| NOT expr %prec prefix_op
{ mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [$2]) }
| any_op expr %prec prefix_op
......@@ -328,8 +332,6 @@ triple:
simple_expr:
| constant
{ mk_expr (Econstant $1) }
| BANG simple_expr
{ mk_prefix "!" $2 }
| qualid
{ mk_expr (Eident $1) }
| LEFTPAR expr RIGHTPAR
......@@ -340,6 +342,8 @@ simple_expr:
{ mk_expr Eskip }
| BEGIN END
{ mk_expr Eskip }
| OPPREF simple_expr
{ mk_prefix $1 $2 }
;
list1_simple_expr:
......
......@@ -292,7 +292,11 @@ and dexpr_desc env loc = function
let s, tyv = specialize_global loc x env.env in
DEglobal (s, tyv), dpurify env tyv
| Pgm_ptree.Eident p ->
let s, tyl, ty = Typing.specialize_fsymbol p env.env.uc in
let s,tyl,ty = Typing.specialize_lsymbol p env.env.uc in
let ty = match ty with
| Some ty -> ty
| None -> dty_bool env.env
in
DElogic s, dcurrying env.env tyl ty
| Pgm_ptree.Eapply (e1, e2) ->
let e1 = dexpr env e1 in
......@@ -536,6 +540,10 @@ and binder gl env (x, tyv) =
let mk_iexpr loc ty d = { iexpr_desc = d; iexpr_loc = loc; iexpr_type = ty }
let mk_t_if gl f =
let ty = ty_app gl.ts_bool [] in
t_if f (t_app gl.ls_True [] ty) (t_app gl.ls_False [] ty)
(* apply ls to a list of expressions, introducing let's if necessary
ls [e1; e2; ...; en]
......@@ -546,10 +554,13 @@ let mk_iexpr loc ty d = { iexpr_desc = d; iexpr_loc = loc; iexpr_type = ty }
let xn = en in
ls(x1,x2,...,xn)
*)
let make_logic_app loc ty ls el =
let make_logic_app gl loc ty ls el =
let rec make args = function
| [] ->
IElogic (t_app ls (List.rev args) ty)
| [] ->
begin match ls.ls_value with
| Some _ -> IElogic (t_app ls (List.rev args) ty)
| None -> IElogic (mk_t_if gl (f_app ls (List.rev args)))
end
| ({ iexpr_desc = IElogic t }, _) :: r ->
make (t :: args) r
| ({ iexpr_desc = IElocal (vs, _) }, _) :: r ->
......@@ -613,10 +624,12 @@ and iexpr_desc gl env loc ty = function
| DEglobal (ls, tyv) ->
IEglobal (ls, type_v gl env tyv)
| DElogic ls ->
begin match ls.ls_args with
| [] ->
begin match ls.ls_args, ls.ls_value with
| [], Some _ ->
IElogic (t_app ls [] ty)
| al ->
| [], None ->
IElogic (mk_t_if gl (f_app ls []))
| al, _ ->
errorm ~loc "function symbol %s is expecting %d arguments"
ls.ls_name.id_string (List.length al)
end
......@@ -628,7 +641,7 @@ and iexpr_desc gl env loc ty = function
if List.length args <> n then
errorm ~loc "function symbol %s is expecting %d arguments"
ls.ls_name.id_string n;
make_logic_app loc ty ls args
make_logic_app gl loc ty ls args
| _ ->
let f = iexpr gl env f in
(make_app gl loc ty f args).iexpr_desc
......
......@@ -3,20 +3,6 @@ theory Prelude
use export int.Int
use export bool.Bool
logic eq_bool 'a 'a : bool
logic ne_bool 'a 'a : bool
logic le_bool 'a 'a : bool
logic lt_bool 'a 'a : bool
logic ge_bool 'a 'a : bool
logic gt_bool 'a 'a : bool
axiom Eq_bool_def : forall x y:'a. eq_bool x y = True <-> x= y
axiom Ne_bool_def : forall x y:'a. ne_bool x y = True <-> x<>y
axiom Le_bool_def : forall x y:int. le_bool x y = True <-> x<=y
axiom Lt_bool_def : forall x y:int. lt_bool x y = True <-> x< y
axiom Ge_bool_def : forall x y:int. ge_bool x y = True <-> x>=y
axiom Gt_bool_def : forall x y:int. gt_bool x y = True <-> x> y
type unit = ()
logic ignore 'a : unit
......
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