@@ -9,14 +9,19 @@ import Core.Elaborate
99import Core.Typecheck
1010
1111import System.Console.Haskeline
12+
1213import Control.Monad.State
14+
1315import Data.List
1416import Data.Char
1517import Data.Either
18+
1619import Debug.Trace
1720
1821import qualified Epic.Epic as E
1922
23+import Util.Pretty
24+
2025data IOption = IOption { opt_logLevel :: Int,
2126 opt_typecase :: Bool,
2227 opt_typeintype :: Bool,
@@ -846,6 +851,66 @@ showImp impl tm = se 10 tm where
846851 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
847852 | otherwise = str
848853
854+{-
855+ PQuote Raw
856+ | PRef FC Name
857+ | PLam Name PTerm PTerm
858+ | PPi Plicity Name PTerm PTerm
859+ | PLet Name PTerm PTerm PTerm
860+ | PTyped PTerm PTerm -- term with explicit type
861+ | PApp FC PTerm [PArg]
862+ | PCase FC PTerm [(PTerm, PTerm)]
863+ | PTrue FC
864+ | PFalse FC
865+ | PRefl FC
866+ | PResolveTC FC
867+ | PEq FC PTerm PTerm
868+ | PPair FC PTerm PTerm
869+ | PDPair FC PTerm PTerm PTerm
870+ | PAlternative [PTerm]
871+ | PHidden PTerm -- irrelevant or hidden pattern
872+ | PSet
873+ | PConstant Const
874+ | Placeholder
875+ | PDoBlock [PDo]
876+ | PIdiom FC PTerm
877+ | PReturn FC
878+ | PMetavar Name
879+ | PProof [PTactic]
880+ | PTactics [PTactic] -- as PProof, but no auto solving
881+ | PElabError Err -- error to report on elaboration
882+ | PImpossible -- special case for declaring when an LHS can't typecheck
883+-}
884+
885+instance Sized PTerm where
886+ size (PQuote rawTerm) = size rawTerm
887+ size (PRef fc name) = size name
888+ size (PLam name ty bdy) = 1 + size ty + size bdy
889+ size (PPi name ty bdy) = 1 + size ty + size bdy
890+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
891+ size (PTyped trm ty) = 1 + size trm + size ty
892+ size (PApp fc name args) = 1 + size args
893+ size (PCase fc trm bdy) = 1 + size trm + size bdy
894+ size (PTrue fc) = 1
895+ size (PFalse fc) = 1
896+ size (PRefl fc) = 1
897+ size (PResolveTC fc) = 1
898+ size (PEq fc left right) = 1 + size left + size right
899+ size (PPair fc left right) = 1 + size left + size right
900+ size (PDPair fs left right) = 1 + size left + size right
901+ size (PAlternative alts) = 1 + size alts
902+ size (PHidden hidden) = size hidden
903+ size PSet = 1
904+ size (PConstant const) = 1 + size const
905+ size Placeholder = 1
906+ size (PDoBlock dos) = 1 + size dos
907+ size (PIdiom fc term) = 1 + size term
908+ size (PReturn fc) = 1
909+ size (PMetavar name) = 1
910+ size (PProof tactics) = size tactics
911+ size (PElabError err) = size err
912+ size PImpossible = 1
913+
849914allNamesIn :: PTerm -> [Name]
850915allNamesIn tm = nub $ ni [] tm
851916 where