Dterm: support for lambdas

src/core/dterm.ml

@@ -160,6 +160,9 @@ and dpattern_node =
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff
 
+type dquant =
+  | DTforall | DTexists | DTlambda
+
 type dterm = {
   dt_node  : dterm_node;
   dt_dty   : dty option;
@@ -176,7 +179,7 @@ and dterm_node =
   | DTlet of dterm * preid * dterm
   | DTcase of dterm * (dpattern * dterm) list
   | DTeps of preid * dty * dterm
-  | DTquant of quant * (preid * dty) list * dterm list list * dterm
+  | DTquant of dquant * (preid * dty) list * dterm list list * dterm
   | DTbinop of dbinop * dterm * dterm
   | DTnot of dterm
   | DTtrue
@@ -324,7 +327,11 @@ let dterm ?loc node =
     | DTeps (_,dty,df) ->
         dfmla_expected_type df;
         Some dty
-    | DTquant (_,_,_,df) ->
+    | DTquant (DTlambda,vl,_,df) ->
+        let res = Opt.get_def dty_bool df.dt_dty in
+        let app (_,l) r = Dapp (ts_func, [l;r]) in
+        Some (List.fold_right app vl res)
+    | DTquant ((DTforall|DTexists),_,_,df) ->
         dfmla_expected_type df;
         None
     | DTbinop (_,df1,df2) ->
@@ -410,8 +417,8 @@ let check_used_var t vs =
   if not (String.length s > 0 && s.[0] = '_') then
   Warning.emit ?loc:vs.vs_name.id_loc "unused variable %s" s
 
-let check_exists_implies q f = match q, f.t_node with
-  | Texists, Tbinop (Timplies,_,_) -> Warning.emit ?loc:f.t_loc
+let check_exists_implies f = match f.t_node with
+  | Tbinop (Timplies,_,_) -> Warning.emit ?loc:f.t_loc
       "form \"exists x. P -> Q\" is likely an error (use \"not P \\/ Q\" if not)"
   | _ -> ()
 
@@ -490,12 +497,20 @@ and try_term strict keep_loc uloc env prop dty node =
       t_eps_close v f
   | DTquant (q,vl,dll,df) ->
       let env, vl = quant_vars ~strict env vl in
+      let prop = q <> DTlambda || df.dt_dty = None in
       let tr_get dt = get env (dt.dt_dty = None) dt in
       let trl = List.map (List.map tr_get) dll in
-      let f = get env true df in
+      let f = get env prop df in
       List.iter (check_used_var f) vl;
-      check_exists_implies q f;
-      t_quant_close q vl trl f
+      begin match q with
+        | DTforall ->
+            t_forall_close vl trl f
+        | DTexists ->
+            check_exists_implies f;
+            t_exists_close vl trl f
+        | DTlambda ->
+            t_lambda vl trl f
+      end
   | DTbinop (DTand,df1,df2) ->
       t_and (get env true df1) (get env true df2)
   | DTbinop (DTand_asym,df1,df2) ->

src/core/dterm.mli

@@ -41,6 +41,9 @@ and dpattern_node =
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff
 
+type dquant =
+  | DTforall | DTexists | DTlambda
+
 type dterm = private {
   dt_node  : dterm_node;
   dt_dty   : dty option;
@@ -57,7 +60,7 @@ and dterm_node =
   | DTlet of dterm * preid * dterm
   | DTcase of dterm * (dpattern * dterm) list
   | DTeps of preid * dty * dterm
-  | DTquant of quant * (preid * dty) list * dterm list list * dterm
+  | DTquant of dquant * (preid * dty) list * dterm list list * dterm
   | DTbinop of dbinop * dterm * dterm
   | DTnot of dterm
   | DTtrue

src/parser/typing.ml

@@ -210,16 +210,11 @@ 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)))
+  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
 
 let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
   let func_app e el =
@@ -332,19 +327,11 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
       let dterm e = dterm uc gvars denv e in
       let trl = List.map (List.map dterm) trl in
       let e1 = dterm e1 in
-      begin match q with
-        | Ptree.Tforall -> DTquant (Term.Tforall, qvl, trl, e1)
-        | Ptree.Texists -> DTquant (Term.Texists, qvl, trl, e1)
-        | Ptree.Tlambda ->
-            let id = id_user "fc" loc and dty = dty_fresh () in
-            let add acc (x, _) =
-              let arg = Dterm.dterm ~loc (denv_get denv (preid_name x)) in
-              DTapp (fs_func_app, [Dterm.dterm ~loc acc; arg]) in
-            let app = List.fold_left add (DTvar ("fc",dty)) qvl in
-            let f = DTapp (ps_equ, [Dterm.dterm ~loc app; e1]) in
-            let f = DTquant (Tforall, qvl, trl, Dterm.dterm ~loc f) in
-            DTeps (id, dty, Dterm.dterm ~loc f)
-      end
+      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
         | Some e -> dterm uc gvars denv e