Make handling of names in mlang nominal (#810)

* Nominal handling of lang contents

* Type-level use

* Keep the info field in a sem pointing at the original definition

* Fix redefinition of cons in syns

* Renaming and merging lang things via 'with'

* Extra note on the limitation

* Fix type of cons in syns

* Re-fix type of cons in syns

* Fix ast.mc

* Fix const-types.mc and value.mc

* Fix pprint.mc

* Partiallly fix type-lift.mc

* Fix eq.mc

* Temp: weird type error

* Fix and.mc and index.mc

* Fix eval.mc

* Fix type-annot.mc

* Resolve sem conflicts in stdlib/ocaml directory

* Fix sem conflicts in stdlib/futhark

* Fix sem name conflicts in stdlib/cuda

* Fix remaining sem name conflicts in stdlib/mexpr

* Resolve remaining sym name conflicts

* Fix syn and sem name conflicts in test/mlang

* Add type-level use to fix type error

* Fix type errors

* Add type-level use to fix type errors

* Add type-level uses in stdlib/parser

* Fix type error in local-search.mc

* Fix gen-ast and partially fix tool

* More fixes to tool.mc

* Fix nominal name errors

* Fix name errors in stdlib

* Fix type errors in old test/mlang code

* Formatting changes in boot

---------

Co-authored-by: Linnea Stjerna <lingmar@kth.se>
Co-authored-by: Lars Hummelgren <larshum@kth.se>
Co-authored-by: Oscar Eriksson <oerikss@kth.se>

src/boot/boot.ml

@@ -104,10 +104,6 @@ let main =
       , Arg.Set Boot.Patterns.pat_example_gives_complete_pattern
       , " Make the pattern analysis in mlang print full patterns instead of \
          partial ones." )
-    ; ( "--subsumption-analysis"
-      , Arg.Set Boot.Mlang.enable_subsumption_analysis
-      , " Enables subsumption analysis of language fragments in mlang \
-         transformations." )
     ; ( "--disable-prune-utests"
       , Arg.Set disable_prune_external_utests
       , " Disables pruning of utests with missing external dependencies." )

src/boot/lib/ast.ml

@@ -231,7 +231,12 @@ and ptree =
   | PTreeInfo of info
 
 (* Terms in MLang *)
-and cdecl = CDecl of info * ustring list * ustring * ty
+and cdecl =
+  | CDecl of
+      info
+      * ustring list (* type-parameters *)
+      * ustring (* constructor name *)
+      * ty (* carried type *)
 
 and param = Param of info * ustring * ty
 
@@ -241,7 +246,12 @@ and decl =
   | Inter of info * ustring * ty * param list option * (pat * tm) list
   | Alias of info * ustring * ustring list * ty
 
-and mlang = Lang of info * ustring * ustring list * decl list
+and with_kind = WithType | WithValue
+
+and lang_with = With of info * with_kind * ustring * (ustring * ustring) list
+
+and mlang =
+  | Lang of info * ustring * ustring list * lang_with list * decl list
 
 and let_decl = Let of info * ustring * ty * tm
 
@@ -383,6 +393,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 =
@@ -476,16 +488,179 @@ let smap_accum_left_tm_tm (f : 'a -> tm -> 'a * tm) (acc : 'a) : tm -> 'a * tm
   | TmBox (_, _) ->
       failwith "TmBox is a runtime value"
 
-(* smap for terms *)
+let smap_accum_left_tm_ty (f : 'a -> ty -> 'a * ty) (acc : 'a) : tm -> 'a * tm
+    = function
+  | TmLam (fi, id, sym, pesym, ty, tm) ->
+      let acc, ty = f acc ty in
+      (acc, TmLam (fi, id, sym, pesym, ty, tm))
+  | TmLet (fi, id, sym, ty, body, inexpr) ->
+      let acc, ty = f acc ty in
+      (acc, TmLet (fi, id, sym, ty, body, inexpr))
+  | TmRecLets (fi, lets, tm) ->
+      let f_bind acc (fi, id, sym, ty, tm) =
+        let acc, ty = f acc ty in
+        (acc, (fi, id, sym, ty, tm))
+      in
+      let acc, lets = List.fold_left_map f_bind acc lets in
+      (acc, TmRecLets (fi, lets, tm))
+  | TmType (fi, name, params, rhs, inexpr) ->
+      let acc, rhs = f acc rhs in
+      (acc, TmType (fi, name, params, rhs, inexpr))
+  | TmConDef (fi, name, sym, ty, tm) ->
+      let acc, ty = f acc ty in
+      (acc, TmConDef (fi, name, sym, ty, tm))
+  | TmExt (fi, name, sym, side, ty, tm) ->
+      let acc, ty = f acc ty in
+      (acc, TmExt (fi, name, sym, side, ty, tm))
+  | ( TmVar _
+    | TmApp _
+    | TmConst _
+    | TmSeq _
+    | TmRecord _
+    | TmRecordUpdate _
+    | TmConApp _
+    | TmMatch _
+    | TmUtest _
+    | TmNever _
+    | TmUse _
+    | TmClos _
+    | TmRef _
+    | TmTensor _
+    | TmDive _
+    | TmPreRun _
+    | TmBox _ ) as tm ->
+      (acc, tm)
+
+let smap_accum_left_ty_ty (f : 'a -> ty -> 'a * ty) (acc : 'a) : ty -> 'a * ty
+    = function
+  | TyArrow (fi, l, r) ->
+      let acc, l = f acc l in
+      let acc, r = f acc r in
+      (acc, TyArrow (fi, l, r))
+  | TyAll (fi, id, ty) ->
+      let acc, ty = f acc ty in
+      (acc, TyAll (fi, id, ty))
+  | TySeq (fi, ty) ->
+      let acc, ty = f acc ty in
+      (acc, TySeq (fi, ty))
+  | TyTensor (fi, ty) ->
+      let acc, ty = f acc ty in
+      (acc, TyTensor (fi, ty))
+  | TyRecord (fi, tys) ->
+      let acc, tys =
+        Record.to_seq tys |> List.of_seq
+        |> List.fold_left_map
+             (fun acc (k, v) ->
+               let acc, v = f acc v in
+               (acc, (k, v)) )
+             acc
+      in
+      (acc, TyRecord (fi, Record.of_seq (List.to_seq tys)))
+  | TyApp (fi, l, r) ->
+      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
+  | TmMatch (fi, scrut, pat, th, el) ->
+      let acc, pat = f acc pat in
+      (acc, TmMatch (fi, scrut, pat, th, el))
+  | tm ->
+      (acc, tm)
+
+let smap_accum_left_pat_pat (f : 'a -> pat -> 'a * pat) (acc : 'a) :
+    pat -> 'a * pat = function
+  | PatSeqTot (fi, pats) ->
+      let acc, pats = Mseq.Helpers.map_accum_left f acc pats in
+      (acc, PatSeqTot (fi, pats))
+  | PatSeqEdge (fi, l, mid, r) ->
+      let acc, l = Mseq.Helpers.map_accum_left f acc l in
+      let acc, r = Mseq.Helpers.map_accum_left f acc r in
+      (acc, PatSeqEdge (fi, l, mid, r))
+  | PatRecord (fi, pats) ->
+      let acc, pats =
+        Record.to_seq pats |> List.of_seq
+        |> List.fold_left_map
+             (fun acc (k, v) ->
+               let acc, v = f acc v in
+               (acc, (k, v)) )
+             acc
+      in
+      (acc, PatRecord (fi, Record.of_seq (List.to_seq pats)))
+  | PatCon (fi, id, sym, pat) ->
+      let acc, pat = f acc pat in
+      (acc, PatCon (fi, id, sym, pat))
+  | PatAnd (fi, l, r) ->
+      let acc, l = f acc l in
+      let acc, r = f acc r in
+      (acc, PatAnd (fi, l, r))
+  | PatOr (fi, l, r) ->
+      let acc, l = f acc l in
+      let acc, r = f acc r in
+      (acc, PatOr (fi, l, r))
+  | PatNot (fi, pat) ->
+      let acc, pat = f acc pat in
+      (acc, PatNot (fi, pat))
+  | (PatNamed _ | PatInt _ | PatChar _ | PatBool _) as pat ->
+      (acc, pat)
+
+(* smap and sfold variants of the smap_accum_lefts above *)
+
 let smap_tm_tm (f : tm -> tm) (t : tm) : tm =
   let _, t' = smap_accum_left_tm_tm (fun _ t -> ((), f t)) () t in
   t'
 
-(* sfold over terms *)
 let sfold_tm_tm (f : 'a -> tm -> 'a) (acc : 'a) (t : tm) : 'a =
   let acc', _ = smap_accum_left_tm_tm (fun acc t -> (f acc t, t)) acc t in
   acc'
 
+let smap_tm_ty (f : ty -> ty) (tm : tm) : tm =
+  let _, tm = smap_accum_left_tm_ty (fun _ ty -> ((), f ty)) () tm in
+  tm
+
+let sfold_tm_ty (f : 'a -> ty -> 'a) (acc : 'a) (tm : tm) : 'a =
+  let acc, _ = smap_accum_left_tm_ty (fun acc ty -> (f acc ty, ty)) acc tm in
+  acc
+
+let smap_ty_ty (f : ty -> ty) (t : ty) : ty =
+  let _, t' = smap_accum_left_ty_ty (fun _ t -> ((), f t)) () t in
+  t'
+
+let sfold_ty_ty (f : 'a -> ty -> 'a) (acc : 'a) (t : ty) : 'a =
+  let acc', _ = smap_accum_left_ty_ty (fun acc t -> (f acc t, t)) acc t in
+  acc'
+
+let smap_tm_pat (f : pat -> pat) (tm : tm) : tm =
+  let _, tm = smap_accum_left_tm_pat (fun _ pat -> ((), f pat)) () tm in
+  tm
+
+let sfold_tm_pat (f : 'a -> pat -> 'a) (acc : 'a) (tm : tm) : 'a =
+  let acc, _ =
+    smap_accum_left_tm_pat (fun acc pat -> (f acc pat, pat)) acc tm
+  in
+  acc
+
+let smap_pat_pat (f : pat -> pat) (t : pat) : pat =
+  let _, t' = smap_accum_left_pat_pat (fun _ t -> ((), f t)) () t in
+  t'
+
+let sfold_pat_pat (f : 'a -> pat -> 'a) (acc : 'a) (t : pat) : 'a =
+  let acc', _ = smap_accum_left_pat_pat (fun acc t -> (f acc t, t)) acc t in
+  acc'
+
 (* Returns arity given an type *)
 let rec ty_arity = function TyArrow (_, _, ty) -> 1 + ty_arity ty | _ -> 0
 
@@ -544,6 +719,7 @@ let ty_info = function
   | TyVariant (fi, _)
   | TyCon (fi, _)
   | TyVar (fi, _)
+  | TyUse (fi, _, _)
   | TyApp (fi, _, _) ->
       fi
 

src/boot/lib/eval.ml

@@ -19,9 +19,8 @@ let evalprog filename =
   if !utest then printf "%s: " filename ;
   utest_fail_local := 0 ;
   ( try
-      filename |> parse_mcore_file |> Mlang.flatten
-      |> Mlang.desugar_post_flatten |> debug_after_mlang
-      |> raise_parse_error_on_non_unique_external_id
+      filename |> parse_mcore_file |> Mlang.translate_program
+      |> debug_after_mlang |> raise_parse_error_on_non_unique_external_id
       |> (fun t -> if !utest then t else remove_all_utests t)
       |> Symbolize.symbolize builtin_name2sym
       |> debug_after_symbolize

src/boot/lib/mexpr.ml

@@ -1049,7 +1049,7 @@ let rec parseMCoreFile
       PTreeTm
         ( filename |> Intrinsics.Mseq.Helpers.to_ustring |> Ustring.to_utf8
         |> Utils.normalize_path |> Parserutils.parse_mcore_file
-        |> Mlang.flatten |> Mlang.desugar_post_flatten
+        |> Mlang.translate_program
         |> Parserutils.raise_parse_error_on_non_unique_external_id
         |> Symbolize.symbolize name2sym
         |> Parserutils.raise_parse_error_on_partially_applied_external