bd8ea0a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4081 from eraserhd/generic-ibc

bd8ea0aNiklas Larsson9 years ago

src/IRTS/Compiler.hs+1−1

compare with master

unifiedsplit

@@ -508,7 +508,7 @@ doForeign vs env (ret : fname : world : args)

508 return (l', r')

509 splitArg _ = ifail $ "Badly formed foreign function call: " ++

510 show (ret : fname : world : args)

511−

511+

512

513 toFDesc (Constant (Str str)) = FStr str

514 toFDesc tm

src/Idris/Core/Binary.hs+15−334

@@ -13,63 +13,14 @@ module Idris.Core.Binary where

13import Idris.Core.TT

15import Control.Applicative ((<$>), (<*>))

16−import Control.Monad (liftM2)

17import Data.Binary

16import Data.Binary

18import Data.Binary.Get

17import Data.Binary.Get

19import Data.Binary.Put

18import Data.Binary.Put

21−instance Binary ErrorReportPart where

20+instance Binary ErrorReportPart

22− put (TextPart msg) = do putWord8 0 ; put msg

23− put (NamePart n) = do putWord8 1 ; put n

24− put (TermPart t) = do putWord8 2 ; put t

25− put (SubReport ps) = do putWord8 3 ; put ps

26− put (RawPart r) = do putWord8 4 ; put r

27−

28− get = do i <- getWord8

29− case i of

30− 0 -> fmap TextPart get

31− 1 -> fmap NamePart get

32− 2 -> fmap TermPart get

33− 3 -> fmap SubReport get

34− 4 -> fmap RawPart get

35− _ -> error "Corrupted binary data for ErrorReportPart"

36−

37−instance Binary Provenance where

21+instance Binary Provenance

38− put ExpectedType = putWord8 0

39− put (SourceTerm t) = do putWord8 1

40− put t

41− put InferredVal = putWord8 2

42− put GivenVal = putWord8 3

43− put (TooManyArgs t) = do putWord8 4

44− put t

45−

46− get = do i <- getWord8

47− case i of

48− 0 -> return ExpectedType

49− 1 -> do x1 <- get

50− return (SourceTerm x1)

51− 2 -> return InferredVal

52− 3 -> return GivenVal

53− 4 -> do x1 <- get

54− return (TooManyArgs x1)

55− _ -> error "Corrupted binary data for Provenance"

56−

57−instance Binary UConstraint where

22+instance Binary UConstraint

58− put (ULT x1 x2) = putWord8 0 >> put x1 >> put x2

59− put (ULE x1 x2) = putWord8 1 >> put x1 >> put x2

60− get = do i <- getWord8

61− case i of

62− 0 -> ULT <$> get <*> get

63− 1 -> ULE <$> get <*> get

64− _ -> error "Corrupted binary data for UConstraint"

65−

66−instance Binary ConstraintFC where

23+instance Binary ConstraintFC

67− put (ConstraintFC x1 x2) = putWord8 0 >> put x1 >> put x2

68− get = do i <- getWord8

69− case i of

70− 0 -> liftM2 ConstraintFC get get

71− _ -> error "Corrupted binary data for ConstraintFC"

72−

73instance Binary a => Binary (Err' a) where

24instance Binary a => Binary (Err' a) where

74 put (Msg str) = do putWord8 0

25 put (Msg str) = do putWord8 0

75 put str

26 put str

@@ -277,119 +228,10 @@ instance Binary a => Binary (Err' a) where

277 _ -> error "Corrupted binary data for Err'"

228 _ -> error "Corrupted binary data for Err'"

278----- Generated by 'derive'

229----- Generated by 'derive'

279

230

280−instance Binary FC where

231+instance Binary FC

281− put x =

282− case x of

283− (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0

284− put x1

285− put (x2 * 65536 + x3)

286− put (x4 * 65536 + x5)

287− NoFC -> putWord8 1

288− FileFC x1 -> do putWord8 2

289− put x1

290− get

291− = do i <- getWord8

292− case i of

293− 0 -> do x1 <- get

294− x2x3 <- get

295− x4x5 <- get

296− return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

297− 1 -> return NoFC

298− 2 -> do x1 <- get

299− return (FileFC x1)

300− _ -> error "Corrupted binary data for FC"

301−

302−instance Binary FC' where

232+instance Binary FC'

303− put (FC' fc) = put fc

304− get = fmap FC' get

305−

306−instance Binary Name where

233+instance Binary Name

307− put x

308− = case x of

309− UN x1 -> do putWord8 0

310− put x1

311− NS x1 x2 -> do putWord8 1

312− put x1

313− put x2

314− MN x1 x2 -> do putWord8 2

315− put x1

316− put x2

317− SN x1 -> do putWord8 3

318− put x1

319− SymRef x1 -> do putWord8 4

320− put x1

321− get

322− = do i <- getWord8

323− case i of

324− 0 -> do x1 <- get

325− return (UN x1)

326− 1 -> do x1 <- get

327− x2 <- get

328− return (NS x1 x2)

329− 2 -> do x1 <- get

330− x2 <- get

331− return (MN x1 x2)

332− 3 -> do x1 <- get

333− return (SN x1)

334− 4 -> do x1 <- get

335− return (SymRef x1)

336− _ -> error "Corrupted binary data for Name"

337−

338−instance Binary SpecialName where

234+instance Binary SpecialName

339− put x

340− = case x of

341− WhereN x1 x2 x3 -> do putWord8 0

342− put x1

343− put x2

344− put x3

345− ImplementationN x1 x2 -> do putWord8 1

346− put x1

347− put x2

348− ParentN x1 x2 -> do putWord8 2

349− put x1

350− put x2

351− MethodN x1 -> do putWord8 3

352− put x1

353− CaseN x1 x2 -> do putWord8 4; put x1; put x2

354− ElimN x1 -> do putWord8 5; put x1

355− ImplementationCtorN x1 -> do putWord8 6; put x1

356− WithN x1 x2 -> do putWord8 7

357− put x1

358− put x2

359− MetaN x1 x2 -> do putWord8 8

360− put x1

361− put x2

362− get

363− = do i <- getWord8

364− case i of

365− 0 -> do x1 <- get

366− x2 <- get

367− x3 <- get

368− return (WhereN x1 x2 x3)

369− 1 -> do x1 <- get

370− x2 <- get

371− return (ImplementationN x1 x2)

372− 2 -> do x1 <- get

373− x2 <- get

374− return (ParentN x1 x2)

375− 3 -> do x1 <- get

376− return (MethodN x1)

377− 4 -> do x1 <- get

378− x2 <- get

379− return (CaseN x1 x2)

380− 5 -> do x1 <- get

381− return (ElimN x1)

382− 6 -> do x1 <- get

383− return (ImplementationCtorN x1)

384− 7 -> do x1 <- get

385− x2 <- get

386− return (WithN x1 x2)

387− 8 -> do x1 <- get

388− x2 <- get

389− return (MetaN x1 x2)

390− _ -> error "Corrupted binary data for SpecialName"

391−

392−

393instance Binary Const where

235instance Binary Const where

394 put x

236 put x

395 = case x of

237 = case x of

@@ -453,56 +295,8 @@ instance Binary Const where

453 29 -> return TheWorld

295 29 -> return TheWorld

454 _ -> error "Corrupted binary data for Const"

296 _ -> error "Corrupted binary data for Const"

455

297

456−

457−instance Binary Raw where

298+instance Binary Raw

458− put x

459− = case x of

460− Var x1 -> do putWord8 0

461− put x1

462− RBind x1 x2 x3 -> do putWord8 1

463− put x1

464− put x2

465− put x3

466− RApp x1 x2 -> do putWord8 2

467− put x1

468− put x2

469− RType -> putWord8 3

470− RConstant x1 -> do putWord8 4

471− put x1

472− RUType x1 -> do putWord8 5

473− put x1

474− get

475− = do i <- getWord8

476− case i of

477− 0 -> do x1 <- get

478− return (Var x1)

479− 1 -> do x1 <- get

480− x2 <- get

481− x3 <- get

482− return (RBind x1 x2 x3)

483− 2 -> do x1 <- get

484− x2 <- get

485− return (RApp x1 x2)

486− 3 -> return RType

487− 4 -> do x1 <- get

488− return (RConstant x1)

489− 5 -> do x1 <- get

490− return (RUType x1)

491− _ -> error "Corrupted binary data for Raw"

492−

493−instance Binary RigCount where

299+instance Binary RigCount

494− put x = case x of

495− Rig0 -> putWord8 0

496− Rig1 -> putWord8 1

497− RigW -> putWord8 2

498− get = do i <- getWord8

499− case i of

500− 0 -> return Rig0

501− 1 -> return Rig1

502− 2 -> return RigW

503− _ -> error "Corrupted binary data for RigCount"

504−

505−

506instance Binary ImplicitInfo where

300instance Binary ImplicitInfo where

507 put x

301 put x

508 = case x of

302 = case x of

@@ -512,124 +306,11 @@ instance Binary ImplicitInfo where

512 x2 <- get

306 x2 <- get

513 return (Impl x1 x2 False)

307 return (Impl x1 x2 False)

514

308

515−instance (Binary b) => Binary (Binder b) where

309+instance (Binary b) => Binary (Binder b)

516− put x

517− = case x of

518− Lam x1 x2 -> do putWord8 0

519− put x1

520− put x2

521− Pi x1 x2 x3 x4 -> do putWord8 1

522− put x1

523− put x2

524− put x3

525− put x4

526− Let x1 x2 -> do putWord8 2

527− put x1

528− put x2

529− NLet x1 x2 -> do putWord8 3

530− put x1

531− put x2

532− Hole x1 -> do putWord8 4

533− put x1

534− GHole x1 x2 x3 -> do putWord8 5

535− put x1

536− put x2

537− put x3

538− Guess x1 x2 -> do putWord8 6

539− put x1

540− put x2

541− PVar x1 x2 -> do putWord8 7

542− put x1

543− put x2

544− PVTy x1 -> do putWord8 8

545− put x1

546− get

547− = do i <- getWord8

548− case i of

549− 0 -> do x1 <- get

550− x2 <- get

551− return (Lam x1 x2)

552− 1 -> do x1 <- get

553− x2 <- get

554− x3 <- get

555− x4 <- get

556− return (Pi x1 x2 x3 x4)

557− 2 -> do x1 <- get

558− x2 <- get

559− return (Let x1 x2)

560− 3 -> do x1 <- get

561− x2 <- get

562− return (NLet x1 x2)

563− 4 -> do x1 <- get

564− return (Hole x1)

565− 5 -> do x1 <- get

566− x2 <- get

567− x3 <- get

568− return (GHole x1 x2 x3)

569− 6 -> do x1 <- get

570− x2 <- get

571− return (Guess x1 x2)

572− 7 -> do x1 <- get

573− x2 <- get

574− return (PVar x1 x2)

575− 8 -> do x1 <- get

576− return (PVTy x1)

577− _ -> error "Corrupted binary data for Binder"

578−

579−

580−instance Binary Universe where

310+instance Binary Universe

581− put x = case x of

582− UniqueType -> putWord8 0

583− AllTypes -> putWord8 1

584− NullType -> putWord8 2

585− get = do i <- getWord8

586− case i of

587− 0 -> return UniqueType

588− 1 -> return AllTypes

589− 2 -> return NullType

590− _ -> error "Corrupted binary data for Universe"

591−

592−instance Binary NameType where

311+instance Binary NameType

593− put x

594− = case x of

595− Bound -> putWord8 0

596− Ref -> putWord8 1

597− DCon x1 x2 x3 -> do putWord8 2

598− put (x1 * 65536 + x2)

599− put x3

600− TCon x1 x2 -> do putWord8 3

601− put (x1 * 65536 + x2)

602− get

603− = do i <- getWord8

604− case i of

605− 0 -> return Bound

606− 1 -> return Ref

607− 2 -> do x1x2 <- get

608− x3 <- get

609− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)

610− 3 -> do x1x2 <- get

611− return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

612− _ -> error "Corrupted binary data for NameType"

613−

614−-- record concrete levels only, for now

615−instance Binary UExp where

312+instance Binary UExp

616− put x = case x of

617− UVar ns t -> do putWord8 0

618− put ns

619− put t

620− UVal t -> do putWord8 1

621− put t

622−

623− get = do i <- getWord8

624− case i of

625− 0 -> do x1 <- get

626− x2 <- get

627− return (UVar x1 x2)

628− 1 -> do x1 <- get

629− return (UVal x1)

630− _ -> error "Corrupted binary data for UExp"

631−

632−instance {- (Binary n) => -} Binary (TT Name) where

313+instance Binary (TT Name) where

633 put x

314 put x

634 = {-# SCC "putTT" #-}

315 = {-# SCC "putTT" #-}

635 case x of

316 case x of

src/Idris/IBC.hs+49−1571

@@ -40,7 +40,7 @@ import System.Directory

40import System.FilePath

42ibcVersion :: Word16

43−ibcVersion = 162

43+ibcVersion = 163

45-- | When IBC is being loaded - we'll load different things (and omit

46-- different structures/definitions) depending on which phase we're in.

@@ -220,9 +220,6 @@ writeIBC src f

220 logIBC 2 $ "Writing IBC for: " ++ show f

221 iReport 2 $ "Writing IBC for: " ++ show f

222 i <- getIState

223−-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

224−-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

225−-- [] -> return ()

226 resetNameIdx

223 resetNameIdx

227 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

224 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

228 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

225 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

@@ -838,120 +835,18 @@ processMetaVars ar = do

838

835

839----- For Cheapskate and docstrings

836----- For Cheapskate and docstrings

840

837

841−instance Binary a => Binary (D.Docstring a) where

838+instance Binary a => Binary (D.Docstring a)

842− put (D.DocString opts lines) = do put opts ; put lines

839+instance Binary CT.Options

843− get = do opts <- get

840+instance Binary D.DocTerm

844− lines <- get

841+instance Binary a => Binary (D.Block a)

845− return (D.DocString opts lines)

842+instance Binary a => Binary (D.Inline a)

846−

847−instance Binary CT.Options where

848− put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4

849− get = do x1 <- get

850− x2 <- get

851− x3 <- get

852− x4 <- get

853− return (CT.Options x1 x2 x3 x4)

854−

855−instance Binary D.DocTerm where

856− put D.Unchecked = putWord8 0

857− put (D.Checked t) = putWord8 1 >> put t

858− put (D.Example t) = putWord8 2 >> put t

859− put (D.Failing e) = putWord8 3 >> put e

860−

861− get = do i <- getWord8

862− case i of

863− 0 -> return D.Unchecked

864− 1 -> fmap D.Checked get

865− 2 -> fmap D.Example get

866− 3 -> fmap D.Failing get

867− _ -> error "Corrupted binary data for DocTerm"

868−

869−instance Binary a => Binary (D.Block a) where

870− put (D.Para lines) = do putWord8 0 ; put lines

871− put (D.Header i lines) = do putWord8 1 ; put i ; put lines

872− put (D.Blockquote bs) = do putWord8 2 ; put bs

873− put (D.List b t xs) = do putWord8 3 ; put b ; put t ; put xs

874− put (D.CodeBlock attr txt src) = do putWord8 4 ; put attr ; put txt ; put src

875− put (D.HtmlBlock txt) = do putWord8 5 ; put txt

876− put D.HRule = putWord8 6

877− get = do i <- getWord8

878− case i of

879− 0 -> fmap D.Para get

880− 1 -> liftM2 D.Header get get

881− 2 -> fmap D.Blockquote get

882− 3 -> liftM3 D.List get get get

883− 4 -> liftM3 D.CodeBlock get get get

884− 5 -> liftM D.HtmlBlock get

885− 6 -> return D.HRule

886− _ -> error "Corrupted binary data for Block"

887−

888−instance Binary a => Binary (D.Inline a) where

889− put (D.Str txt) = do putWord8 0 ; put txt

890− put D.Space = putWord8 1

891− put D.SoftBreak = putWord8 2

892− put D.LineBreak = putWord8 3

893− put (D.Emph xs) = putWord8 4 >> put xs

894− put (D.Strong xs) = putWord8 5 >> put xs

895− put (D.Code xs tm) = putWord8 6 >> put xs >> put tm

896− put (D.Link a b c) = putWord8 7 >> put a >> put b >> put c

897− put (D.Image a b c) = putWord8 8 >> put a >> put b >> put c

898− put (D.Entity a) = putWord8 9 >> put a

899− put (D.RawHtml x) = putWord8 10 >> put x

900− get = do i <- getWord8

901− case i of

902− 0 -> liftM D.Str get

903− 1 -> return D.Space

904− 2 -> return D.SoftBreak

905− 3 -> return D.LineBreak

906− 4 -> liftM D.Emph get

907− 5 -> liftM D.Strong get

908− 6 -> liftM2 D.Code get get

909− 7 -> liftM3 D.Link get get get

910− 8 -> liftM3 D.Image get get get

911− 9 -> liftM D.Entity get

912− 10 -> liftM D.RawHtml get

913− _ -> error "Corrupted binary data for Inline"

914−

915−instance Binary CT.ListType where

916− put (CT.Bullet c) = putWord8 0 >> put c

917− put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i

918− get = do i <- getWord8

919− case i of

920− 0 -> liftM CT.Bullet get

921− 1 -> liftM2 CT.Numbered get get

922− _ -> error "Corrupted binary data for ListType"

923−

924−instance Binary CT.CodeAttr where

925− put (CT.CodeAttr a b) = put a >> put b

926− get = liftM2 CT.CodeAttr get get

927−

928−instance Binary CT.NumWrapper where

843+instance Binary CT.ListType

929− put (CT.PeriodFollowing) = putWord8 0

844+instance Binary CT.CodeAttr

930− put (CT.ParenFollowing) = putWord8 1

845+instance Binary CT.NumWrapper

931− get = do i <- getWord8

932− case i of

933− 0 -> return CT.PeriodFollowing

934− 1 -> return CT.ParenFollowing

935− _ -> error "Corrupted binary data for NumWrapper"

936

846

937----- Generated by 'derive'

847----- Generated by 'derive'

938

848

939−instance Binary SizeChange where

849+instance Binary SizeChange

940− put x

941− = case x of

942− Smaller -> putWord8 0

943− Same -> putWord8 1

944− Bigger -> putWord8 2

945− Unknown -> putWord8 3

946− get

947− = do i <- getWord8

948− case i of

949− 0 -> return Smaller

950− 1 -> return Same

951− 2 -> return Bigger

952− 3 -> return Unknown

953− _ -> error "Corrupted binary data for SizeChange"

954−

955instance Binary CGInfo where

850instance Binary CGInfo where

956 put (CGInfo x1 x2 x3 x4)

851 put (CGInfo x1 x2 x3 x4)

957 = do put x1

852 = do put x1

@@ -964,110 +859,11 @@ instance Binary CGInfo where

964 x3 <- get

859 x3 <- get

965 return (CGInfo x1 x2 [] x3)

860 return (CGInfo x1 x2 [] x3)

966

861

967−instance Binary CaseType where

862+instance Binary CaseType

968− put x = case x of

969− Updatable -> putWord8 0

970− Shared -> putWord8 1

971− get = do i <- getWord8

972− case i of

973− 0 -> return Updatable

974− 1 -> return Shared

975− _ -> error "Corrupted binary data for CaseType"

976−

977−instance Binary SC where

863+instance Binary SC

978− put x

979− = case x of

980− Case x1 x2 x3 -> do putWord8 0

981− put x1

982− put x2

983− put x3

984− ProjCase x1 x2 -> do putWord8 1

985− put x1

986− put x2

987− STerm x1 -> do putWord8 2

988− put x1

989− UnmatchedCase x1 -> do putWord8 3

990− put x1

991− ImpossibleCase -> do putWord8 4

992− get

993− = do i <- getWord8

994− case i of

995− 0 -> do x1 <- get

996− x2 <- get

997− x3 <- get

998− return (Case x1 x2 x3)

999− 1 -> do x1 <- get

1000− x2 <- get

1001− return (ProjCase x1 x2)

1002− 2 -> do x1 <- get

1003− return (STerm x1)

1004− 3 -> do x1 <- get

1005− return (UnmatchedCase x1)

1006− 4 -> return ImpossibleCase

1007− _ -> error "Corrupted binary data for SC"

1008−

1009−

1010−instance Binary CaseAlt where

864+instance Binary CaseAlt

1011− put x

1012− = {-# SCC "putCaseAlt" #-}

1013− case x of

1014− ConCase x1 x2 x3 x4 -> do putWord8 0

1015− put x1

1016− put x2

1017− put x3

1018− put x4

1019− ConstCase x1 x2 -> do putWord8 1

1020− put x1

1021− put x2

1022− DefaultCase x1 -> do putWord8 2

1023− put x1

1024− FnCase x1 x2 x3 -> do putWord8 3

1025− put x1

1026− put x2

1027− put x3

1028− SucCase x1 x2 -> do putWord8 4

1029− put x1

1030− put x2

1031− get

1032− = do i <- getWord8

1033− case i of

1034− 0 -> do x1 <- get

1035− x2 <- get

1036− x3 <- get

1037− x4 <- get

1038− return (ConCase x1 x2 x3 x4)

1039− 1 -> do x1 <- get

1040− x2 <- get

1041− return (ConstCase x1 x2)

1042− 2 -> do x1 <- get

1043− return (DefaultCase x1)

1044− 3 -> do x1 <- get

1045− x2 <- get

1046− x3 <- get

1047− return (FnCase x1 x2 x3)

1048− 4 -> do x1 <- get

1049− x2 <- get

1050− return (SucCase x1 x2)

1051− _ -> error "Corrupted binary data for CaseAlt"

1052−

1053−instance Binary CaseDefs where

865+instance Binary CaseDefs

1054− put (CaseDefs x1 x2)

1055− = do put x1

1056− put x2

1057− get

1058− = do x1 <- get

1059− x2 <- get

1060− return (CaseDefs x1 x2)

1061−

1062−instance Binary CaseInfo where

866+instance Binary CaseInfo

1063− put x@(CaseInfo x1 x2 x3) = do put x1

1064− put x2

1065− put x3

1066− get = do x1 <- get

1067− x2 <- get

1068− x3 <- get

1069− return (CaseInfo x1 x2 x3)

1070−

1071instance Binary Def where

867instance Binary Def where

1072 put x

868 put x

1073 = {-# SCC "putDef" #-}

869 = {-# SCC "putDef" #-}

@@ -1106,219 +902,16 @@ instance Binary Def where

1106 return (CaseOp x1 x2 x3 [] [] x5)

902 return (CaseOp x1 x2 x3 [] [] x5)

1107 _ -> error "Corrupted binary data for Def"

903 _ -> error "Corrupted binary data for Def"

1108

904

1109−instance Binary Accessibility where

905+instance Binary Accessibility

1110− put x

1111− = case x of

1112− Public -> putWord8 0

1113− Frozen -> putWord8 1

1114− Private -> putWord8 2

1115− Hidden -> putWord8 3

1116− get

1117− = do i <- getWord8

1118− case i of

1119− 0 -> return Public

1120− 1 -> return Frozen

1121− 2 -> return Private

1122− 3 -> return Hidden

1123− _ -> error "Corrupted binary data for Accessibility"

1124−

1125−instance Binary PReason where

906+instance Binary PReason

1126− put x

1127− = case x of

1128− Other x1 -> do putWord8 0

1129− put x1

1130− Itself -> putWord8 1

1131− NotCovering -> putWord8 2

1132− NotPositive -> putWord8 3

1133− Mutual x1 -> do putWord8 4

1134− put x1

1135− NotProductive -> putWord8 5

1136− BelieveMe -> putWord8 6

1137− UseUndef x1 -> do putWord8 7

1138− put x1

1139− ExternalIO -> putWord8 8

1140− get

1141− = do i <- getWord8

1142− case i of

1143− 0 -> do x1 <- get

1144− return (Other x1)

1145− 1 -> return Itself

1146− 2 -> return NotCovering

1147− 3 -> return NotPositive

1148− 4 -> do x1 <- get

1149− return (Mutual x1)

1150− 5 -> return NotProductive

1151− 6 -> return BelieveMe

1152− 7 -> do x1 <- get

1153− return (UseUndef x1)

1154− 8 -> return ExternalIO

1155− _ -> error "Corrupted binary data for PReason"

1156−

1157−instance Binary Totality where

907+instance Binary Totality

1158− put x

1159− = case x of

1160− Total x1 -> do putWord8 0

1161− put x1

1162− Partial x1 -> do putWord8 1

1163− put x1

1164− Unchecked -> do putWord8 2

1165− Productive -> do putWord8 3

1166− Generated -> do putWord8 4

1167− get

1168− = do i <- getWord8

1169− case i of

1170− 0 -> do x1 <- get

1171− return (Total x1)

1172− 1 -> do x1 <- get

1173− return (Partial x1)

1174− 2 -> return Unchecked

1175− 3 -> return Productive

1176− 4 -> return Generated

1177− _ -> error "Corrupted binary data for Totality"

1178−

1179−instance Binary MetaInformation where

908+instance Binary MetaInformation

1180− put x

1181− = case x of

1182− EmptyMI -> do putWord8 0

1183− DataMI x1 -> do putWord8 1

1184− put x1

1185− get = do i <- getWord8

1186− case i of

1187− 0 -> return EmptyMI

1188− 1 -> do x1 <- get

1189− return (DataMI x1)

1190− _ -> error "Corrupted binary data for MetaInformation"

1191−

1192−instance Binary DataOpt where

909+instance Binary DataOpt

1193− put x = case x of

1194− Codata -> putWord8 0

1195− DefaultEliminator -> putWord8 1

1196− DataErrRev -> putWord8 2

1197− DefaultCaseFun -> putWord8 3

1198− get = do i <- getWord8

1199− case i of

1200− 0 -> return Codata

1201− 1 -> return DefaultEliminator

1202− 2 -> return DataErrRev

1203− 3 -> return DefaultCaseFun

1204− _ -> error "Corrupted binary data for DataOpt"

1205−

1206−instance Binary FnOpt where

910+instance Binary FnOpt

1207− put x

1208− = case x of

1209− Inlinable -> putWord8 0

1210− TotalFn -> putWord8 1

1211− Dictionary -> putWord8 2

1212− AssertTotal -> putWord8 3

1213− Specialise x -> do putWord8 4

1214− put x

1215− AllGuarded -> putWord8 5

1216− PartialFn -> putWord8 6

1217− Implicit -> putWord8 7

1218− Reflection -> putWord8 8

1219− ErrorHandler -> putWord8 9

1220− ErrorReverse -> putWord8 10

1221− CoveringFn -> putWord8 11

1222− NoImplicit -> putWord8 12

1223− Constructor -> putWord8 13

1224− CExport x1 -> do putWord8 14

1225− put x1

1226− AutoHint -> putWord8 15

1227− PEGenerated -> putWord8 16

1228− StaticFn -> putWord8 17

1229− OverlappingDictionary -> putWord8 18

1230− ErrorReduce -> putWord8 20

1231− get

1232− = do i <- getWord8

1233− case i of

1234− 0 -> return Inlinable

1235− 1 -> return TotalFn

1236− 2 -> return Dictionary

1237− 3 -> return AssertTotal

1238− 4 -> do x <- get

1239− return (Specialise x)

1240− 5 -> return AllGuarded

1241− 6 -> return PartialFn

1242− 7 -> return Implicit

1243− 8 -> return Reflection

1244− 9 -> return ErrorHandler

1245− 10 -> return ErrorReverse

1246− 11 -> return CoveringFn

1247− 12 -> return NoImplicit

1248− 13 -> return Constructor

1249− 14 -> do x1 <- get

1250− return $ CExport x1

1251− 15 -> return AutoHint

1252− 16 -> return PEGenerated

1253− 17 -> return StaticFn

1254− 18 -> return OverlappingDictionary

1255− 20 -> return ErrorReduce

1256− _ -> error "Corrupted binary data for FnOpt"

1257−

1258−instance Binary Fixity where

911+instance Binary Fixity

1259− put x

1260− = case x of

1261− Infixl x1 -> do putWord8 0

1262− put x1

1263− Infixr x1 -> do putWord8 1

1264− put x1

1265− InfixN x1 -> do putWord8 2

1266− put x1

1267− PrefixN x1 -> do putWord8 3

1268− put x1

1269− get

1270− = do i <- getWord8

1271− case i of

1272− 0 -> do x1 <- get

1273− return (Infixl x1)

1274− 1 -> do x1 <- get

1275− return (Infixr x1)

1276− 2 -> do x1 <- get

1277− return (InfixN x1)

1278− 3 -> do x1 <- get

1279− return (PrefixN x1)

1280− _ -> error "Corrupted binary data for Fixity"

1281−

1282−

1283−instance Binary FixDecl where

912+instance Binary FixDecl

1284− put (Fix x1 x2)

1285− = do put x1

1286− put x2

1287− get

1288− = do x1 <- get

1289− x2 <- get

1290− return (Fix x1 x2)

1291−

1292−

1293−instance Binary ArgOpt where

913+instance Binary ArgOpt

1294− put x

1295− = case x of

1296− HideDisplay -> putWord8 0

1297− InaccessibleArg -> putWord8 1

1298− AlwaysShow -> putWord8 2

1299− UnknownImp -> putWord8 3

1300− get

1301− = do i <- getWord8

1302− case i of

1303− 0 -> return HideDisplay

1304− 1 -> return InaccessibleArg

1305− 2 -> return AlwaysShow

1306− 3 -> return UnknownImp

1307− _ -> error "Corrupted binary data for Static"

1308−

1309−instance Binary Static where

914+instance Binary Static

1310− put x

1311− = case x of

1312− Static -> putWord8 0

1313− Dynamic -> putWord8 1

1314− get

1315− = do i <- getWord8

1316− case i of

1317− 0 -> return Static

1318− 1 -> return Dynamic

1319− _ -> error "Corrupted binary data for Static"

1320−

1321−

1322instance Binary Plicity where

915instance Binary Plicity where

1323 put x

916 put x

1324 = case x of

917 = case x of

@@ -1371,283 +964,12 @@ instance Binary Plicity where

1371 return (TacImp x1 x2 x3 x4)

964 return (TacImp x1 x2 x3 x4)

1372 _ -> error "Corrupted binary data for Plicity"

965 _ -> error "Corrupted binary data for Plicity"

1373

966

1374−

1375−instance (Binary t) => Binary (PDecl' t) where

967+instance Binary DefaultTotality

1376− put x

968+instance Binary LanguageExt

1377− = case x of

969+instance Binary Directive

1378− PFix x1 x2 x3 -> do putWord8 0

970+instance (Binary t) => Binary (PDecl' t)

1379− put x1

1380− put x2

1381− put x3

1382− PTy x1 x2 x3 x4 x5 x6 x7 x8

1383− -> do putWord8 1

1384− put x1

1385− put x2

1386− put x3

1387− put x4

1388− put x5

1389− put x6

1390− put x7

1391− put x8

1392− PClauses x1 x2 x3 x4 -> do putWord8 2

1393− put x1

1394− put x2

1395− put x3

1396− put x4

1397− PData x1 x2 x3 x4 x5 x6 ->

1398− do putWord8 3

1399− put x1

1400− put x2

1401− put x3

1402− put x4

1403− put x5

1404− put x6

1405− PParams x1 x2 x3 -> do putWord8 4

1406− put x1

1407− put x2

1408− put x3

1409− PNamespace x1 x2 x3 -> do putWord8 5

1410− put x1

1411− put x2

1412− put x3

1413− PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->

1414− do putWord8 6

1415− put x1

1416− put x2

1417− put x3

1418− put x4

1419− put x5

1420− put x6

1421− put x7

1422− put x8

1423− put x9

1424− put x10

1425− put x11

1426− put x12

1427− PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12

1428− -> do putWord8 7

1429− put x1

1430− put x2

1431− put x3

1432− put x4

1433− put x5

1434− put x6

1435− put x7

1436− put x8

1437− put x9

1438− put x10

1439− put x11

1440− put x12

1441− PImplementation x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ->

1442− do putWord8 8

1443− put x1

1444− put x2

1445− put x3

1446− put x4

1447− put x5

1448− put x6

1449− put x7

1450− put x8

1451− put x9

1452− put x10

1453− put x11

1454− put x12

1455− put x13

1456− put x14

1457− put x15

1458− PDSL x1 x2 -> do putWord8 9

1459− put x1

1460− put x2

1461− PCAF x1 x2 x3 -> do putWord8 10

1462− put x1

1463− put x2

1464− put x3

1465− PMutual x1 x2 -> do putWord8 11

1466− put x1

1467− put x2

1468− PPostulate x1 x2 x3 x4 x5 x6 x7 x8

1469− -> do putWord8 12

1470− put x1

1471− put x2

1472− put x3

1473− put x4

1474− put x5

1475− put x6

1476− put x7

1477− put x8

1478− PSyntax x1 x2 -> do putWord8 13

1479− put x1

1480− put x2

1481− PDirective x1 -> error "Cannot serialize PDirective"

1482− PProvider x1 x2 x3 x4 x5 x6 ->

1483− do putWord8 15

1484− put x1

1485− put x2

1486− put x3

1487− put x4

1488− put x5

1489− put x6

1490− PTransform x1 x2 x3 x4 -> do putWord8 16

1491− put x1

1492− put x2

1493− put x3

1494− put x4

1495− PRunElabDecl x1 x2 x3 -> do putWord8 17

1496− put x1

1497− put x2

1498− put x3

1499− POpenInterfaces x1 x2 x3 -> do putWord8 18

1500− put x1

1501− put x2

1502− put x3

1503− get

1504− = do i <- getWord8

1505− case i of

1506− 0 -> do x1 <- get

1507− x2 <- get

1508− x3 <- get

1509− return (PFix x1 x2 x3)

1510− 1 -> do x1 <- get

1511− x2 <- get

1512− x3 <- get

1513− x4 <- get

1514− x5 <- get

1515− x6 <- get

1516− x7 <- get

1517− x8 <- get

1518− return (PTy x1 x2 x3 x4 x5 x6 x7 x8)

1519− 2 -> do x1 <- get

1520− x2 <- get

1521− x3 <- get

1522− x4 <- get

1523− return (PClauses x1 x2 x3 x4)

1524− 3 -> do x1 <- get

1525− x2 <- get

1526− x3 <- get

1527− x4 <- get

1528− x5 <- get

1529− x6 <- get

1530− return (PData x1 x2 x3 x4 x5 x6)

1531− 4 -> do x1 <- get

1532− x2 <- get

1533− x3 <- get

1534− return (PParams x1 x2 x3)

1535− 5 -> do x1 <- get

1536− x2 <- get

1537− x3 <- get

1538− return (PNamespace x1 x2 x3)

1539− 6 -> do x1 <- get

1540− x2 <- get

1541− x3 <- get

1542− x4 <- get

1543− x5 <- get

1544− x6 <- get

1545− x7 <- get

1546− x8 <- get

1547− x9 <- get

1548− x10 <- get

1549− x11 <- get

1550− x12 <- get

1551− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

1552− 7 -> do x1 <- get

1553− x2 <- get

1554− x3 <- get

1555− x4 <- get

1556− x5 <- get

1557− x6 <- get

1558− x7 <- get

1559− x8 <- get

1560− x9 <- get

1561− x10 <- get

1562− x11 <- get

1563− x12 <- get

1564− return (PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

1565− 8 -> do x1 <- get

1566− x2 <- get

1567− x3 <- get

1568− x4 <- get

1569− x5 <- get

1570− x6 <- get

1571− x7 <- get

1572− x8 <- get

1573− x9 <- get

1574− x10 <- get

1575− x11 <- get

1576− x12 <- get

1577− x13 <- get

1578− x14 <- get

1579− x15 <- get

1580− return (PImplementation x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

1581− 9 -> do x1 <- get

1582− x2 <- get

1583− return (PDSL x1 x2)

1584− 10 -> do x1 <- get

1585− x2 <- get

1586− x3 <- get

1587− return (PCAF x1 x2 x3)

1588− 11 -> do x1 <- get

1589− x2 <- get

1590− return (PMutual x1 x2)

1591− 12 -> do x1 <- get

1592− x2 <- get

1593− x3 <- get

1594− x4 <- get

1595− x5 <- get

1596− x6 <- get

1597− x7 <- get

1598− x8 <- get

1599− return (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)

1600− 13 -> do x1 <- get

1601− x2 <- get

1602− return (PSyntax x1 x2)

1603− 14 -> do error "Cannot deserialize PDirective"

1604− 15 -> do x1 <- get

1605− x2 <- get

1606− x3 <- get

1607− x4 <- get

1608− x5 <- get

1609− x6 <- get

1610− return (PProvider x1 x2 x3 x4 x5 x6)

1611− 16 -> do x1 <- get

1612− x2 <- get

1613− x3 <- get

1614− x4 <- get

1615− return (PTransform x1 x2 x3 x4)

1616− 17 -> do x1 <- get

1617− x2 <- get

1618− x3 <- get

1619− return (PRunElabDecl x1 x2 x3)

1620− 18 -> do x1 <- get

1621− x2 <- get

1622− x3 <- get

1623− return (POpenInterfaces x1 x2 x3)

1624− _ -> error "Corrupted binary data for PDecl'"

1625−

1626−instance Binary t => Binary (ProvideWhat' t) where

971+instance Binary t => Binary (ProvideWhat' t)

1627− put (ProvTerm x1 x2) = do putWord8 0

1628− put x1

1629− put x2

1630− put (ProvPostulate x1) = do putWord8 1

1631− put x1

1632− get = do y <- getWord8

1633− case y of

1634− 0 -> do x1 <- get

1635− x2 <- get

1636− return (ProvTerm x1 x2)

1637− 1 -> do x1 <- get

1638− return (ProvPostulate x1)

1639− _ -> error "Corrupted binary data for ProvideWhat"

1640−

1641−instance Binary Using where

972+instance Binary Using

1642− put (UImplicit x1 x2) = do putWord8 0; put x1; put x2

1643− put (UConstraint x1 x2) = do putWord8 1; put x1; put x2

1644−

1645− get = do i <- getWord8

1646− case i of

1647− 0 -> do x1 <- get; x2 <- get; return (UImplicit x1 x2)

1648− 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1649− _ -> error "Corrupted binary data for Using"

1650−

1651instance Binary SyntaxInfo where

973instance Binary SyntaxInfo where

1652 put (Syn x1 x2 x3 x4 _ _ x5 x6 x7 _ _ x8 _ _ _)

974 put (Syn x1 x2 x3 x4 _ _ x5 x6 x7 _ _ x8 _ _ _)

1653 = do put x1

975 = do put x1

@@ -1669,711 +991,14 @@ instance Binary SyntaxInfo where

1669 x8 <- get

991 x8 <- get

1670 return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True True)

992 return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True True)

1671

993

1672−instance (Binary t) => Binary (PClause' t) where

994+instance (Binary t) => Binary (PClause' t)

1673− put x

995+instance (Binary t) => Binary (PData' t)

1674− = case x of

996+instance Binary PunInfo

1675− PClause x1 x2 x3 x4 x5 x6 -> do putWord8 0

997+instance Binary PTerm

1676− put x1

998+instance Binary PAltType

1677− put x2

999+instance (Binary t) => Binary (PTactic' t)

1678− put x3

1000+instance (Binary t) => Binary (PDo' t)

1679− put x4

1001+instance (Binary t) => Binary (PArg' t)

1680− put x5

1681− put x6

1682− PWith x1 x2 x3 x4 x5 x6 x7 -> do putWord8 1

1683− put x1

1684− put x2

1685− put x3

1686− put x4

1687− put x5

1688− put x6

1689− put x7

1690− PClauseR x1 x2 x3 x4 -> do putWord8 2

1691− put x1

1692− put x2

1693− put x3

1694− put x4

1695− PWithR x1 x2 x3 x4 x5 -> do putWord8 3

1696− put x1

1697− put x2

1698− put x3

1699− put x4

1700− put x5

1701− get

1702− = do i <- getWord8

1703− case i of

1704− 0 -> do x1 <- get

1705− x2 <- get

1706− x3 <- get

1707− x4 <- get

1708− x5 <- get

1709− x6 <- get

1710− return (PClause x1 x2 x3 x4 x5 x6)

1711− 1 -> do x1 <- get

1712− x2 <- get

1713− x3 <- get

1714− x4 <- get

1715− x5 <- get

1716− x6 <- get

1717− x7 <- get

1718− return (PWith x1 x2 x3 x4 x5 x6 x7)

1719− 2 -> do x1 <- get

1720− x2 <- get

1721− x3 <- get

1722− x4 <- get

1723− return (PClauseR x1 x2 x3 x4)

1724− 3 -> do x1 <- get

1725− x2 <- get

1726− x3 <- get

1727− x4 <- get

1728− x5 <- get

1729− return (PWithR x1 x2 x3 x4 x5)

1730− _ -> error "Corrupted binary data for PClause'"

1731−

1732−instance (Binary t) => Binary (PData' t) where

1733− put x

1734− = case x of

1735− PDatadecl x1 x2 x3 x4 -> do putWord8 0

1736− put x1

1737− put x2

1738− put x3

1739− put x4

1740− PLaterdecl x1 x2 x3 -> do putWord8 1

1741− put x1

1742− put x2

1743− put x3

1744− get

1745− = do i <- getWord8

1746− case i of

1747− 0 -> do x1 <- get

1748− x2 <- get

1749− x3 <- get

1750− x4 <- get

1751− return (PDatadecl x1 x2 x3 x4)

1752− 1 -> do x1 <- get

1753− x2 <- get

1754− x3 <- get

1755− return (PLaterdecl x1 x2 x3)

1756− _ -> error "Corrupted binary data for PData'"

1757−

1758−instance Binary PunInfo where

1759− put x

1760− = case x of

1761− TypeOrTerm -> putWord8 0

1762− IsType -> putWord8 1

1763− IsTerm -> putWord8 2

1764− get

1765− = do i <- getWord8

1766− case i of

1767− 0 -> return TypeOrTerm

1768− 1 -> return IsType

1769− 2 -> return IsTerm

1770− _ -> error "Corrupted binary data for PunInfo"

1771−

1772−instance Binary PTerm where

1773− put x

1774− = case x of

1775− PQuote x1 -> do putWord8 0

1776− put x1

1777− PRef x1 x2 x3 -> do putWord8 1

1778− put x1

1779− put x2

1780− put x3

1781− PInferRef x1 x2 x3 -> do putWord8 2

1782− put x1

1783− put x2

1784− put x3

1785− PPatvar x1 x2 -> do putWord8 3

1786− put x1

1787− put x2

1788− PLam x1 x2 x3 x4 x5 -> do putWord8 4

1789− put x1

1790− put x2

1791− put x3

1792− put x4

1793− put x5

1794− PPi x1 x2 x3 x4 x5 -> do putWord8 5

1795− put x1

1796− put x2

1797− put x3

1798− put x4

1799− put x5

1800− PLet x1 x2 x3 x4 x5 x6 -> do putWord8 6

1801− put x1

1802− put x2

1803− put x3

1804− put x4

1805− put x5

1806− put x6

1807− PTyped x1 x2 -> do putWord8 7

1808− put x1

1809− put x2

1810− PAppImpl x1 x2 -> error "PAppImpl in final term"

1811− PApp x1 x2 x3 -> do putWord8 8

1812− put x1

1813− put x2

1814− put x3

1815− PAppBind x1 x2 x3 -> do putWord8 9

1816− put x1

1817− put x2

1818− put x3

1819− PMatchApp x1 x2 -> do putWord8 10

1820− put x1

1821− put x2

1822− PCase x1 x2 x3 -> do putWord8 11

1823− put x1

1824− put x2

1825− put x3

1826− PTrue x1 x2 -> do putWord8 12

1827− put x1

1828− put x2

1829− PResolveTC x1 -> do putWord8 15

1830− put x1

1831− PRewrite x1 x2 x3 x4 x5 -> do putWord8 17

1832− put x1

1833− put x2

1834− put x3

1835− put x4

1836− put x5

1837− PPair x1 x2 x3 x4 x5 -> do putWord8 18

1838− put x1

1839− put x2

1840− put x3

1841− put x4

1842− put x5

1843− PDPair x1 x2 x3 x4 x5 x6 -> do putWord8 19

1844− put x1

1845− put x2

1846− put x3

1847− put x4

1848− put x5

1849− put x6

1850− PAlternative x1 x2 x3 -> do putWord8 20

1851− put x1

1852− put x2

1853− put x3

1854− PHidden x1 -> do putWord8 21

1855− put x1

1856− PType x1 -> do putWord8 22

1857− put x1

1858− PGoal x1 x2 x3 x4 -> do putWord8 23

1859− put x1

1860− put x2

1861− put x3

1862− put x4

1863− PConstant x1 x2 -> do putWord8 24

1864− put x1

1865− put x2

1866− Placeholder -> putWord8 25

1867− PDoBlock x1 -> do putWord8 26

1868− put x1

1869− PIdiom x1 x2 -> do putWord8 27

1870− put x1

1871− put x2

1872− PMetavar x1 x2 -> do putWord8 29

1873− put x1

1874− put x2

1875− PProof x1 -> do putWord8 30

1876− put x1

1877− PTactics x1 -> do putWord8 31

1878− put x1

1879− PImpossible -> putWord8 33

1880− PCoerced x1 -> do putWord8 34

1881− put x1

1882− PUnifyLog x1 -> do putWord8 35

1883− put x1

1884− PNoImplicits x1 -> do putWord8 36

1885− put x1

1886− PDisamb x1 x2 -> do putWord8 37

1887− put x1

1888− put x2

1889− PUniverse x1 x2 -> do putWord8 38

1890− put x1

1891− put x2

1892− PRunElab x1 x2 x3 -> do putWord8 39

1893− put x1

1894− put x2

1895− put x3

1896− PAs x1 x2 x3 -> do putWord8 40

1897− put x1

1898− put x2

1899− put x3

1900− PElabError x1 -> do putWord8 41

1901− put x1

1902− PQuasiquote x1 x2 -> do putWord8 42

1903− put x1

1904− put x2

1905− PUnquote x1 -> do putWord8 43

1906− put x1

1907− PQuoteName x1 x2 x3 -> do putWord8 44

1908− put x1

1909− put x2

1910− put x3

1911− PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1912− put x1

1913− put x2

1914− put x3

1915− put x4

1916− PConstSugar x1 x2 -> do putWord8 46

1917− put x1

1918− put x2

1919− PWithApp x1 x2 x3 -> do putWord8 47

1920− put x1

1921− put x2

1922− put x3

1923−

1924− get

1925− = do i <- getWord8

1926− case i of

1927− 0 -> do x1 <- get

1928− return (PQuote x1)

1929− 1 -> do x1 <- get

1930− x2 <- get

1931− x3 <- get

1932− return (PRef x1 x2 x3)

1933− 2 -> do x1 <- get

1934− x2 <- get

1935− x3 <- get

1936− return (PInferRef x1 x2 x3)

1937− 3 -> do x1 <- get

1938− x2 <- get

1939− return (PPatvar x1 x2)

1940− 4 -> do x1 <- get

1941− x2 <- get

1942− x3 <- get

1943− x4 <- get

1944− x5 <- get

1945− return (PLam x1 x2 x3 x4 x5)

1946− 5 -> do x1 <- get

1947− x2 <- get

1948− x3 <- get

1949− x4 <- get

1950− x5 <- get

1951− return (PPi x1 x2 x3 x4 x5)

1952− 6 -> do x1 <- get

1953− x2 <- get

1954− x3 <- get

1955− x4 <- get

1956− x5 <- get

1957− x6 <- get

1958− return (PLet x1 x2 x3 x4 x5 x6)

1959− 7 -> do x1 <- get

1960− x2 <- get

1961− return (PTyped x1 x2)

1962− 8 -> do x1 <- get

1963− x2 <- get

1964− x3 <- get

1965− return (PApp x1 x2 x3)

1966− 9 -> do x1 <- get

1967− x2 <- get

1968− x3 <- get

1969− return (PAppBind x1 x2 x3)

1970− 10 -> do x1 <- get

1971− x2 <- get

1972− return (PMatchApp x1 x2)

1973− 11 -> do x1 <- get

1974− x2 <- get

1975− x3 <- get

1976− return (PCase x1 x2 x3)

1977− 12 -> do x1 <- get

1978− x2 <- get

1979− return (PTrue x1 x2)

1980− 15 -> do x1 <- get

1981− return (PResolveTC x1)

1982− 17 -> do x1 <- get

1983− x2 <- get

1984− x3 <- get

1985− x4 <- get

1986− x5 <- get

1987− return (PRewrite x1 x2 x3 x4 x5)

1988− 18 -> do x1 <- get

1989− x2 <- get

1990− x3 <- get

1991− x4 <- get

1992− x5 <- get

1993− return (PPair x1 x2 x3 x4 x5)

1994− 19 -> do x1 <- get

1995− x2 <- get

1996− x3 <- get

1997− x4 <- get

1998− x5 <- get

1999− x6 <- get

2000− return (PDPair x1 x2 x3 x4 x5 x6)

2001− 20 -> do x1 <- get

2002− x2 <- get

2003− x3 <- get

2004− return (PAlternative x1 x2 x3)

2005− 21 -> do x1 <- get

2006− return (PHidden x1)

2007− 22 -> do x1 <- get

2008− return (PType x1)

2009− 23 -> do x1 <- get

2010− x2 <- get

2011− x3 <- get

2012− x4 <- get

2013− return (PGoal x1 x2 x3 x4)

2014− 24 -> do x1 <- get

2015− x2 <- get

2016− return (PConstant x1 x2)

2017− 25 -> return Placeholder

2018− 26 -> do x1 <- get

2019− return (PDoBlock x1)

2020− 27 -> do x1 <- get

2021− x2 <- get

2022− return (PIdiom x1 x2)

2023− 29 -> do x1 <- get

2024− x2 <- get

2025− return (PMetavar x1 x2)

2026− 30 -> do x1 <- get

2027− return (PProof x1)

2028− 31 -> do x1 <- get

2029− return (PTactics x1)

2030− 33 -> return PImpossible

2031− 34 -> do x1 <- get

2032− return (PCoerced x1)

2033− 35 -> do x1 <- get

2034− return (PUnifyLog x1)

2035− 36 -> do x1 <- get

2036− return (PNoImplicits x1)

2037− 37 -> do x1 <- get

2038− x2 <- get

2039− return (PDisamb x1 x2)

2040− 38 -> do x1 <- get

2041− x2 <- get

2042− return (PUniverse x1 x2)

2043− 39 -> do x1 <- get

2044− x2 <- get

2045− x3 <- get

2046− return (PRunElab x1 x2 x3)

2047− 40 -> do x1 <- get

2048− x2 <- get

2049− x3 <- get

2050− return (PAs x1 x2 x3)

2051− 41 -> do x1 <- get

2052− return (PElabError x1)

2053− 42 -> do x1 <- get

2054− x2 <- get

2055− return (PQuasiquote x1 x2)

2056− 43 -> do x1 <- get

2057− return (PUnquote x1)

2058− 44 -> do x1 <- get

2059− x2 <- get

2060− x3 <- get

2061− return (PQuoteName x1 x2 x3)

2062− 45 -> do x1 <- get

2063− x2 <- get

2064− x3 <- get

2065− x4 <- get

2066− return (PIfThenElse x1 x2 x3 x4)

2067− 46 -> do x1 <- get

2068− x2 <- get

2069− return (PConstSugar x1 x2)

2070− 47 -> do x1 <- get

2071− x2 <- get

2072− x3 <- get

2073− return (PWithApp x1 x2 x3)

2074− _ -> error "Corrupted binary data for PTerm"

2075−

2076−instance Binary PAltType where

2077− put x

2078− = case x of

2079− ExactlyOne x1 -> do putWord8 0

2080− put x1

2081− FirstSuccess -> putWord8 1

2082− TryImplicit -> putWord8 2

2083− get

2084− = do i <- getWord8

2085− case i of

2086− 0 -> do x1 <- get

2087− return (ExactlyOne x1)

2088− 1 -> return FirstSuccess

2089− 2 -> return TryImplicit

2090− _ -> error "Corrupted binary data for PAltType"

2091−

2092−

2093−instance (Binary t) => Binary (PTactic' t) where

2094− put x

2095− = case x of

2096− Intro x1 -> do putWord8 0

2097− put x1

2098− Focus x1 -> do putWord8 1

2099− put x1

2100− Refine x1 x2 -> do putWord8 2

2101− put x1

2102− put x2

2103− Rewrite x1 -> do putWord8 3

2104− put x1

2105− LetTac x1 x2 -> do putWord8 4

2106− put x1

2107− put x2

2108− Exact x1 -> do putWord8 5

2109− put x1

2110− Compute -> putWord8 6

2111− Trivial -> putWord8 7

2112− Solve -> putWord8 8

2113− Attack -> putWord8 9

2114− ProofState -> putWord8 10

2115− ProofTerm -> putWord8 11

2116− Undo -> putWord8 12

2117− Try x1 x2 -> do putWord8 13

2118− put x1

2119− put x2

2120− TSeq x1 x2 -> do putWord8 14

2121− put x1

2122− put x2

2123− Qed -> putWord8 15

2124− ApplyTactic x1 -> do putWord8 16

2125− put x1

2126− Reflect x1 -> do putWord8 17

2127− put x1

2128− Fill x1 -> do putWord8 18

2129− put x1

2130− Induction x1 -> do putWord8 19

2131− put x1

2132− ByReflection x1 -> do putWord8 20

2133− put x1

2134− ProofSearch x1 x2 x3 x4 x5 x6 -> do putWord8 21

2135− put x1

2136− put x2

2137− put x3

2138− put x4

2139− put x5

2140− put x6

2141− DoUnify -> putWord8 22

2142− CaseTac x1 -> do putWord8 23

2143− put x1

2144− SourceFC -> putWord8 24

2145− Intros -> putWord8 25

2146− Equiv x1 -> do putWord8 26

2147− put x1

2148− Claim x1 x2 -> do putWord8 27

2149− put x1

2150− put x2

2151− Unfocus -> putWord8 28

2152− MatchRefine x1 -> do putWord8 29

2153− put x1

2154− LetTacTy x1 x2 x3 -> do putWord8 30

2155− put x1

2156− put x2

2157− put x3

2158− TCImplementation -> putWord8 31

2159− GoalType x1 x2 -> do putWord8 32

2160− put x1

2161− put x2

2162− TCheck x1 -> do putWord8 33

2163− put x1

2164− TEval x1 -> do putWord8 34

2165− put x1

2166− TDocStr x1 -> do putWord8 35

2167− put x1

2168− TSearch x1 -> do putWord8 36

2169− put x1

2170− Skip -> putWord8 37

2171− TFail x1 -> do putWord8 38

2172− put x1

2173− Abandon -> putWord8 39

2174− get

2175− = do i <- getWord8

2176− case i of

2177− 0 -> do x1 <- get

2178− return (Intro x1)

2179− 1 -> do x1 <- get

2180− return (Focus x1)

2181− 2 -> do x1 <- get

2182− x2 <- get

2183− return (Refine x1 x2)

2184− 3 -> do x1 <- get

2185− return (Rewrite x1)

2186− 4 -> do x1 <- get

2187− x2 <- get

2188− return (LetTac x1 x2)

2189− 5 -> do x1 <- get

2190− return (Exact x1)

2191− 6 -> return Compute

2192− 7 -> return Trivial

2193− 8 -> return Solve

2194− 9 -> return Attack

2195− 10 -> return ProofState

2196− 11 -> return ProofTerm

2197− 12 -> return Undo

2198− 13 -> do x1 <- get

2199− x2 <- get

2200− return (Try x1 x2)

2201− 14 -> do x1 <- get

2202− x2 <- get

2203− return (TSeq x1 x2)

2204− 15 -> return Qed

2205− 16 -> do x1 <- get

2206− return (ApplyTactic x1)

2207− 17 -> do x1 <- get

2208− return (Reflect x1)

2209− 18 -> do x1 <- get

2210− return (Fill x1)

2211− 19 -> do x1 <- get

2212− return (Induction x1)

2213− 20 -> do x1 <- get

2214− return (ByReflection x1)

2215− 21 -> do x1 <- get

2216− x2 <- get

2217− x3 <- get

2218− x4 <- get

2219− x5 <- get

2220− x6 <- get

2221− return (ProofSearch x1 x2 x3 x4 x5 x6)

2222− 22 -> return DoUnify

2223− 23 -> do x1 <- get

2224− return (CaseTac x1)

2225− 24 -> return SourceFC

2226− 25 -> return Intros

2227− 26 -> do x1 <- get

2228− return (Equiv x1)

2229− 27 -> do x1 <- get

2230− x2 <- get

2231− return (Claim x1 x2)

2232− 28 -> return Unfocus

2233− 29 -> do x1 <- get

2234− return (MatchRefine x1)

2235− 30 -> do x1 <- get

2236− x2 <- get

2237− x3 <- get

2238− return (LetTacTy x1 x2 x3)

2239− 31 -> return TCImplementation

2240− 32 -> do x1 <- get

2241− x2 <- get

2242− return (GoalType x1 x2)

2243− 33 -> do x1 <- get

2244− return (TCheck x1)

2245− 34 -> do x1 <- get

2246− return (TEval x1)

2247− 35 -> do x1 <- get

2248− return (TDocStr x1)

2249− 36 -> do x1 <- get

2250− return (TSearch x1)

2251− 37 -> return Skip

2252− 38 -> do x1 <- get

2253− return (TFail x1)

2254− 39 -> return Abandon

2255− _ -> error "Corrupted binary data for PTactic'"

2256−

2257−

2258−instance (Binary t) => Binary (PDo' t) where

2259− put x

2260− = case x of

2261− DoExp x1 x2 -> do putWord8 0

2262− put x1

2263− put x2

2264− DoBind x1 x2 x3 x4 -> do putWord8 1

2265− put x1

2266− put x2

2267− put x3

2268− put x4

2269− DoBindP x1 x2 x3 x4 -> do putWord8 2

2270− put x1

2271− put x2

2272− put x3

2273− put x4

2274− DoLet x1 x2 x3 x4 x5 -> do putWord8 3

2275− put x1

2276− put x2

2277− put x3

2278− put x4

2279− put x5

2280− DoLetP x1 x2 x3 -> do putWord8 4

2281− put x1

2282− put x2

2283− put x3

2284− DoRewrite x1 x2 -> do putWord8 5

2285− put x1

2286− put x2

2287− get

2288− = do i <- getWord8

2289− case i of

2290− 0 -> do x1 <- get

2291− x2 <- get

2292− return (DoExp x1 x2)

2293− 1 -> do x1 <- get

2294− x2 <- get

2295− x3 <- get

2296− x4 <- get

2297− return (DoBind x1 x2 x3 x4)

2298− 2 -> do x1 <- get

2299− x2 <- get

2300− x3 <- get

2301− x4 <- get

2302− return (DoBindP x1 x2 x3 x4)

2303− 3 -> do x1 <- get

2304− x2 <- get

2305− x3 <- get

2306− x4 <- get

2307− x5 <- get

2308− return (DoLet x1 x2 x3 x4 x5)

2309− 4 -> do x1 <- get

2310− x2 <- get

2311− x3 <- get

2312− return (DoLetP x1 x2 x3)

2313− 5 -> do

2314− x1 <- get

2315− x2 <- get

2316− return (DoRewrite x1 x2)

2317− _ -> error "Corrupted binary data for PDo'"

2318−

2319−

2320−instance (Binary t) => Binary (PArg' t) where

2321− put x

2322− = case x of

2323− PImp x1 x2 x3 x4 x5 ->

2324− do putWord8 0

2325− put x1

2326− put x2

2327− put x3

2328− put x4

2329− put x5

2330− PExp x1 x2 x3 x4 ->

2331− do putWord8 1

2332− put x1

2333− put x2

2334− put x3

2335− put x4

2336− PConstraint x1 x2 x3 x4 ->

2337− do putWord8 2

2338− put x1

2339− put x2

2340− put x3

2341− put x4

2342− PTacImplicit x1 x2 x3 x4 x5 ->

2343− do putWord8 3

2344− put x1

2345− put x2

2346− put x3

2347− put x4

2348− put x5

2349− get

2350− = do i <- getWord8

2351− case i of

2352− 0 -> do x1 <- get

2353− x2 <- get

2354− x3 <- get

2355− x4 <- get

2356− x5 <- get

2357− return (PImp x1 x2 x3 x4 x5)

2358− 1 -> do x1 <- get

2359− x2 <- get

2360− x3 <- get

2361− x4 <- get

2362− return (PExp x1 x2 x3 x4)

2363− 2 -> do x1 <- get

2364− x2 <- get

2365− x3 <- get

2366− x4 <- get

2367− return (PConstraint x1 x2 x3 x4)

2368− 3 -> do x1 <- get

2369− x2 <- get

2370− x3 <- get

2371− x4 <- get

2372− x5 <- get

2373− return (PTacImplicit x1 x2 x3 x4 x5)

2374− _ -> error "Corrupted binary data for PArg'"

2375−

2376−

2377instance Binary InterfaceInfo where

1002instance Binary InterfaceInfo where

2378 put (CI x1 x2 x3 x4 x5 x6 x7 _ x8)

1003 put (CI x1 x2 x3 x4 x5 x6 x7 _ x8)

2379 = do put x1

1004 = do put x1

@@ -2395,160 +1020,13 @@ instance Binary InterfaceInfo where

2395 x8 <- get

1020 x8 <- get

2396 return (CI x1 x2 x3 x4 x5 x6 x7 [] x8)

1021 return (CI x1 x2 x3 x4 x5 x6 x7 [] x8)

2397

1022

2398−instance Binary RecordInfo where

1023+instance Binary RecordInfo

2399− put (RI x1 x2 x3)

2400− = do put x1

2401− put x2

2402− put x3

2403− get

2404− = do x1 <- get

2405− x2 <- get

2406− x3 <- get

2407− return (RI x1 x2 x3)

2408−

2409−instance Binary OptInfo where

1024+instance Binary OptInfo

2410− put (Optimise x1 x2 x3)

2411− = do put x1

2412− put x2

2413− put x3

2414− get

2415− = do x1 <- get

2416− x2 <- get

2417− x3 <- get

2418− return (Optimise x1 x2 x3)

2419−

2420−instance Binary FnInfo where

1025+instance Binary FnInfo

2421− put (FnInfo x1)

2422− = put x1

2423− get

2424− = do x1 <- get

2425− return (FnInfo x1)

2426−

2427−instance Binary TypeInfo where

1026+instance Binary TypeInfo

2428− put (TI x1 x2 x3 x4 x5 x6) = do put x1

2429− put x2

2430− put x3

2431− put x4

2432− put x5

2433− put x6

2434− get = do x1 <- get

2435− x2 <- get

2436− x3 <- get

2437− x4 <- get

2438− x5 <- get

2439− x6 <- get

2440− return (TI x1 x2 x3 x4 x5 x6)

2441−

2442−instance Binary SynContext where

1027+instance Binary SynContext

2443− put x

2444− = case x of

2445− PatternSyntax -> putWord8 0

2446− TermSyntax -> putWord8 1

2447− AnySyntax -> putWord8 2

2448− get

2449− = do i <- getWord8

2450− case i of

2451− 0 -> return PatternSyntax

2452− 1 -> return TermSyntax

2453− 2 -> return AnySyntax

2454− _ -> error "Corrupted binary data for SynContext"

2455−

2456−

2457−instance Binary Syntax where

1028+instance Binary Syntax

2458− put (Rule x1 x2 x3)

2459− = do putWord8 0

2460− put x1

2461− put x2

2462− put x3

2463− put (DeclRule x1 x2)

2464− = do putWord8 1

2465− put x1

2466− put x2

2467− get

2468− = do i <- getWord8

2469− case i of

2470− 0 -> do x1 <- get

2471− x2 <- get

2472− x3 <- get

2473− return (Rule x1 x2 x3)

2474− 1 -> do x1 <- get

2475− x2 <- get

2476− return (DeclRule x1 x2)

2477− _ -> error "Corrupted binary data for Syntax"

2478−

2479−instance (Binary t) => Binary (DSL' t) where

1029+instance (Binary t) => Binary (DSL' t)

2480− put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2481− = do put x1

2482− put x2

2483− put x3

2484− put x4

2485− put x5

2486− put x6

2487− put x7

2488− put x8

2489− put x9

2490− get

2491− = do x1 <- get

2492− x2 <- get

2493− x3 <- get

2494− x4 <- get

2495− x5 <- get

2496− x6 <- get

2497− x7 <- get

2498− x8 <- get

2499− x9 <- get

2500− return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2501−

2502−instance Binary SSymbol where

1030+instance Binary SSymbol

2503− put x

2504− = case x of

2505− Keyword x1 -> do putWord8 0

2506− put x1

2507− Symbol x1 -> do putWord8 1

2508− put x1

2509− Expr x1 -> do putWord8 2

2510− put x1

2511− SimpleExpr x1 -> do putWord8 3

2512− put x1

2513− Binding x1 -> do putWord8 4

2514− put x1

2515− get

2516− = do i <- getWord8

2517− case i of

2518− 0 -> do x1 <- get

2519− return (Keyword x1)

2520− 1 -> do x1 <- get

2521− return (Symbol x1)

2522− 2 -> do x1 <- get

2523− return (Expr x1)

2524− 3 -> do x1 <- get

2525− return (SimpleExpr x1)

2526− 4 -> do x1 <- get

2527− return (Binding x1)

2528− _ -> error "Corrupted binary data for SSymbol"

2529−

2530−instance Binary Codegen where

1031+instance Binary Codegen

2531− put x

2532− = case x of

2533− Via ir str -> do putWord8 0

2534− put ir

2535− put str

2536− Bytecode -> putWord8 1

2537− get

2538− = do i <- getWord8

2539− case i of

2540− 0 -> do x1 <- get

2541− x2 <- get

2542− return (Via x1 x2)

2543− 1 -> return Bytecode

2544− _ -> error "Corrupted binary data for Codegen"

2545−

2546−instance Binary IRFormat where

1032+instance Binary IRFormat

2547− put x = case x of

2548− IBCFormat -> putWord8 0

2549− JSONFormat -> putWord8 1

2550− get = do i <- getWord8

2551− case i of

2552− 0 -> return IBCFormat

2553− 1 -> return JSONFormat

2554− _ -> error "Corrupted binary data for IRFormat"

test/TestData.hs−1

@@ -1,7 +1,6 @@

1module TestData where

3import Data.IntMap as IMap

4−import Data.Map.Strict as Map

5import Data.Set as Set

4import Data.Set as Set

7data Codegen = C | JS deriving (Show, Eq, Ord)

6data Codegen = C | JS deriving (Show, Eq, Ord)

test/TestRun.hs−2

@@ -6,13 +6,11 @@ import TestData

6import Control.Monad

7import Data.Char (isLetter)

8import qualified Data.IntMap as IMap

9−import Data.List

10import Data.Monoid ((<>))

9import Data.Monoid ((<>))

11import Data.Proxy

10import Data.Proxy

12import Data.Typeable

11import Data.Typeable

13import Options.Applicative

12import Options.Applicative

14import System.Directory

13import System.Directory

15−import System.Environment

16import System.Exit

14import System.Exit

17import System.FilePath ((</>))

15import System.FilePath ((</>))

18import System.Info

16import System.Info