module Core.TTC import Core.CaseTreeimport Core.CompileExprimport Core.Contextimport Core.Coreimport Core.Envimport Core.FCimport Core.Nameimport Core.Optionsimport Core.TT import Data.NameMapimport Data.Vect import Utils.Binary %default covering exportTTC FC where  toBuf b (MkFC file startPos endPos)      = do tag 0; toBuf b file; toBuf b startPos; toBuf b endPos  toBuf b EmptyFC = tag 1   fromBuf b      = case !getTag of             0 => do f <- fromBuf b;                     s <- fromBuf b; e <- fromBuf b                     pure (MkFC f s e)             1 => pure EmptyFC             _ => corrupt "FC" exportTTC Name where  toBuf b (NS xs x) = do tag 0; toBuf b xs; toBuf b x  toBuf b (UN x) = do tag 1; toBuf b x  toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y  toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y  toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y  toBuf b (Nested x y) = do tag 5; toBuf b x; toBuf b y  toBuf b (CaseBlock x y) = do tag 6; toBuf b x; toBuf b y  toBuf b (WithBlock x y) = do tag 7; toBuf b x; toBuf b y  toBuf b (Resolved x)      = throw (InternalError ("Can't write resolved name " ++ show x))   fromBuf b      = case !getTag of             0 => do xs <- fromBuf b                     x <- fromBuf b                     pure (NS xs x)             1 => do x <- fromBuf b                     pure (UN x)             2 => do x <- fromBuf b                     y <- fromBuf b                     pure (MN x y)             3 => do x <- fromBuf b                     y <- fromBuf b                     pure (PV x y)             4 => do x <- fromBuf b                     y <- fromBuf b                     pure (DN x y)             5 => do x <- fromBuf b                     y <- fromBuf b                     pure (Nested x y)             6 => do x <- fromBuf b                     y <- fromBuf b                     pure (CaseBlock x y)             7 => do x <- fromBuf b                     y <- fromBuf b                     pure (WithBlock x y)             _ => corrupt "Name" exportTTC RigCount where  toBuf b Rig0 = tag 0  toBuf b Rig1 = tag 1  toBuf b RigW = tag 2   fromBuf b      = case !getTag of             0 => pure Rig0             1 => pure Rig1             2 => pure RigW             _ => corrupt "RigCount" exportTTC t => TTC (PiInfo t) where  toBuf b Implicit = tag 0  toBuf b Explicit = tag 1  toBuf b AutoImplicit = tag 2  toBuf b (DefImplicit r) = do tag 3; toBuf b r   fromBuf b      = case !getTag of             0 => pure Implicit             1 => pure Explicit             2 => pure AutoImplicit             3 => do t <- fromBuf b; pure (DefImplicit t)             _ => corrupt "PiInfo" exportTTC Constant where  toBuf b (I x) = do tag 0; toBuf b x  toBuf b (BI x) = do tag 1; toBuf b x  toBuf b (Str x) = do tag 2; toBuf b x  toBuf b (Ch x) = do tag 3; toBuf b x  toBuf b (Db x) = do tag 4; toBuf b x   toBuf b WorldVal = tag 5  toBuf b IntType = tag 6  toBuf b IntegerType = tag 7  toBuf b StringType = tag 8  toBuf b CharType = tag 9  toBuf b DoubleType = tag 10  toBuf b WorldType = tag 11   fromBuf b      = case !getTag of             0 => do x <- fromBuf b; pure (I x)             1 => do x <- fromBuf b; pure (BI x)             2 => do x <- fromBuf b; pure (Str x)             3 => do x <- fromBuf b; pure (Ch x)             4 => do x <- fromBuf b; pure (Db x)             5 => pure WorldVal             6 => pure IntType             7 => pure IntegerType             8 => pure StringType             9 => pure CharType             10 => pure DoubleType             11 => pure WorldType             _ => corrupt "Constant" exportTTC LazyReason where  toBuf b LInf = tag 0  toBuf b LLazy = tag 1  toBuf b LUnknown = tag 2   fromBuf b      = case !getTag of             0 => pure LInf             1 => pure LLazy             2 => pure LUnknown             _ => corrupt "LazyReason" exportTTC NameType where  toBuf b Bound = tag 0  toBuf b Func = tag 1  toBuf b (DataCon t arity) = do tag 2; toBuf b t; toBuf b arity  toBuf b (TyCon t arity) = do tag 3; toBuf b t; toBuf b arity   fromBuf b      = case !getTag of             0 => pure Bound             1 => pure Func             2 => do x <- fromBuf b; y <- fromBuf b; pure (DataCon x y)             3 => do x <- fromBuf b; y <- fromBuf b; pure (TyCon x y)             _ => corrupt "NameType" -- Assumption is that it was type safe when we wrote it out, so believe_me-- to rebuild proofs is fine.-- We're just making up the implicit arguments - this is only fine at run-- time because those arguments get erased!-- (Indeed, we're expecting the whole IsVar proof to be erased because-- we have the idx...)mkPrf : (idx : Nat) -> IsVar n idx nsmkPrf {n} {ns} Z = believe_me (First {n} {ns = n :: ns})mkPrf {n} {ns} (S k) = believe_me (Later {m=n} (mkPrf {n} {ns} k)) getName : (idx : Nat) -> List Name -> Maybe NamegetName Z (x :: xs) = Just xgetName (S k) (x :: xs) = getName k xsgetName _ [] = Nothing exportTTC (Var vars) where  toBuf b (MkVar {i} {n} v) = do toBuf b n; toBuf b i  fromBuf b      = do n <- fromBuf b           i <- fromBuf b           pure (MkVar {n} (mkPrf i)) mutual  export  TTC (Binder (Term vars)) where    toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty    toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val -- ; toBuf b ty    toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty    toBuf b (PVar c p ty) = do tag 3; toBuf b c; toBuf b p; toBuf b ty    toBuf b (PLet c val ty) = do tag 4; toBuf b c; toBuf b val -- ; toBuf b ty    toBuf b (PVTy c ty) = do tag 5; toBuf b c -- ; toBuf b ty     fromBuf b        = case !getTag of               0 => do c <- fromBuf b; x <- fromBuf b; ty <- fromBuf b; pure (Lam c x ty)               1 => do c <- fromBuf b; x <- fromBuf b; pure (Let c x (Erased emptyFC False))               2 => do c <- fromBuf b; x <- fromBuf b; y <- fromBuf b; pure (Pi c x y)               3 => do c <- fromBuf b; p <- fromBuf b; ty <- fromBuf b; pure (PVar c p ty)               4 => do c <- fromBuf b; x <- fromBuf b; pure (PLet c x (Erased emptyFC False))               5 => do c <- fromBuf b; pure (PVTy c (Erased emptyFC False))               _ => corrupt "Binder"   export  TTC UseSide where    toBuf b UseLeft = tag 0    toBuf b UseRight = tag 1     fromBuf b        = case !getTag of               0 => pure UseLeft               1 => pure UseRight               _ => corrupt "UseSide"    export  TTC (Term vars) where    toBuf b (Local {name} fc c idx y)        = if idx < 244             then do toBuf b (prim__truncBigInt_B8 (12 + cast idx))                     toBuf b c             else do tag 0                     toBuf b c                     toBuf b idx    toBuf b (Ref fc nt name)        = do tag 1;             toBuf b nt; toBuf b name    toBuf b (Meta fc n i xs)        = do tag 2;             toBuf b n; toBuf b xs    toBuf b (Bind fc x bnd scope)        = do tag 3;             toBuf b x;             toBuf b bnd; toBuf b scope    toBuf b (App fc fn arg)        = do tag 4;             toBuf b fn; toBuf b arg--              let (fn, args) = getFnArgs (App fc fn arg)--              toBuf b fn; -- toBuf b p;--              toBuf b args    toBuf b (As fc s as tm)        = do tag 5;             toBuf b as; toBuf b s; toBuf b tm    toBuf b (TDelayed fc r tm)        = do tag 6;             toBuf b r; toBuf b tm    toBuf b (TDelay fc r ty tm)        = do tag 7;             toBuf b r; toBuf b ty; toBuf b tm    toBuf b (TForce fc r tm)        = do tag 8;             toBuf b r; toBuf b tm    toBuf b (PrimVal fc c)        = do tag 9;             toBuf b c    toBuf b (Erased fc _)        = tag 10    toBuf b (TType fc)        = tag 11     fromBuf {vars} b        = case !getTag of               0 => do c <- fromBuf b                       idx <- fromBuf b                       name <- maybe (corrupt "Term") pure                                     (getName idx vars)                       pure (Local {name} emptyFC c idx (mkPrf idx))               1 => do nt <- fromBuf b; name <- fromBuf b                       pure (Ref emptyFC nt name)               2 => do n <- fromBuf b                       xs <- fromBuf b                       pure (Meta emptyFC n 0 xs) -- needs resolving               3 => do x <- fromBuf b                       bnd <- fromBuf b; scope <- fromBuf b                       pure (Bind emptyFC x bnd scope)               4 => do fn <- fromBuf b                       arg <- fromBuf b                       pure (App emptyFC fn arg)               5 => do as <- fromBuf b; s <- fromBuf b; tm <- fromBuf b                       pure (As emptyFC s as tm)               6 => do lr <- fromBuf b; tm <- fromBuf b                       pure (TDelayed emptyFC lr tm)               7 => do lr <- fromBuf b;                       ty <- fromBuf b; tm <- fromBuf b                       pure (TDelay emptyFC lr ty tm)               8 => do lr <- fromBuf b; tm <- fromBuf b                       pure (TForce emptyFC lr tm)               9 => do c <- fromBuf b                       pure (PrimVal emptyFC c)               10 => pure (Erased emptyFC False)               11 => pure (TType emptyFC)               idxp => do c <- fromBuf b                          let idx : Nat = fromInteger (prim__sextB8_BigInt idxp - 12)                          name <- maybe (corrupt "Term") pure                                        (getName idx vars)                          pure (Local {name} emptyFC c idx (mkPrf idx)) exportTTC Pat where  toBuf b (PAs fc x y)      = do tag 0; toBuf b fc; toBuf b x; toBuf b y  toBuf b (PCon fc x t arity xs)      = do tag 1; toBuf b fc; toBuf b x; toBuf b t; toBuf b arity; toBuf b xs  toBuf b (PTyCon fc x arity xs)      = do tag 2; toBuf b fc; toBuf b x; toBuf b arity; toBuf b xs  toBuf b (PConst fc c)      = do tag 3; toBuf b fc; toBuf b c  toBuf b (PArrow fc x s t)      = do tag 4; toBuf b fc; toBuf b x; toBuf b s; toBuf b t  toBuf b (PDelay fc x t y)      = do tag 5; toBuf b fc; toBuf b x; toBuf b t; toBuf b y  toBuf b (PLoc fc x)      = do tag 6; toBuf b fc; toBuf b x  toBuf b (PUnmatchable fc x)      = do tag 7; toBuf b fc; toBuf b x   fromBuf b      = case !getTag of             0 => do fc <- fromBuf b; x <- fromBuf b;                     y <- fromBuf b                     pure (PAs fc x y)             1 => do fc <- fromBuf b; x <- fromBuf b                     t <- fromBuf b; arity <- fromBuf b                     xs <- fromBuf b                     pure (PCon fc x t arity xs)             2 => do fc <- fromBuf b; x <- fromBuf b                     arity <- fromBuf b                     xs <- fromBuf b                     pure (PTyCon fc x arity xs)             3 => do fc <- fromBuf b; c <- fromBuf b                     pure (PConst fc c)             4 => do fc <- fromBuf b; x <- fromBuf b                     s <- fromBuf b; t <- fromBuf b                     pure (PArrow fc x s t)             5 => do fc <- fromBuf b; x <- fromBuf b;                     t <- fromBuf b; y <- fromBuf b                     pure (PDelay fc x t y)             6 => do fc <- fromBuf b; x <- fromBuf b                     pure (PLoc fc x)             7 => do fc <- fromBuf b; x <- fromBuf b                     pure (PUnmatchable fc x)             _ => corrupt "Pat" mutual  export  TTC (CaseTree vars) where    toBuf b (Case {name} idx x scTy xs)        = do tag 0; toBuf b name; toBuf b idx; toBuf b xs    toBuf b (STerm x)        = do tag 1; toBuf b x    toBuf b (Unmatched msg)        = do tag 2; toBuf b msg    toBuf b Impossible = tag 3     fromBuf b        = case !getTag of               0 => do name <- fromBuf b; idx <- fromBuf b                       xs <- fromBuf b                       pure (Case {name} idx (mkPrf idx) (Erased emptyFC False) xs)               1 => do x <- fromBuf b                       pure (STerm x)               2 => do msg <- fromBuf b                       pure (Unmatched msg)               3 => pure Impossible               _ => corrupt "CaseTree"   export  TTC (CaseAlt vars) where    toBuf b (ConCase x t args y)        = do tag 0; toBuf b x; toBuf b t; toBuf b args; toBuf b y    toBuf b (DelayCase ty arg y)        = do tag 1; toBuf b ty; toBuf b arg; toBuf b y    toBuf b (ConstCase x y)        = do tag 2; toBuf b x; toBuf b y    toBuf b (DefaultCase x)        = do tag 3; toBuf b x     fromBuf b        = case !getTag of               0 => do x <- fromBuf b; t <- fromBuf b                       args <- fromBuf b; y <- fromBuf b                       pure (ConCase x t args y)               1 => do ty <- fromBuf b; arg <- fromBuf b; y <- fromBuf b                       pure (DelayCase ty arg y)               2 => do x <- fromBuf b; y <- fromBuf b                       pure (ConstCase x y)               3 => do x <- fromBuf b                       pure (DefaultCase x)               _ => corrupt "CaseAlt" exportTTC (Env Term vars) where  toBuf b [] = pure ()  toBuf b ((::) bnd env)      = do toBuf b bnd; toBuf b env   -- Length has to correspond to length of 'vars'  fromBuf {vars = []} b = pure Nil  fromBuf {vars = x :: xs} b      = do bnd <- fromBuf b           env <- fromBuf b           pure (bnd :: env) exportTTC Visibility where  toBuf b Private = tag 0  toBuf b Export = tag 1  toBuf b Public = tag 2   fromBuf b      = case !getTag of             0 => pure Private             1 => pure Export             2 => pure Public             _ => corrupt "Visibility" exportTTC PartialReason where  toBuf b NotStrictlyPositive = tag 0  toBuf b (BadCall xs) = do tag 1; toBuf b xs  toBuf b (RecPath xs) = do tag 2; toBuf b xs   fromBuf b      = case !getTag of             0 => pure NotStrictlyPositive             1 => do xs <- fromBuf b                     pure (BadCall xs)             2 => do xs <- fromBuf b                     pure (RecPath xs)             _ => corrupt "PartialReason" exportTTC Terminating where  toBuf b Unchecked = tag 0  toBuf b IsTerminating = tag 1  toBuf b (NotTerminating p) = do tag 2; toBuf b p   fromBuf b      = case !getTag of             0 => pure Unchecked             1 => pure IsTerminating             2 => do p <- fromBuf b                     pure (NotTerminating p)             _ => corrupt "Terminating" exportTTC Covering where  toBuf b IsCovering = tag 0  toBuf b (MissingCases ms)      = do tag 1           toBuf b ms  toBuf b (NonCoveringCall ns)      = do tag 2           toBuf b ns   fromBuf b      = case !getTag of             0 => pure IsCovering             1 => do ms <- fromBuf b                     pure (MissingCases ms)             2 => do ns <- fromBuf b                     pure (NonCoveringCall ns)             _ => corrupt "Covering" exportTTC Totality where  toBuf b (MkTotality term cov) = do toBuf b term; toBuf b cov   fromBuf b      = do term <- fromBuf b           cov <- fromBuf b           pure (MkTotality term cov) exportTTC (PrimFn n) where  toBuf b (Add ty) = do tag 0; toBuf b ty  toBuf b (Sub ty) = do tag 1; toBuf b ty  toBuf b (Mul ty) = do tag 2; toBuf b ty  toBuf b (Div ty) = do tag 3; toBuf b ty  toBuf b (Mod ty) = do tag 4; toBuf b ty  toBuf b (Neg ty) = do tag 5; toBuf b ty  toBuf b (ShiftL ty) = do tag 35; toBuf b ty  toBuf b (ShiftR ty) = do tag 36; toBuf b ty  toBuf b (BAnd ty) = do tag 37; toBuf b ty  toBuf b (BOr ty) = do tag 38; toBuf b ty  toBuf b (BXOr ty) = do tag 39; toBuf b ty  toBuf b (LT ty) = do tag 6; toBuf b ty  toBuf b (LTE ty) = do tag 7; toBuf b ty  toBuf b (EQ ty) = do tag 8; toBuf b ty  toBuf b (GTE ty) = do tag 9; toBuf b ty  toBuf b (GT ty) = do tag 10; toBuf b ty  toBuf b StrLength = tag 11  toBuf b StrHead = tag 12  toBuf b StrTail = tag 13  toBuf b StrIndex = tag 14  toBuf b StrCons = tag 15  toBuf b StrAppend = tag 16  toBuf b StrReverse = tag 17  toBuf b StrSubstr = tag 18

Lines 1–500 of 975. Load more