Add a typechecker

1 files changed, 89 insertions, 3 deletions

diff --git a/ShowSyntax.sml b/ShowSyntax.sml
index 651ddda..f28895d 100644
--- a/ShowSyntax.sml
+++ b/ShowSyntax.sml
@@ -47,7 +47,9 @@ and patToStringI (indent : string) (Syntax.PWild : Syntax.pat) : string =
 and patToString (x : Syntax.pat) : string = patToStringI "" x
 
 and exprToStringI (indent : string) (Syntax.EIdent x : Syntax.expr) : string =
-      "EIdent " ^ listToString (stringToStringI) indent x
+      "EIdent " ^ stringToStringI indent x
+  | exprToStringI (indent : string) (Syntax.EDot x : Syntax.expr) : string =
+      "EDot " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ structExprToStringI indent' x0 ^ ",\n" ^ indent' ^ stringToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
   | exprToStringI (indent : string) (Syntax.EBuiltin x : Syntax.expr) : string =
       "EBuiltin " ^ stringToStringI indent x
   | exprToStringI (indent : string) (Syntax.EInt x : Syntax.expr) : string =
@@ -81,7 +83,7 @@ and decToStringI (indent : string) (Syntax.DVal x : Syntax.dec) : string =
   | decToStringI (indent : string) (Syntax.DFun x : Syntax.dec) : string =
       "DFun " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString (patToStringI) indent' x0 ^ ",\n" ^ indent' ^ exprToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
   | decToStringI (indent : string) (Syntax.DDatatype x : Syntax.dec) : string =
-      "DDatatype " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ optionToString (etypeToStringI) indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+      "DDatatype " ^ (fn indent => fn (x0, x1, x2) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString (stringToStringI) indent' x0 ^ ",\n" ^ indent' ^ stringToStringI indent' x1 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ optionToString (etypeToStringI) indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x2 ^ "\n" ^ indent ^ ")" end) indent x
   | decToStringI (indent : string) (Syntax.DType x : Syntax.dec) : string =
       "DType " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ etypeToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
   | decToStringI (indent : string) (Syntax.DStruct x : Syntax.dec) : string =
@@ -89,11 +91,95 @@ and decToStringI (indent : string) (Syntax.DVal x : Syntax.dec) : string =
 and decToString (x : Syntax.dec) : string = decToStringI "" x
 
 and structExprToStringI (indent : string) (Syntax.SIdent x : Syntax.structExpr) : string =
-      "SIdent " ^ listToString (stringToStringI) indent x
+      "SIdent " ^ stringToStringI indent x
+  | structExprToStringI (indent : string) (Syntax.SDot x : Syntax.structExpr) : string =
+      "SDot " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ structExprToStringI indent' x0 ^ ",\n" ^ indent' ^ stringToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
   | structExprToStringI (indent : string) (Syntax.SStruct x : Syntax.structExpr) : string =
       "SStruct " ^ listToString (decToStringI) indent x
 and structExprToString (x : Syntax.structExpr) : string = structExprToStringI "" x
 
+and tyToStringI (indent : string) (Syntax.TInt : Syntax.ty) : string =
+      "TInt"
+  | tyToStringI (indent : string) (Syntax.TBool : Syntax.ty) : string =
+      "TBool"
+  | tyToStringI (indent : string) (Syntax.TString : Syntax.ty) : string =
+      "TString"
+  | tyToStringI (indent : string) (Syntax.TVar x : Syntax.ty) : string =
+      "TVar " ^ intToStringI indent x
+  | tyToStringI (indent : string) (Syntax.TTuple x : Syntax.ty) : string =
+      "TTuple " ^ listToString (tyToStringI) indent x
+  | tyToStringI (indent : string) (Syntax.TFun x : Syntax.ty) : string =
+      "TFun " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ tyToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | tyToStringI (indent : string) (Syntax.TList x : Syntax.ty) : string =
+      "TList " ^ tyToStringI indent x
+  | tyToStringI (indent : string) (Syntax.TDatatype x : Syntax.ty) : string =
+      "TDatatype " ^ listToString (stringToStringI) indent x
+and tyToString (x : Syntax.ty) : string = tyToStringI "" x
+
+and structTypeToStringI (indent : string) (Syntax.TStruct x : Syntax.structType) : string =
+      "TStruct " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ structTypeToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+and structTypeToString (x : Syntax.structType) : string = structTypeToStringI "" x
+
+and typedPatToStringI (indent : string) (Syntax.TPWild : Syntax.typedPat) : string =
+      "TPWild"
+  | typedPatToStringI (indent : string) (Syntax.TPVar x : Syntax.typedPat) : string =
+      "TPVar " ^ stringToStringI indent x
+  | typedPatToStringI (indent : string) (Syntax.TPInt x : Syntax.typedPat) : string =
+      "TPInt " ^ intToStringI indent x
+  | typedPatToStringI (indent : string) (Syntax.TPTuple x : Syntax.typedPat) : string =
+      "TPTuple " ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent x
+  | typedPatToStringI (indent : string) (Syntax.TPCon x : Syntax.typedPat) : string =
+      "TPCon " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString (stringToStringI) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+and typedPatToString (x : Syntax.typedPat) : string = typedPatToStringI "" x
+
+and typedExprToStringI (indent : string) (Syntax.TEIdent x : Syntax.typedExpr) : string =
+      "TEIdent " ^ stringToStringI indent x
+  | typedExprToStringI (indent : string) (Syntax.TEDot x : Syntax.typedExpr) : string =
+      "TEDot " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedStructExprToStringI indent' x0 ^ ",\n" ^ indent' ^ structTypeToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ stringToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TEBuiltin x : Syntax.typedExpr) : string =
+      "TEBuiltin " ^ stringToStringI indent x
+  | typedExprToStringI (indent : string) (Syntax.TEInt x : Syntax.typedExpr) : string =
+      "TEInt " ^ intToStringI indent x
+  | typedExprToStringI (indent : string) (Syntax.TEStr x : Syntax.typedExpr) : string =
+      "TEStr " ^ stringToStringI indent x
+  | typedExprToStringI (indent : string) (Syntax.TETuple x : Syntax.typedExpr) : string =
+      "TETuple " ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent x
+  | typedExprToStringI (indent : string) (Syntax.TEList x : Syntax.typedExpr) : string =
+      "TEList " ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent x
+  | typedExprToStringI (indent : string) (Syntax.TEApp x : Syntax.typedExpr) : string =
+      "TEApp " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TEAndAlso x : Syntax.typedExpr) : string =
+      "TEAndAlso " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TEOrElse x : Syntax.typedExpr) : string =
+      "TEOrElse " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TELet x : Syntax.typedExpr) : string =
+      "TELet " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString (typedDecToStringI) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TELambda x : Syntax.typedExpr) : string =
+      "TELambda " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedExprToStringI (indent : string) (Syntax.TECase x : Syntax.typedExpr) : string =
+      "TECase " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+and typedExprToString (x : Syntax.typedExpr) : string = typedExprToStringI "" x
+
+and typedDecToStringI (indent : string) (Syntax.TDVal x : Syntax.typedDec) : string =
+      "TDVal " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedDecToStringI (indent : string) (Syntax.TDValRec x : Syntax.typedDec) : string =
+      "TDValRec " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedDecToStringI (indent : string) (Syntax.TDFun x : Syntax.typedDec) : string =
+      "TDFun " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedPatToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedExprToStringI indent' x0 ^ ",\n" ^ indent' ^ tyToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedDecToStringI (indent : string) (Syntax.TDDatatype x : Syntax.typedDec) : string =
+      "TDDatatype " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ listToString ((fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ optionToString (tyToStringI) indent' x1 ^ "\n" ^ indent ^ ")" end)) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedDecToStringI (indent : string) (Syntax.TDStruct x : Syntax.typedDec) : string =
+      "TDStruct " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ stringToStringI indent' x0 ^ ",\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedStructExprToStringI indent' x0 ^ ",\n" ^ indent' ^ structTypeToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+and typedDecToString (x : Syntax.typedDec) : string = typedDecToStringI "" x
+
+and typedStructExprToStringI (indent : string) (Syntax.TSIdent x : Syntax.typedStructExpr) : string =
+      "TSIdent " ^ stringToStringI indent x
+  | typedStructExprToStringI (indent : string) (Syntax.TSDot x : Syntax.typedStructExpr) : string =
+      "TSDot " ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ (fn indent => fn (x0, x1) => let val indent' = indent ^ "  " in "(\n" ^ indent' ^ typedStructExprToStringI indent' x0 ^ ",\n" ^ indent' ^ structTypeToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent' x0 ^ ",\n" ^ indent' ^ stringToStringI indent' x1 ^ "\n" ^ indent ^ ")" end) indent x
+  | typedStructExprToStringI (indent : string) (Syntax.TSStruct x : Syntax.typedStructExpr) : string =
+      "TSStruct " ^ listToString (typedDecToStringI) indent x
+and typedStructExprToString (x : Syntax.typedStructExpr) : string = typedStructExprToStringI "" x
+
 and primopToStringI (indent : string) (Syntax.PExit : Syntax.primop) : string =
       "PExit"
   | primopToStringI (indent : string) (Syntax.PAdd : Syntax.primop) : string =