Commit c67b99bd authored by Andrei Paskevich's avatar Andrei Paskevich

Parser: relation chaining is guided by the operator group

All infix operations in the weakest priority group (those containing
at least one of the characters '=', '<', '>', or '~') are considered
non-associative and the chains (t1 OP t2 OP t3) are translated into
conjunctions (t1 OP t2 /\ t2 OP t3).

This does not concern implication '->' and equivalence '<->'
which are right-associative. like the rest of propositional
connectives.
parent 6e120719
...@@ -167,18 +167,6 @@ let reunify_regions () = ...@@ -167,18 +167,6 @@ let reunify_regions () =
Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue; Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue;
Queue.clear unify_queue Queue.clear unify_queue
(** Chainable relations *)
let rec dity_is_bool = function
| Dvar { contents = Dval dty } -> dity_is_bool dty
| Dpur (s,_) -> its_equal s its_bool
| _ -> false
let dvty_is_chainable = function
| [t1;t2],t ->
dity_is_bool t && not (dity_is_bool t1) && not (dity_is_bool t2)
| _ -> false
(** Built-in types *) (** Built-in types *)
let dity_int = Dpur (its_int, []) let dity_int = Dpur (its_int, [])
......
...@@ -25,10 +25,6 @@ val dity_of_ity : ity -> dity ...@@ -25,10 +25,6 @@ val dity_of_ity : ity -> dity
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *) type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
val dity_is_bool : dity -> bool
val dvty_is_chainable : dvty -> bool
(** Patterns *) (** Patterns *)
type dpattern = private { type dpattern = private {
......
...@@ -146,7 +146,7 @@ ...@@ -146,7 +146,7 @@
%right OR BARBAR %right OR BARBAR
%right AND AMPAMP %right AND AMPAMP
%nonassoc NOT %nonassoc NOT
%left EQUAL LTGT OP1 %right EQUAL LTGT OP1
%nonassoc AT OLD %nonassoc AT OLD
%nonassoc LARROW %nonassoc LARROW
%nonassoc RIGHTSQ (* stronger than <- for e1[e2 <- e3] *) %nonassoc RIGHTSQ (* stronger than <- for e1[e2 <- e3] *)
...@@ -472,8 +472,10 @@ term_: ...@@ -472,8 +472,10 @@ term_:
{ Tidapp (Qident $1, [$2]) } { Tidapp (Qident $1, [$2]) }
| l = term ; o = bin_op ; r = term | l = term ; o = bin_op ; r = term
{ Tbinop (l, o, r) } { Tbinop (l, o, r) }
| l = term ; o = infix_op ; r = term | l = term ; o = infix_op_1 ; r = term
{ Tinfix (l, o, r) } { Tinfix (l, o, r) }
| l = term ; o = infix_op_234 ; r = term
{ Tidapp (Qident o, [l; r]) }
| term_arg located(term_arg)+ (* FIXME/TODO: "term term_arg" *) | term_arg located(term_arg)+ (* FIXME/TODO: "term term_arg" *)
{ let join f (a,_,e) = mk_term (Tapply (f,a)) $startpos e in { let join f (a,_,e) = mk_term (Tapply (f,a)) $startpos e in
(List.fold_left join $1 $2).term_desc } (List.fold_left join $1 $2).term_desc }
...@@ -635,8 +637,10 @@ expr_: ...@@ -635,8 +637,10 @@ expr_:
{ Enot $2 } { Enot $2 }
| prefix_op expr %prec prec_prefix_op | prefix_op expr %prec prec_prefix_op
{ Eidapp (Qident $1, [$2]) } { Eidapp (Qident $1, [$2]) }
| l = expr ; o = infix_op ; r = expr | l = expr ; o = infix_op_1 ; r = expr
{ Einfix (l,o,r) } { Einfix (l,o,r) }
| l = expr ; o = infix_op_234 ; r = expr
{ Eidapp (Qident o, [l;r]) }
| expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *) | expr_arg located(expr_arg)+ (* FIXME/TODO: "expr expr_arg" *)
{ let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in { let join f (a,_,e) = mk_expr (Eapply (f,a)) $startpos e in
(List.fold_left join $1 $2).expr_desc } (List.fold_left join $1 $2).expr_desc }
...@@ -898,13 +902,15 @@ op_symbol: ...@@ -898,13 +902,15 @@ op_symbol:
prefix_op: prefix_op:
| op_symbol { mk_id (prefix $1) $startpos $endpos } | op_symbol { mk_id (prefix $1) $startpos $endpos }
%inline infix_op: %inline infix_op_1:
| o = OP1 { mk_id (infix o) $startpos $endpos } | o = OP1 { mk_id (infix o) $startpos $endpos }
| EQUAL { mk_id (infix "=") $startpos $endpos }
| LTGT { mk_id (infix "<>") $startpos $endpos }
%inline infix_op_234:
| o = OP2 { mk_id (infix o) $startpos $endpos } | o = OP2 { mk_id (infix o) $startpos $endpos }
| o = OP3 { mk_id (infix o) $startpos $endpos } | o = OP3 { mk_id (infix o) $startpos $endpos }
| o = OP4 { mk_id (infix o) $startpos $endpos } | o = OP4 { mk_id (infix o) $startpos $endpos }
| EQUAL { mk_id (infix "=") $startpos $endpos }
| LTGT { mk_id (infix "<>") $startpos $endpos }
(* Qualified idents *) (* Qualified idents *)
......
...@@ -195,6 +195,12 @@ let quant_var tuc (loc, id, gh, ty) = ...@@ -195,6 +195,12 @@ let quant_var tuc (loc, id, gh, ty) =
| None -> dty_fresh () in | None -> dty_fresh () in
Opt.map create_user_id id, ty, Some loc Opt.map create_user_id id, ty, Some loc
let loc_cutoff loc13 loc23 loc2 =
let f,l,b,e = Loc.get loc13 in
let _,_,_,w = Loc.get loc23 in
let _,_,_,m = Loc.get loc2 in
Loc.user_position f l b (e - (w - m))
let is_reusable dt = match dt.dt_node with let is_reusable dt = match dt.dt_node with
| DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
| DTapp (_,[]) -> true | DTapp (_,[]) -> true
...@@ -209,16 +215,6 @@ let mk_var n dt = ...@@ -209,16 +215,6 @@ let mk_var n dt =
let mk_let ~loc n dt node = let mk_let ~loc n dt node =
DTlet (dt, id_user n loc, Dterm.dterm ~loc node) DTlet (dt, id_user n loc, Dterm.dterm ~loc node)
let chainable_op tuc op =
(* non-bool -> non-bool -> bool *)
op.id_str = "infix =" || op.id_str = "infix <>" ||
match find_lsymbol tuc (Qident op) with
| {ls_args = [ty1;ty2]; ls_value = ty} ->
Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty
&& not (ty_equal ty1 ty_bool)
&& not (ty_equal ty2 ty_bool)
| _ -> false
let mk_closure loc ls = let mk_closure loc ls =
let mk dt = Dterm.dterm ~loc dt in let mk dt = Dterm.dterm ~loc dt in
let mk_v i _ = let mk_v i _ =
...@@ -270,31 +266,25 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = ...@@ -270,31 +266,25 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
| Ptree.Ttuple tl -> | Ptree.Ttuple tl ->
let tl = List.map (dterm tuc gvars at denv) tl in let tl = List.map (dterm tuc gvars at denv) tl in
DTapp (fs_tuple (List.length tl), tl) DTapp (fs_tuple (List.length tl), tl)
| Ptree.Tinfix (e12, op2, e3) | Ptree.Tinfix (e1, op1, e23)
| Ptree.Tinnfix (e12, op2, e3) -> | Ptree.Tinnfix (e1, op1, e23) ->
let make_app de1 op de2 = if op.id_str = "infix <>" then let apply loc de1 op de2 =
let op = { op with id_str = "infix =" } in if op.id_str = "infix <>" then
let ls = find_lsymbol tuc (Qident op) in let op = { op with id_str = "infix =" } in
DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2]))) let ls = find_lsymbol tuc (Qident op) in
else DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
DTapp (find_lsymbol tuc (Qident op), [de1;de2]) else
in DTapp (find_lsymbol tuc (Qident op), [de1;de2]) in
let rec make_chain de1 = function let rec chain loc de1 op1 = function
| [op,de2] -> | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
make_app de1 op de2 let de2 = dterm tuc gvars at denv e2 in
| (op,de2) :: ch -> let loc12 = loc_cutoff loc loc23 e2.term_loc in
let de12 = Dterm.dterm ~loc (make_app de1 op de2) in let de12 = Dterm.dterm ~loc:loc12 (apply loc12 de1 op1 de2) in
let de23 = Dterm.dterm ~loc (make_chain de2 ch) in let de23 = Dterm.dterm ~loc:loc23 (chain loc23 de2 op2 e3) in
DTbinop (DTand, de12, de23) DTbinop (DTand, de12, de23)
| [] -> assert false in | e23 ->
let rec get_chain e12 acc = match e12.term_desc with apply loc de1 op1 (dterm tuc gvars at denv e23) in
| Tinfix (e1, op1, e2) when chainable_op tuc op1 -> chain loc (dterm tuc gvars at denv e1) op1 e23
get_chain e1 ((op1, dterm tuc gvars at denv e2) :: acc)
| _ -> e12, acc in
let ch = [op2, dterm tuc gvars at denv e3] in
let e1, ch = if chainable_op tuc op2
then get_chain e12 ch else e12, ch in
make_chain (dterm tuc gvars at denv e1) ch
| Ptree.Tconst c -> | Ptree.Tconst c ->
DTconst c DTconst c
| Ptree.Tlet (x, e1, e2) -> | Ptree.Tlet (x, e1, e2) ->
...@@ -352,13 +342,13 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} = ...@@ -352,13 +342,13 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
| Ptree.Tupdate (e1, fl) -> | Ptree.Tupdate (e1, fl) ->
let e1 = dterm tuc gvars at denv e1 in let e1 = dterm tuc gvars at denv e1 in
let re = is_reusable e1 in let re = is_reusable e1 in
let v = if re then e1 else mk_var "_q " e1 in let v = if re then e1 else mk_var "q " e1 in
let get_val _ pj = function let get_val _ pj = function
| Some e -> dterm tuc gvars at denv e | Some e -> dterm tuc gvars at denv e
| None -> Dterm.dterm ~loc (DTapp (pj,[v])) in | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
let cs, fl = parse_record ~loc tuc get_val fl in let cs, fl = parse_record ~loc tuc get_val fl in
let d = DTapp (cs, fl) in let d = DTapp (cs, fl) in
if re then d else mk_let ~loc "_q " e1 d if re then d else mk_let ~loc "q " e1 d
| Ptree.Tat (e1, l) -> | Ptree.Tat (e1, l) ->
DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty) DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty)
| Ptree.Tnamed (Lpos uloc, e1) -> | Ptree.Tnamed (Lpos uloc, e1) ->
...@@ -542,10 +532,7 @@ let dbinder muc (_,id,gh,pty) = dbinder muc id gh pty ...@@ -542,10 +532,7 @@ let dbinder muc (_,id,gh,pty) = dbinder muc id gh pty
(* expressions *) (* expressions *)
let is_reusable de = match de.de_node with let is_reusable de = match de.de_node with
| DEvar _ | DEpv _ | DEconst _ | DEtrue | DEfalse -> true | DEvar _ | DEpv _ -> true | _ -> false
| DErs {rs_logic = (RLls _|RLpv _); rs_cty = cty} ->
cty.cty_args = [] && cty.cty_result.ity_pure
| _ -> false
let mk_var n de = let mk_var n de =
Dexpr.dexpr ?loc:de.de_loc (DEvar (n, de.de_dvty)) Dexpr.dexpr ?loc:de.de_loc (DEvar (n, de.de_dvty))
...@@ -554,26 +541,6 @@ let mk_let ~loc n de node = ...@@ -554,26 +541,6 @@ let mk_let ~loc n de node =
let de1 = Dexpr.dexpr ~loc node in let de1 = Dexpr.dexpr ~loc node in
DElet ((id_user n loc, false, RKnone, de), de1) DElet ((id_user n loc, false, RKnone, de), de1)
let chainable_rs = function
| {rs_cty = { cty_args = [pv1;pv2]; cty_result = ity}} ->
ity_equal ity ity_bool
&& not (ity_equal pv1.pv_ity ity_bool)
&& not (ity_equal pv2.pv_ity ity_bool)
| _ -> false
let chainable_qualid muc p = match find_prog_symbol muc p with
| RS s -> chainable_rs s
| _ -> false
let chainable_op muc denv op =
(* non-bool -> non-bool -> bool *)
op.id_str = "infix =" || op.id_str = "infix <>" ||
match denv_get_opt denv op.id_str with
| Some (DEvar (_,t)) -> dvty_is_chainable t
| Some (DErs s) -> chainable_rs s
| Some _ -> false (* can never happen *)
| None -> chainable_qualid muc (Qident op)
let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let expr_app loc e el = let expr_app loc e el =
List.fold_left (fun e1 e2 -> List.fold_left (fun e1 e2 ->
...@@ -600,34 +567,28 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = ...@@ -600,34 +567,28 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Etuple el -> | Ptree.Etuple el ->
let e = DErs (rs_tuple (List.length el)) in let e = DErs (rs_tuple (List.length el)) in
expr_app loc e (List.map (dexpr muc denv) el) expr_app loc e (List.map (dexpr muc denv) el)
| Ptree.Einfix (e12, op2, e3) | Ptree.Einfix (e1, op1, e23)
| Ptree.Einnfix (e12, op2, e3) -> | Ptree.Einnfix (e1, op1, e23) ->
let make_app de1 op de2 = if op.id_str = "infix <>" then let apply loc de1 op de2 =
let oq = Qident { op with id_str = "infix =" } in if op.id_str = "infix <>" then
let dt = qualid_app op.id_loc oq [de1; de2] in let oq = Qident { op with id_str = "infix =" } in
DEnot (Dexpr.dexpr ~loc dt) let dt = qualid_app op.id_loc oq [de1;de2] in
else DEnot (Dexpr.dexpr ~loc dt)
qualid_app op.id_loc (Qident op) [de1; de2] else
in qualid_app op.id_loc (Qident op) [de1;de2] in
let rec make_chain n1 n2 de1 = function let rec chain n1 n2 loc de1 op1 = function
| [op,de2] -> | { expr_desc = Ptree.Einfix (e2, op2, e3); expr_loc = loc23 } ->
make_app de1 op de2 let de2 = dexpr muc denv e2 in
| (op,de2) :: ch ->
let re = is_reusable de2 in let re = is_reusable de2 in
let v = if re then de2 else mk_var n1 de2 in let v = if re then de2 else mk_var n1 de2 in
let de12 = Dexpr.dexpr ~loc (make_app de1 op v) in let loc12 = loc_cutoff loc loc23 e2.expr_loc in
let de23 = Dexpr.dexpr ~loc (make_chain n2 n1 v ch) in let de12 = Dexpr.dexpr ~loc:loc12 (apply loc12 de1 op1 v) in
let de23 = Dexpr.dexpr ~loc:loc23 (chain n2 n1 loc23 v op2 e3) in
let d = DEand (de12, de23) in let d = DEand (de12, de23) in
if re then d else mk_let ~loc n1 de2 d if re then d else mk_let ~loc n1 de2 d
| [] -> assert false in | e23 ->
let rec get_chain e12 acc = match e12.expr_desc with apply loc de1 op1 (dexpr muc denv e23) in
| Ptree.Einfix (e1, op1, e2) when chainable_op muc denv op1 -> chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
get_chain e1 ((op1, dexpr muc denv e2) :: acc)
| _ -> e12, acc in
let ch = [op2, dexpr muc denv e3] in
let e1, ch = if chainable_op muc denv op2
then get_chain e12 ch else e12, ch in
make_chain "q1 " "q2 " (dexpr muc denv e1) ch
| Ptree.Econst c -> DEconst c | Ptree.Econst c -> DEconst c
| Ptree.Erecord fl -> | Ptree.Erecord fl ->
let ls_of_rs rs = match rs.rs_logic with let ls_of_rs rs = match rs.rs_logic with
...@@ -641,7 +602,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = ...@@ -641,7 +602,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Eupdate (e1, fl) -> | Ptree.Eupdate (e1, fl) ->
let e1 = dexpr muc denv e1 in let e1 = dexpr muc denv e1 in
let re = is_reusable e1 in let re = is_reusable e1 in
let v = if re then e1 else mk_var "_q " e1 in let v = if re then e1 else mk_var "q " e1 in
let get_val _ pj = function let get_val _ pj = function
| None -> | None ->
let pj = Dexpr.dexpr ~loc (DErs pj) in let pj = Dexpr.dexpr ~loc (DErs pj) in
...@@ -649,7 +610,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} = ...@@ -649,7 +610,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Some e -> dexpr muc denv e in | Some e -> dexpr muc denv e in
let cs,fl = parse_record ~loc muc get_val fl in let cs,fl = parse_record ~loc muc get_val fl in
let d = expr_app loc (DErs cs) fl in let d = expr_app loc (DErs cs) fl in
if re then d else mk_let ~loc "_q " e1 d if re then d else mk_let ~loc "q " e1 d
| Ptree.Elet (id, gh, kind, e1, e2) -> | Ptree.Elet (id, gh, kind, e1, e2) ->
let ld = create_user_id id, gh, kind, dexpr muc denv e1 in let ld = create_user_id id, gh, kind, dexpr muc denv e1 in
DElet (ld, dexpr muc (denv_add_let denv ld) e2) DElet (ld, dexpr muc (denv_add_let denv ld) e2)
......
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