Commit 3912a062 authored by Andrei Paskevich's avatar Andrei Paskevich

Parser: chained equivalence

Translate a chain of equivalences A <-> B <-> C into a conjunction
(A <-> B) /\ (B <-> C). Implication is weaker than equivalence when
it occurs to the left of it, and is forbidden at the right hand side.
In other words, A -> B <-> C <-> D is allowed and translated into
A -> ((B <-> C) /\ (C <-> D)), and A <-> B -> C is not allowed,
and requires explicit parentheses.
parent c67b99bd
......@@ -461,9 +461,11 @@ term: t = mk_term(term_) { t }
term_:
| term_arg_
{ match $1 with (* break the infix relation chain *)
| Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
| Tinfix (l,o,r) -> Tinnfix (l,o,r)
| Tbinop (l,o,r) -> Tbinnop (l,o,r)
| d -> d }
| NOT term
{ Tunop (Tnot, $2) }
{ Tnot $2 }
| OLD term
{ Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
| term AT uident
......@@ -506,7 +508,7 @@ term_:
| quant comma_list1(quant_vars) triggers DOT term
{ Tquant ($1, List.concat $2, $3, $5) }
| FUN binders ARROW term
{ Tquant (Tlambda, $2, [], $4) }
{ Tquant (Dterm.DTlambda, $2, [], $4) }
| EPSILON
{ Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
......@@ -515,7 +517,7 @@ term_:
{ Tcast ($1, $2) }
lam_defn:
| binders EQUAL term { Tquant (Tlambda, $1, [], $3) }
| binders EQUAL term { Tquant (Dterm.DTlambda, $1, [], $3) }
term_arg: mk_term(term_arg_) { $1 }
term_dot: mk_term(term_dot_) { $1 }
......@@ -565,16 +567,16 @@ triggers:
| LEFTSQ separated_nonempty_list(BAR,comma_list1(term)) RIGHTSQ { $2 }
%inline bin_op:
| ARROW { Timplies }
| LRARROW { Tiff }
| OR { Tor }
| BARBAR { Tor_asym }
| AND { Tand }
| AMPAMP { Tand_asym }
| ARROW { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR { Dterm.DTor }
| BARBAR { Dterm.DTor_asym }
| AND { Dterm.DTand }
| AMPAMP { Dterm.DTand_asym }
quant:
| FORALL { Tforall }
| EXISTS { Texists }
| FORALL { Dterm.DTforall }
| EXISTS { Dterm.DTexists }
numeral:
| INTEGER { Number.ConstInt $1 }
......
......@@ -23,15 +23,6 @@ type label =
| Lstr of Ident.label
| Lpos of Loc.position
type quant =
| Tforall | Texists | Tlambda
type binop =
| Tand | Tand_asym | Tor | Tor_asym | Timplies | Tiff
type unop =
| Tnot
type ident = {
id_str : string;
id_lab : label list;
......@@ -83,10 +74,11 @@ and term_desc =
| Tapply of term * term
| Tinfix of term * ident * term
| Tinnfix of term * ident * term
| Tbinop of term * binop * term
| Tunop of unop * term
| Tbinop of term * Dterm.dbinop * term
| Tbinnop of term * Dterm.dbinop * term
| Tnot of term
| Tif of term * term * term
| Tquant of quant * binder list * term list list * term
| Tquant of Dterm.dquant * binder list * term list list * term
| Tnamed of label * term
| Tlet of ident * term * term
| Tmatch of term * (pattern * term) list
......
......@@ -309,18 +309,27 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
DTtrue
| Ptree.Tfalse ->
DTfalse
| Ptree.Tunop (Ptree.Tnot, e1) ->
| Ptree.Tnot e1 ->
DTnot (dterm tuc gvars at denv e1)
| Ptree.Tbinop (e1, op, e2) ->
| Ptree.Tbinop (e1, Dterm.DTiff, e23)
| Ptree.Tbinnop (e1, Dterm.DTiff, e23) ->
let rec chain loc de1 = function
| { term_desc = Ptree.Tbinop (e2, DTiff, e3); term_loc = loc23 } ->
let de2 = dterm tuc gvars at denv e2 in
let loc12 = loc_cutoff loc loc23 e2.term_loc in
let de12 = Dterm.dterm ~loc:loc12 (DTbinop (DTiff, de1, de2)) in
let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 e3) in
DTbinop (DTand, de12, de23)
| { term_desc = Ptree.Tbinop (_, DTimplies, _); term_loc = loc23 } ->
Loc.errorm ~loc:loc23 "An unparenthesized implication cannot be \
placed at the right hand side of an equivalence"
| e23 ->
DTbinop (DTiff, de1, (dterm tuc gvars at denv e23)) in
chain loc (dterm tuc gvars at denv e1) e23
| Ptree.Tbinop (e1, op, e2)
| Ptree.Tbinnop (e1, op, e2) ->
let e1 = dterm tuc gvars at denv e1 in
let e2 = dterm tuc gvars at denv e2 in
let op = match op with
| Ptree.Tand -> DTand
| Ptree.Tand_asym -> DTand_asym
| Ptree.Tor -> DTor
| Ptree.Tor_asym -> DTor_asym
| Ptree.Timplies -> DTimplies
| Ptree.Tiff -> DTiff in
DTbinop (op, e1, e2)
| Ptree.Tquant (q, uqu, trl, e1) ->
let qvl = List.map (quant_var tuc) uqu in
......@@ -328,10 +337,6 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
let dterm e = dterm tuc gvars at denv e in
let trl = List.map (List.map dterm) trl in
let e1 = dterm e1 in
let q = match q with
| Ptree.Tforall -> DTforall
| Ptree.Texists -> DTexists
| Ptree.Tlambda -> DTlambda in
DTquant (q, qvl, trl, e1)
| Ptree.Trecord fl ->
let get_val cs pj = function
......
  • This change could have been added to CHANGES for 1.0.0 . Because before (A <-> B <-> C) was parsed as (A <-> (B <-> C)). @paskevyc @melquion

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