higher order application

examples/list.why

+theory Map
+  use import list.List
+
+  use HighOrd as HO
+
+  logic map (fn : HO.func 'a 'b) (l : list 'a) : list 'b = match l with
+    | Cons x r -> Cons (fn x) (map fn r)
+    | Nil -> Nil
+  end
+
+  logic forall2 (pr : HO.func 'a (HO.pred 'b)) (l1 : list 'a) (l2 : list 'b) =
+    match l1, l2 with
+    | Cons x1 r1, Cons x2 r2 -> pr x1 x2 and forall2 pr r1 r2
+    | _, _ -> true
+    end
+
+  use export int.Int
+
+  logic double (l : list int) : list int = map (\ i : int . i * 2) l
+
+  logic lequal (l1 l2 : list int) = forall2 (\ i1 i2 : int . i1 = i2) l1 l2
+end
+
 theory Induction2
   use import list.List
   use import list.Length

examples/programs/ropes.mlw

@@ -11,7 +11,7 @@
   logic inv (r: rope) = match r with
     | Str s ofs len -> 
         len = 0 or 0 <= ofs < S.length s and ofs + len <= S.length s
-    | App l r   len -> 
+    | App l r _ ->
         0 < len l and inv l and 0 < len r and inv r
   end
 

src/parser/parser.mly

@@ -441,8 +441,6 @@ lexpr:
    { mk_pp (PPif ($2, $4, $6)) }
 | quant list1_param_var_sep_comma triggers DOT lexpr
    { mk_pp (PPquant ($1, $2, $3, $5)) }
-| EXISTS list1_param_var_sep_comma triggers DOT lexpr
-   { mk_pp (PPquant (PPexists, $2, $3, $5)) }
 | STRING lexpr %prec prec_named
    { mk_pp (PPnamed (Ident.label ~loc:(loc ()) $1, $2)) }
 | LET pattern EQUAL lexpr IN lexpr

src/parser/typing.ml

@@ -350,6 +350,15 @@ let check_quant_linearity uqu =
   in
   List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
 
+let check_highord env x tl = match x with
+  | Qident { id = x } when Mstr.mem x env.dvars -> true
+  | _ -> List.length tl > List.length ((find_lsymbol x env.uc).ls_args)
+
+let apply_highord loc x tl = match List.rev tl with
+  | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
+  | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
+  | [] -> assert false
+
 let rec dterm env t =
   let n, ty = dterm_node t.pp_loc env t.pp_desc in
   { dt_node = n; dt_ty = ty }
@@ -365,6 +374,11 @@ and dterm_node loc env = function
       let n = List.length tyl in
       if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
       Tapp (s, []), ty
+  | PPapp (x, tl) when check_highord env x tl ->
+      let tl = apply_highord loc x tl in
+      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
+      let tl = dtype_args fs_func_app.ls_name loc env atyl tl in
+      Tapp (fs_func_app, tl), Util.of_option aty
   | PPapp (x, tl) ->
       let s, tyl, ty = specialize_fsymbol x env.uc in
       let tl = dtype_args s.ls_name loc env tyl tl in
@@ -515,6 +529,11 @@ and dfmla env e = match e.pp_desc with
         | _ -> error ~loc:e.pp_loc PredicateExpected
       in
       Fquant (q, uqu, trl, dfmla env a)
+  | PPapp (x, tl) when check_highord env x tl ->
+      let tl = apply_highord e.pp_loc x tl in
+      let atyl, _ = Denv.specialize_lsymbol ~loc:(e.pp_loc) ps_pred_app in
+      let tl = dtype_args ps_pred_app.ls_name e.pp_loc env atyl tl in
+      Fapp (ps_pred_app, tl)
   | PPapp (x, tl) ->
       let s, tyl = specialize_psymbol x env.uc in
       let tl = dtype_args s.ls_name e.pp_loc env tyl tl in

src/programs/pgm_typing.ml

@@ -135,6 +135,10 @@ let create_type_var loc =
   let tv = Ty.create_tvsymbol (id_user "a" loc) in
   Tyvar (create_ty_decl_var ~loc ~user:false tv)
 
+let add_pure_var id ty env = match ty with
+  | Tyapp (ts, _) when Ty.ts_equal ts env.env.ts_arrow -> env.denv
+  | _ -> Typing.add_var id ty env.denv
+
 let dcurrying gl tyl ty =
   let make_arrow_type ty1 ty2 = dty_app (gl.ts_arrow, [ty1; ty2]) in
   List.fold_right make_arrow_type tyl ty
@@ -205,23 +209,21 @@ let dpost env ty (q, ql) =
     let s, tyl, _ = dexception env id in
     let denv = match tyl with
       | [] -> env.denv
-      | [ty] -> Typing.add_var id_result ty env.denv
+      | [ty] -> add_pure_var id_result ty env
       | _ -> assert false
     in
     s, dfmla denv l
   in
-  let denv = Typing.add_var id_result ty env.denv in
+  let denv = add_pure_var id_result ty env in
   dfmla denv q, List.map dexn ql
 
+let add_local_top env x tyv =
+  { env with locals = Mstr.add x tyv env.locals }
+
 let add_local env x tyv = 
   let ty = dpurify env tyv in
-  match tyv with
-    | DTpure _ ->
-	{ env with 
-	    locals = Mstr.add x tyv env.locals;
-	    denv = Typing.add_var x ty env.denv } 
-    | DTarrow _ ->
-	{ env with locals = Mstr.add x tyv env.locals }
+  { env with locals = Mstr.add x tyv env.locals;
+             denv = add_pure_var x ty env }
 
 let rec dtype_v env = function
   | Pgm_ptree.Tpure pt -> 
@@ -425,7 +427,7 @@ and dexpr_desc env loc = function
       if Typing.mem_var s env.denv then 
 	errorm ~loc "clash with previous label %s" s;
       let ty = dty_label env.env in
-      let env = { env with denv = Typing.add_var s ty env.denv } in
+      let env = { env with denv = add_pure_var s ty env } in
       let e1 = dexpr env e1 in
       DElabel (s, e1), e1.dexpr_type
   | Pgm_ptree.Ecast (e1, ty) ->
@@ -441,7 +443,7 @@ and dletrec env dl =
   (* add all functions into environment *)
   let add_one env (id, bl, var, t) = 
     let ty = create_type_var id.id_loc in
-    let env = add_local env id.id (DTpure ty) in
+    let env = add_local_top env id.id (DTpure ty) in
     env, ((id, ty), bl, var, t)
   in
   let env, dl = map_fold_left add_one env dl in