From 99b26ef8f5c0b7f53e77a8374d4d958c7cd041e3 Mon Sep 17 00:00:00 2001
From: Viktor Palmkvist <vipa@kth.se>
Date: Wed, 15 Nov 2023 14:19:08 +0100
Subject: [PATCH] Type-level use

---
 src/boot/lib/ast.ml     | 6 ++++++
 src/boot/lib/mlang.ml   | 6 ++++++
 src/boot/lib/parser.mly | 3 +++
 src/boot/lib/pprint.ml  | 2 ++
 4 files changed, 17 insertions(+)

diff --git a/src/boot/lib/ast.ml b/src/boot/lib/ast.ml
index 28cf6cd73..6e7d3f380 100644
--- a/src/boot/lib/ast.ml
+++ b/src/boot/lib/ast.ml
@@ -383,6 +383,8 @@ and ty =
   | TyVar of info * ustring
   (* Type application *)
   | TyApp of info * ty * ty
+  (* Type-level use *)
+  | TyUse of info * ustring * ty
 
 (* Kind of identifier *)
 and ident =
@@ -523,6 +525,9 @@ let smap_accum_left_ty_ty (f : 'a -> ty -> 'a * ty) (acc : 'a) : ty -> 'a * ty =
      let acc, l = f acc l in
      let acc, r = f acc r in
      (acc, TyApp (fi, l, r))
+  | TyUse (fi, lang, ty) ->
+     let acc, ty = f acc ty in
+     (acc, TyUse (fi, lang, ty))
   | (TyUnknown _ | TyBool _ | TyInt _ | TyFloat _ | TyChar _ | TyVariant _ | TyCon _ | TyVar _) as ty -> (acc, ty)
 
 let smap_accum_left_tm_pat (f : 'a -> pat -> 'a * pat) (acc : 'a) : tm -> 'a * tm = function
@@ -660,6 +665,7 @@ let ty_info = function
   | TyVariant (fi, _)
   | TyCon (fi, _)
   | TyVar (fi, _)
+  | TyUse (fi, _, _)
   | TyApp (fi, _, _) ->
       fi
 
diff --git a/src/boot/lib/mlang.ml b/src/boot/lib/mlang.ml
index ff6d99fd6..3475ed40a 100644
--- a/src/boot/lib/mlang.ml
+++ b/src/boot/lib/mlang.ml
@@ -386,6 +386,12 @@ let rec translate_ty (env : mlang_env) : ty -> ty = function
      | Some id -> TyCon (fi, id)
      | None -> TyCon (fi, empty_mangle id)
      end
+  | TyUse (fi, lang, ty) ->
+     begin match Record.find_opt lang env.language_envs with
+     | Some new_env -> translate_ty (merge_env_prefer_right env new_env) ty
+     | None -> raise_error fi
+                 ( "Unbound language fragment '" ^ Ustring.to_utf8 lang ^ "'" )
+     end
   | ty ->
      let ty = smap_ty_ty (translate_ty env) ty in
      ty
diff --git a/src/boot/lib/parser.mly b/src/boot/lib/parser.mly
index b6e88f90d..5e4b49342 100644
--- a/src/boot/lib/parser.mly
+++ b/src/boot/lib/parser.mly
@@ -555,6 +555,9 @@ ty:
   | ALL var_ident DOT ty
       { let fi = mkinfo $1.i (ty_info $4) in
         TyAll(fi, $2.v, $4) }
+  | USE ident IN ty
+      { let fi = mkinfo $1.i $3.i in
+        TyUse(fi, $2.v, $4) }
 
 ty_left:
   | ty_atom
diff --git a/src/boot/lib/pprint.ml b/src/boot/lib/pprint.ml
index 8090d86c4..693aebaf2 100644
--- a/src/boot/lib/pprint.ml
+++ b/src/boot/lib/pprint.ml
@@ -208,6 +208,8 @@ let rec ustring_of_ty = function
       pprint_type_str x
   | TyVar (_, x) ->
       pprint_var_str x
+  | TyUse (_, lang, ty) ->
+     us"use " ^. lang ^. us" in " ^. ustring_of_ty ty
   | TyApp (_, ty1, ty2) ->
       us "(" ^. ustring_of_ty ty1 ^. us " " ^. ustring_of_ty ty2 ^. us ")"