Commit 8c0e2f70 authored by Andrei Paskevich's avatar Andrei Paskevich

fix the syntax of quantifiers

parent 4cd5a72c
......@@ -134,7 +134,7 @@
%right prec_named
%left COLONEQUAL
%right prec_forall prec_exists
%right prec_quant
%right ARROW LRARROW
%right OR BARBAR
%right AND AMPAMP
......@@ -423,17 +423,10 @@ lexpr:
{ mk_pp (PPapp ($1, $3)) }
| IF lexpr THEN lexpr ELSE lexpr %prec prec_if
{ mk_pp (PPif ($2, $4, $6)) }
| FORALL list1_lident_sep_comma COLON primitive_type triggers DOT lexpr
%prec prec_forall
{ mk_pp (PPforall ($2, $4, $5, $7))
(*let rec mk = function
| [] -> assert false
| [id] -> mk_pp (PPforall (id, $4, $5, $7))
| id :: l -> mk_pp (PPforall (id, $4, [], mk l))
in
mk $2 *) }
| EXISTS lident COLON primitive_type DOT lexpr %prec prec_exists
{ mk_pp (PPexists ($2, $4, $6)) }
| FORALL list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant
{ mk_pp (PPquant (PPforall, $2, $3, $5)) }
| EXISTS list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant
{ mk_pp (PPquant (PPexists, $2, $3, $5)) }
| INTEGER
{ mk_pp (PPconst (Term.ConstInt $1)) }
| FLOAT
......@@ -452,6 +445,13 @@ lexpr:
{ mk_pp (PPmatch ($2, $5)) }
;
list1_uquant_sep_comma:
| uquant { [$1] }
| uquant COMMA list1_uquant_sep_comma { $1::$3 }
uquant:
| list1_lident_sep_comma COLON primitive_type { $1,$3 }
match_cases:
| match_case { [$1] }
| match_case BAR match_cases { $1::$3 }
......
......@@ -26,6 +26,9 @@ type loc = Loc.position
type real_constant = Term.real_constant
type constant = Term.constant
type pp_quant =
| PPforall | PPexists
type pp_infix =
| PPand | PPor | PPimplies | PPiff
......@@ -42,6 +45,9 @@ type pty =
| PPTtyvar of ident
| PPTtyapp of pty list * qualid
type uquant =
ident list * pty
type lexpr =
{ pp_loc : loc; pp_desc : pp_desc }
......@@ -54,10 +60,9 @@ and pp_desc =
| PPinfix of lexpr * pp_infix * lexpr
| PPprefix of pp_prefix * lexpr
| PPif of lexpr * lexpr * lexpr
| PPforall of ident list * pty * lexpr list list * lexpr
| PPexists of ident * pty * lexpr
| PPquant of pp_quant * uquant list * lexpr list list * lexpr
| PPnamed of string * lexpr
| PPlet of ident* lexpr * lexpr
| PPlet of ident * lexpr * lexpr
| PPmatch of lexpr * ((qualid * ident list * loc) * lexpr) list
(*s Declarations. *)
......
......@@ -367,6 +367,8 @@ let rec ty_of_dty = function
(** Typing terms and formulas *)
type uquant = string list * dty
type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node =
......@@ -380,7 +382,7 @@ and dterm_node =
and dfmla =
| Fapp of lsymbol * dterm list
| Fquant of quant * string list * dty * dtrigger list list * dfmla
| Fquant of quant * uquant list * dtrigger list list * dfmla
| Fbinop of binop * dfmla * dfmla
| Fnot of dfmla
| Ftrue
......@@ -441,7 +443,7 @@ and dterm_node loc env = function
| PPnamed (x, e1) ->
let e1 = dterm env e1 in
Tnamed (x, e1), e1.dt_ty
| PPexists _ | PPforall _ | PPif _
| PPquant _ | PPif _
| PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
error ~loc TermExpected
......@@ -456,13 +458,17 @@ and dfmla env e = match e.pp_desc with
Fbinop (binop op, dfmla env a, dfmla env b)
| PPif (a, b, c) ->
Fif (dfmla env a, dfmla env b, dfmla env c)
| PPforall (idl, ty, trl, a) ->
let ty = dty env ty in
let env, idl =
map_fold_left
(fun env {id=x} -> { env with dvars = M.add x ty env.dvars }, x)
env idl
| PPquant (q, uqu, trl, a) ->
let uquant env (idl,ty) =
let ty = dty env ty in
let env, idl =
map_fold_left
(fun env {id=x} -> { env with dvars = M.add x ty env.dvars }, x)
env idl
in
env, (idl,ty)
in
let env, uqu = map_fold_left uquant env uqu in
let trigger e = (* FIXME? *)
try
TRterm (dterm env e)
......@@ -470,11 +476,11 @@ and dfmla env e = match e.pp_desc with
TRfmla (dfmla env e)
in
let trl = List.map (List.map trigger) trl in
Fquant (Fforall, idl, ty, trl, dfmla env a)
| PPexists ({id=x}, ty, a) -> (* TODO: triggers? *)
let ty = dty env ty in
let env = { env with dvars = M.add x ty env.dvars } in
Fquant (Fexists, [x], ty, [], dfmla env a)
let q = match q with
| PPforall -> Fforall
| PPexists -> Fexists
in
Fquant (q, uqu, trl, dfmla env a)
| PPapp (x, tl) ->
let s = find_lsymbol x env.th in
let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
......@@ -546,16 +552,18 @@ and fmla env = function
f_binary op (fmla env f1) (fmla env f2)
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, xl, ty, trl, f1) ->
| Fquant (q, uqu, trl, f1) ->
(* TODO: shouldn't we localize this ident? *)
let ty = ty_of_dty ty in
let env, vl =
map_fold_left
(fun env x ->
let v = create_vsymbol (id_fresh x) ty in M.add x v env, v)
env xl
let uquant env (xl,ty) =
let ty = ty_of_dty ty in
map_fold_left
(fun env x ->
let v = create_vsymbol (id_fresh x) ty in M.add x v env, v)
env xl
in
f_quant q vl [] (fmla env f1)
let env, vl = map_fold_left uquant env uqu in
(* TODO: triggers *)
f_quant q (List.concat vl) [] (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, x, f2) ->
......
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