diff --git a/Idrall/Check.idr b/Idrall/Check.idr index f494f0b..d20ca62 100644 --- a/Idrall/Check.idr +++ b/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 diff --git a/Idrall/Expr.idr b/Idrall/Expr.idr index ef52cce..1e71f16 100644 --- a/Idrall/Expr.idr +++ 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 diff --git a/Idrall/Parser.idr b/Idrall/Parser.idr index 5ddfe12..703b615 100644 --- a/Idrall/Parser.idr +++ b/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) diff --git a/Idrall/Resolve.idr b/Idrall/Resolve.idr index f0b8214..a797ccf 100644 --- a/Idrall/Resolve.idr +++ b/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 diff --git a/Idrall/Value.idr b/Idrall/Value.idr index 684e739..2cba0b3 100644 --- a/Idrall/Value.idr +++ b/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