Update

src/zrun/coiteration.ml

@@ -305,16 +305,14 @@ let rec size env { desc; loc } =
 
 (* mutually recursive definitions must either define *)
 (* functions parameterized by a size or stream values *)
-let sizefun_defs_or_values genv env l_eq =
+let sizefun_defs_or_values genv env apply l_eq =
   let rec split (acc, one_value) { eq_desc; eq_loc } =
     match eq_desc with
     | EQsizefun { sf_id; sf_id_list; sf_e } ->
        if one_value then
          error { kind = Esizefun_def_recursive; loc = eq_loc }
-       else return (Env.add sf_id { s_params = sf_id_list; 
-                                    s_body = sf_e; s_genv = genv; 
-                                    s_env = env } acc,
-                 one_value)
+       else return (Env.add sf_id { s_body = fun v_list -> apply v_list } acc,
+                    one_value)
     | EQand { eq_list } ->
        fold split (acc, one_value) eq_list
     | EQempty -> 
@@ -328,8 +326,8 @@ let sizefun_defs_or_values genv env l_eq =
   else
     return (Either.Right(acc))
 
-let sizefun_defs genv env { l_eq; l_loc } =
-  let* v = sizefun_defs_or_values genv env l_eq in
+let sizefun_defs genv env apply { l_eq; l_loc } =
+  let* v = sizefun_defs_or_values genv env apply l_eq in
   match v with 
   | Right(defs) -> return defs 
   | Left _ -> error { kind = Esizefun_def_recursive; loc = l_loc }
@@ -426,9 +424,8 @@ let rec iexp is_fun genv env { e_desc; e_loc  } =
           let* v =
             Primitives.get_node v |>
             Opt.to_result ~none: { kind = Eshould_be_a_node; loc = e_loc1} in
-          let* si = instance e_loc1 v in
           let* s2 = iexp is_fun genv env e2 in
-          return (Slist [Sinstance(si); s2])
+          return (Slist [Sinstance(v); s2])
      | (Eatomic | Etest), [e] -> iexp is_fun genv env e
      | Edisc, [e] -> 
        if is_fun then error { kind = Eshould_be_combinatorial; loc = e_loc }
@@ -468,12 +465,11 @@ let rec iexp is_fun genv env { e_desc; e_loc  } =
      let* se = iexp is_fun genv env e in
      let* s =
        match v with
-       | Vclosure ({ c_funexp = { f_kind = Knode _; f_args = [_] } } as c) ->
+       | Vnode(si) ->
           (* [f e] with [f] a node is a short-cut for [run f e] *)
           if is_fun then error { kind = Eshould_be_combinatorial; loc = e_loc }
-          else let* si = instance l_loc c in
-            return (Sinstance(si))
-       | Vclosure _ | Vfun _ -> return Sempty
+          else return (Sinstance(si))
+       | Vifun _ | Vfun _ -> return Sempty
        | _ -> error { kind = Etype; loc = e_loc } in
      return (Slist [s; se])
   | Eapp { f; arg_list } ->
@@ -812,14 +808,25 @@ and iresult is_fun genv env { r_desc } =
   | Exp(e) -> iexp is_fun genv env e
   | Returns(b) -> iblock is_fun genv env b
 
-(* an instance of a node *)
-and instance loc ({ c_funexp = { f_args; f_body }; c_genv; c_env } as c) =
+(* the instance value from a node definition *)
+and instance_of_funexp genv env tkind ({ f_args; f_body; f_loc } as f) = 
   match f_args with
   | [ arg ] ->
-     let* s_list = map (ivardec false true c_genv c_env) arg in
-     let* s_body = iresult false c_genv c_env f_body in
-     return { init = Slist (s_body :: s_list); step = c }
-  | _ -> error { kind = Etype; loc }
+     let* s_list = map (ivardec false true genv env) arg in
+     let* s_body = iresult false genv env f_body in
+     return { tkind;
+              init = Slist (s_body :: s_list);
+              step = fun s v -> runstep genv env f s v }
+  | _ -> error { kind = Etype; loc = f_loc }
+
+and value_of_funexp genv env ({ f_kind; f_args; f_loc; f_body } as f) =
+  match f_kind with
+  | Zelus.Kfun _ ->
+     return (Vfun { arity = List.length f_args;
+                      f = fun v_list -> vresult genv env f_body v_list })
+  | Zelus.Knode(tkind) ->
+     let* si = instance_of_funexp genv env tkind f in
+     return (Vnode(si))
 
 (* The main step function *)
 (* the value of an expression [e] in a global environment [genv] and local *)
@@ -1069,7 +1076,8 @@ and sexp genv env { e_desc; e_loc } s =
      let* v, s = sexp genv env e s in
      return (v, Slist [s_eq; s])
   | Efun(fe), s ->
-     return (Value(Vclosure { c_funexp = fe; c_genv = genv; c_env = env }), s)
+     let* v = value_of_funexp genv env fe in
+     return (Value(v), s)
   | Ematch { e; handlers }, Slist(se :: s_list) ->
      let* ve, se = sexp genv env e se in
      let* v, s_list =
@@ -1326,7 +1334,7 @@ and vleq genv env ({ l_rec; l_eq } as leq) =
   (* for the moment, only recursive definitions of *)
   (* functions of sizes are allowed *)
   if l_rec then
-    let* defs = sizefun_defs genv env leq in
+    let* defs = sizefun_defs genv env apply leq in
     return (Fix.sizefixpoint defs)
   else let* s = ieq true genv env l_eq in
     let* env, _ = seq genv env l_eq s in
@@ -1448,11 +1456,11 @@ and sarg genv env ({ e_desc; e_loc } as e) s =
      sexp genv env e s
 
 (* application of a node *)
-and run loc { init; step } v =
+and run loc ({ init; step } as i) v =
   let* v, init = runstep loc init step v in
-  return (v, { init; step })
+  return (v, { i with init; step })
 
-and runstep loc s { c_funexp = { f_args; f_body }; c_genv; c_env } v =
+and funstep genv env { f_args; f_body } s v =
   let match_in_list a_list s_list v_list =
     let match_in acc vdec s v =
       let* acc, s = svardec c_genv c_env acc vdec s v in
@@ -1493,7 +1501,7 @@ and sleq genv env { l_kind; l_rec; l_eq = ({ eq_write } as l_eq); l_loc } s_eq =
      if l_rec then
        (* Either it is a collection of mutually recursive functions *)
        (* parameterized by a size or stream values *)
-       let* defs = sizefun_defs_or_values genv env l_eq in
+       let* defs = sizefun_defs_or_values genv env apply l_eq in
        let* (env_eq, s_eq) =
          match defs with
          | Either.Right(defs) ->
@@ -2281,13 +2289,24 @@ and apply loc fv v_list =
      let* fv =
        op v |> Opt.to_result ~none:{ kind = Etype; loc = loc } in
      apply loc fv v_list
-  | Vclosure { c_funexp = { f_kind; f_args; f_body } as fe;
-               c_genv; c_env }, _ ->
-     apply_closure loc c_genv c_env fe f_args f_body v_list
+  | Vcofun { arity; f }, v_list ->
+     apply_cofun loc arity f v_list
   | _ ->
      (* typing error *)
      error { kind = Etype; loc = loc }
 
+and apply_cofun loc arity f v_list =
+  let actual_arity = List.length v_list in
+  if actual_arity = arity then
+    f v_list
+  else if actual_arity < arity
+  then error { kind = Etype; loc = loc }
+  else
+    (* the result is a function *)
+    return
+      (Value(Vcofun { arity = actual_arity - arity;
+                      f = fun v_list_extra -> f (v_list @ v_list_extra) }))
+
 (* apply a closure to a list of arguments *)
 and apply_closure loc genv env ({ f_kind; f_loc } as fe) f_args f_body v_list =
   match f_args, v_list with

src/zrun/output.ml

@@ -48,10 +48,10 @@ let rec pvalue ff v =
   | Vstate1(id, l) ->
      fprintf
        ff "@[<hov 1>%a(%a)@]" Ident.fprint_t id pvalue_list l
-  | Vfun _ ->
+  | Vifun _ ->
      fprintf ff "<fun>"
-  | Vcofun _ -> fprintf ff "<fun>"
-  | Vconode { tkind } ->
+  | Vfun _ -> fprintf ff "<fun>"
+  | Vnode { tkind } ->
      fprintf ff "<%s>" (Printer.tkind tkind)
   | Vsizefun _ ->
      fprintf ff "<sizefun>"

src/zrun/primitives.ml

@@ -72,7 +72,7 @@ let test v =
 
 let get_node v =
   match v with
-  | Vconode(instance) -> return instance
+  | Vnode(instance) -> return instance
   | _ -> None
 
 let get_record r =
@@ -222,7 +222,7 @@ let rec compare_pvalue v1 v2 =
   | Vrecord _, Vrecord _ -> none
   | Vtuple(v_list1), Vtuple(v_list2) ->
      compare_list compare_value v_list1 v_list2
-  | (Vfun _, Vfun _) | (Vcofun _, Vcofun _) | (Vconode _, Vconode _) -> none
+  | (Vifun _, Vifun _) | (Vfun _, Vfun _) | (Vnode _, Vnode _) -> none
   | _ -> none
 
 (* comparison of present/absent with one the representation of the other *)
@@ -423,7 +423,7 @@ let atomic v =
   let+ v = v in
   match v with
   | Vtuple(l) -> stuple l
-  | Vcofun _ | Vconode _ ->
+  | Vfun _ | Vnode _ ->
       (* this part should be changed into [atomic(f) = lambda x.let+ x in f x] *)
       (* that is, even if [f] is not strict, make it a strict function *)
       (* this is necessary to avoid unbounded recursion with f = \x. x x and f f *)
@@ -438,12 +438,12 @@ let void = Value(Vvoid)
 let max_float = Value(Vfloat(max_float))
 let zero_float = Value(Vfloat(0.0))
 
-let zerop op = Vfun (fun _ -> op ())
+let zerop op = Vifun (fun _ -> op ())
 
-let unop op = Vfun op
+let unop op = Vifun op
 
 let binop op =
-  Vfun(fun v1 -> return (Vfun (fun v2 -> op v1 v2)))
+  Vifun(fun v1 -> return (Vifun (fun v2 -> op v1 v2)))
 
 (*
 (* state processes *)

src/zrun/value.ml

@@ -53,10 +53,10 @@ and pvalue =
   | Varray of pvalue array
   (* imported stateless functions; they must verify that *)
   (* f(atomic v) not= bot *)
-  | Vfun of (pvalue -> pvalue option)
+  | Vifun of (pvalue -> pvalue option)
   (* user defined functions and nodes *)
-  | Vcofun of (value -> value result)
-  | Vconode of instance
+  | Vfun of { arity: int; f : value list -> value result }
+  | Vnode of instance
   (* function parameterized by sizes *)
   | Vsizefun of sizefun
 (* mutually recursive definition of size functions *)
@@ -78,7 +78,7 @@ and 'a array =
 and 'a map =
   { m_length : int; m_u : int -> 'a result }
 
-and sizefun = int -> value
+and sizefun = { s_body: int list -> value result; }
 
 (* instance of a node *)
 and instance =
@@ -105,7 +105,7 @@ and state =
   | Senv of value ientry Ident.Env.t
 
 (*
-  Intuition: a expression is interpreted as a value of type:
+  Intuition: an expression is interpreted as a value of type:
 
   type ('a, 's) costream =
   | CoF : { init : 's;
@@ -119,9 +119,7 @@ and state =
   | CoNode : { init : 's;
                step : 's -> 'a list -> ('b * 's) option } -> ('a, 'b, 's) node
 
- Here, the set of values is a big bag in which all kinds of value is put; in
- particular values that do not of bounded sizes. This could be constrained because,
- values on streams are actually of bounded sizes. That which belong to a CPO of
- unbounded height (e.g., functions) are computed only at "compilation time" or
- "instanciation time".
+  Here, the set of values contains all the possible value; those that are
+  produced at every step and those that are produced only at "compile time"
+  or "instancitation time". They could be separated into two distinct sets
 *)