Error reflection demo from today

ErrorReflectionDemo.idr

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

ErrorReflectionDemoHandlers.idr

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

ReflectionDemo1.idr

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

ReflectionDemo2.idr

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]