Start removing the reference to expressions in values.

src/global/printer.ml

@@ -378,8 +378,10 @@ and result ff { r_desc } =
 and kind f_kind =
   match f_kind with
   | Kfun _ -> "fun"
-  | Knode(k) ->
-     (match k with | Kdiscrete -> "node" | Kcont -> "hybrid")
+  | Knode(t_kind) -> tkind t_kind
+
+and tkind t_kind =
+  match t_kind with | Kdiscrete -> "node" | Kcont -> "hybrid"
 
 and funexp ff { f_vkind; f_kind; f_args; f_body; f_env } =
   let vkind =

src/zrun/forloop.ml

@@ -38,9 +38,9 @@ let (and+) v1 v2 =
   | Value(v1), Value(v2) -> Value(v1, v2)
 
 (* index in a loop body *)
-type ('info, 'ienv) index =
+type index =
   (* [xi in e by e'] means that in the i-th iteration, xi = e.(e' * i) *)
-  | Vinput of { ve : ('info, 'ienv) pvalue array; by : int option }
+  | Vinput of { ve : pvalue array; by : int option }
   (* [j in e0 to e1 or j in e0 downto e1] means that in the i-th iteration *)
   (* j = i + e0 in the first case; j = e1 - i in the second with i in [0..n-1] *)
   | Vindex of { ve_left : int; ve_right : int; dir : bool }

src/zrun/output.ml

@@ -50,8 +50,9 @@ let rec pvalue ff v =
        ff "@[<hov 1>%a(%a)@]" Ident.fprint_t id pvalue_list l
   | Vfun _ ->
      fprintf ff "<fun>"
-  | Vclosure { c_funexp = { f_kind } } ->
-     fprintf ff "<%s>" (Printer.kind f_kind)
+  | Vcofun _ -> fprintf ff "<fun>"
+  | Vconode { tkind } ->
+     fprintf ff "<%s>" (Printer.tkind tkind)
   | Vsizefun _ ->
      fprintf ff "<sizefun>"
   | Vsizefix { bound; name; defs } ->

src/zrun/primitives.ml

@@ -72,7 +72,7 @@ let test v =
 
 let get_node v =
   match v with
-  | Vclosure ({ c_funexp = { f_kind = Knode _ } } as c) -> return c
+  | Vconode(instance) -> return instance
   | _ -> None
 
 let get_record r =
@@ -222,8 +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 _ -> none
-  | Vclosure _, Vclosure _ -> none
+  | (Vfun _, Vfun _) | (Vcofun _, Vcofun _) | (Vconode _, Vconode _) -> none
   | _ -> none
 
 (* comparison of present/absent with one the representation of the other *)
@@ -424,7 +423,7 @@ let atomic v =
   let+ v = v in
   match v with
   | Vtuple(l) -> stuple l
-  | Vclosure _ -> 
+  | Vcofun _ | Vconode _ ->
       (* 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 *)

src/zrun/value.ml

@@ -32,106 +32,96 @@ type 'a star =
   | Vbot (* bottom value *)
   | Value of 'a (* value *)
 
-type ('info, 'ienv) value = ('info, 'ienv) pvalue star
+type value = pvalue star
 
-and ('info, 'ienv) pvalue =
+and pvalue =
   | Vint of int
   | Vbool of bool
   | Vfloat of float
   | Vchar of char
   | Vstring of string
   | Vvoid 
   | Vconstr0 of Lident.t
-  | Vconstr1 of Lident.t * ('info, 'ienv) pvalue list
-  | Vrecord of ('info, 'ienv) pvalue Zelus.record list
-  | Vpresent of ('info, 'ienv) pvalue 
+  | Vconstr1 of Lident.t * pvalue list
+  | Vrecord of pvalue Zelus.record list
+  | Vpresent of pvalue 
   | Vabsent 
-  | Vstuple of ('info, 'ienv) pvalue list
-  | Vtuple of ('info, 'ienv) pvalue star list
+  | Vstuple of pvalue list
+  | Vtuple of pvalue star list
   | Vstate0 of Ident.t
-  | Vstate1 of Ident.t * ('info, 'ienv) pvalue list
-  | Varray of ('info, 'ienv) pvalue array
+  | Vstate1 of Ident.t * pvalue list
+  | Varray of pvalue array
   (* imported stateless functions; they must verify that *)
   (* f(atomic v) not= bot *)
-  | Vfun of (('info, 'ienv) pvalue -> ('info, 'ienv) pvalue option)
-  | Vclosure of ('info, 'ienv) closure
+  | Vfun of (pvalue -> pvalue option)
+  (* user defined functions and nodes *)
+  | Vcofun of (value -> value result)
+  | Vconode of instance
   (* function parameterized by sizes *)
-  | Vsizefun of ('info, 'ienv) sizefun
-  (* a representation for mutually recursive functions over sizes *)
-  (* f where rec [f1<s,...> = e1 and ... fk<s,...> = ek] *)
-  | Vsizefix of 
+  | Vsizefun of sizefun
+(* mutually recursive definition of size functions *)
+  | Vsizefix of
       { bound: int list option; (* the maximum number of iterations *)
         name: Ident.t; (* name of the defined function *)
-        defs: ('info, 'ienv) sizefun Ident.Env.t;
+        defs: sizefun Ident.Env.t;
         (* the set of mutually recursive function definitions *) 
       }
 
-  (* to do: replace the last three entries which refers to the source *)
-  (* by a functional value *)
-  (*
-          | Vnode of
-      { s: ('info, 'ienv) state;
-        step : ('info, 'ienv) state -> ('info, 'ienv) value ->
-               (('info, 'ienv) value * ('info, 'ienv) state) result }
-  | Vsizefun of { sizes: int list option;
-                   f : int -> ('info, 'ienv) value }
-   *)
-
 and 'a array =
-  | Vflat : 'a Array.t -> 'a array
-  | Vmap : 'a map -> 'a array
+  | Vflat of 'a Array.t
+  | Vmap of 'a map
 
 (* bounded maps *)
 (* [get x i = v if x.left <= i <= right then x i
                   else match otherwise with | None -> error 
                                             | Some(x) -> get x i *)
 and 'a map =
   { m_length : int; m_u : int -> 'a result }
-
-(* a size parameterized expression - f <n1,...,nk> = e *)
-and ('info, 'ienv) sizefun = 
-  { s_params: Ident.t list; 
-    s_body: ('info, 'ienv) Zelus.exp; 
-    s_genv: ('info, 'ienv) pvalue Genv.genv; 
-    s_env: ('info, 'ienv) pvalue star ientry Ident.Env.t }
-
-(* a functional value - [fun|node] x1 ... xn -> e *)
-and ('info, 'ienv) closure =
-  { c_funexp : ('info, 'ienv) Zelus.funexp;
-    c_genv: ('info, 'ienv) pvalue Genv.genv;
-    c_env: ('info, 'ienv) pvalue star ientry Ident.Env.t }
-
+
+and sizefun = int -> value
+
 (* instance of a node *)
-and ('info, 'ienv) instance =
-  { init : ('info, 'ienv) state; (* current state *)
-    step : ('info, 'ienv) closure; (* step function *)
+and instance =
+  { tkind: Zelus.tkind; (* discrete only or discrete/continuous-time state *)
+    init : state; (* current state *)
+    step : state -> value -> (value * state) result; (* step function *)
   }
 
-and ('info, 'ienv) state =
+and state =
   | Sbot 
   | Snil 
   | Sempty 
-  | Sval of ('info, 'ienv) value
-  | Sstatic of ('info, 'ienv) pvalue
-  | Slist of ('info, 'ienv) state list
-  | Sopt of ('info, 'ienv) value option
-  | Sinstance of ('info, 'ienv) instance
-  | Scstate of { pos : ('info, 'ienv) value; der : ('info, 'ienv) value }
-  | Szstate of { zin : bool; zout : ('info, 'ienv) value }
+  | Sval of value
+  | Sstatic of pvalue
+  | Slist of state list
+  | Sopt of value option
+  | Sinstance of instance
+  | Scstate of { pos : value; der : value }
+  | Szstate of { zin : bool; zout : value }
   | Shorizon of { zin : bool; horizon : float }
   | Speriod of
       { zin : bool; phase : float; period : float; horizon : float }
   (* environment of values *)
-  | Senv of ('info, 'ienv) value ientry Ident.Env.t
+  | Senv of value ientry Ident.Env.t
 
 (*
-type ('a, 's) costream =
+  Intuition: a expression is interpreted as a value of type:
+
+  type ('a, 's) costream =
   | CoF : { init : 's;
             step : 's -> ('a * 's) option } ->
           ('a, 's) costream
 
-type ('a, 'b, 's) node =
+  A functional value, combinatorial or stateful is interpreted as a value of type:
+
+  type ('a, 'b, 's) node =
   | CoFun : ('a list -> 'b option) -> ('a, 'b, 's) node
   | 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".
+*)