accept partially applied symbols in logic

Will be supported in programs as soon, as we enable lambdas.

src/parser/parser.mly

@@ -38,15 +38,13 @@ end
   let floc_ij i j = Loc.extract (loc_ij i j)
 *)
 
-  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
-  let mk_pp d = mk_ppl (floc ()) d
-  let mk_pat p = { pat_loc = floc (); pat_desc = p }
+  let mk_pp_l loc d = { pp_loc = loc; pp_desc = d }
+  let mk_pp d = { pp_loc = floc (); pp_desc = d }
 
-  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
-  let infix_pp a i b = infix_ppl (floc ()) a i b
+  let mk_pat p = { pat_loc = floc (); pat_desc = p }
 
-  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
-  let prefix_pp p a = prefix_ppl (floc ()) p a
+  let infix_pp a i b = mk_pp (PPbinop (a, i, b))
+  let prefix_pp p a = mk_pp (PPunop (p, a))
 
   let infix  s = "infix "  ^ s
   let prefix s = "prefix " ^ s
@@ -56,10 +54,6 @@ end
 
   let add_lab id l = { id with id_lab = l }
 
-  let mk_l_apply f a =
-    let loc = Loc.join f.pp_loc a.pp_loc in
-    { pp_loc = loc; pp_desc = PPapply (f,a) }
-
   let mk_l_prefix op e1 =
     let id = mk_id (prefix op) (floc_i 1) in
     mk_pp (PPidapp (Qident id, [e1]))
@@ -81,14 +75,9 @@ end
       | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
       | _ -> raise exn)
 
+  let mk_expr_l loc d = { expr_loc = loc; expr_desc = d }
   let mk_expr d = { expr_loc = floc (); expr_desc = d }
 
-  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
-
-  let mk_apply f a =
-    let loc = Loc.join f.expr_loc a.expr_loc in
-    { expr_loc = loc; expr_desc = Eapply (f,a) }
-
   let mk_prefix op e1 =
     let id = mk_id (prefix op) (floc_i 1) in
     mk_expr (Eidapp (Qident id, [e1]))
@@ -609,12 +598,10 @@ lexpr:
    { mk_l_infix $1 $2 $3 }
 | prefix_op lexpr %prec prec_prefix_op
    { mk_l_prefix $1 $2 }
-| qualid list1_lexpr_arg
-   { mk_pp (PPidapp ($1, $2)) }
-| lexpr_arg_noid list1_lexpr_arg
-   { match $1.pp_desc with
-     | PPidapp (id,al) -> mk_pp (PPidapp (id, al @ $2))
-     | _ -> List.fold_left mk_l_apply $1 $2 }
+| lexpr_arg list1_lexpr_arg /* FIXME/TODO: "lexpr lexpr_arg" */
+   { let b = rhs_start_pos 1 in
+     List.fold_left (fun f (e,a) ->
+       mk_pp_l (Loc.extract (b,e)) (PPapply (f,a))) $1 $2 }
 | IF lexpr THEN lexpr ELSE lexpr
    { mk_pp (PPif ($2, $4, $6)) }
 | quant list1_quant_vars triggers DOT lexpr
@@ -650,8 +637,8 @@ field_value:
 ;
 
 list1_lexpr_arg:
-| lexpr_arg                 { [$1] }
-| lexpr_arg list1_lexpr_arg { $1::$2 }
+| lexpr_arg                 { [rhs_end_pos 1, $1] }
+| lexpr_arg list1_lexpr_arg { (rhs_end_pos 1, $1) :: $2 }
 ;
 
 constant:
@@ -661,10 +648,6 @@ constant:
 
 lexpr_arg:
 | qualid            { mk_pp (PPident $1) }
-| lexpr_arg_noid    { $1 }
-;
-
-lexpr_arg_noid:
 | constant          { mk_pp (PPconst $1) }
 | TRUE              { mk_pp PPtrue }
 | FALSE             { mk_pp PPfalse }
@@ -1194,12 +1177,10 @@ expr:
    { mk_expr (Enot $2) }
 | prefix_op expr %prec prec_prefix_op
    { mk_prefix $1 $2 }
-| qualid list1_expr_arg
-   { mk_expr (Eidapp ($1, $2)) }
-| expr_arg_noid list1_expr_arg
-   { match $1.expr_desc with
-     | Eidapp (id,al) -> mk_expr (Eidapp (id, al @ $2))
-     | _ -> List.fold_left mk_apply $1 $2 }
+| expr_arg list1_expr_arg /* FIXME/TODO: "expr expr_arg" */
+   { let b = rhs_start_pos 1 in
+     List.fold_left (fun f (e,a) ->
+       mk_expr_l (Loc.extract (b,e)) (Eapply (f,a))) $1 $2 }
 | IF final_expr THEN expr ELSE expr
    { mk_expr (Eif ($2, $4, $6)) }
 | IF final_expr THEN expr %prec prec_no_else
@@ -1247,7 +1228,7 @@ expr:
 | fun_expr
    { mk_expr (Elam $1) }
 | VAL top_ghost lident_rich labels tail_type_c IN expr
-   { mk_expr (Elet (add_lab $3 $4, $2, mk_expr_i 5 (Eany $5), $7)) }
+   { mk_expr (Elet (add_lab $3 $4, $2, mk_expr_l (floc_i 5) (Eany $5), $7)) }
 | MATCH final_expr WITH bar_ program_match_cases END
    { mk_expr (Ematch ($2, $5)) }
 | MATCH list2_expr_sep_comma WITH bar_ program_match_cases END
@@ -1287,10 +1268,6 @@ final_expr:
 
 expr_arg:
 | qualid          { mk_expr (Eident $1) }
-| expr_arg_noid   { $1 }
-;
-
-expr_arg_noid:
 | constant        { mk_expr (Econst $1) }
 | TRUE            { mk_expr Etrue }
 | FALSE           { mk_expr Efalse }
@@ -1337,8 +1314,8 @@ field_expr:
 ;
 
 list1_expr_arg:
-| expr_arg                   { [$1] }
-| expr_arg list1_expr_arg    { $1 :: $2 }
+| expr_arg                   { [rhs_end_pos 1, $1] }
+| expr_arg list1_expr_arg    { (rhs_end_pos 1, $1) :: $2 }
 ;
 
 list2_expr_sep_comma:

src/parser/typing.ml

@@ -203,39 +203,59 @@ let chainable_op uc op =
 
 type global_vs = Ptree.qualid -> vsymbol option
 
+let mk_closure loc ls =
+  let mk dt = Dterm.dterm ~loc dt in
+  let id = id_user "fc" loc and dty = dty_fresh () in
+  let mk_v i _ =
+    id_user ("y" ^ string_of_int i) loc, dty_fresh () in
+  let mk_t (id, dty) = mk (DTvar (id.pre_name, dty)) in
+  let vl = Lists.mapi mk_v ls.ls_args in
+  let tl = List.map mk_t vl in
+  let app e1 e2 = DTapp (fs_func_app, [mk e1; e2]) in
+  let e = List.fold_left app (DTvar ("fc", dty)) tl in
+  let f = DTapp (ps_equ, [mk e; mk (DTapp (ls, tl))]) in
+  DTeps (id, dty, mk (DTquant (Tforall, vl, [], mk f)))
+
 let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
-  let func_app loc e el =
-    let app (loc, e) e1 = Loc.join loc e1.pp_loc,
-      DTfapp (Dterm.dterm ~loc e, dterm uc gvars denv e1) in
-    snd (List.fold_left app (loc, e) el)
+  let func_app e el =
+    List.fold_left (fun e1 (loc, e2) ->
+      DTfapp (Dterm.dterm ~loc e1, e2)) e el
   in
-  let rec take loc al l el = match l, el with
-    | (_::l), (e::el) ->
-        take (Loc.join loc e.pp_loc) (dterm uc gvars denv e :: al) l el
-    | _, _ -> loc, List.rev al, el
+  let rec apply_ls loc ls al l el = match l, el with
+    | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
+    | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
+    | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el)
   in
-  let qualid_app loc q el = match gvars q with
-    | Some vs ->
-        func_app loc (DTgvar vs) el
+  let qualid_app q el = match gvars q with
+    | Some vs -> func_app (DTgvar vs) el
     | None ->
         let ls = find_lsymbol uc q in
-        let loc, al, el = take loc [] ls.ls_args el in
-        func_app loc (DTapp (ls,al)) el
+        apply_ls (qloc q) ls [] ls.ls_args el
   in
-  let qualid_app loc q el = match q with
+  let qualid_app q el = match q with
     | Qident {id = n} ->
         (match denv_get_opt denv n with
-        | Some d -> func_app loc d el
-        | None -> qualid_app loc q el)
-    | _ -> qualid_app loc q el
+        | Some d -> func_app d el
+        | None -> qualid_app q el)
+    | _ -> qualid_app q el
+  in
+  let rec unfold_app e1 e2 el = match e1.pp_desc with
+    | PPapply (e11,e12) ->
+        let e12 = dterm uc gvars denv e12 in
+        unfold_app e11 e12 ((e1.pp_loc, e2)::el)
+    | PPident q ->
+        qualid_app q ((e1.pp_loc, e2)::el)
+    | _ ->
+        func_app (DTfapp (dterm uc gvars denv e1, e2)) el
   in
   Dterm.dterm ~loc (match desc with
   | PPident q ->
-      qualid_app loc q []
+      qualid_app q []
   | PPidapp (q, tl) ->
-      qualid_app (qloc q) q tl
+      let tl = List.map (dterm uc gvars denv) tl in
+      DTapp (find_lsymbol uc q, tl)
   | PPapply (e1, e2) ->
-      DTfapp (dterm uc gvars denv e1, dterm uc gvars denv e2)
+      unfold_app e1 (dterm uc gvars denv e2) []
   | PPtuple tl ->
       let tl = List.map (dterm uc gvars denv) tl in
       DTapp (fs_tuple (List.length tl), tl)

src/whyml/mlw_typing.ml

@@ -380,41 +380,71 @@ let chainable_op uc denv op =
   | Some _ -> false (* can never happen *)
   | None -> chainable_qualid uc (Qident op)
 
+let mk_closure loc _ls =
+  Loc.errorm ~loc "Partial@ application@ of@ logical@ symbols@ \
+    is@ currently@ not@ supported@ in@ programs."
+(*
+  let mk dt = Dterm.dterm ~loc dt in
+  let id = id_user "fc" loc and dty = dty_fresh () in
+  let mk_v i _ =
+    id_user ("y" ^ string_of_int i) loc, dty_fresh () in
+  let mk_t (id, dty) = mk (DTvar (id.pre_name, dty)) in
+  let vl = Lists.mapi mk_v ls.ls_args in
+  let tl = List.map mk_t vl in
+  let app e1 e2 = DTapp (fs_func_app, [mk e1; e2]) in
+  let e = List.fold_left app (DTvar ("fc", dty)) tl in
+  let f = DTapp (ps_equ, [mk e; mk (DTapp (ls, tl))]) in
+  DTeps (id, dty, mk (DTquant (Tforall, vl, [], mk f)))
+*)
+
 let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
-  let expr_app loc e el =
-    let app (loc, e) e1 = Opt.fold Loc.join loc e1.de_loc,
-      DEapply (Mlw_dexpr.dexpr ~loc e, e1) in
-    snd (List.fold_left app (loc, e) el)
+  let expr_app e el =
+    List.fold_left (fun e1 (loc, e2) ->
+      DEapply (Mlw_dexpr.dexpr ~loc e1, e2)) e el
+  in
+  let rec apply_pl loc pl al l el = match l, el with
+    | (_::l), (e::el) -> apply_pl loc pl (e::al) l el
+    | [], _ -> expr_app (DEplapp (pl, List.rev_map snd al)) el
+    | _, [] -> expr_app (mk_closure loc pl) (List.rev_append al el)
   in
-  let rec take loc al l el = match l, el with
-    | (_::l), (e::el) ->
-        take (Opt.fold Loc.join loc e.de_loc) (e::al) l el
-    | _, _ -> loc, List.rev al, el
+  let rec apply_ls loc ls al l el = match l, el with
+    | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
+    | [], _ -> expr_app (DElsapp (ls, List.rev_map snd al)) el
+    | _, [] -> expr_app (mk_closure loc ls) (List.rev_append al el)
   in
-  let qualid_app loc q el = match uc_find_ps uc q with
-    | PV pv -> expr_app loc (DEgpvar pv) el
-    | PS ps -> expr_app loc (DEgpsym ps) el
-    | PL pl -> let loc,al,el = take loc [] pl.pl_args el in
-               expr_app loc (DEplapp (pl, al)) el
-    | LS ls -> let loc,al,el = take loc [] ls.ls_args el in
-               expr_app loc (DElsapp (ls, al)) el
+  let qualid_app q el = match uc_find_ps uc q with
+    | PV pv -> expr_app (DEgpvar pv) el
+    | PS ps -> expr_app (DEgpsym ps) el
+    | PL pl -> apply_pl (qloc q) pl [] pl.pl_args el
+    | LS ls -> apply_ls (qloc q) ls [] ls.ls_args el
     | XS xs -> Loc.errorm ~loc:(qloc q)
         "unexpected exception symbol %a" print_xs xs
   in
-  let qualid_app loc q el = match q with
+  let qualid_app q el = match q with
     | Qident {id = n} ->
         (match denv_get_opt denv n with
-        | Some d -> expr_app loc d el
-        | None -> qualid_app loc q el)
-    | _ -> qualid_app loc q el
+        | Some d -> expr_app d el
+        | None -> qualid_app q el)
+    | _ -> qualid_app q el
+  in
+  let rec unfold_app e1 e2 el = match e1.expr_desc with
+    | Ptree.Eapply (e11,e12) ->
+        let e12 = dexpr lenv denv e12 in
+        unfold_app e11 e12 ((e1.expr_loc, e2)::el)
+    | Ptree.Eident q ->
+        qualid_app q ((e1.expr_loc, e2)::el)
+    | _ ->
+        expr_app (DEapply (dexpr lenv denv e1, e2)) el
   in
   Mlw_dexpr.dexpr ~loc (match desc with
   | Ptree.Eident q ->
-      qualid_app loc q []
+      qualid_app q []
   | Ptree.Eidapp (q, tl) ->
-      qualid_app (qloc q) q (List.map (dexpr lenv denv) tl)
+      (* FIXME: qloc q is wrong for the 2nd and later arguments *)
+      let loc = qloc q in
+      qualid_app q (List.map (fun t -> loc, dexpr lenv denv t) tl)
   | Ptree.Eapply (e1, e2) ->
-      DEapply (dexpr lenv denv e1, dexpr lenv denv e2)
+      unfold_app e1 (dexpr lenv denv e2) []
   | Ptree.Etuple el ->
       let el = List.map (dexpr lenv denv) el in
       DElsapp (fs_tuple (List.length el), el)
@@ -422,10 +452,11 @@ let rec dexpr ({uc = uc} as lenv) denv {expr_desc = desc; expr_loc = loc} =
   | Ptree.Einnfix (e12, op2, e3) ->
       let make_app de1 op de2 = if op.id = "infix <>" then
         let oq = Qident { op with id = "infix =" } in
-        let dt = qualid_app op.id_loc oq [de1;de2] in
+        (* FIXME: op.id_loc is wrong for the 2nd argument *)
+        let dt = qualid_app oq [(op.id_loc, de1); (op.id_loc, de2)] in
         DEnot (Mlw_dexpr.dexpr ~loc dt)
       else
-        qualid_app op.id_loc (Qident op) [de1;de2]
+        qualid_app (Qident op) [(op.id_loc, de1); (op.id_loc, de2)]
       in
       let rec make_chain n1 n2 de1 = function
         | [op,de2] ->