Use FieldName instead of String for Unions

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>

Idrall/Check.idr

@@ -106,8 +106,8 @@ mutual
   aEquivList i ns1 _ ns2 _ = False
 
   aEquivUnion : (i : Integer) ->
-                Namespace -> List (String, (Maybe (Expr Void))) ->
-                Namespace -> List (String, (Maybe (Expr Void))) -> Bool
+                Namespace -> List (FieldName, (Maybe (Expr Void))) ->
+                Namespace -> List (FieldName, (Maybe (Expr Void))) -> Bool
   aEquivUnion i ns1 [] ns2 [] = True
   aEquivUnion i ns1 ((k, Nothing) :: xs) ns2 ((k', Nothing) :: ys) =
     k == k' && aEquivUnion i ns1 xs ns2 ys
@@ -459,13 +459,13 @@ mutual
            do aRB <- traverse (readBackUnion ctx) (toList a)
               arg'' <- readBackTyped ctx k' arg'
               Right (EApp (EField (EUnion (fromList aRB)) k) (arg''))
-         (Just Nothing, Just arg') => Left (FieldArgMismatchError ("No type for param " ++ k))
+         (Just Nothing, Just arg') => Left (FieldArgMismatchError ("No type for param " ++ show k))
          (Just _, _) => Right (EField
                                       (EUnion (fromList !(traverse (readBackUnion ctx) (toList a)))) k)
-         (Nothing, _) => Left (FieldNotFoundError k)
+         (Nothing, _) => Left (FieldNotFoundError (show k))
   readBackTyped _ t v = Left (ReadBackError ("error reading back: " ++ (show v) ++ " of type: " ++ (show t)))
 
-  readBackUnion : Ctx -> (String, Maybe Value) -> Either Error (String, Maybe (Expr Void))
+  readBackUnion : Ctx -> (FieldName, Maybe Value) -> Either Error (FieldName, Maybe (Expr Void))
   readBackUnion ctx (k, Nothing) = Right (k, Nothing)
   readBackUnion ctx (k, Just v) = Right (k, Just !(readBackTyped ctx (VConst CType) v))
     -- TODO is (VConst CType) always right here ^^^? Looks like rBT ignores the Ty param when reading back VConsts so maybe?
@@ -732,7 +732,7 @@ mutual
       ty <- foldl getHighestType (Right (VConst CType)) (map snd types)
       Right ty
     where
-      synthUnion : (String, Maybe (Expr Void)) -> Either Error (String, Maybe Ty)
+      synthUnion : (FieldName, Maybe (Expr Void)) -> Either Error (FieldName, Maybe Ty)
       synthUnion (k, Nothing) = Right (k, Nothing)
       synthUnion (k, Just b) = do
         b' <- synth ctx b

Idrall/Expr.idr

@@ -6,6 +6,21 @@ public export
 Name : Type
 Name = String
 
+public export
+data FieldName = MkFieldName String
+
+public export
+Show FieldName where
+  show (MkFieldName x) = "(MkFieldName " ++ x
+
+public export
+Eq FieldName where
+  (==) (MkFieldName x) (MkFieldName y) = x == y
+
+public export
+Ord FieldName where
+  compare (MkFieldName x) (MkFieldName y) = compare x y
+
 public export
 Namespace : Type
 Namespace = List (Name, Integer)
@@ -88,8 +103,8 @@ mutual
     | EOptional (Expr a)
     | ENone (Expr a)
     | ESome (Expr a)
-    | EUnion (SortedMap String (Maybe (Expr a)))
-    | EField (Expr a) String
+    | EUnion (SortedMap FieldName (Maybe (Expr a)))
+    | EField (Expr a) FieldName
     | EEmbed (Import a)
 
 export

Idrall/Parser.idr

@@ -128,7 +128,7 @@ field : Parser ((Expr ImportStatement) -> (Expr ImportStatement))
 field = do
   token "."
   i <- identity
-  pure (\e => (EField e i))
+  pure (\e => (EField e (MkFieldName i)))
 
 table : OperatorTable (Expr ImportStatement)
 table = [ [ Postfix field]
@@ -141,19 +141,19 @@ table = [ [ Postfix field]
         , [ Infix (do token "#"; pure EListAppend) AssocLeft]]
 
 mutual
-  unionSimpleElem : Parser (String, Maybe (Expr ImportStatement))
+  unionSimpleElem : Parser (FieldName, Maybe (Expr ImportStatement))
   unionSimpleElem = do
     k <- identity
-    pure (k, Nothing)
+    pure (MkFieldName k, Nothing)
 
-  unionComplexElem : Parser (String, Maybe (Expr ImportStatement))
+  unionComplexElem : Parser (FieldName, Maybe (Expr ImportStatement))
   unionComplexElem = do
     k <- identity
     token ":"
     e <- expr
-    pure (k, Just e)
+    pure (MkFieldName k, Just e)
 
-  unionElem : Parser (String, Maybe (Expr ImportStatement))
+  unionElem : Parser (FieldName, Maybe (Expr ImportStatement))
   unionElem = unionComplexElem <|> unionSimpleElem
 
   union : Parser (Expr ImportStatement)

Idrall/Resolve.idr

@@ -143,8 +143,8 @@ mutual
 
   resolveUnion :  (history : List FilePath) -- TODO try use traverse instead?
                -> Maybe FilePath
-               -> List (String, Maybe (Expr ImportStatement))
-               -> IOEither Error (List (String, Maybe (Expr Void)))
+               -> List (FieldName, Maybe (Expr ImportStatement))
+               -> IOEither Error (List (FieldName, Maybe (Expr Void)))
   resolveUnion h p [] = MkIOEither (pure (Right []))
   resolveUnion h p ((k,v) :: xs) = do
     rest <- resolveUnion h p xs

Idrall/Value.idr

@@ -55,8 +55,8 @@ mutual
     | VOptional Ty
     | VNone Ty
     | VSome Ty
-    | VUnion (SortedMap String (Maybe Value))
-    | VInject (SortedMap String (Maybe Value)) String (Maybe Value) -- TODO proof that key is in SM?
+    | VUnion (SortedMap FieldName (Maybe Value))
+    | VInject (SortedMap FieldName (Maybe Value)) FieldName (Maybe Value) -- TODO proof that key is in SM?
     | VPrimVar
     | VNeutral Ty Neutral