From 9ad3d2155a5a1268365a4c8ba7e873e898bd0230 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Thu, 3 Mar 2022 10:31:52 +0100
Subject: [PATCH 1/5] Get started.

---
 src/Makefile       |  2 +-
 src/lang/term.ml   |  2 +-
 src/lang/termDB.ml | 23 +++++++++++++++++++++++
 3 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 src/lang/termDB.ml

diff --git a/src/Makefile b/src/Makefile
index 258659422c..c5d274755a 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -261,7 +261,7 @@ liquidsoap_sources = \
 
 liquidsoap_sources += \
 	lang/type.ml lang/repr.ml lang/typing.ml \
-	lang/profiler.ml lang/term.ml lang/value.ml \
+	lang/profiler.ml lang/term.ml lang/termDB.ml lang/value.ml \
 	lang/lang_encoder.ml $(lang_encoders) \
 	lang/environment.ml lang/typechecking.ml \
 	lang/evaluation.ml lang/error.ml \
diff --git a/src/lang/term.ml b/src/lang/term.ml
index e5cfa0c09c..854ca7260d 100644
--- a/src/lang/term.ml
+++ b/src/lang/term.ml
@@ -321,7 +321,7 @@ and pattern =
   | PTuple of pattern list  (** a tuple *)
   | PList of (pattern list * string option * pattern list) (* a list *)
   | PMeth of (pattern option * (string * pattern option) list)
-(* a value with methods *)
+      (** a value with methods *)
 
 type term = t
 
diff --git a/src/lang/termDB.ml b/src/lang/termDB.ml
new file mode 100644
index 0000000000..0cbde2b668
--- /dev/null
+++ b/src/lang/termDB.ml
@@ -0,0 +1,23 @@
+(*****************************************************************************
+
+  Liquidsoap, a programmable audio stream generator.
+  Copyright 2003-2022 Savonet team
+
+  This program is free software; you can redistribute it and/or modify
+  it under the terms of the GNU General Public License as published by
+  the Free Software Foundation; either version 2 of the License, or
+  (at your option) any later version.
+
+  This program is distributed in the hope that it will be useful,
+  but WITHOUT ANY WARRANTY; without even the implied warranty of
+  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+  GNU General Public License for more details, fully stated in the COPYING
+  file at the root of the liquidsoap distribution.
+
+  You should have received a copy of the GNU General Public License
+  along with this program; if not, write to the Free Software
+  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301  USA
+
+ *****************************************************************************)
+
+(** Optimized representation of terms with de Bruijn indices. *)

From d16063d3a5f6bbcb390d91e058c98a6cde13fb45 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Thu, 3 Mar 2022 15:33:53 +0100
Subject: [PATCH 2/5] Progressing.

---
 src/Makefile             |   2 +-
 src/lang/evaluation.ml   |  11 +--
 src/lang/runtime.ml      |   4 +-
 src/lang/term.ml         |   1 +
 src/lang/termDB.ml       |  39 ++++++++++
 src/lang/typechecking.ml | 140 ++++++++++++++++++++++--------------
 src/lang/value.ml        | 152 +++++++++++++++++----------------------
 7 files changed, 202 insertions(+), 147 deletions(-)

diff --git a/src/Makefile b/src/Makefile
index c5d274755a..1439f6c7e7 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -290,7 +290,7 @@ export OCAMLPATH := $(OCAMLPATH)
 
 OCAMLDEP_FLAGS = $(patsubst %,-I %,$(INCDIRS))
 OCAML_CFLAGS = -thread $(OCAMLDEP_FLAGS)
-_OCAML_CFLAGS = $(liquidsoap_ocamlcflags)
+_OCAML_CFLAGS = $(liquidsoap_ocamlcflags) -w -40-42
 _OCAML_LFLAGS = $(liquidsoap_ocamllflags)
 
 liquidsoap_mly = $(wildcard $(liquidsoap_sources:.ml=.mly))
diff --git a/src/lang/evaluation.ml b/src/lang/evaluation.ml
index b71b585ba0..6af1bab606 100644
--- a/src/lang/evaluation.ml
+++ b/src/lang/evaluation.ml
@@ -106,7 +106,7 @@ let rec eval_pat pat v =
   in
   aux [] pat v
 
-let rec eval ~env tm =
+let rec eval ~env (tm : TermDB.t) : Value.t =
   let env = (env : Value.lazy_env) in
   let prepare_fun fv p env =
     (* Unlike OCaml we always evaluate default values, and we do that early. I
@@ -132,6 +132,8 @@ let rec eval ~env tm =
     in
     (p, env)
   in
+  let mk v = { Value.pos = tm.t.Type.pos; Value.value = v } in
+  (*
   let mk v =
     (* Ensure that the kind computed at runtime for sources will agree with
        the typing. *)
@@ -176,7 +178,8 @@ let rec eval ~env tm =
       | _ -> ());
     { Value.pos = tm.t.Type.pos; Value.value = v }
   in
-  match tm.term with
+  *)
+  match tm with
     | Ground g -> mk (Value.Ground g)
     | Encoder (e, p) ->
         let pos = tm.t.Type.pos in
@@ -465,8 +468,8 @@ let toplevel_add (doc, params, methods) pat ~t v =
         ((generalized, t), v))
     (eval_pat pat v)
 
-let rec eval_toplevel ?(interactive = false) t =
-  match t.term with
+let rec eval_toplevel ?(interactive = false) (t : TermDB.t) =
+  match t with
     | Let { doc = comment; gen = generalized; replace; pat; def; body } ->
         let def_t, def =
           if not replace then (def.t, eval def)
diff --git a/src/lang/runtime.ml b/src/lang/runtime.ml
index d558d19fd3..86c7e75c30 100644
--- a/src/lang/runtime.ml
+++ b/src/lang/runtime.ml
@@ -28,14 +28,14 @@ let type_and_run ~throw ~lib ast =
   Clock.collect_after (fun () ->
       if Lazy.force Term.debug then Printf.eprintf "Type checking...\n%!";
       (* Type checking *)
-      Typechecking.check ~throw ~ignored:true ast;
+      let ast' = Typechecking.check ~throw ~ignored:true ast in
 
       if Lazy.force Term.debug then
         Printf.eprintf "Checking for unused variables...\n%!";
       (* Check for unused variables, relies on types *)
       Term.check_unused ~throw ~lib ast;
       if Lazy.force Term.debug then Printf.eprintf "Evaluating...\n%!";
-      ignore (Evaluation.eval_toplevel ast))
+      ignore (Evaluation.eval_toplevel ast'))
 
 (** {1 Error reporting} *)
 
diff --git a/src/lang/term.ml b/src/lang/term.ml
index 854ca7260d..af22dedfae 100644
--- a/src/lang/term.ml
+++ b/src/lang/term.ml
@@ -311,6 +311,7 @@ and in_term =
    * variables occurring in the function. It is used to
    * restrict the environment captured when a closure is
    * formed. *)
+  (* TODO: remove Vars.t and update above comment. *)
   | Fun of Vars.t * (string * string * Type.t * t option) list * t
   | RFun of string * Vars.t * (string * string * Type.t * t option) list * t
 
diff --git a/src/lang/termDB.ml b/src/lang/termDB.ml
index 0cbde2b668..91892eb25e 100644
--- a/src/lang/termDB.ml
+++ b/src/lang/termDB.ml
@@ -21,3 +21,42 @@
  *****************************************************************************)
 
 (** Optimized representation of terms with de Bruijn indices. *)
+
+module Ground = Term.Ground
+
+type pos = Pos.t
+
+(* No need to duplicate, we simply ignore variable names. *)
+type pattern = Term.pattern
+
+type t =
+  | Ground of Ground.t
+  | Encoder of encoder
+  | List of t list
+  | Tuple of t list
+  | Null
+  | Meth of string * t * t (* TODO: have an hashtbl of methods *)
+  | Invoke of t * string
+  | Open of t * t
+  | Let of let_t
+  | Var of int
+  | Seq of t * t
+  (* TODO: we should pre-compute applications when the type is fully known (be
+     careful of subtyping!) *)
+  | App of t * (string * t) list
+  | Fun of (string * t option) list * t
+  | RFun of (string * t option) list * t
+
+and let_t = {
+  replace : bool;
+  (* whether the definition replaces a previously existing one (keeping methods) *)
+  pat : pattern;
+  def : t;
+  body : t;
+}
+
+(** Parameters for encoders. *)
+and encoder_params = (string * [ `Term of t | `Encoder of encoder ]) list
+
+(** A formal encoder. *)
+and encoder = string * encoder_params
diff --git a/src/lang/typechecking.ml b/src/lang/typechecking.ml
index 13e47dad1e..1aae801c2d 100644
--- a/src/lang/typechecking.ml
+++ b/src/lang/typechecking.ml
@@ -120,14 +120,17 @@ let rec type_of_pat ~level ~pos = function
       in
       (env, ty)
 
-(* Type-check an expression. *)
-let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
+(** Type-check an expression. In passing, we also produce an optimized
+    representation of the term. *)
+let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
+    TermDB.t =
   let check = check ~throw in
   if !debug then Printf.printf "\n# %s : ?\n\n%!" (Term.to_string e);
   let check ?print_toplevel ~level ~env e =
-    check ?print_toplevel ~level ~env e;
+    let e' = check ?print_toplevel ~level ~env e in
     if !debug then
-      Printf.printf "\n# %s : %s\n\n%!" (Term.to_string e) (Type.to_string e.t)
+      Printf.printf "\n# %s : %s\n\n%!" (Term.to_string e) (Type.to_string e.t);
+    e'
   in
   (* The toplevel position of the (un-dereferenced) type is the actual parsing
      position of the value. When we synthesize a type against which the type of
@@ -138,34 +141,43 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
   let mkg t = mk (Type.Ground t) in
   let check_fun ~proto ~env e body =
     let base_check = check ~level ~env in
-    let proto_t, env =
+    let proto', proto_t, env =
       List.fold_left
-        (fun (p, env) -> function
+        (fun (proto', p, env) -> function
           | lbl, var, kind, None ->
               update_level level kind;
-              ((false, lbl, kind) :: p, (var, ([], kind)) :: env)
+              ( (var, None) :: proto',
+                (false, lbl, kind) :: p,
+                (var, ([], kind)) :: env )
           | lbl, var, kind, Some v ->
               update_level level kind;
-              base_check v;
+              let v' = base_check v in
               v.t <: kind;
-              ((true, lbl, kind) :: p, (var, ([], kind)) :: env))
-        ([], env) proto
+              ( (var, Some v') :: proto',
+                (true, lbl, kind) :: p,
+                (var, ([], kind)) :: env ))
+        ([], [], env) proto
     in
     let proto_t = List.rev proto_t in
-    check ~level ~env body;
-    e.t >: mk (Type.Arrow (proto_t, body.t))
+    let body' = check ~level ~env body in
+    e.t >: mk (Type.Arrow (proto_t, body.t));
+    (proto', body')
   in
   match e.term with
-    | Ground g -> e.t >: mkg (Ground.to_type g)
+    | Ground g ->
+        e.t >: mkg (Ground.to_type g);
+        Ground g
     | Encoder f ->
         (* Ensure that we only use well-formed terms. *)
-        let rec check_enc (_, p) =
-          List.iter
-            (function
-              | _, `Term t -> check ~level ~env t | _, `Encoder e -> check_enc e)
-            p
+        let rec check_enc (enc, p) : TermDB.encoder =
+          ( enc,
+            List.map
+              (function
+                | p, `Term t -> (p, `Term (check ~level ~env t))
+                | p, `Encoder e -> (p, `Encoder (check_enc e)))
+              p )
         in
-        check_enc f;
+        let f' = check_enc f in
         let t =
           try Lang_encoder.type_of_encoder ~pos:e.t.Type.pos f
           with Not_found ->
@@ -174,23 +186,29 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
               (Unsupported_format (pos, Term.to_string e))
               bt
         in
-        e.t >: t
+        e.t >: t;
+        Encoder f'
     | List l ->
-        List.iter (fun x -> check ~level ~env x) l;
+        let l' = List.map (fun x -> check ~level ~env x) l in
         let t = Type.var ~level ?pos () in
         List.iter (fun e -> e.t <: t) l;
-        e.t >: mk Type.(List { t; json_repr = `Tuple })
+        e.t >: mk Type.(List { t; json_repr = `Tuple });
+        List l'
     | Tuple l ->
-        List.iter (fun a -> check ~level ~env a) l;
-        e.t >: mk (Type.Tuple (List.map (fun a -> a.t) l))
-    | Null -> e.t >: mk (Type.Nullable (Type.var ~level ?pos ()))
+        let l' = List.map (fun a -> check ~level ~env a) l in
+        e.t >: mk (Type.Tuple (List.map (fun a -> a.t) l));
+        Tuple l'
+    | Null ->
+        e.t >: mk (Type.Nullable (Type.var ~level ?pos ()));
+        Null
     | Cast (a, t) ->
-        check ~level ~env a;
+        let a' = check ~level ~env a in
         a.t <: t;
-        e.t >: t
+        e.t >: t;
+        a'
     | Meth (l, a, b) ->
-        check ~level ~env a;
-        check ~level ~env b;
+        let a' = check ~level ~env a in
+        let b' = check ~level ~env b in
         e.t
         >: mk
              (Type.Meth
@@ -200,9 +218,10 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
                     doc = "";
                     json_name = None;
                   },
-                  b.t ))
+                  b.t ));
+        Meth (l, a', b')
     | Invoke (a, l) ->
-        check ~level ~env a;
+        let a' = check ~level ~env a in
         let rec aux t =
           match (Type.deref t).Type.descr with
             | Type.(Meth ({ meth = l'; scheme = generalized, b }, c)) ->
@@ -227,9 +246,10 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
                            y ));
                 x
         in
-        e.t >: aux a.t
+        e.t >: aux a.t;
+        Invoke (a', l)
     | Open (a, b) ->
-        check ~level ~env a;
+        let a' = check ~level ~env a in
         a.t <: mk Type.unit;
         let rec aux env t =
           match (Type.deref t).Type.descr with
@@ -238,22 +258,23 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
             | _ -> env
         in
         let env = aux env a.t in
-        check ~level ~env b;
-        e.t >: b.t
+        let b' = check ~level ~env b in
+        e.t >: b.t;
+        Open (a', b')
     | Seq (a, b) ->
-        check ~env ~level a;
+        let a' = check ~env ~level a in
         if not (can_ignore a.t) then throw (Ignored a);
-        check ~print_toplevel ~level ~env b;
-        e.t >: b.t
-    | App (a, l) -> (
-        check ~level ~env a;
-        List.iter (fun (_, b) -> check ~env ~level b) l;
-
+        let b' = check ~print_toplevel ~level ~env b in
+        e.t >: b.t;
+        Seq (a', b')
+    | App (a, l) ->
+        let a' = check ~level ~env a in
+        let l' = List.map (fun (l, b) -> (l, check ~env ~level b)) l in
         (* If [a] is known to have a function type, manually dig through it for
            better error messages. Otherwise generate its type and unify -- in
            that case the optionality can't be guessed and mandatory is the
            default. *)
-        match (Type.demeth a.t).Type.descr with
+        (match (Type.demeth a.t).Type.descr with
           | Type.Arrow (ap, t) ->
               (* Find in l the first arg labeled lbl, return it together with the
                  remaining of the list. *)
@@ -291,22 +312,35 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
               e.t >: t
           | _ ->
               let p = List.map (fun (lbl, b) -> (false, lbl, b.t)) l in
-              a.t <: Type.make (Type.Arrow (p, e.t)))
-    | Fun (_, proto, body) -> check_fun ~proto ~env e body
+              a.t <: Type.make (Type.Arrow (p, e.t)));
+        App (a', l')
+    | Fun (_, proto, body) ->
+        let proto, body = check_fun ~proto ~env e body in
+        Fun (proto, body)
     | RFun (x, _, proto, body) ->
         let env = (x, ([], e.t)) :: env in
-        check_fun ~proto ~env e body
+        let proto, body = check_fun ~proto ~env e body in
+        RFun (proto, body)
     | Var var ->
         let generalized, orig =
           try List.assoc var env
           with Not_found -> raise (Unbound (e.t.Type.pos, var))
         in
+        let list_index p l =
+          let rec aux i = function
+            | x :: l -> if p x then i else aux (i + 1) l
+            | [] -> raise Not_found
+          in
+          aux 0 l
+        in
+        let i = list_index (fun (x, _) -> x = var) env in
         e.t >: Typing.instantiate ~level ~generalized orig;
         if Lazy.force Term.debug then
           Printf.eprintf "Instantiate %s : %s becomes %s\n" var
-            (Type.to_string orig) (Type.to_string e.t)
+            (Type.to_string orig) (Type.to_string e.t);
+        Var i
     | Let ({ pat; replace; def; body; _ } as l) ->
-        check ~level:(level + 1) ~env def;
+        let def' = check ~level:(level + 1) ~env def in
         let generalized =
           (* Printf.printf "generalize at %d: %B\n\n!" level (value_restriction def); *)
           if value_restriction def then fst (generalize ~level def.t) else []
@@ -349,20 +383,22 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e =
                  if l >= max then name else name ^ String.make (max - l) ' ')
                 (fun f t -> Repr.print_scheme f (generalized, t))
                 def.t);
-        check ~print_toplevel ~level ~env body;
-        e.t >: body.t
+        let body' = check ~print_toplevel ~level ~env body in
+        e.t >: body.t;
+        Let { replace = l.replace; pat = l.pat; def = def'; body = body' }
 
 (* The simple definition for external use. *)
 let check ?(ignored = false) ~throw e =
   let print_toplevel = !Configure.display_types in
   try
     let env = Environment.default_typing_environment () in
-    check ~print_toplevel ~throw ~level:0 ~env e;
+    let e' = check ~print_toplevel ~throw ~level:0 ~env e in
     if print_toplevel && (Type.deref e.t).Type.descr <> Type.unit then
       add_task (fun () ->
           Format.printf "@[<2>-     :@ %a@]@." Repr.print_type e.t);
     if ignored && not (can_ignore e.t) then throw (Ignored e);
-    pop_tasks ()
+    pop_tasks ();
+    e'
   with e ->
     let bt = Printexc.get_raw_backtrace () in
     pop_tasks ();
diff --git a/src/lang/value.ml b/src/lang/value.ml
index 013aa5d221..371d68e20e 100644
--- a/src/lang/value.ml
+++ b/src/lang/value.ml
@@ -25,14 +25,7 @@
 (** Ground values. *)
 module Ground = Term.Ground
 
-type t = { pos : Pos.Option.t; value : in_value }
-
-and env = (string * t) list
-
-(* Some values have to be lazy in the environment because of recursive functions. *)
-and lazy_env = (string * t Lazy.t) list
-
-and in_value =
+type t =
   | Ground of Ground.t
   | Source of Source.source
   | Encoder of Encoder.format
@@ -51,63 +44,64 @@ and in_value =
      doesn't capture anything in the environment. *)
   | FFI of (string * string * t option) list * (env -> t)
 
+and env = (string * t) list
+
+(* Some values have to be lazy in the environment because of recursive functions. *)
+and lazy_env = (string * t Lazy.t) list
+
 type encoder_params = (string * [ `Value of t | `Encoder of encoder ]) list
 
 (** The type of evaluated encoder terms. *)
 and encoder = string * encoder_params
 
-let unit : in_value = Tuple []
+let unit : t = Tuple []
 
 let string_of_float f =
   let s = string_of_float f in
   if s.[String.length s - 1] = '.' then s ^ "0" else s
 
-let rec print_value v =
-  match v.value with
-    | Ground g -> Ground.to_string g
-    | Source _ -> "<source>"
-    | Encoder e -> Encoder.string_of_format e
-    | List l -> "[" ^ String.concat ", " (List.map print_value l) ^ "]"
-    | Ref a -> Printf.sprintf "ref(%s)" (print_value !a)
-    | Tuple l -> "(" ^ String.concat ", " (List.map print_value l) ^ ")"
-    | Null -> "null"
-    | Meth (l, v, e) when Lazy.force Term.debug ->
-        print_value e ^ ".{" ^ l ^ "=" ^ print_value v ^ "}"
-    | Meth _ ->
-        let rec split e =
-          match e.value with
-            | Meth (l, v, e) ->
-                let m, e = split e in
-                ((l, v) :: m, e)
-            | _ -> ([], e)
-        in
-        let m, e = split v in
-        let m =
-          List.rev m
-          |> List.map (fun (l, v) -> l ^ " = " ^ print_value v)
-          |> String.concat ", "
-        in
-        let e =
-          match e.value with Tuple [] -> "" | _ -> print_value e ^ "."
-        in
-        e ^ "{" ^ m ^ "}"
-    | Fun ([], _, x) when Term.is_ground x -> "{" ^ Term.to_string x ^ "}"
-    | Fun (l, _, x) when Term.is_ground x ->
-        let f (label, _, value) =
-          match (label, value) with
-            | "", None -> "_"
-            | "", Some v -> Printf.sprintf "_=%s" (print_value v)
-            | label, Some v -> Printf.sprintf "~%s=%s" label (print_value v)
-            | label, None -> Printf.sprintf "~%s=_" label
-        in
-        let args = List.map f l in
-        Printf.sprintf "fun (%s) -> %s" (String.concat "," args)
-          (Term.to_string x)
-    | Fun _ | FFI _ -> "<fun>"
+let rec print_value = function
+  | Ground g -> Ground.to_string g
+  | Source _ -> "<source>"
+  | Encoder e -> Encoder.string_of_format e
+  | List l -> "[" ^ String.concat ", " (List.map print_value l) ^ "]"
+  | Ref a -> Printf.sprintf "ref(%s)" (print_value !a)
+  | Tuple l -> "(" ^ String.concat ", " (List.map print_value l) ^ ")"
+  | Null -> "null"
+  | Meth (l, v, e) when Lazy.force Term.debug ->
+      print_value e ^ ".{" ^ l ^ "=" ^ print_value v ^ "}"
+  | Meth _ as v ->
+      let rec split = function
+        | Meth (l, v, e) ->
+            let m, e = split e in
+            ((l, v) :: m, e)
+        | e -> ([], e)
+      in
+      let m, e = split v in
+      let m =
+        List.rev m
+        |> List.map (fun (l, v) -> l ^ " = " ^ print_value v)
+        |> String.concat ", "
+      in
+      let e = match e with Tuple [] -> "" | _ -> print_value e ^ "." in
+      e ^ "{" ^ m ^ "}"
+  | Fun ([], _, x) when Term.is_ground x -> "{" ^ Term.to_string x ^ "}"
+  | Fun (l, _, x) when Term.is_ground x ->
+      let f (label, _, value) =
+        match (label, value) with
+          | "", None -> "_"
+          | "", Some v -> Printf.sprintf "_=%s" (print_value v)
+          | label, Some v -> Printf.sprintf "~%s=%s" label (print_value v)
+          | label, None -> Printf.sprintf "~%s=_" label
+      in
+      let args = List.map f l in
+      Printf.sprintf "fun (%s) -> %s" (String.concat "," args)
+        (Term.to_string x)
+  | Fun _ | FFI _ -> "<fun>"
 
 (** Find a method in a value. *)
 let rec invoke x l =
-  match x.value with
+  match x with
     | Meth (l', y, _) when l' = l -> y
     | Meth (_, _, x) -> invoke x l
     | _ -> failwith ("Could not find method " ^ l ^ " of " ^ print_value x)
@@ -116,23 +110,20 @@ let rec invoke x l =
 let rec invokes x = function l :: ll -> invokes (invoke x l) ll | [] -> x
 
 let split_meths e =
-  let rec aux hide e =
-    match e.value with
-      | Meth (l, v, e) ->
-          if List.mem l hide then aux hide e
-          else (
-            let m, e = aux (l :: hide) e in
-            ((l, v) :: m, e))
-      | _ -> ([], e)
+  let rec aux hide = function
+    | Meth (l, v, e) ->
+        if List.mem l hide then aux hide e
+        else (
+          let m, e = aux (l :: hide) e in
+          ((l, v) :: m, e))
+    | _ -> ([], e)
   in
   aux [] e
 
-let rec demeth v = match v.value with Meth (_, _, v) -> demeth v | _ -> v
+let rec demeth = function Meth (_, _, v) -> demeth v | v -> v
 
 let rec remeth t u =
-  match t.value with
-    | Meth (l, v, t) -> { t with value = Meth (l, v, remeth t u) }
-    | _ -> u
+  match t with Meth (l, v, t) -> Meth (l, v, remeth t u) | _ -> u
 
 let compare a b =
   let rec aux = function
@@ -159,7 +150,7 @@ let compare a b =
     let a' = demeth a in
     let b' = demeth b in
     (* For records, we compare the list ["label", field; ..] of common fields. *)
-    if a'.value = Tuple [] && b'.value = Tuple [] then (
+    if a' = Tuple [] && b' = Tuple [] then (
       let r a =
         let m, _ = split_meths a in
         m
@@ -177,28 +168,14 @@ let compare a b =
       let b = List.sort (fun x x' -> Stdlib.compare (fst x) (fst x')) b in
       let a =
         Tuple
-          (List.map
-             (fun (lbl, v) ->
-               {
-                 pos = None;
-                 value =
-                   Tuple [{ pos = None; value = Ground (Ground.String lbl) }; v];
-               })
-             a)
+          (List.map (fun (lbl, v) -> Tuple [Ground (Ground.String lbl); v]) a)
       in
       let b =
         Tuple
-          (List.map
-             (fun (lbl, v) ->
-               {
-                 pos = None;
-                 value =
-                   Tuple [{ pos = None; value = Ground (Ground.String lbl) }; v];
-               })
-             b)
+          (List.map (fun (lbl, v) -> Tuple [Ground (Ground.String lbl); v]) b)
       in
       aux (a, b))
-    else aux (a'.value, b'.value)
+    else aux (a', b')
   in
   compare a b
 
@@ -217,14 +194,13 @@ module type AbstractDef = Term.AbstractDef
 module MkAbstractFromTerm (Term : Term.Abstract) = struct
   include Term
 
-  let to_value c = { pos = None; value = Ground (to_ground c) }
+  let to_value c = Ground (to_ground c)
 
-  let of_value t =
-    match t.value with
-      | Ground g when is_ground g -> of_ground g
-      | _ -> assert false
+  let of_value = function
+    | Ground g when is_ground g -> of_ground g
+    | _ -> assert false
 
-  let is_value t = match t.value with Ground g -> is_ground g | _ -> false
+  let is_value = function Ground g -> is_ground g | _ -> false
 end
 
 module MkAbstract (Def : AbstractDef) = struct

From 3b88c32e1469a9b70dc393908159c3ea9e57fff8 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Fri, 4 Mar 2022 09:20:52 +0100
Subject: [PATCH 3/5] More.

---
 src/Makefile             |  14 ++---
 src/lang/environment.ml  |   5 +-
 src/lang/evaluation.ml   | 116 +++++++++++++++++----------------------
 src/lang/lang_encoder.ml |   4 +-
 src/lang/term.ml         |  19 +++----
 src/lang/termDB.ml       |   6 +-
 src/lang/typechecking.ml |   7 ++-
 src/lang/value.ml        |  13 +++++
 8 files changed, 90 insertions(+), 94 deletions(-)

diff --git a/src/Makefile b/src/Makefile
index 1439f6c7e7..fbc5c22b4e 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -127,13 +127,13 @@ encoders = \
 	$(if $(W_TAGLIB),encoder/taglib_id3v2.ml) \
 	$(if $(W_GSTREAMER),encoder/gstreamer_encoder.ml)
 
-lang_encoders = \
-	lang_encoders/lang_avi.ml lang_encoders/lang_external_encoder.ml lang_encoders/lang_fdkaac.ml \
-	lang_encoders/lang_ffmpeg.ml $(if $(W_FFMPEG),lang_encoders/lang_ffmpeg_opt.ml) \
-	lang_encoders/lang_flac.ml lang_encoders/lang_gstreamer.ml \
-	lang_encoders/lang_mp3.ml lang_encoders/lang_opus.ml lang_encoders/lang_shine.ml \
-	lang_encoders/lang_speex.ml lang_encoders/lang_theora.ml lang_encoders/lang_vorbis.ml \
-	lang_encoders/lang_wav.ml lang_encoders/lang_ogg.ml
+# lang_encoders = \
+	# lang_encoders/lang_avi.ml lang_encoders/lang_external_encoder.ml lang_encoders/lang_fdkaac.ml \
+	# lang_encoders/lang_ffmpeg.ml $(if $(W_FFMPEG),lang_encoders/lang_ffmpeg_opt.ml) \
+	# lang_encoders/lang_flac.ml lang_encoders/lang_gstreamer.ml \
+	# lang_encoders/lang_mp3.ml lang_encoders/lang_opus.ml lang_encoders/lang_shine.ml \
+	# lang_encoders/lang_speex.ml lang_encoders/lang_theora.ml lang_encoders/lang_vorbis.ml \
+	# lang_encoders/lang_wav.ml lang_encoders/lang_ogg.ml
 
 encoder_formats = \
 	encoder_formats.ml \
diff --git a/src/lang/environment.ml b/src/lang/environment.ml
index 96ea05a135..a664e63665 100644
--- a/src/lang/environment.ml
+++ b/src/lang/environment.ml
@@ -75,7 +75,7 @@ let add_builtin ?(override = false) ?(register = true) ?doc name ((g, t), v) =
               in
               (* Update value for x.l1...li. *)
               let value = Value.Meth (l, lv, v) in
-              ((vg, t), { Value.pos = v.Value.pos; value })
+              ((vg, t), value)
           | [] -> ((g, t), v)
         in
         let (g, t), v = aux [] ll in
@@ -108,8 +108,7 @@ let add_module name =
           ignore (Value.invoke e l);
           failwith ("Module " ^ String.concat "." name ^ " already exists")
         with _ -> ()));
-  add_builtin ~register:false name
-    (([], Type.make Type.unit), { Value.pos = None; value = Value.unit })
+  add_builtin ~register:false name (([], Type.make Type.unit), Value.unit)
 
 (* Builtins are only used for documentation now. *)
 let builtins = (builtins :> Doc.item)
diff --git a/src/lang/evaluation.ml b/src/lang/evaluation.ml
index 6af1bab606..3ce1c4aa16 100644
--- a/src/lang/evaluation.ml
+++ b/src/lang/evaluation.ml
@@ -41,21 +41,14 @@ let remove_first filter =
 let rec rev_map_append f l1 l2 =
   match l1 with [] -> l2 | a :: l -> rev_map_append f l (f a :: l2)
 
-let lookup (env : Value.lazy_env) var =
-  try Lazy.force (List.assoc var env)
-  with Not_found ->
-    failwith
-      (Printf.sprintf "Internal error: variable %s not in environment." var)
-
 let rec eval_pat pat v =
-  let rec aux env pat v =
+  let rec aux env pat (v : Value.t) =
     match (pat, v) with
       | PVar x, v -> (x, v) :: env
-      | PTuple pl, { Value.value = Value.Tuple l } ->
-          List.fold_left2 aux env pl l
+      | PTuple pl, Tuple l -> List.fold_left2 aux env pl l
       (* The parser parses [x,y,z] as PList ([], None, l) *)
-      | PList (([] as l'), (None as spread), l), { Value.value = Value.List lv }
-      | PList (l, spread, l'), { Value.value = Value.List lv } ->
+      | PList (([] as l'), (None as spread), l), List lv
+      | PList (l, spread, l'), List lv ->
           let ln = List.length l in
           let ln' = List.length l' in
           let lvn = List.length lv in
@@ -84,9 +77,7 @@ let rec eval_pat pat v =
             List.map snd (List.filter (fun (lbl, _) -> lbl = `Second) lv)
           in
           let spread_env =
-            match spread with
-              | None -> []
-              | Some s -> [([s], Value.{ v with value = List ls })]
+            match spread with None -> [] | Some s -> [([s], Value.List ls)]
           in
           List.fold_left2 aux [] l' ll'
           @ spread_env @ env
@@ -106,8 +97,7 @@ let rec eval_pat pat v =
   in
   aux [] pat v
 
-let rec eval ~env (tm : TermDB.t) : Value.t =
-  let env = (env : Value.lazy_env) in
+let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
   let prepare_fun fv p env =
     (* Unlike OCaml we always evaluate default values, and we do that early. I
        think the only reason is homogeneity with FFI, which are declared with
@@ -115,7 +105,7 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
     let p =
       List.map
         (function
-          | lbl, var, _, Some v -> (lbl, var, Some (eval ~env v))
+          | lbl, var, _, Some v -> (lbl, var, Some (eval env v))
           | lbl, var, _, None -> (lbl, var, None))
         p
     in
@@ -132,26 +122,23 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
     in
     (p, env)
   in
-  let mk v = { Value.pos = tm.t.Type.pos; Value.value = v } in
-  (*
-  let mk v =
-    (* Ensure that the kind computed at runtime for sources will agree with
-       the typing. *)
-    (match (Type.deref tm.t).Type.descr with
-      | Type.Constr
-          { Type.constructor = "source"; params = [(Type.Invariant, k)] } -> (
+  (* Ensure that the kind computed at runtime for sources will agree with the
+     typing. *)
+  let cast v t =
+    match (Type.deref t).descr with
+      | Constr { Type.constructor = "source"; params = [(Type.Invariant, k)] }
+        -> (
           let frame_content_of_t t =
             match (Type.deref t).Type.descr with
-              | Type.Var _ -> `Any
-              | Type.Constr { Type.constructor; params = [(_, t)] } -> (
+              | Var _ -> `Any
+              | Constr { Type.constructor; params = [(_, t)] } -> (
                   match (Type.deref t).Type.descr with
                     | Type.Ground (Type.Format fmt) -> `Format fmt
                     | Type.Var _ -> `Kind (Content.kind_of_string constructor)
-                    | _ -> failwith ("Unhandled content: " ^ Type.to_string tm.t)
-                  )
-              | Type.Constr { Type.constructor = "none" } ->
+                    | _ -> failwith ("Unhandled content: " ^ Type.to_string t))
+              | Constr { Type.constructor = "none" } ->
                   `Kind (Content.kind_of_string "none")
-              | _ -> failwith ("Unhandled content: " ^ Type.to_string tm.t)
+              | _ -> failwith ("Unhandled content: " ^ Type.to_string t)
           in
           let k = of_frame_kind_t k in
           let k =
@@ -163,7 +150,7 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
               }
           in
           let rec demeth = function
-            | Value.Meth (_, _, v) -> demeth v.Value.value
+            | Value.Meth (_, _, v) -> demeth v
             | v -> v
           in
           match demeth v with
@@ -171,17 +158,16 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
             | _ ->
                 raise
                   (Internal_error
-                     ( Option.to_list tm.t.Type.pos,
+                     ( Option.to_list t.Type.pos,
                        "term has type source but is not a source: "
-                       ^ Value.print_value
-                           { Value.pos = tm.t.Type.pos; Value.value = v } )))
-      | _ -> ());
-    { Value.pos = tm.t.Type.pos; Value.value = v }
+                       ^ Value.print_value v )))
+      | _ -> ()
   in
-  *)
   match tm with
-    | Ground g -> mk (Value.Ground g)
-    | Encoder (e, p) ->
+    | Ground g -> Ground g
+    | Encoder _ ->
+        (* | Encoder (e, p) -> *)
+        (*
         let pos = tm.t.Type.pos in
         let rec eval_param p =
           List.map
@@ -196,13 +182,16 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
         let enc : Value.encoder = (e, p) in
         let e = Lang_encoder.make_encoder ~pos tm enc in
         mk (Value.Encoder e)
-    | List l -> mk (Value.List (List.map (eval ~env) l))
-    | Tuple l -> mk (Value.Tuple (List.map (fun a -> eval ~env a) l))
-    | Null -> mk Value.Null
-    | Cast (e, _) ->
-        let e = eval ~env e in
-        mk e.Value.value
-    | Meth (l, u, v) -> mk (Value.Meth (l, eval ~env u, eval ~env v))
+*)
+        failwith "TODO"
+    | List l -> List (List.map (eval env) l)
+    | Tuple l -> Tuple (List.map (fun a -> eval env a) l)
+    | Null -> Null
+    | Cast (e, t) ->
+        let e = eval env e in
+        cast e t;
+        e
+    | Meth (l, u, v) -> Meth (l, eval env u, eval env v)
     | Invoke (t, l) ->
         let rec aux t =
           match t.Value.value with
@@ -211,22 +200,22 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
             | _ ->
                 raise
                   (Internal_error
-                     ( Option.to_list tm.t.Type.pos,
+                     ( [] (* TODO: can we find a relevant position ? *),
                        "invoked method `" ^ l ^ "` not found" ))
         in
-        aux (eval ~env t)
+        aux (eval env t)
     | Open (t, u) ->
-        let t = eval ~env t in
-        let rec aux env t =
-          match t.Value.value with
-            | Value.Meth (l, v, t) -> aux ((l, Lazy.from_val v) :: env) t
-            | Value.Tuple [] -> env
+        let t = eval env t in
+        let rec aux env (t : Value.t) =
+          match t with
+            | Meth (l, v, t) -> aux ((l, Lazy.from_val v) :: env) t
+            | Tuple [] -> env
             | _ -> assert false
         in
         let env = aux env t in
-        eval ~env u
+        eval env u
     | Let { pat; replace; def = v; body = b; _ } ->
-        let v = eval ~env v in
+        let v = eval env v in
         let penv =
           List.map
             (fun (ll, v) ->
@@ -241,14 +230,11 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
                     (x, Lazy.from_fun v)
                 | l :: ll ->
                     (* Add method ll with value v to t *)
-                    let rec meths ll v t =
-                      let mk ~pos value = { Value.pos; value } in
+                    let rec meths ll v t : Value.t =
                       match ll with
                         | [] -> assert false
-                        | [l] -> mk ~pos:tm.t.Type.pos (Value.Meth (l, v, t))
-                        | l :: ll ->
-                            mk ~pos:t.Value.pos
-                              (Value.Meth (l, meths ll v (Value.invoke t l), t))
+                        | [l] -> Meth (l, v, t)
+                        | l :: ll -> Meth (l, meths ll v (Value.invoke t l), t)
                     in
                     let v () =
                       let t = Lazy.force (List.assoc l env) in
@@ -263,15 +249,15 @@ let rec eval ~env (tm : TermDB.t) : Value.t =
             (eval_pat pat v)
         in
         let env = penv @ env in
-        eval ~env b
+        eval env b
     | Fun (fv, p, body) ->
         let p, env = prepare_fun fv p env in
-        mk (Value.Fun (p, env, body))
+        Fun (p, env, body)
     | RFun (x, fv, p, body) ->
         let p, env = prepare_fun fv p env in
         let rec v () =
           let env = (x, Lazy.from_fun v) :: env in
-          { Value.pos = tm.t.Type.pos; value = Value.Fun (p, env, body) }
+          Fun (p, env, body)
         in
         v ()
     | Var var -> lookup env var
diff --git a/src/lang/lang_encoder.ml b/src/lang/lang_encoder.ml
index af9351d0ae..f927aaedf7 100644
--- a/src/lang/lang_encoder.ml
+++ b/src/lang/lang_encoder.ml
@@ -40,10 +40,10 @@ let error ~pos msg =
               pos = (match pos with None -> [] | Some pos -> [pos]);
             })
 
-let generic_error (l, t) : exn =
+let generic_error (l, pos, t) : exn =
   match t with
     | `Value v ->
-        error ~pos:v.Value.pos
+        error ~pos
           (Printf.sprintf
              "unknown parameter name (%s) or invalid parameter value (%s)" l
              (Value.print_value v))
diff --git a/src/lang/term.ml b/src/lang/term.ml
index af22dedfae..e598ccfdeb 100644
--- a/src/lang/term.ml
+++ b/src/lang/term.ml
@@ -306,14 +306,9 @@ and in_term =
   | Seq of t * t
   | App of t * (string * t) list
   (* [fun ~l1:x1 .. ?li:(xi=defi) .. -> body] =
-   * [Fun (V, [(l1,x1,None)..(li,xi,Some defi)..], body)]
-   * The first component [V] is the list containing all
-   * variables occurring in the function. It is used to
-   * restrict the environment captured when a closure is
-   * formed. *)
-  (* TODO: remove Vars.t and update above comment. *)
-  | Fun of Vars.t * (string * string * Type.t * t option) list * t
-  | RFun of string * Vars.t * (string * string * Type.t * t option) list * t
+     [Fun (V, [(l1,x1,None)..(li,xi,Some defi)..], body)]. *)
+  | Fun of (string * string * Type.t * t option) list * t
+  | RFun of string * (string * string * Type.t * t option) list * t
 
 (* A recursive function, the first string is the name of the recursive
    variable. *)
@@ -379,7 +374,7 @@ let rec to_string v =
     | Meth (l, v, e) -> to_string e ^ ".{" ^ l ^ " = " ^ to_string v ^ "}"
     | Invoke (e, l) -> to_string e ^ "." ^ l
     | Open (m, e) -> "open " ^ to_string m ^ " " ^ to_string e
-    | Fun (_, [], v) when is_ground v -> "{" ^ to_string v ^ "}"
+    | Fun ([], v) when is_ground v -> "{" ^ to_string v ^ "}"
     | Fun _ | RFun _ -> "<fun>"
     | Var s -> s
     | App (hd, tl) ->
@@ -474,7 +469,7 @@ let rec free_vars tm =
         List.fold_left
           (fun v (_, t) -> Vars.union v (free_vars t))
           (free_vars hd) l
-    | RFun (_, fv, _, _) | Fun (fv, _, _) -> fv
+    | RFun (_, _, _) | Fun (_, _) -> failwith "TODO"
     | Let l ->
         Vars.union (free_vars l.def)
           (Vars.diff (free_vars l.body) (bound_vars_pat l.pat))
@@ -536,8 +531,8 @@ let check_unused ~throw ~lib tm =
       | App (hd, l) ->
           let v = check v hd in
           List.fold_left (fun v (_, t) -> check v t) v l
-      | RFun (_, arg, p, body) -> check v { tm with term = Fun (arg, p, body) }
-      | Fun (_, p, body) ->
+      | RFun (arg, p, body) -> check v { tm with term = Fun (p, body) }
+      | Fun (p, body) ->
           let v =
             List.fold_left
               (fun v -> function
diff --git a/src/lang/termDB.ml b/src/lang/termDB.ml
index 91892eb25e..c456f53860 100644
--- a/src/lang/termDB.ml
+++ b/src/lang/termDB.ml
@@ -35,6 +35,7 @@ type t =
   | List of t list
   | Tuple of t list
   | Null
+  | Cast of t * Type.t
   | Meth of string * t * t (* TODO: have an hashtbl of methods *)
   | Invoke of t * string
   | Open of t * t
@@ -56,7 +57,8 @@ and let_t = {
 }
 
 (** Parameters for encoders. *)
-and encoder_params = (string * [ `Term of t | `Encoder of encoder ]) list
+and encoder_params =
+  (string * [ `Term of pos option * t | `Encoder of encoder ]) list
 
 (** A formal encoder. *)
-and encoder = string * encoder_params
+and encoder = pos option * string * encoder_params
diff --git a/src/lang/typechecking.ml b/src/lang/typechecking.ml
index 1aae801c2d..deda59c47a 100644
--- a/src/lang/typechecking.ml
+++ b/src/lang/typechecking.ml
@@ -170,10 +170,11 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
     | Encoder f ->
         (* Ensure that we only use well-formed terms. *)
         let rec check_enc (enc, p) : TermDB.encoder =
-          ( enc,
+          ( e.t.pos,
+            enc,
             List.map
               (function
-                | p, `Term t -> (p, `Term (check ~level ~env t))
+                | p, `Term t -> (p, `Term (t.t.pos, check ~level ~env t))
                 | p, `Encoder e -> (p, `Encoder (check_enc e)))
               p )
         in
@@ -205,7 +206,7 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
         let a' = check ~level ~env a in
         a.t <: t;
         e.t >: t;
-        a'
+        Cast (a', t)
     | Meth (l, a, b) ->
         let a' = check ~level ~env a in
         let b' = check ~level ~env b in
diff --git a/src/lang/value.ml b/src/lang/value.ml
index 371d68e20e..0582dbb30a 100644
--- a/src/lang/value.ml
+++ b/src/lang/value.ml
@@ -179,6 +179,19 @@ let compare a b =
   in
   compare a b
 
+(** Operations on evaluation environments. *)
+module Env = struct
+  type nonrec t = t Lazy.t list
+
+  let lookup (env : t) var =
+    match List.nth_opt env var with
+      | Some v -> Lazy.force v
+      | None ->
+          failwith
+            (Printf.sprintf "Internal error: variable %d not in environment."
+               var)
+end
+
 (* Abstract values. *)
 
 module type Abstract = sig

From 7811ac007d3892bb7c28770f9dca0088456c62c7 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Fri, 4 Mar 2022 10:26:05 +0100
Subject: [PATCH 4/5] More.

---
 src/lang/evaluation.ml   | 62 ++++++++++++++--------------------------
 src/lang/term.ml         |  9 +++---
 src/lang/termDB.ml       | 25 +++++++++++++---
 src/lang/typechecking.ml | 35 ++++++++++++++++++++---
 src/lang/value.ml        | 16 +++++++----
 5 files changed, 87 insertions(+), 60 deletions(-)

diff --git a/src/lang/evaluation.ml b/src/lang/evaluation.ml
index 3ce1c4aa16..add5fd54b7 100644
--- a/src/lang/evaluation.ml
+++ b/src/lang/evaluation.ml
@@ -97,30 +97,14 @@ let rec eval_pat pat v =
   in
   aux [] pat v
 
-let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
-  let prepare_fun fv p env =
+module Env = Value.Env
+
+let rec eval (env : Env.t) (tm : TermDB.t) : Value.t =
+  let eval_fun_params p =
     (* Unlike OCaml we always evaluate default values, and we do that early. I
        think the only reason is homogeneity with FFI, which are declared with
        values as defaults. *)
-    let p =
-      List.map
-        (function
-          | lbl, var, _, Some v -> (lbl, var, Some (eval env v))
-          | lbl, var, _, None -> (lbl, var, None))
-        p
-    in
-    (* Keep only once the variables we might use in the environment. *)
-    let env =
-      let fv = ref fv in
-      let mem x =
-        if Vars.mem x !fv then (
-          fv := Vars.remove x !fv;
-          true)
-        else false
-      in
-      List.filter (fun (x, _) -> mem x) env
-    in
-    (p, env)
+    List.map (fun (lbl, var, _, v) -> (lbl, var, Option.map (eval env) v)) p
   in
   (* Ensure that the kind computed at runtime for sources will agree with the
      typing. *)
@@ -194,7 +178,7 @@ let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
     | Meth (l, u, v) -> Meth (l, eval env u, eval env v)
     | Invoke (t, l) ->
         let rec aux t =
-          match t.Value.value with
+          match t with
             | Value.Meth (l', t, _) when l = l' -> t
             | Value.Meth (_, _, t) -> aux t
             | _ ->
@@ -206,9 +190,9 @@ let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
         aux (eval env t)
     | Open (t, u) ->
         let t = eval env t in
-        let rec aux env (t : Value.t) =
+        let rec aux (env : Env.t) (t : Value.t) =
           match t with
-            | Meth (l, v, t) -> aux ((l, Lazy.from_val v) :: env) t
+            | Meth (l, v, t) -> aux (Env.add env v) t
             | Tuple [] -> env
             | _ -> assert false
         in
@@ -223,9 +207,7 @@ let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
                 | [] -> assert false
                 | [x] ->
                     let v () =
-                      if replace then
-                        Value.remeth (Lazy.force (List.assoc x env)) v
-                      else v
+                      if replace then Value.remeth (Env.lookup env x) v else v
                     in
                     (x, Lazy.from_fun v)
                 | l :: ll ->
@@ -250,30 +232,28 @@ let rec eval (env : Value.Env.t) (tm : TermDB.t) : Value.t =
         in
         let env = penv @ env in
         eval env b
-    | Fun (fv, p, body) ->
-        let p, env = prepare_fun fv p env in
+    | Fun (p, body) ->
+        let p = eval_fun_params p in
         Fun (p, env, body)
-    | RFun (x, fv, p, body) ->
-        let p, env = prepare_fun fv p env in
+    | RFun (p, body) ->
+        let p = eval_fun_params p in
         let rec v () =
-          let env = (x, Lazy.from_fun v) :: env in
-          Fun (p, env, body)
+          let env = Env.add_lazy env (Lazy.from_fun v) in
+          Value.Fun (p, env, body)
         in
         v ()
-    | Var var -> lookup env var
+    | Var var -> Env.lookup env var
     | Seq (a, b) ->
-        ignore (eval ~env a);
-        eval ~env b
+        ignore (eval env a);
+        eval env b
     | App (f, l) ->
         let ans () =
-          let f = eval ~env f in
-          let l = List.map (fun (l, t) -> (l, eval ~env t)) l in
+          let f = eval env f in
+          let l = List.map (fun (l, t) -> (l, eval env t)) l in
           apply f l
         in
         if !profile then (
-          match f.term with
-            | Var fname -> Profiler.time fname ans ()
-            | _ -> ans ())
+          match f with Var fname -> Profiler.time fname ans () | _ -> ans ())
         else ans ()
 
 and apply f l =
diff --git a/src/lang/term.ml b/src/lang/term.ml
index e598ccfdeb..ac4c064ef2 100644
--- a/src/lang/term.ml
+++ b/src/lang/term.ml
@@ -315,7 +315,7 @@ and in_term =
 and pattern =
   | PVar of string list  (** a field *)
   | PTuple of pattern list  (** a tuple *)
-  | PList of (pattern list * string option * pattern list) (* a list *)
+  | PList of (pattern list * string option * pattern list)  (** a list *)
   | PMeth of (pattern option * (string * pattern option) list)
       (** a value with methods *)
 
@@ -323,9 +323,8 @@ type term = t
 
 let unit = Tuple []
 
-(* Only used for printing very simple functions. *)
-let is_ground x =
-  match x.term with Ground _ -> true (* | Ref x -> is_ground x *) | _ -> false
+(** Used for printing very simple functions. *)
+let is_ground x = match x.term with Ground _ -> true | _ -> false
 
 let rec string_of_pat = function
   | PVar l -> String.concat "." l
@@ -531,7 +530,7 @@ let check_unused ~throw ~lib tm =
       | App (hd, l) ->
           let v = check v hd in
           List.fold_left (fun v (_, t) -> check v t) v l
-      | RFun (arg, p, body) -> check v { tm with term = Fun (p, body) }
+      | RFun (_, p, body) -> check v { tm with term = Fun (p, body) }
       | Fun (p, body) ->
           let v =
             List.fold_left
diff --git a/src/lang/termDB.ml b/src/lang/termDB.ml
index c456f53860..cd54a9e67e 100644
--- a/src/lang/termDB.ml
+++ b/src/lang/termDB.ml
@@ -25,9 +25,7 @@
 module Ground = Term.Ground
 
 type pos = Pos.t
-
-(* No need to duplicate, we simply ignore variable names. *)
-type pattern = Term.pattern
+type var = int
 
 type t =
   | Ground of Ground.t
@@ -40,7 +38,7 @@ type t =
   | Invoke of t * string
   | Open of t * t
   | Let of let_t
-  | Var of int
+  | Var of var * string (* The string is only used for debugging. *)
   | Seq of t * t
   (* TODO: we should pre-compute applications when the type is fully known (be
      careful of subtyping!) *)
@@ -48,6 +46,8 @@ type t =
   | Fun of (string * t option) list * t
   | RFun of (string * t option) list * t
 
+and closure = t Lazy.t list
+
 and let_t = {
   replace : bool;
   (* whether the definition replaces a previously existing one (keeping methods) *)
@@ -56,9 +56,26 @@ and let_t = {
   body : t;
 }
 
+and pattern =
+  | PVar  (** a variable *)
+  | PField of var * string list  (** a field *)
+  | PTuple of pattern list  (** a tuple *)
+  | PList of (pattern list * bool * pattern list)  (** a list *)
+  (* TODO: it would be cleaner to have a _ pattern instead of options below *)
+  | PMeth of (pattern option * (string * pattern option) list)
+      (** a value with methods *)
+
 (** Parameters for encoders. *)
 and encoder_params =
   (string * [ `Term of pos option * t | `Encoder of encoder ]) list
 
 (** A formal encoder. *)
 and encoder = pos option * string * encoder_params
+
+(** Used for printing very simple functions. *)
+let is_ground = function Ground _ -> true | _ -> false
+
+(** String representation of ground terms. *)
+let string_of_ground t =
+  assert (is_ground t);
+  match t with Ground g -> Ground.to_string g | _ -> assert false
diff --git a/src/lang/typechecking.ml b/src/lang/typechecking.ml
index deda59c47a..318100c93f 100644
--- a/src/lang/typechecking.ml
+++ b/src/lang/typechecking.ml
@@ -25,6 +25,18 @@ open Typing
 
 let debug = ref false
 
+module List = struct
+  include List
+
+  (** Index where a predicate is satisfied. *)
+  let index p l =
+    let rec aux n = function
+      | x :: l -> if p x then n else aux (n + 1) l
+      | [] -> raise Not_found
+    in
+    aux 0 l
+end
+
 (** {1 Type checking / inference} *)
 
 (** Terms for which generalization is safe. *)
@@ -315,10 +327,10 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
               let p = List.map (fun (lbl, b) -> (false, lbl, b.t)) l in
               a.t <: Type.make (Type.Arrow (p, e.t)));
         App (a', l')
-    | Fun (_, proto, body) ->
+    | Fun (proto, body) ->
         let proto, body = check_fun ~proto ~env e body in
         Fun (proto, body)
-    | RFun (x, _, proto, body) ->
+    | RFun (x, proto, body) ->
         let env = (x, ([], e.t)) :: env in
         let proto, body = check_fun ~proto ~env e body in
         RFun (proto, body)
@@ -339,7 +351,7 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
         if Lazy.force Term.debug then
           Printf.eprintf "Instantiate %s : %s becomes %s\n" var
             (Type.to_string orig) (Type.to_string e.t);
-        Var i
+        Var (i, var)
     | Let ({ pat; replace; def; body; _ } as l) ->
         let def' = check ~level:(level + 1) ~env def in
         let generalized =
@@ -374,6 +386,21 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
                     with Not_found -> raise (Unbound (pos, l))))
             penv
         in
+        (* Pre-compile the pattern. This could be done in type_of_pat, but this
+           is safer this way and should not have a big effect on performance. *)
+        let rec pat_of_pat : Term.pattern -> TermDB.pattern = function
+          | PVar [_] -> PVar
+          | PVar (x :: l) -> PField (List.index (fun (y, _) -> y = x) env, l)
+          | PVar [] -> assert false
+          | PTuple l -> PTuple (List.map pat_of_pat l)
+          | PList (l, p, l') ->
+              PList (List.map pat_of_pat l, p <> None, List.map pat_of_pat l')
+          | PMeth (p, l) ->
+              PMeth
+                ( Option.map pat_of_pat p,
+                  List.map (fun (l, p) -> (l, Option.map pat_of_pat p)) l )
+        in
+        let pat' = pat_of_pat l.pat in
         let env = penv @ env in
         l.gen <- generalized;
         if print_toplevel then
@@ -386,7 +413,7 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
                 def.t);
         let body' = check ~print_toplevel ~level ~env body in
         e.t >: body.t;
-        Let { replace = l.replace; pat = l.pat; def = def'; body = body' }
+        Let { replace = l.replace; pat = pat'; def = def'; body = body' }
 
 (* The simple definition for external use. *)
 let check ?(ignored = false) ~throw e =
diff --git a/src/lang/value.ml b/src/lang/value.ml
index 0582dbb30a..6e4be0d787 100644
--- a/src/lang/value.ml
+++ b/src/lang/value.ml
@@ -39,7 +39,7 @@ type t =
   | Ref of t ref
   (* Function with given list of argument name, argument variable and default
      value, the (relevant part of the) closure, and the body. *)
-  | Fun of (string * string * t option) list * lazy_env * Term.t
+  | Fun of (string * string * t option) list * lazy_env * TermDB.t
   (* For a foreign function only the arguments are visible, the closure
      doesn't capture anything in the environment. *)
   | FFI of (string * string * t option) list * (env -> t)
@@ -47,7 +47,7 @@ type t =
 and env = (string * t) list
 
 (* Some values have to be lazy in the environment because of recursive functions. *)
-and lazy_env = (string * t Lazy.t) list
+and lazy_env = t Lazy.t list
 
 type encoder_params = (string * [ `Value of t | `Encoder of encoder ]) list
 
@@ -85,8 +85,9 @@ let rec print_value = function
       in
       let e = match e with Tuple [] -> "" | _ -> print_value e ^ "." in
       e ^ "{" ^ m ^ "}"
-  | Fun ([], _, x) when Term.is_ground x -> "{" ^ Term.to_string x ^ "}"
-  | Fun (l, _, x) when Term.is_ground x ->
+  | Fun ([], _, x) when TermDB.is_ground x ->
+      "{" ^ TermDB.string_of_ground x ^ "}"
+  | Fun (l, _, x) when TermDB.is_ground x ->
       let f (label, _, value) =
         match (label, value) with
           | "", None -> "_"
@@ -96,7 +97,7 @@ let rec print_value = function
       in
       let args = List.map f l in
       Printf.sprintf "fun (%s) -> %s" (String.concat "," args)
-        (Term.to_string x)
+        (TermDB.string_of_ground x)
   | Fun _ | FFI _ -> "<fun>"
 
 (** Find a method in a value. *)
@@ -181,7 +182,10 @@ let compare a b =
 
 (** Operations on evaluation environments. *)
 module Env = struct
-  type nonrec t = t Lazy.t list
+  type nonrec t = lazy_env
+
+  let add (env : t) v : t = Lazy.from_val v :: env
+  let add_lazy (env : t) v : t = v :: env
 
   let lookup (env : t) var =
     match List.nth_opt env var with

From ff803f37df55ab997ba07135bf4f46a5cd8fe5df Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@gmail.com>
Date: Mon, 7 Mar 2022 10:52:05 +0100
Subject: [PATCH 5/5] More.

---
 src/lang/evaluation.ml   | 6 +++---
 src/lang/termDB.ml       | 3 +++
 src/lang/typechecking.ml | 3 +++
 src/lang/typing.ml       | 2 +-
 src/lang/value.ml        | 1 +
 5 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/lang/evaluation.ml b/src/lang/evaluation.ml
index add5fd54b7..0abbef93ad 100644
--- a/src/lang/evaluation.ml
+++ b/src/lang/evaluation.ml
@@ -42,11 +42,11 @@ let rec rev_map_append f l1 l2 =
   match l1 with [] -> l2 | a :: l -> rev_map_append f l (f a :: l2)
 
 let rec eval_pat pat v =
-  let rec aux env pat (v : Value.t) =
+  let rec aux env (pat : TermDB.pattern) (v : Value.t) =
     match (pat, v) with
       | PVar x, v -> (x, v) :: env
       | PTuple pl, Tuple l -> List.fold_left2 aux env pl l
-      (* The parser parses [x,y,z] as PList ([], None, l) *)
+      (* The parser parses [x,y,z] as PList ([], false, l) *)
       | PList (([] as l'), (None as spread), l), List lv
       | PList (l, spread, l'), List lv ->
           let ln = List.length l in
@@ -242,7 +242,7 @@ let rec eval (env : Env.t) (tm : TermDB.t) : Value.t =
           Value.Fun (p, env, body)
         in
         v ()
-    | Var var -> Env.lookup env var
+    | Var (var, _) -> Env.lookup env var
     | Seq (a, b) ->
         ignore (eval env a);
         eval env b
diff --git a/src/lang/termDB.ml b/src/lang/termDB.ml
index cd54a9e67e..69084d8734 100644
--- a/src/lang/termDB.ml
+++ b/src/lang/termDB.ml
@@ -56,6 +56,7 @@ and let_t = {
   body : t;
 }
 
+(*
 and pattern =
   | PVar  (** a variable *)
   | PField of var * string list  (** a field *)
@@ -64,6 +65,8 @@ and pattern =
   (* TODO: it would be cleaner to have a _ pattern instead of options below *)
   | PMeth of (pattern option * (string * pattern option) list)
       (** a value with methods *)
+*)
+and pattern = Term.pattern
 
 (** Parameters for encoders. *)
 and encoder_params =
diff --git a/src/lang/typechecking.ml b/src/lang/typechecking.ml
index 318100c93f..f70df74f32 100644
--- a/src/lang/typechecking.ml
+++ b/src/lang/typechecking.ml
@@ -386,6 +386,7 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
                     with Not_found -> raise (Unbound (pos, l))))
             penv
         in
+        (*
         (* Pre-compile the pattern. This could be done in type_of_pat, but this
            is safer this way and should not have a big effect on performance. *)
         let rec pat_of_pat : Term.pattern -> TermDB.pattern = function
@@ -401,6 +402,8 @@ let rec check ?(print_toplevel = false) ~throw ~level ~(env : Typing.env) e :
                   List.map (fun (l, p) -> (l, Option.map pat_of_pat p)) l )
         in
         let pat' = pat_of_pat l.pat in
+        *)
+        let pat' = l.pat in
         let env = penv @ env in
         l.gen <- generalized;
         if print_toplevel then
diff --git a/src/lang/typing.ml b/src/lang/typing.ml
index 55cb2b7d5b..7eeb9d0429 100644
--- a/src/lang/typing.ml
+++ b/src/lang/typing.ml
@@ -32,7 +32,7 @@ let debug_subtyping = ref false
 
 (** Allow functions to forget arguments during subtyping. This would not be a
     good idea if we had de Bruijn indices for instance. *)
-let forget_arguments = true
+let forget_arguments = false
 
 type env = (string * scheme) list
 
diff --git a/src/lang/value.ml b/src/lang/value.ml
index 6e4be0d787..5071614fcb 100644
--- a/src/lang/value.ml
+++ b/src/lang/value.ml
@@ -186,6 +186,7 @@ module Env = struct
 
   let add (env : t) v : t = Lazy.from_val v :: env
   let add_lazy (env : t) v : t = v :: env
+  let add_list env l = List.fold_right (fun v env -> add env v) l env
 
   let lookup (env : t) var =
     match List.nth_opt env var with