Update internal state of the typer

type:internal

The typer (src/pass/10-checking) keeps information around about the context of E_application in an ad-hoc way through variables last and args. This MR improves the representation by keeping an application context structure where things are pushed/popped.

src/passes/10-checking/checking.ml

@@ -9,14 +9,16 @@ open O.Combinators
 module Pair = Simple_utils.Pair
 
 type context = Context.t
-type app_context = O.type_expression option * (O.expression list * O.type_expression option) list
-let pop_app_context = function
-    _, (args, r) :: vs -> Some (args, (r , vs)) | _, [] -> None
-let get_tv_opt ((c, _) : app_context) = c
-let push_app_context tv_opt args ctxt =
-  let old_tv_opt, ctxt = ctxt in
-  tv_opt, (args, old_tv_opt) :: ctxt
-let update_tv_opt_app_context tv_opt (_, r) = (tv_opt, r)
+module App_context = struct
+  type t = O.type_expression option * (O.expression list * O.type_expression option) list
+  let pop_app_context = function
+      _, (args, r) :: vs -> Some (args, (r , vs)) | _, [] -> None
+  let get_tv_opt ((c, _) : t) = c
+  let push_app_context tv_opt args ctxt =
+    let old_tv_opt, ctxt = ctxt in
+    tv_opt, (args, old_tv_opt) :: ctxt
+  let update_tv_opt_app_context tv_opt (_, r) = (tv_opt, r)
+end
 
 let assert_type_expression_eq = Helpers.assert_type_expression_eq
 
@@ -310,15 +312,15 @@ and infer_t_insts ~raise ~loc app_context ( (tc,t) : O.expression_content * O.ty
   | { type_content = T_for_all _ ; type_meta = _; orig_var=_ ; location=_} ->
     (* TODO: This is some inference, and we should reconcile it with the inference pass. *)
     let avs, type_ = O.Helpers.destruct_for_alls t in
-    let last = get_tv_opt app_context in 
-    let args, _ = match pop_app_context app_context with | None -> [], (None, []) | Some v -> v in 
+    let last = App_context.get_tv_opt app_context in
+    let args, _ = match App_context.pop_app_context app_context with | None -> [], (None, []) | Some v -> v in
     let table = Inference.infer_type_applications ~raise ~loc avs type_ (List.map ~f:(fun ({type_expression;_} : O.expression) -> type_expression) args) last in
     let lamb = make_e ~location:loc tc t in
     let x = Inference.build_type_insts ~raise ~loc lamb table avs in
     x.expression_content , x.type_expression
   | _ -> tc, t
 
-and type_expression' ~raise ~options : app_context -> context -> ?tv_opt:O.type_expression -> I.expression -> O.expression = fun app_context context ?tv_opt e ->
+and type_expression' ~raise ~options : App_context.t -> context -> ?tv_opt:O.type_expression -> I.expression -> O.expression = fun app_context context ?tv_opt e ->
   let return expr tv =
     let () =
       match tv_opt with
@@ -604,7 +606,7 @@ and type_expression' ~raise ~options : app_context -> context -> ?tv_opt:O.type_
      let lamb, args = I.Helpers.destruct_applications e in
      (* Type-check all the involved subexpressions *)
      let args = List.map ~f:(type_expression' ~raise ~options app_context context) args in
-     let lamb = type_expression' ~raise ~options (push_app_context tv_opt args app_context) context lamb in
+     let lamb = type_expression' ~raise ~options (App_context.push_app_context tv_opt args app_context) context lamb in
      (* Remove and save prefix for_alls in the lambda *)
      let avs, lamb_type = O.Helpers.destruct_for_alls lamb.type_expression in
      (* Try to infer/check types for the type variables *)
@@ -694,7 +696,7 @@ and type_expression' ~raise ~options : app_context -> context -> ?tv_opt:O.type_
     return (E_recursive {fun_name;fun_type;lambda}) fun_type
   | E_ascription {anno_expr; type_annotation} ->
     let tv = evaluate_type ~raise context type_annotation in
-    let app_context = update_tv_opt_app_context (Some tv) app_context in
+    let app_context = App_context.update_tv_opt_app_context (Some tv) app_context in
     let expr' = type_expression' ~raise ~options ~tv_opt:tv app_context context anno_expr in
     let type_annotation =
       trace_option ~raise (corner_case "merge_annotations (Some ...) (Some ...) failed") @@
@@ -949,7 +951,7 @@ and untype_declaration_module : O.declaration_module -> I.declaration_module =
     let module_ = untype_module_expr module_ in
     let module_attr = (I.{public}: I.module_attribute) in
     I.{module_binder; module_ ; module_attr}
-      
+
 and untype_declaration =
   let return (d: I.declaration_content) = d in
   fun (d: O.declaration_content) -> match d with
@@ -964,7 +966,7 @@ and untype_declaration =
     return @@ Declaration_module dm
 and untype_declarations : O.module_ -> I.module_ = fun p ->
   List.map ~f:(Location.map untype_declaration) p
-    
+
 and untype_module : O.module_ -> I.module_ = fun x -> untype_declarations x
 
 let untype_program = untype_module