Quasiquote005.idr

module Quasiquote005

-- Test Raw quasiquotes

test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =
       RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))
                  (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
                        (Var (NS (UN "Z") ["Nat", "Prelude"]))))
            (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
                  (Var (NS (UN "Z") ["Nat", "Prelude"])))
test = Refl

firstAddend : Raw -> Maybe Raw
firstAddend `(plus ~first ~_) = Just first
firstAddend _ = Nothing

firstAddendOk : firstAddend (RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))
                                        (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
                                              (Var (NS (UN "Z") ["Nat", "Prelude"]))))
                                  (Var (NS (UN "Z") ["Nat", "Prelude"]))) =
                the (Maybe Raw) (Just `(S Z))
firstAddendOk = Refl