Finish adding constructor types

src/boot/lib/ast.ml

@@ -378,7 +378,7 @@ and ty =
   (* Variant type *)
   | TyVariant of info * ustring list
   (* Type constructors *)
-  | TyCon of info * ustring
+  | TyCon of info * ustring * (bool * ustring list) option
   (* Type variables *)
   | TyVar of info * ustring
   (* Type application *)
@@ -542,7 +542,7 @@ let ty_info = function
   | TyTensor (fi, _)
   | TyRecord (fi, _)
   | TyVariant (fi, _)
-  | TyCon (fi, _)
+  | TyCon (fi, _, _)
   | TyVar (fi, _)
   | TyApp (fi, _, _) ->
       fi

src/boot/lib/mexpr.ml

@@ -229,8 +229,12 @@ let getData = function
   | PTreeTy (TyVariant (fi, strs)) ->
       let len = List.length strs in
       (idTyVariant, [fi], [len], [], [], strs, [], [], [], [])
-  | PTreeTy (TyCon (fi, x)) ->
-      (idTyCon, [fi], [], [], [], [x], [], [], [], [])
+  | PTreeTy (TyCon (fi, x, None)) ->
+      (idTyCon, [fi], [], [], [], [x], [0], [], [], [])
+  | PTreeTy (TyCon (fi, x, Some (positive, cons))) ->
+      let pos = if positive then 1 else 2 in
+      let len = List.length cons + 1 in
+      (idTyCon, [fi], [len], [], [], x :: cons, [pos], [], [], [])
   | PTreeTy (TyVar (fi, x)) ->
       (idTyVar, [fi], [], [], [], [x], [], [], [], [])
   | PTreeTy (TyApp (fi, ty1, ty2)) ->

src/boot/lib/mlang.ml

@@ -653,8 +653,8 @@ let rec desugar_ty env = function
       TyRecord (fi, Record.map (desugar_ty env) bindings)
   | TyVariant (fi, constrs) ->
       TyVariant (fi, constrs)
-  | TyCon (fi, id) ->
-      TyCon (fi, resolve_alias env id)
+  | TyCon (fi, id, data) ->
+      TyCon (fi, resolve_alias env id, data)
   | TyVar (fi, id) ->
       TyVar (fi, id)
   | TyApp (fi, lty, rty) ->
@@ -862,7 +862,7 @@ let desugar_top (nss, langs, subs, syns, (stack : (tm -> tm) list)) = function
       let wrap_con ty_name (CDecl (fi, params, cname, ty)) tm =
         let app_param ty param = TyApp (fi, ty, TyVar (fi, param)) in
         let all_param param ty = TyAll (fi, param, ty) in
-        let con = List.fold_left app_param (TyCon (fi, ty_name)) params in
+        let con = List.fold_left app_param (TyCon (fi, ty_name, None)) params in
         TmConDef
           ( fi
           , mangle cname

src/boot/lib/parser.mly

@@ -596,17 +596,33 @@ ty_atom:
     { TyChar $1.i }
   | TSTRING
     { TySeq($1.i,TyChar $1.i) }
-  | type_ident
-    { TyCon($1.i,$1.v) }
+  | type_ident ty_data
+    { TyCon ($1.i, $1.v, $2)}
   | var_ident
     { TyVar($1.i,$1.v)}
 
+ty_data:
+  |
+    { None }
+  | AND LBRACKET con_list RBRACKET
+    { Some (true, $3) }
+  | NOT LBRACKET con_list RBRACKET
+    { Some (false, $3) }
+
 ty_list:
   | ty COMMA ty_list
     { $1 :: $3 }
   | ty
     { [$1] }
 
+con_list:
+  | type_ident BAR con_list
+    { $1.v :: $3 }
+  | type_ident
+    { [$1.v] }
+  |
+    { [] }
+
 label_tys:
   | label_ident COLON ty
     {[($1.v, $3)]}

src/boot/lib/pprint.ml

@@ -204,7 +204,7 @@ let rec ustring_of_ty = function
       us "<>"
   | TyVariant _ ->
       failwith "Printing of non-empty variant types not yet supported"
-  | TyCon (_, x) ->
+  | TyCon (_, x, _) ->
       pprint_type_str x
   | TyVar (_, x) ->
       pprint_var_str x

stdlib/mexpr/ast.mc

@@ -1414,6 +1414,32 @@ lang ConTypeAst = Ast
   | TyCon r -> r.info
 end
 
+lang DataTypeAst = Ast
+  type DataRec =
+    {info     : Info,
+     universe : Map Name (Set Name),
+     positive : Bool,
+     cons     : Set Name}
+
+  syn Type =
+  | TyData DataRec
+
+  sem tyWithInfo (info : Info) =
+  | TyData t -> TyData {t with info = info}
+
+  sem infoTy =
+  | TyData r -> r.info
+
+  sem computeData : DataRec -> Map Name (Set Name)
+  sem computeData =
+  | r ->
+    if r.positive then
+      mapMap (setIntersect r.cons) r.universe
+    else
+      mapMap (lam x. setSubtract x r.cons) r.universe
+end
+
+
 lang VarTypeAst = Ast
   syn Type =
   -- Rigid type variable
@@ -1559,5 +1585,5 @@ lang MExprAst =
   -- Types
   UnknownTypeAst + BoolTypeAst + IntTypeAst + FloatTypeAst + CharTypeAst +
   FunTypeAst + SeqTypeAst + RecordTypeAst + VariantTypeAst + ConTypeAst +
-  VarTypeAst + AppTypeAst + TensorTypeAst + AllTypeAst + AliasTypeAst
+  DataTypeAst + VarTypeAst + AppTypeAst + TensorTypeAst + AllTypeAst + AliasTypeAst
 end

stdlib/mexpr/boot-parser.mc

@@ -273,9 +273,22 @@ lang BootParser = MExprAst + ConstTransformer
                  constrs = mapEmpty nameCmp}
     else error "Parsing of non-empty variant types not yet supported"
   | 209 /-TyCon-/ ->
+    let data =
+      let makeData = lam positive.
+        let cons = setOfSeq nameCmp (map (gname t) (range 1 (glistlen t 0) 1)) in
+        TyData { info = ginfo t 0, universe = mapEmpty nameCmp,
+                 positive = positive, cons = cons }
+      in
+      switch gint t 0
+      case 0 then TyUnknown { info = ginfo t 0 }
+      case 1 then makeData true
+      case 2 then makeData false
+      case _ then error "BootParser.matchTerm: Invalid data specifier for TyCon"
+      end
+    in
     TyCon {info = ginfo t 0,
            ident = gname t 0,
-           data = TyUnknown { info = ginfo t 0 }}
+           data = data}
   | 210 /-TyVar-/ ->
     TyVar {info = ginfo t 0,
            ident = gname t 0}

stdlib/mexpr/cmp.mc

@@ -411,6 +411,12 @@ lang ConTypeCmp = Cmp + ConTypeAst
     else nameDiff
 end
 
+lang DataTypeCmp = Cmp + DataTypeAst
+  sem cmpTypeH =
+  | (TyData l, TyData r) ->
+    mapCmp setCmp (computeData l) (computeData r)
+end
+
 lang VarTypeCmp = Cmp + VarTypeAst
   sem cmpTypeH =
   | (TyVar t1, TyVar t2) -> nameCmp t1.ident t2.ident
@@ -472,7 +478,7 @@ lang MExprCmp =
   -- Types
   UnknownTypeCmp + BoolTypeCmp + IntTypeCmp + FloatTypeCmp + CharTypeCmp +
   FunTypeCmp + SeqTypeCmp + TensorTypeCmp + RecordTypeCmp + VariantTypeCmp +
-  ConTypeCmp + VarTypeCmp + AppTypeCmp + AllTypeCmp + AliasTypeCmp
+  ConTypeCmp + DataTypeCmp + VarTypeCmp + AppTypeCmp + AllTypeCmp + AliasTypeCmp
 end
 
 -----------

stdlib/mexpr/const-types.mc

@@ -6,7 +6,6 @@ include "ast-builder.mc"
 
 let tysym_ = tycon_ "Symbol"
 let tyref_ = lam a. tyapp_ (tycon_ "Ref") a
-let tymap_ = lam k. lam v. tyapp_ (tyapp_ (tycon_ "Map") k) v
 let tybootparsetree_ = tycon_ "BootParseTree"
 
 let tyvarseq_ = lam id. tyseq_ (tyvar_ id)

stdlib/mexpr/eq.mc

@@ -637,6 +637,15 @@ lang ConTypeEq = Eq + ConTypeAst
     else None ()
 end
 
+lang DataTypeEq = Eq + DataTypeAst
+  sem eqTypeH (typeEnv : EqTypeEnv) (free : EqTypeFreeEnv) (lhs : Type) =
+  | rhs & TyData r ->
+    match unwrapType lhs with TyData l then
+      if mapEq setEq (computeData l) (computeData r) then Some free
+      else None ()
+    else None ()
+end
+
 lang VarTypeEq = Eq + VarTypeAst
   sem eqTypeH (typeEnv : EqTypeEnv) (free : EqTypeFreeEnv) (lhs : Type) =
   | TyVar r ->
@@ -714,8 +723,8 @@ lang MExprEq =
 
   -- Types
   + UnknownTypeEq + BoolTypeEq + IntTypeEq + FloatTypeEq + CharTypeEq +
-  FunTypeEq + SeqTypeEq + RecordTypeEq + VariantTypeEq + ConTypeEq + VarTypeEq +
-  AllTypeEq + AppTypeEq + TensorTypeEq + AliasTypeEq
+  FunTypeEq + SeqTypeEq + RecordTypeEq + VariantTypeEq + ConTypeEq + DataTypeEq +
+  VarTypeEq + AllTypeEq + AppTypeEq + TensorTypeEq + AliasTypeEq
 end
 
 -----------

stdlib/mexpr/pprint.mc

@@ -1144,13 +1144,24 @@ lang VariantTypePrettyPrint = VariantTypeAst
     -- still use TyVariant in the AST and might get compilation errors for it.
 end
 
-lang ConTypePrettyPrint = IdentifierPrettyPrint + ConTypeAst + UnknownTypeAst
+lang ConTypePrettyPrint = IdentifierPrettyPrint + ConTypeAst + UnknownTypeAst + DataTypeAst
   sem getTypeStringCode (indent : Int) (env: PprintEnv) =
   | TyCon t ->
     match pprintTypeName env t.ident with (env, idstr) in
-    match t.data with TyUnknown {} then (env, idstr) else
-      match getTypeStringCode indent env t.data with (env, str) in
-      (env, join [str, ".", idstr])
+    let d = unwrapType t.data in
+    match d with TyUnknown _ then (env, idstr) else
+      match getTypeStringCode indent env t.data with (env, datastr) in
+      match d with TyData _ then (env, concat idstr datastr) else
+        (env, join [idstr, "&", datastr])
+end
+
+lang DataTypePrettyPrint = IdentifierPrettyPrint + DataTypeAst
+  sem getTypeStringCode (indent : Int) (env: PprintEnv) =
+  | TyData t ->
+    let consstr = strJoin "|" (map nameGetStr (setToSeq t.cons)) in
+    let datastr =
+      join [if t.positive then "&" else "!", "{", consstr, "}"]
+    in (env, datastr)
 end
 
 lang VarTypePrettyPrint = IdentifierPrettyPrint + VarTypeAst
@@ -1159,22 +1170,19 @@ lang VarTypePrettyPrint = IdentifierPrettyPrint + VarTypeAst
     pprintVarName env t.ident
 end
 
-lang KindPrettyPrint = PrettyPrint + RecordTypeAst + KindAst
+lang KindPrettyPrint = PrettyPrint + RecordTypeAst + DataTypeAst + KindAst
   sem getKindStringCode (indent : Int) (env : PprintEnv) =
   | Record r ->
-    let recty = TyRecord {info = NoInfo (), fields = r.fields} in
-    match getTypeStringCode indent env recty with (env, recstr) in
-    (env, join [init recstr, " ... ", [last recstr]])
+    let tyrec = TyRecord {info = NoInfo (), fields = r.fields} in
+    getTypeStringCode indent env tyrec
   | Data r ->
-    let tstr =
-      mapFoldWithKey (lam strs. lam t. lam ks.
-        snoc strs (join [ nameGetStr t, "{"
-                        , strJoin ", " (map nameGetStr (setToSeq ks))
-                        , "}" ])
-    ) "" r.types in
-    (env, join ["<", strJoin ", " tstr, ">"])
-  | Poly () -> (env, "*")
-  | Mono () -> (env, "o")
+    let consstr =
+      mapFoldWithKey (lam strs. lam. lam ks.
+        snoc strs (strJoin "|" (map nameGetStr (setToSeq ks))))
+        [] r.types in
+    (env, join ["{", strJoin "|" consstr, "}"])
+  | Poly () -> (env, "Poly")
+  | Mono () -> (env, "Mono")
 end
 
 lang AllTypePrettyPrint = IdentifierPrettyPrint + AllTypeAst + KindPrettyPrint
@@ -1187,7 +1195,7 @@ lang AllTypePrettyPrint = IdentifierPrettyPrint + AllTypeAst + KindPrettyPrint
     match
       match t.kind with Mono () | Poly () then (env, "") else
         match getKindStringCode indent env t.kind with (env, kistr) in
-        (env, concat " :: " kistr)
+        (env, concat "::" kistr)
     with (env, kistr) in
     match getTypeStringCode indent env t.ty with (env, tystr) in
     (env, join ["all ", idstr, kistr, ". ", tystr])
@@ -1250,7 +1258,7 @@ lang MExprPrettyPrint =
   UnknownTypePrettyPrint + BoolTypePrettyPrint + IntTypePrettyPrint +
   FloatTypePrettyPrint + CharTypePrettyPrint + FunTypePrettyPrint +
   SeqTypePrettyPrint + RecordTypePrettyPrint + VariantTypePrettyPrint +
-  ConTypePrettyPrint + VarTypePrettyPrint +
+  ConTypePrettyPrint + DataTypePrettyPrint + VarTypePrettyPrint +
   AppTypePrettyPrint + TensorTypePrettyPrint + AllTypePrettyPrint +
   AliasTypePrettyPrint
 

stdlib/mexpr/symbolize.mc

@@ -304,7 +304,20 @@ lang ConTypeSym = Sym + ConTypeAst
                  allowFree = env.allowFree}
         env.tyConEnv t.ident
     in
-    TyCon {t with ident = ident}
+    TyCon {t with ident = ident, data = symbolizeType env t.data}
+end
+
+lang DataTypeSym = Sym + DataTypeAst
+  sem symbolizeType env =
+  | TyData t ->
+    let cons =
+      setOfSeq nameCmp
+        (map (getSymbol {kind = "constructor",
+                         info = [t.info],
+                         allowFree = env.allowFree}
+                env.conEnv)
+           (setToSeq t.cons))
+    in TyData {t with cons = cons}
 end
 
 lang VarTypeSym = Sym + VarTypeAst + UnknownTypeAst
@@ -411,7 +424,7 @@ lang MExprSym =
   MatchSym +
 
   -- Non-default implementations (Types)
-  VariantTypeSym + ConTypeSym + VarTypeSym + AllTypeSym +
+  VariantTypeSym + ConTypeSym + DataTypeSym + VarTypeSym + AllTypeSym +
 
   -- Non-default implementations (Patterns)
   NamedPatSym + SeqEdgePatSym + DataPatSym + NotPatSym