New Unif intermediate language

This commit introduces a new Unif intermediate language: it is designed
for type inference. Effect inference will be done in the next phase of
the compiler and will produce a program in another representation.
Currently, TypeInference and ToCore translations are commented-out.

src/Lang/Unif.ml

@@ -20,6 +20,8 @@ module Scope = UnifPriv.Scope
 
 module Name = UnifPriv.Name
 
+module Effect = UnifPriv.Effect
+
 module Type = struct
   include UnifPriv.TypeBase
   include UnifPriv.Type
@@ -28,10 +30,9 @@ module Type = struct
   let subst = UnifPriv.Subst.in_type
 end
 
-module Effect = UnifPriv.Effect
-
 module Scheme = struct
   let of_type        = UnifPriv.Type.mono_scheme
+  let to_type        = UnifPriv.Type.scheme_to_type
   let is_monomorphic = UnifPriv.Type.scheme_is_monomorphic
   let uvars          = UnifPriv.Type.scheme_uvars
   let collect_uvars  = UnifPriv.Type.collect_scheme_uvars
@@ -56,70 +57,22 @@ end
 module Subst = UnifPriv.Subst
 module BuiltinType = UnifPriv.BuiltinType
 
-type var = Var.t
-
-type data_def =
-  | DD_Data of
-    { tvar              : tvar;
-      proof             : var;
-      args              : named_tvar list;
-      ctors             : ctor_decl list;
-      strictly_positive : bool
-    }
-
-  | DD_Label of
-    { tvar      : tvar;
-      var       : var;
-      delim_tp  : typ;
-      delim_eff : effrow
-    }
-
-type pattern = pattern_data node
-and pattern_data =
-  | PWildcard
-  | PVar  of var * scheme
-  | PCtor of string * int * expr * ctor_decl list * tvar list * pattern list
-
-and expr = expr_data node
-and expr_data =
-  | EUnitPrf
-  | ENum        of int
-  | ENum64      of int64
-  | EStr        of string
-  | EChr        of char
-  | EVar        of var
-  | EPureFn     of var * scheme * expr
-  | EFn         of var * scheme * expr
-  | ETFun       of tvar * expr
-  | EApp        of expr * expr
-  | ETApp       of expr * typ
-  | ELet        of var * scheme * expr * expr
-  | ELetRec     of rec_def list * expr
-  | ECtor       of expr * int * typ list * expr list
-  | EData       of data_def list * expr
-  | EMatchEmpty of expr * expr * typ * effrow option
-  | EMatch      of expr * match_clause list * typ * effrow option
-  | EHandle     of tvar * var * typ * expr * expr
-  | EHandler    of
-    { label     : var;
-      effect    : tvar;
-      delim_tp  : typ;
-      delim_eff : effect;
-      cap_type  : typ;
-      cap_body  : expr;
-      ret_var   : var;
-      body_tp   : typ;
-      ret_body  : expr;
-      fin_var   : var;
-      fin_body  : expr;
-    }
-  | EEffect     of expr * var * expr * typ
-  | EExtern     of string * typ
-  | ERepl       of (unit -> expr) * typ * effrow
-  | EReplExpr   of expr * string * expr
-
-and rec_def = var * scheme * expr
-
-and match_clause = pattern * expr
-
-type program = expr
+include UnifPriv.Syntax
+
+module TypeExpr = struct
+  let to_type = UnifPriv.TypeExpr.to_type
+end
+
+module SchemeExpr = struct
+  let of_type_expr = UnifPriv.TypeExpr.mono_scheme_expr
+  let to_type_expr = UnifPriv.TypeExpr.of_scheme_expr
+  let to_scheme    = UnifPriv.TypeExpr.to_scheme
+end
+
+module NamedSchemeExpr = struct
+  let to_named_scheme = UnifPriv.TypeExpr.to_named_scheme
+end
+
+module CtorDeclExpr = struct
+  let to_ctor_decl = UnifPriv.TypeExpr.to_ctor_decl
+end