Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Error reflection demo from today
module ErrorReflectionDemo
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Col = BOOL | STRING | INT
%name Col t
interp : Col -> Type
interp BOOL = Bool
interp STRING = String
interp INT = Integer
infix 7 :::
instance Show Col where
show BOOL = "BOOL"
show STRING = "STRING"
show INT = "INT"
instance Eq Col where
BOOL == BOOL = True
STRING == STRING = True
INT == INT = True
_ == _ = False
data Attr = (:::) String Col
instance Show Attr where
show (a:::b) = show a ++ ":::" ++ show b
Schema : Type
Schema = List Attr
%name Schema s
namespace Row
data Row : Schema -> Type where
Nil : Row []
(::) : (interp t) -> (Row s) -> Row ((name:::t)::s)
%name Row r
namespace Table
data Table : Schema -> Type where
Nil : Table s
(::) : Row s -> Table s -> Table s
colType : Schema -> String -> Maybe Col
colType [] x = Nothing
colType ((name:::ty)::s) x =
if name == x
then Just ty
else colType s x
data Disjointness = Disjoint | Overlapping String
data IsDisjoint : Disjointness -> Type where
Ok : IsDisjoint Disjoint
isDisjoint : Schema -> Schema -> Disjointness
isDisjoint [] s = Disjoint
isDisjoint ((name:::ty)::s') s =
case colType s name of
Nothing => isDisjoint s' s
Just _ => Overlapping name
getName : TT -> Maybe String
getName (App con (TConst (Str name))) = if isOverlappingCon con then Just name else Nothing
where isOverlappingCon : TT -> Bool
isOverlappingCon (P (DCon _ _) (NS (UN "Overlapping") _) _) = True
isOverlappingCon _ = False
getName _ = Nothing
total
getSchemas : TT -> Maybe (TT, TT)
getSchemas (App (P (TCon _ _) (NS (UN "IsDisjoint") _) _) call) =
getSchemas' call
where total
getSchemas' : TT -> Maybe (TT, TT)
getSchemas' (App (App (P _ (NS (UN "isDisjoint") _) _) s1) s2) = Just (s1, s2)
getSchemas' _ = Nothing
getSchemas _ = Nothing
inConstr : TTName -> TT -> Maybe TT
inConstr n (App (P (DCon _ _) n' _) tm) = if n == n' then Just tm else Nothing
inConstr _ _ = Nothing
inConstr2 : TTName -> TT -> Maybe (TT, TT)
inConstr2 n (App (App (P (DCon _ _) n' _) tm) tm') = if n == n' then Just (tm, tm') else Nothing
inConstr2 _ _ = Nothing
inConstr3 : TTName -> TT -> Maybe (TT, TT, TT)
inConstr3 n (App (App (App (P (DCon _ _) n' _) tm) tm') tm'') = if n == n' then Just (tm, tm', tm'') else Nothing
inConstr3 _ _ = Nothing
inTCon : TTName -> TT -> Maybe TT
inTCon n (App (P (TCon _ _) n' _) tm) = if n == n' then Just tm else Nothing
inTCon _ _ = Nothing
funArg : TT -> Maybe TT
funArg (App f x) = Just x
funArg _ = Nothing
funArg2 : TT -> Maybe (TT, TT)
funArg2 (App (App f x) y) = Just (x, y)
funArg2 _ = Nothing
maybeToList : Maybe a -> List a
maybeToList Nothing = []
maybeToList (Just x) = [x]
data Subness = Subschema | MissingCol String | TypeMismatch String Col Col
-- the second is subschema of the first
total isSub : Schema -> Schema -> Subness
isSub s1 [] = Subschema
isSub s1 ((name:::ty)::s2) =
case colType s1 name of
Nothing => MissingCol name
Just ty' => if ty == ty' then isSub s1 s2 else TypeMismatch name ty ty'
data IsSub : Subness -> Type where
Sub : IsSub Subschema
getIsSubSchemas : TT -> Maybe (TT, TT)
getIsSubSchemas tm = funArg2 !(inTCon (NS (UN "IsSub") ["ErrorReflectionDemo"]) tm)
data RA : Schema -> Type where
T : Table s -> RA s
U : RA s -> RA s -> RA s
(\\) : RA s -> RA s -> RA s
Product : {default Ok ok : IsDisjoint (isDisjoint s1 s2)} ->
RA s1 -> RA s2 -> RA (s1 ++ s2)
Project : RA s1 -> (s2 : Schema) ->
{default Sub ok : IsSub (isSub s1 s2)} ->
RA s2
-- Missing select, rename
module ErrorReflectionDemoHandlers
import ErrorReflectionDemo
import Language.Reflection.Errors
%language ErrorReflection
%error_handler total
disjointness : Err -> Maybe (List ErrorReportPart)
disjointness (CantUnify _ tm1 tm2 err _ _) =
let next = disjointness err in
case (getSchemas tm2, getName tm2) of
(Just (s1, s2), _) => Just $ [TextPart "Cannot take the product of queries with schemas",
SubReport [TermPart s1],
TextPart "and",
SubReport [TermPart s2],
TextPart "because"] ++ map SubReport (maybeToList next)
(Nothing, Just name) => Just [TextPart "both contain column", TermPart (TConst (Str name))]
(Nothing, Nothing) => next
disjointness e = Nothing
%error_handler total
subness : Err -> Maybe (List ErrorReportPart)
subness (CantUnify _ tm1 tm2 err _ _) = firstTry (getIsSubSchemas tm2)
where total
firstTry : Maybe (TT, TT) -> Maybe (List ErrorReportPart)
firstTry (Just (super, sub)) =
Just $ [ TermPart sub
, TextPart "is not a subschema of"
, TermPart super
, TextPart "because"] ++ map SubReport (maybeToList (subness err))
firstTry Nothing = secondTry (inConstr3 (NS (UN "TypeMismatch") ["ErrorReflectionDemo"]) tm2)
where total
secondTry : Maybe (TT, TT ,TT) -> Maybe (List ErrorReportPart)
secondTry (Just (column, supt, subt)) =
Just $ [ TextPart "The column"
, TermPart column
, TextPart "has mismatching types"
, TermPart supt
, TextPart "and"
, TermPart subt] ++ map SubReport (maybeToList (subness err))
secondTry Nothing = thirdTry (inConstr (NS (UN "MissingCol") ["ErrorReflectionDemo"]) tm2)
where thirdTry (Just name) =
Just $ [ TextPart "The column"
, TermPart name
, TextPart "does not exist"] ++ map SubReport (maybeToList (subness err))
thirdTry Nothing = subness err
subness _ = Nothing
module ReflectionDemo1
import ErrorReflectionDemo
import ErrorReflectionDemoHandlers
t1 : Table ["name":::STRING, "age":::INT]
t1 = [["David", 29], ["Joe", 30]]
t2 : Table ["name":::STRING, "bike":::BOOL]
t2 = [["David", True], ["Joe", False]]
prod : RA ["name":::STRING, "age":::INT, "name":::STRING,"bike":::BOOL]
prod = T t1 `Product` T t2
module ReflectionDemo2
import ErrorReflectionDemo
import ErrorReflectionDemoHandlers
t1 : Table ["name":::STRING, "age":::INT]
t1 = [["David", 29], ["Joe", 30]]
t2 : Table ["name":::STRING, "bike":::BOOL]
t2 = [["David", True], ["Joe", False]]
proj : RA ["foo":::INT]
proj = T t1 `Project` ["foo" ::: INT]
proj2 : RA ["name":::INT]
proj2 = T t1 `Project` ["name":::INT]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.