module Language.Reflection import Builtins import Prelude.Applicative import Prelude.Basics import Prelude.Bool import Prelude.Either import Prelude.Foldable import Prelude.Functor import Prelude.List import Prelude.Maybe import Prelude.Nat import Prelude.Traversable import Prelude.Uninhabited import Decidable.Equality %access public export ||| A source location in an Idris file record SourceLocation where ||| Either a source span or a source location. `start` and `end` ||| will be the same if it's a point location. constructor FileLoc ||| The file name of the source location filename : String ||| The line and column of the beginning of the source span start : (Int, Int) ||| The line and column of the end of the source span end : (Int, Int) %name SourceLocation loc, loc' private fileLocInj : (FileLoc fn s e = FileLoc fn' s' e') -> (fn = fn', s = s', e = e') fileLocInj Refl = (Refl, Refl, Refl) implementation DecEq SourceLocation where decEq (FileLoc f s e) (FileLoc f' s' e') with (decEq f f') decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl with (decEq s s') decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl with (decEq e e') decEq (FileLoc f s e) (FileLoc f s e) | Yes Refl | Yes Refl | Yes Refl = Yes Refl decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl | No contra = No $ contra . snd . snd . fileLocInj decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl | No contra = No $ contra . fst . snd . fileLocInj decEq (FileLoc f s e) (FileLoc f' s' e') | No contra = No $ contra . fst . fileLocInj mutual data TTName = ||| A user-provided name UN String | ||| A name in some namespace. ||| ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])` ||| represents the name `A.B.foo` NS TTName (List String) | ||| Machine-chosen names MN Int String | ||| Special names, to make conflicts impossible and language features ||| predictable SN SpecialName %name TTName n, n' data SpecialName = WhereN Int TTName TTName | WithN Int TTName | ImplementationN TTName (List String) | ParentN TTName String | MethodN TTName | CaseN SourceLocation TTName | ImplementationCtorN TTName | MetaN TTName TTName %name SpecialName sn, sn' -- Rather than implement one-off private functions, we make the -- disjointness of the constructors available to all Idris programs, -- at the cost of a bit of scrolling here. implementation Uninhabited (UN _ = NS _ _) where uninhabited Refl impossible implementation Uninhabited (UN _ = MN _ _) where uninhabited Refl impossible implementation Uninhabited (UN _ = SN _) where uninhabited Refl impossible implementation Uninhabited (NS _ _ = UN _) where uninhabited Refl impossible implementation Uninhabited (NS _ _ = MN _ _) where uninhabited Refl impossible implementation Uninhabited (NS _ _ = SN _) where uninhabited Refl impossible implementation Uninhabited (MN _ _ = UN _) where uninhabited Refl impossible implementation Uninhabited (MN _ _ = NS _ _) where uninhabited Refl impossible implementation Uninhabited (MN _ _ = SN _) where uninhabited Refl impossible implementation Uninhabited (SN _ = UN _) where uninhabited Refl impossible implementation Uninhabited (SN _ = MN _ _) where uninhabited Refl impossible implementation Uninhabited (SN _ = NS _ _) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (WithN y z)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (ImplementationN y xs)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (ParentN y z)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (MethodN y)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (ImplementationCtorN y)) where uninhabited Refl impossible implementation Uninhabited ((WhereN x n n') = (MetaN y z)) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (WhereN y n' z)) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (ImplementationN n' xs)) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (ParentN n' y)) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (MethodN n')) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (CaseN loc n')) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (ImplementationCtorN n')) where uninhabited Refl impossible implementation Uninhabited ((WithN x n) = (MetaN n' y)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (WhereN x n' y)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (WithN x n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (ParentN n' x)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (MethodN n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (CaseN loc n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (ImplementationCtorN n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationN n xs) = (MetaN n' x)) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (WhereN y n' z)) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (WithN y n')) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (ImplementationN n' xs)) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (MethodN n')) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (ImplementationCtorN n')) where uninhabited Refl impossible implementation Uninhabited ((ParentN n x) = (MetaN n' y)) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (WhereN x n' y)) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (WithN x n')) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (ImplementationN n' xs)) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (ParentN n' x)) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (CaseN loc n')) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (ImplementationCtorN n')) where uninhabited Refl impossible implementation Uninhabited ((MethodN n) = (MetaN n' x)) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (WhereN x n' y)) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (WithN x n')) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (ImplementationN n' xs)) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (ParentN n' x)) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (MethodN n')) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (ImplementationCtorN n')) where uninhabited Refl impossible implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (WhereN x n' y)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (WithN x n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (ImplementationN n' xs)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (ParentN n' x)) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (MethodN n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (CaseN loc n')) where uninhabited Refl impossible implementation Uninhabited ((ImplementationCtorN n) = (MetaN n' x)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (WhereN x y z)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (WithN x y)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (ImplementationN x xs)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (ParentN x y)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (MethodN x)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where uninhabited Refl impossible implementation Uninhabited ((MetaN n n') = (ImplementationCtorN x)) where uninhabited Refl impossible mutual private unInj : (UN x = UN y) -> x = y unInj Refl = Refl private nsInj : (NS n ns = NS n' ns') -> (n = n', ns = ns') nsInj Refl = (Refl, Refl) private mnInj : (MN i s = MN i' s') -> (i = i', s = s') mnInj Refl = (Refl, Refl) private snInj : SN sn = SN sn' -> sn = sn' snInj Refl = Refl private decTTNameEq : (n1, n2 : TTName) -> Dec (n1 = n2) decTTNameEq (UN x) (UN y) with (decEq x y) decTTNameEq (UN x) (UN y) | Yes prf = Yes (cong prf) decTTNameEq (UN x) (UN y) | No contra = No $ contra . unInj decTTNameEq (UN x) (NS n xs) = No absurd decTTNameEq (UN x) (MN y z) = No absurd decTTNameEq (UN x) (SN y) = No absurd decTTNameEq (NS n xs) (UN x) = No absurd decTTNameEq (NS n ns) (NS n' ns') with (decTTNameEq n n') decTTNameEq (NS n ns) (NS n ns') | Yes Refl with (decEq ns ns') decTTNameEq (NS n ns) (NS n ns) | Yes Refl | Yes Refl = Yes Refl decTTNameEq (NS n ns) (NS n ns') | Yes Refl | No contra = No $ contra . snd . nsInj decTTNameEq (NS n ns) (NS n' ns') | No contra = No $ contra . fst . nsInj decTTNameEq (NS n xs) (MN x y) = No absurd decTTNameEq (NS n xs) (SN x) = No absurd decTTNameEq (MN x y) (UN z) = No absurd decTTNameEq (MN x y) (NS n xs) = No absurd decTTNameEq (MN x y) (MN z w) with (decEq x z) decTTNameEq (MN x y) (MN x w) | Yes Refl with (decEq y w) decTTNameEq (MN x y) (MN x y) | Yes Refl | Yes Refl = Yes Refl decTTNameEq (MN x y) (MN x w) | Yes Refl | No contra = No $ contra . snd . mnInj decTTNameEq (MN x y) (MN z w) | No contra = No $ contra . fst . mnInj decTTNameEq (MN x y) (SN z) = No absurd decTTNameEq (SN x) (UN y) = No absurd decTTNameEq (SN x) (NS n xs) = No absurd decTTNameEq (SN x) (MN y z) = No absurd decTTNameEq (SN x) (SN y) with (decSNEq x y) decTTNameEq (SN x) (SN x) | Yes Refl = Yes Refl decTTNameEq (SN x) (SN y) | (No contra) = No $ contra . snInj private whereNInj : (WhereN x n n' = WhereN y z w) -> (x = y, n = z, n' = w) whereNInj Refl = (Refl, Refl, Refl) private withNInj : (WithN x n = WithN y n') -> (x = y, n = n') withNInj Refl = (Refl, Refl) private instanceNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys) instanceNInj Refl = (Refl, Refl) private implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys) implementationNInj Refl = (Refl, Refl) private parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y) parentNInj Refl = (Refl, Refl) private methodNInj : (MethodN n = MethodN n') -> n = n' methodNInj Refl = Refl private caseNInj : (CaseN loc n = CaseN loc' n') -> (loc = loc', n = n') caseNInj Refl = (Refl, Refl) private implementationCtorNInj : (ImplementationCtorN n = ImplementationCtorN n') -> n = n' implementationCtorNInj Refl = Refl private metaNInj : (MetaN n m = MetaN n' m') -> (n = n', m = m') metaNInj Refl = (Refl, Refl) private decSNEq : (n1, n2 : SpecialName) -> Dec (n1 = n2) decSNEq (WhereN x n n') (WhereN y z w) with (decEq x y) decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl with (assert_total $ decTTNameEq n z) decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl with (assert_total $ decTTNameEq n' w) decSNEq (WhereN x n n') (WhereN x n n') | Yes Refl | Yes Refl | Yes Refl = Yes Refl decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl | No contra = No $ contra . snd . snd . whereNInj decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl | No contra = No $ contra . fst . snd . whereNInj decSNEq (WhereN x n n') (WhereN y z w) | No contra = No $ contra . fst . whereNInj decSNEq (WhereN x n n') (WithN y z) = No absurd decSNEq (WhereN x n n') (ImplementationN y xs) = No absurd decSNEq (WhereN x n n') (ParentN y z) = No absurd decSNEq (WhereN x n n') (MethodN y) = No absurd decSNEq (WhereN x n n') (CaseN loc y) = No absurd decSNEq (WhereN x n n') (ImplementationCtorN y) = No absurd decSNEq (WhereN x n n') (MetaN y z) = No absurd decSNEq (WithN x n) (WhereN y n' z) = No absurd decSNEq (WithN x n) (WithN y n') with (decEq x y) decSNEq (WithN x n) (WithN x n') | Yes Refl with (assert_total $ decTTNameEq n n') decSNEq (WithN x n) (WithN x n) | Yes Refl | Yes Refl = Yes Refl decSNEq (WithN x n) (WithN x n') | Yes Refl | No contra = No $ contra . snd . withNInj decSNEq (WithN x n) (WithN y n') | No contra = No $ contra . fst . withNInj decSNEq (WithN x n) (ImplementationN n' xs) = No absurd decSNEq (WithN x n) (ParentN n' y) = No absurd decSNEq (WithN x n) (MethodN n') = No absurd decSNEq (WithN x n) (CaseN loc n') = No absurd decSNEq (WithN x n) (ImplementationCtorN n') = No absurd decSNEq (WithN x n) (MetaN n' y) = No absurd decSNEq (ImplementationN n xs) (WhereN x n' y) = No absurd decSNEq (ImplementationN n xs) (WithN x n') = No absurd decSNEq (ImplementationN n xs) (ImplementationN n' ys) with (assert_total $ decTTNameEq n n') decSNEq (ImplementationN n xs) (ImplementationN n ys) | Yes Refl with (decEq xs ys) decSNEq (ImplementationN n xs) (ImplementationN n xs) | Yes Refl | Yes Refl = Yes Refl decSNEq (ImplementationN n xs) (ImplementationN n ys) | Yes Refl | No contra = No $ contra . snd . implementationNInj decSNEq (ImplementationN n xs) (ImplementationN n' ys) | No contra = No $ contra . fst . implementationNInj decSNEq (ImplementationN n xs) (ParentN n' x) = No absurd decSNEq (ImplementationN n xs) (MethodN n') = No absurd decSNEq (ImplementationN n xs) (CaseN loc n') = No absurd decSNEq (ImplementationN n xs) (ImplementationCtorN n') = No absurd decSNEq (ImplementationN n xs) (MetaN n' x) = No absurd decSNEq (ParentN n x) (WhereN y n' z) = No absurd decSNEq (ParentN n x) (WithN y n') = No absurd decSNEq (ParentN n x) (ImplementationN n' xs) = No absurd decSNEq (ParentN n x) (ParentN n' y) with (assert_total $ decTTNameEq n n') decSNEq (ParentN n x) (ParentN n y) | Yes Refl with (decEq x y) decSNEq (ParentN n x) (ParentN n x) | Yes Refl | Yes Refl = Yes Refl decSNEq (ParentN n x) (ParentN n y) | Yes Refl | No contra = No $ contra . snd . parentNInj decSNEq (ParentN n x) (ParentN n' y) | No contra = No $ contra . fst . parentNInj decSNEq (ParentN n x) (MethodN n') = No absurd decSNEq (ParentN n x) (CaseN loc n') = No absurd decSNEq (ParentN n x) (ImplementationCtorN n') = No absurd decSNEq (ParentN n x) (MetaN n' y) = No absurd decSNEq (MethodN n) (WhereN x n' y) = No absurd decSNEq (MethodN n) (WithN x n') = No absurd decSNEq (MethodN n) (ImplementationN n' xs) = No absurd decSNEq (MethodN n) (ParentN n' x) = No absurd decSNEq (MethodN n) (MethodN n') with (assert_total $ decTTNameEq n n') decSNEq (MethodN n) (MethodN n) | Yes Refl = Yes Refl decSNEq (MethodN n) (MethodN n') | No contra = No $ contra . methodNInj decSNEq (MethodN n) (CaseN loc n') = No absurd decSNEq (MethodN n) (ImplementationCtorN n') = No absurd decSNEq (MethodN n) (MetaN n' x) = No absurd decSNEq (CaseN loc n) (WhereN x n' y) = No absurd decSNEq (CaseN loc n) (WithN x n') = No absurd decSNEq (CaseN loc n) (ImplementationN n' xs) = No absurd decSNEq (CaseN loc n) (ParentN n' x) = No absurd decSNEq (CaseN loc n) (MethodN n') = No absurd decSNEq (CaseN loc n) (CaseN loc' n') with (decEq loc loc') decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl with (assert_total $ decTTNameEq n n') decSNEq (CaseN loc n) (CaseN loc n) | Yes Refl | Yes Refl = Yes Refl decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl | No contra = No $ contra . snd . caseNInj decSNEq (CaseN loc n) (CaseN loc' n') | No contra = No $ contra . fst . caseNInj decSNEq (CaseN loc n) (ImplementationCtorN n') = No absurd decSNEq (CaseN loc n) (MetaN n' x) = No absurd decSNEq (ImplementationCtorN n) (WhereN x n' y) = No absurd decSNEq (ImplementationCtorN n) (WithN x n') = No absurd decSNEq (ImplementationCtorN n) (ImplementationN n' xs) = No absurd decSNEq (ImplementationCtorN n) (ParentN n' x) = No absurd decSNEq (ImplementationCtorN n) (MethodN n') = No absurd decSNEq (ImplementationCtorN n) (CaseN loc n') = No absurd decSNEq (ImplementationCtorN n) (ImplementationCtorN n') with (assert_total $ decTTNameEq n n') decSNEq (ImplementationCtorN n) (ImplementationCtorN n) | Yes Refl = Yes Refl decSNEq (ImplementationCtorN n) (ImplementationCtorN n') | No contra = No $ contra . implementationCtorNInj decSNEq (ImplementationCtorN n) (MetaN n' x) = No absurd decSNEq (MetaN n n') (WhereN x y z) = No absurd decSNEq (MetaN n n') (WithN x y) = No absurd decSNEq (MetaN n n') (ImplementationN x xs) = No absurd decSNEq (MetaN n n') (ParentN x y) = No absurd decSNEq (MetaN n n') (MethodN x) = No absurd decSNEq (MetaN n n') (CaseN loc x) = No absurd decSNEq (MetaN n n') (ImplementationCtorN x) = No absurd decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x) decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y) decSNEq (MetaN n n') (MetaN n n') | Yes Refl | Yes Refl = Yes Refl decSNEq (MetaN n n') (MetaN n y) | Yes Refl | No contra = No $ contra . snd . metaNInj decSNEq (MetaN n n') (MetaN x y) | No contra = No $ contra . fst . metaNInj -- (Temporarily?) Outside the mutual block, since otherwise we get the -- warning on the second pass! %deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead." implementation DecEq TTName where decEq = decTTNameEq implementation DecEq SpecialName where decEq = decSNEq data TTUExp = ||| Universe variable UVar String Int | ||| Explicit universe level UVal Int %name TTUExp uexp data NativeTy = IT8 | IT16 | IT32 | IT64 data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar data ArithTy = ATInt Language.Reflection.IntTy | ATDouble ||| Primitive constants data Const = I Int | BI Integer | Fl Double | Ch Char | Str String | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64 | AType ArithTy | StrType | VoidType | Forgot | WorldType | TheWorld %name Const c, c' export interface ReflConst (a : Type) where toConst : a -> Const implementation ReflConst Int where toConst x = I x implementation ReflConst Integer where toConst = BI implementation ReflConst Double where toConst = Fl implementation ReflConst Char where toConst = Ch implementation ReflConst String where toConst = Str implementation ReflConst Bits8 where toConst = B8 implementation ReflConst Bits16 where toConst = B16 implementation ReflConst Bits32 where toConst = B32 implementation ReflConst Bits64 where toConst = B64 implicit export reflectConstant: (ReflConst a) => a -> Const reflectConstant = toConst ||| Types of named references data NameType = ||| A reference which is just bound, e.g. by intro Bound | ||| A reference to a de Bruijn-indexed variable Ref | ||| Data constructor with tag and number DCon Int Int | ||| Type constructor with tag and number TCon Int Int %name NameType nt, nt' ||| Types annotations for bound variables in different ||| binding contexts ||| ||| @ tmTy the terms that can occur inside the binder, as type ||| annotations or bound values data Binder : (tmTy : Type) -> Type where ||| Lambdas ||| ||| @ ty the type of the argument Lam : (ty : a) -> Binder a ||| Function types. ||| ||| @ kind The kind of arrow. Only relevant when dealing with ||| uniqueness, so you can usually pretend that this ||| field doesn't exist. For ordinary functions, use the ||| type of types here. Pi : (ty, kind : a) -> Binder a ||| A let binder ||| ||| @ ty the type of the bound variable ||| @ val the bound value Let : (ty, val : a) -> Binder a ||| A hole that can occur during elaboration, and must be filled ||| ||| @ ty the type of the value that will eventually be put into the hole Hole : (ty : a) -> Binder a ||| A hole that will later become a top-level metavariable GHole : (ty : a) -> Binder a ||| A hole with a solution in it. Computationally inert. ||| ||| @ ty the type of the value in the hole ||| @ val the value in the hole Guess : (ty, val : a) -> Binder a ||| A pattern variable. These bindings surround the terms that make ||| up the left and right sides of pattern-matching definition ||| clauses. ||| ||| @ ty the type of the pattern variable PVar : (ty : a) -> Binder a ||| The type of a pattern binding. This is to `PVar` as `Pi` is to ||| `Lam`. ||| ||| @ ty the type of the pattern variable PVTy : (ty : a) -> Binder a %name Binder b, b' implementation Functor Binder where map f (Lam x) = Lam (f x) map f (Pi x k) = Pi (f x) (f k) map f (Let x y) = Let (f x) (f y) map f (Hole x) = Hole (f x) map f (GHole x) = GHole (f x) map f (Guess x y) = Guess (f x) (f y) map f (PVar x) = PVar (f x) map f (PVTy x) = PVTy (f x) implementation Foldable Binder where foldr f z (Lam x) = f x z foldr f z (Pi x k) = f x (f k z) foldr f z (Let x y) = f x (f y z) foldr f z (Hole x) = f x z foldr f z (GHole x) = f x z foldr f z (Guess x y) = f x (f y z) foldr f z (PVar x) = f x z foldr f z (PVTy x) = f x z implementation Traversable Binder where traverse f (Lam x) = [| Lam (f x) |] traverse f (Pi x k) = [| Pi (f x) (f k) |] traverse f (Let x y) = [| Let (f x) (f y) |] traverse f (Hole x) = [| Hole (f x) |] traverse f (GHole x) = [| GHole (f x) |] traverse f (Guess x y) = [| Guess (f x) (f y) |] traverse f (PVar x) = [| PVar (f x) |] traverse f (PVTy x) = [| PVTy (f x) |] ||| The various universes involved in the uniqueness mechanism data Universe = NullType | UniqueType | AllTypes ||| Reflection of the well typed core language data TT = ||| A reference to some name (P for Parameter) P NameType TTName TT | ||| de Bruijn variables V Int | ||| Bind a variable Bind TTName (Binder TT) TT | ||| Apply one term to another App TT TT | ||| Embed a constant TConst Const | ||| Erased terms Erased | ||| The type of types along (with universe constraints) TType TTUExp | ||| Alternative universes for dealing with uniqueness UType Universe %name TT tm, tm' ||| Raw terms without types data Raw = ||| Variables, global or local Var TTName | ||| Bind a variable RBind TTName (Binder Raw) Raw | ||| Application RApp Raw Raw | ||| The type of types RType | ||| Alternative universes for dealing with uniqueness RUType Universe | ||| Embed a constant RConstant Const %name Raw tm, tm' ||| Error reports are a list of report parts data ErrorReportPart = ||| A human-readable string TextPart String | ||| An Idris name (to be semantically coloured) NamePart TTName | ||| An Idris term, to be pretty printed TermPart TT | ||| A Raw term to be displayed by the compiler RawPart Raw | ||| An indented sub-report, to provide more details SubReport (List ErrorReportPart) %name ErrorReportPart part, p ||| A representation of Idris's old tactics that can be returned from custom ||| tactic implementations. Generate these using `applyTactic`. data Tactic = ||| Try the first tactic and resort to the second one on failure Try Tactic Tactic | ||| Only run if the goal has the right type GoalType String Tactic | ||| Resolve function name, find matching arguments in the ||| context and compute the proof target Refine TTName | ||| Apply both tactics in sequence Seq Tactic Tactic | ||| Introduce a new hole with a particular type Claim TTName TT | ||| Move the current hole to the end Unfocus | ||| Intelligently construct the proof target from the context Trivial | ||| Build a proof by applying contructors up to a maximum depth Search Int | ||| Resolve an interface Implementation | ||| Infer the proof target from the context Solve | ||| introduce all variables into the context Intros | ||| Introduce a named variable into the context, use the ||| first one if the given name is not found Intro TTName | ||| Invoke the reflected rep. of another tactic ApplyTactic TT | ||| Turn a value into its reflected representation Reflect TT | ||| Use a `%reflection` function ByReflection TT | ||| Turn a raw value back into a term Fill Raw | ||| Use the given value to conclude the proof Exact TT | ||| Focus on a particular hole Focus TTName | ||| Rewrite with an equality Rewrite TT | ||| Perform induction on a particular expression Induction TT | ||| Perform case analysis on a particular expression Case TT | ||| Name a reflected term LetTac TTName TT | ||| Name a reflected term and type it LetTacTy TTName TT TT | ||| Normalise the goal Compute | ||| Do nothing Skip | ||| Fail with an error message Fail (List ErrorReportPart) | ||| Attempt to fill the hole with source code information SourceFC %name Tactic tac, tac' ||| Things with a canonical representation as a reflected term. ||| ||| This interface is intended to be used during proof automation and the ||| construction of custom tactics. ||| ||| @ a the type to be quoted ||| @ t the type to quote it to (typically `TT` or `Raw`) interface Quotable a t where ||| A representation of the type `a`. ||| ||| This is to enable quoting polymorphic datatypes quotedTy : t ||| Quote a particular element of `a`. ||| ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))``` quote : a -> t implementation Quotable Nat TT where quotedTy = `(Nat) quote Z = `(Z) quote (S k) = `(S ~(quote k)) implementation Quotable Nat Raw where quotedTy = `(Nat) quote Z = `(Z) quote (S k) = `(S ~(quote k)) implementation Quotable Bool TT where quotedTy = `(Bool) quote True = `(True) quote False = `(False) implementation Quotable Bool Raw where quotedTy = `(Bool) quote True = `(True) quote False = `(False) implementation Quotable Int TT where quotedTy = `(Int) quote x = TConst (I x) implementation Quotable Int Raw where quotedTy = `(Int) quote x = RConstant (I x) implementation Quotable Double TT where quotedTy = `(Double) quote x = TConst (Fl x) implementation Quotable Double Raw where quotedTy = `(Double) quote x = RConstant (Fl x) implementation Quotable Char TT where quotedTy = `(Char) quote x = TConst (Ch x) implementation Quotable Char Raw where quotedTy = `(Char) quote x = RConstant (Ch x) implementation Quotable Bits8 TT where quotedTy = `(Bits8) quote x = TConst (B8 x) implementation Quotable Bits8 Raw where quotedTy = `(Bits8) quote x = RConstant (B8 x) implementation Quotable Bits16 TT where quotedTy = `(Bits16) quote x = TConst (B16 x) implementation Quotable Bits16 Raw where quotedTy = `(Bits16) quote x = RConstant (B16 x) implementation Quotable Bits32 TT where quotedTy = `(Bits32) quote x = TConst (B32 x) implementation Quotable Bits32 Raw where quotedTy = `(Bits32) quote x = RConstant (B32 x) implementation Quotable Bits64 TT where quotedTy = `(Bits64) quote x = TConst (B64 x) implementation Quotable Bits64 Raw where quotedTy = `(Bits64) quote x = RConstant (B64 x) implementation Quotable Integer TT where quotedTy = `(Integer) quote x = TConst (BI x) implementation Quotable Integer Raw where quotedTy = `(Integer) quote x = RConstant (BI x) implementation Quotable String TT where quotedTy = `(String) quote x = TConst (Str x) implementation Quotable String Raw where quotedTy = `(String) quote x = RConstant (Str x) implementation Quotable a TT => Quotable (List a) TT where quotedTy = `(List ~(quotedTy {a})) quote [] = `(List.Nil {elem=~(quotedTy {a})}) quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs)) implementation Quotable a Raw => Quotable (List a) Raw where quotedTy = `(List ~(quotedTy {a})) quote [] = `(List.Nil {elem=~(quotedTy {a})}) quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs)) implementation Quotable a TT => Quotable (Maybe a) TT where quotedTy = `(Maybe ~(quotedTy {a})) quote (Just x) = `(Just {a=~(quotedTy {a})} ~(quote x)) quote Nothing = `(Nothing {a=~(quotedTy {a})}) implementation Quotable a Raw => Quotable (Maybe a) Raw where quotedTy = `(Maybe ~(quotedTy {a})) quote (Just x) = `(Just {a=~(quotedTy {a})} ~(quote x)) quote Nothing = `(Nothing {a=~(quotedTy {a})}) implementation (Quotable a TT, Quotable b TT) => Quotable (Either a b) TT where quotedTy = `(Either ~(quotedTy {a}) ~(quotedTy {a=b})) quote (Left x) = `(Left {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x)) quote (Right x) = `(Right {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x)) implementation (Quotable a Raw, Quotable b Raw) => Quotable (Either a b) Raw where quotedTy = `(Either ~(quotedTy {a}) ~(quotedTy {a=b})) quote (Left x) = `(Left {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x)) quote (Right x) = `(Right {a=~(quotedTy {a})} {b=~(quotedTy {a=b})} ~(quote x)) implementation Quotable () TT where quotedTy = `(Unit) quote () = `(MkUnit) implementation Quotable () Raw where quotedTy = `(Unit) quote () = `(MkUnit) implementation (Quotable a TT, Quotable b TT) => Quotable (a, b) TT where quotedTy = `(Pair ~(quotedTy {a=a}) ~(quotedTy {a=b})) quote (x, y) = `(MkPair {A=~(quotedTy {a=a})} {B=~(quotedTy {a=b})} ~(quote x) ~(quote y)) implementation (Quotable a Raw, Quotable b Raw) => Quotable (a, b) Raw where quotedTy = `(Pair ~(quotedTy {a=a}) ~(quotedTy {a=b})) quote (x, y) = `(MkPair {A=~(quotedTy {a=a})} {B=~(quotedTy {a=b})} ~(quote x) ~(quote y)) implementation Quotable SourceLocation TT where quotedTy = `(SourceLocation) quote (FileLoc fn (sl, sc) (el, ec)) = `(FileLoc ~(quote fn) (~(quote sl), ~(quote sc)) (~(quote el), ~(quote ec))) implementation Quotable SourceLocation Raw where quotedTy = `(SourceLocation) quote (FileLoc fn (sl, sc) (el, ec)) = `(FileLoc ~(quote {t=Raw} fn) (~(quote {t=Raw} sl), ~(quote {t=Raw} sc)) (~(quote {t=Raw} el), ~(quote {t=Raw} ec))) mutual implementation Quotable TTName TT where quotedTy = `(TTName) quote (UN x) = `(UN ~(quote x)) quote (NS n xs) = `(NS ~(quote n) ~(quote xs)) quote (MN x y) = `(MN ~(quote x) ~(quote y)) quote (SN sn) = `(SN ~(assert_total $ quote sn)) implementation Quotable SpecialName TT where quotedTy = `(SpecialName) quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2)) quote (WithN i n) = `(WithN ~(quote i) ~(quote n)) quote (ImplementationN i ss) = `(ImplementationN ~(quote i) ~(quote ss)) quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s)) quote (MethodN n) = `(MethodN ~(quote n)) quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n)) quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n)) quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta)) mutual implementation Quotable TTName Raw where quotedTy = `(TTName) quote (UN x) = `(UN ~(quote {t=Raw} x)) quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs)) quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y)) quote (SN sn) = `(SN ~(assert_total $ quote sn)) implementation Quotable SpecialName Raw where quotedTy = `(SpecialName) quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2)) quote (WithN i n) = `(WithN ~(quote i) ~(quote n)) quote (ImplementationN i ss) = `(ImplementationN ~(quote i) ~(quote ss)) quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s)) quote (MethodN n) = `(MethodN ~(quote n)) quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n)) quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n)) quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta)) implementation Quotable TTUExp TT where quotedTy = `(TTUExp) quote (UVar ns x) = `(UVar ~(quote ns) ~(quote x)) quote (UVal x) = `(UVal ~(quote x)) implementation Quotable TTUExp Raw where quotedTy = `(TTUExp) quote (UVar ns x) = `(UVar ~(quote ns) ~(quote {t=Raw} x)) quote (UVal x) = `(UVal ~(quote {t=Raw} x)) implementation Quotable NativeTy TT where quotedTy = `(NativeTy) quote IT8 = `(Reflection.IT8) quote IT16 = `(Reflection.IT16) quote IT32 = `(Reflection.IT32) quote IT64 = `(Reflection.IT64) implementation Quotable NativeTy Raw where quotedTy = `(NativeTy) quote IT8 = `(Reflection.IT8) quote IT16 = `(Reflection.IT16) quote IT32 = `(Reflection.IT32) quote IT64 = `(Reflection.IT64) implementation Quotable Reflection.IntTy TT where quotedTy = `(Reflection.IntTy) quote (ITFixed x) = `(ITFixed ~(quote x)) quote ITNative = `(Reflection.ITNative) quote ITBig = `(ITBig) quote ITChar = `(Reflection.ITChar) implementation Quotable Reflection.IntTy Raw where quotedTy = `(Reflection.IntTy) quote (ITFixed x) = `(ITFixed ~(quote {t=Raw} x)) quote ITNative = `(Reflection.ITNative) quote ITBig = `(ITBig) quote ITChar = `(Reflection.ITChar) implementation Quotable ArithTy TT where quotedTy = `(ArithTy) quote (ATInt x) = `(ATInt ~(quote x)) quote ATDouble = `(ATDouble) implementation Quotable ArithTy Raw where quotedTy = `(ArithTy) quote (ATInt x) = `(ATInt ~(quote {t=Raw} x)) quote ATDouble = `(ATDouble) implementation Quotable Const TT where quotedTy = `(Const) quote (I x) = `(I ~(quote x)) quote (BI x) = `(BI ~(quote x)) quote (Fl x) = `(Fl ~(quote x)) quote (Ch x) = `(Ch ~(quote x)) quote (Str x) = `(Str ~(quote x)) quote (B8 x) = `(B8 ~(quote x)) quote (B16 x) = `(B16 ~(quote x)) quote (B32 x) = `(B32 ~(quote x)) quote (B64 x) = `(B64 ~(quote x)) quote (AType x) = `(AType ~(quote x)) quote StrType = `(StrType) quote VoidType = `(VoidType) quote Forgot = `(Forgot) quote WorldType = `(WorldType) quote TheWorld = `(TheWorld) implementation Quotable Const Raw where quotedTy = `(Const) quote (I x) = `(I ~(quote {t=Raw} x)) quote (BI x) = `(BI ~(quote {t=Raw} x)) quote (Fl x) = `(Fl ~(quote {t=Raw} x)) quote (Ch x) = `(Ch ~(quote {t=Raw} x)) quote (Str x) = `(Str ~(quote {t=Raw} x)) quote (B8 x) = `(B8 ~(quote {t=Raw} x)) quote (B16 x) = `(B16 ~(quote {t=Raw} x)) quote (B32 x) = `(B32 ~(quote {t=Raw} x)) quote (B64 x) = `(B64 ~(quote {t=Raw} x)) quote (AType x) = `(AType ~(quote {t=Raw} x)) quote StrType = `(StrType) quote VoidType = `(VoidType) quote Forgot = `(Forgot) quote WorldType = `(WorldType) quote TheWorld = `(TheWorld) implementation Quotable NameType TT where quotedTy = `(NameType) quote Bound = `(Bound) quote Ref = `(Ref) quote (DCon x y) = `(DCon ~(quote x) ~(quote y)) quote (TCon x y) = `(TCon ~(quote x) ~(quote y)) implementation Quotable NameType Raw where quotedTy = `(NameType) quote Bound = `(Bound) quote Ref = `(Ref) quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y)) quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y)) implementation Quotable Universe TT where quotedTy = `(Universe) quote Reflection.NullType = `(NullType) quote Reflection.UniqueType = `(UniqueType) quote Reflection.AllTypes = `(AllTypes) implementation Quotable Universe Raw where quotedTy = `(Universe) quote Reflection.NullType = `(NullType) quote Reflection.UniqueType = `(UniqueType) quote Reflection.AllTypes = `(AllTypes) mutual implementation Quotable TT TT where quotedTy = `(TT) quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm)) quote (V x) = `(V ~(quote x)) quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm)) quote (App f x) = `(App ~(quote f) ~(quote x)) quote (TConst c) = `(TConst ~(quote c)) quote Erased = `(Erased) quote (TType uexp) = `(TType ~(quote uexp)) quote (UType u) = `(UType ~(quote u)) implementation Quotable (Binder TT) TT where quotedTy = `(Binder TT) quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x))) quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x)) ~(assert_total (quote k))) quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x)) ~(assert_total (quote y))) quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x))) quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x))) quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x)) ~(assert_total (quote y))) quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x))) quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x))) mutual quoteTTRaw : TT -> Raw quoteTTRaw (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quoteTTRaw tm)) quoteTTRaw (V x) = `(V ~(quote x)) quoteTTRaw (Bind n b tm) = `(Bind ~(quote n) ~(assert_total $ quoteTTBinderRaw b) ~(quoteTTRaw tm)) quoteTTRaw (App f x) = `(App ~(quoteTTRaw f) ~(quoteTTRaw x)) quoteTTRaw (TConst c) = `(TConst ~(quote c)) quoteTTRaw Erased = `(Erased) quoteTTRaw (TType uexp) = `(TType ~(quote uexp)) quoteTTRaw (UType u) = `(UType ~(quote u)) quoteTTBinderRaw : Binder TT -> Raw quoteTTBinderRaw (Lam x) = `(Lam {a=TT} ~(quoteTTRaw x)) quoteTTBinderRaw (Pi x k) = `(Pi {a=TT} ~(quoteTTRaw x) ~(quoteTTRaw k)) quoteTTBinderRaw (Let x y) = `(Let {a=TT} ~(quoteTTRaw x) ~(quoteTTRaw y)) quoteTTBinderRaw (Hole x) = `(Hole {a=TT} ~(quoteTTRaw x)) quoteTTBinderRaw (GHole x) = `(GHole {a=TT} ~(quoteTTRaw x)) quoteTTBinderRaw (Guess x y) = `(Guess {a=TT} ~(quoteTTRaw x) ~(quoteTTRaw y)) quoteTTBinderRaw (PVar x) = `(PVar {a=TT} ~(quoteTTRaw x)) quoteTTBinderRaw (PVTy x) = `(PVTy {a=TT} ~(quoteTTRaw x)) implementation Quotable TT Raw where quotedTy = `(TT) quote = quoteTTRaw implementation Quotable (Binder TT) Raw where quotedTy = `(Binder TT) quote = quoteTTBinderRaw mutual quoteRawTT : Raw -> TT quoteRawTT (Var n) = `(Var ~(quote n)) quoteRawTT (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderTT b) ~(quoteRawTT tm)) quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm')) quoteRawTT RType = `(RType) quoteRawTT (RUType u) = `(RUType ~(quote u)) quoteRawTT (RConstant c) = `(RConstant ~(quote c)) quoteRawBinderTT : Binder Raw -> TT quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x)) quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k)) quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y)) quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x)) quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x)) quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y)) quoteRawBinderTT (PVar x) = `(PVar {a=Raw} ~(quoteRawTT x)) quoteRawBinderTT (PVTy x) = `(PVTy {a=Raw} ~(quoteRawTT x)) implementation Quotable Raw TT where quotedTy = `(Raw) quote = quoteRawTT implementation Quotable (Binder Raw) TT where quotedTy = `(Binder Raw) quote = quoteRawBinderTT mutual quoteRawRaw : Raw -> Raw quoteRawRaw (Var n) = `(Var ~(quote n)) quoteRawRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderRaw b) ~(quoteRawRaw tm)) quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm')) quoteRawRaw RType = `(RType) quoteRawRaw (RUType u) = `(RUType ~(quote u)) quoteRawRaw (RConstant c) = `(RConstant ~(quote c)) quoteRawBinderRaw : Binder Raw -> Raw quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x)) quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k)) quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y)) quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x)) quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x)) quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y)) quoteRawBinderRaw (PVar x) = `(PVar {a=Raw} ~(quoteRawRaw x)) quoteRawBinderRaw (PVTy x) = `(PVTy {a=Raw} ~(quoteRawRaw x)) implementation Quotable Raw Raw where quotedTy = `(Raw) quote = quoteRawRaw implementation Quotable (Binder Raw) Raw where quotedTy = `(Binder Raw) quote = quoteRawBinderRaw implementation Quotable ErrorReportPart TT where quotedTy = `(ErrorReportPart) quote (TextPart x) = `(TextPart ~(quote x)) quote (NamePart n) = `(NamePart ~(quote n)) quote (TermPart tm) = `(TermPart ~(quote tm)) quote (RawPart tm) = `(RawPart ~(quote tm)) quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs)) implementation Quotable ErrorReportPart Raw where quotedTy = `(ErrorReportPart) quote (TextPart x) = `(TextPart ~(quote x)) quote (NamePart n) = `(NamePart ~(quote n)) quote (TermPart tm) = `(TermPart ~(quote tm)) quote (RawPart tm) = `(RawPart ~(quote tm)) quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs)) implementation Quotable Tactic TT where quotedTy = `(Tactic) quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac')) quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac)) quote (Refine n) = `(Refine ~(quote n)) quote (Claim n ty) = `(Claim ~(quote n) ~(quote ty)) quote Unfocus = `(Unfocus) quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac')) quote Trivial = `(Trivial) quote (Search x) = `(Search ~(quote x)) quote Implementation = `(Implementation) quote Solve = `(Solve) quote Intros = `(Intros) quote (Intro n) = `(Intro ~(quote n)) quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm)) quote (Reflect tm) = `(Reflect ~(quote tm)) quote (ByReflection tm) = `(ByReflection ~(quote tm)) quote (Fill tm) = `(Fill ~(quote tm)) quote (Exact tm) = `(Exact ~(quote tm)) quote (Focus n) = `(Focus ~(quote n)) quote (Rewrite tm) = `(Rewrite ~(quote tm)) quote (Induction tm) = `(Induction ~(quote tm)) quote (Case tm) = `(Case ~(quote tm)) quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm)) quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm')) quote Compute = `(Compute) quote Skip = `(Skip) quote (Fail xs) = `(Fail ~(quote xs)) quote SourceFC = `(SourceFC) implementation Quotable Tactic Raw where quotedTy = `(Tactic) quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac')) quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac)) quote (Refine n) = `(Refine ~(quote n)) quote (Claim n ty) = `(Claim ~(quote n) ~(quote ty)) quote Unfocus = `(Unfocus) quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac')) quote Trivial = `(Trivial) quote (Search x) = `(Search ~(quote x)) quote Implementation = `(Implementation) quote Solve = `(Solve) quote Intros = `(Intros) quote (Intro n) = `(Intro ~(quote n)) quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm)) quote (Reflect tm) = `(Reflect ~(quote tm)) quote (ByReflection tm) = `(ByReflection ~(quote tm)) quote (Fill tm) = `(Fill ~(quote tm)) quote (Exact tm) = `(Exact ~(quote tm)) quote (Focus n) = `(Focus ~(quote n)) quote (Rewrite tm) = `(Rewrite ~(quote tm)) quote (Induction tm) = `(Induction ~(quote tm)) quote (Case tm) = `(Case ~(quote tm)) quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm)) quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm')) quote Compute = `(Compute) quote Skip = `(Skip) quote (Fail xs) = `(Fail ~(quote xs)) quote SourceFC = `(SourceFC)