7c7bf28 · Idris-dev · git.iko.soy

1325 PRef x1 x2 -> do putWord8 1

1326 put x1

1327 put x2

1328+ PInferRef x1 x2 -> do putWord8 2

1329+ put x1

1330+ put x2

1331+ PPatvar x1 x2 -> do putWord8 3

1332+ put x1

1333+ put x2

1328− PLam x1 x2 x3 -> do putWord8 2

1334+ PLam x1 x2 x3 -> do putWord8 4

1329 put x1

1335 put x1

1330 put x2

1336 put x2

1331 put x3

1337 put x3

1332− PPi x1 x2 x3 x4 -> do putWord8 3

1338+ PPi x1 x2 x3 x4 -> do putWord8 5

1333 put x1

1339 put x1

1334 put x2

1340 put x2

1335 put x3

1341 put x3

1336 put x4

1342 put x4

1337− PLet x1 x2 x3 x4 -> do putWord8 4

1343+ PLet x1 x2 x3 x4 -> do putWord8 6

1338 put x1

1344 put x1

1339 put x2

1345 put x2

1340 put x3

1346 put x3

1341 put x4

1347 put x4

1342− PTyped x1 x2 -> do putWord8 5

1348+ PTyped x1 x2 -> do putWord8 7

1343 put x1

1349 put x1

1344 put x2

1350 put x2

1345− PApp x1 x2 x3 -> do putWord8 6

1351+ PApp x1 x2 x3 -> do putWord8 8

1346 put x1

1352 put x1

1347 put x2

1353 put x2

1348 put x3

1354 put x3

1355+ PAppBind x1 x2 x3 -> do putWord8 9

1356+ put x1

1357+ put x2

1358+ put x3

1359+ PMatchApp x1 x2 -> do putWord8 10

1360+ put x1

1361+ put x2

1349− PCase x1 x2 x3 -> do putWord8 7

1362+ PCase x1 x2 x3 -> do putWord8 11

1350 put x1

1363 put x1

1351 put x2

1364 put x2

1352 put x3

1365 put x3

1353− PTrue x1 -> do putWord8 8

1366+ PTrue x1 -> do putWord8 12

1354 put x1

1367 put x1

1355− PFalse x1 -> do putWord8 9

1368+ PFalse x1 -> do putWord8 13

1356 put x1

1369 put x1

1357− PRefl x1 x2 -> do putWord8 10

1370+ PRefl x1 x2 -> do putWord8 14

1358 put x1

1371 put x1

1359 put x2

1372 put x2

1360− PResolveTC x1 -> do putWord8 11

1373+ PResolveTC x1 -> do putWord8 15

1361 put x1

1374 put x1

1362− PEq x1 x2 x3 -> do putWord8 12

1375+ PEq x1 x2 x3 -> do putWord8 16

1363 put x1

1376 put x1

1364 put x2

1377 put x2

1365 put x3

1378 put x3

1379+ PRewrite x1 x2 x3 x4 -> do putWord8 17

1380+ put x1

1381+ put x2

1382+ put x3

1383+ put x4

1366− PPair x1 x2 x3 -> do putWord8 13

1384+ PPair x1 x2 x3 -> do putWord8 18

1367 put x1

1385 put x1

1368 put x2

1386 put x2

1369 put x3

1387 put x3

1370− PDPair x1 x2 x3 x4 -> do putWord8 14

1388+ PDPair x1 x2 x3 x4 -> do putWord8 19

1371 put x1

1389 put x1

1372 put x2

1390 put x2

1373 put x3

1391 put x3

1374 put x4

1392 put x4

1375− PAlternative x1 x2 -> do putWord8 15

1393+ PAlternative x1 x2 -> do putWord8 20

1376 put x1

1394 put x1

1377 put x2

1395 put x2

1378− PHidden x1 -> do putWord8 16

1396+ PHidden x1 -> do putWord8 21

1379 put x1

1397 put x1

1380− PType -> putWord8 17

1398+ PType -> putWord8 22

1399+ PGoal x1 x2 x3 x4 -> do putWord8 23

1400+ put x1

1401+ put x2

1402+ put x3

1403+ put x4

1381− PConstant x1 -> do putWord8 18

1404+ PConstant x1 -> do putWord8 24

1382 put x1

1405 put x1

1383− Placeholder -> putWord8 19

1406+ Placeholder -> putWord8 25

1384− PDoBlock x1 -> do putWord8 20

1407+ PDoBlock x1 -> do putWord8 26

1385 put x1

1408 put x1

1386− PIdiom x1 x2 -> do putWord8 21

1409+ PIdiom x1 x2 -> do putWord8 27

1387 put x1

1410 put x1

1388 put x2

1411 put x2

1389− PReturn x1 -> do putWord8 22

1412+ PReturn x1 -> do putWord8 28

1390 put x1

1413 put x1

1391− PMetavar x1 -> do putWord8 23

1414+ PMetavar x1 -> do putWord8 29

1392 put x1

1415 put x1

1393− PProof x1 -> do putWord8 24

1416+ PProof x1 -> do putWord8 30

1394 put x1

1417 put x1

1395− PTactics x1 -> do putWord8 25

1418+ PTactics x1 -> do putWord8 31

1396 put x1

1419 put x1

1397− PImpossible -> putWord8 27

1420+ PImpossible -> putWord8 33

1398− PPatvar x1 x2 -> do putWord8 28

1421+ PCoerced x1 -> do putWord8 34

1399− put x1

1422+ put x1

1423+ PUnifyLog x1 -> do putWord8 35

1400− put x2

1424+ put x1

1401− PInferRef x1 x2 -> do putWord8 29

1425+ PNoImplicits x1 -> do putWord8 36

1402 put x1

1426 put x1

1403− put x2

1404− PRewrite x1 x2 x3 x4 -> do putWord8 30

1405− put x1

1406− put x2

1407− put x3

1408− put x4

1409− PGoal x1 x2 x3 x4 -> do putWord8 31

1410− put x1

1411− put x2

1412− put x3

1413− put x4

1414− PAppBind x1 x2 x3 -> do putWord8 32

1415− put x1

1416− put x2

1417− put x3

1418 get

1427 get

1419 = do i <- getWord8

1428 = do i <- getWord8

1420 case i of

1429 case i of

1424 x2 <- get

1433 x2 <- get

1425 return (PRef x1 x2)

1434 return (PRef x1 x2)

1426 2 -> do x1 <- get

1435 2 -> do x1 <- get

1436+ x2 <- get

1437+ return (PInferRef x1 x2)

1438+ 3 -> do x1 <- get

1439+ x2 <- get

1440+ return (PPatvar x1 x2)

1441+ 4 -> do x1 <- get

1427 x2 <- get

1442 x2 <- get

1428 x3 <- get

1443 x3 <- get

1429 return (PLam x1 x2 x3)

1444 return (PLam x1 x2 x3)

1430− 3 -> do x1 <- get

1445+ 5 -> do x1 <- get

1431 x2 <- get

1446 x2 <- get

1432 x3 <- get

1447 x3 <- get

1433 x4 <- get

1448 x4 <- get

1434 return (PPi x1 x2 x3 x4)

1449 return (PPi x1 x2 x3 x4)

1435− 4 -> do x1 <- get

1450+ 6 -> do x1 <- get

1436 x2 <- get

1451 x2 <- get

1437 x3 <- get

1452 x3 <- get

1438 x4 <- get

1453 x4 <- get

1439 return (PLet x1 x2 x3 x4)

1454 return (PLet x1 x2 x3 x4)

1440− 5 -> do x1 <- get

1455+ 7 -> do x1 <- get

1441 x2 <- get

1456 x2 <- get

1442 return (PTyped x1 x2)

1457 return (PTyped x1 x2)

1443− 6 -> do x1 <- get

1458+ 8 -> do x1 <- get

1444 x2 <- get

1459 x2 <- get

1445 x3 <- get

1460 x3 <- get

1446 return (PApp x1 x2 x3)

1461 return (PApp x1 x2 x3)

1447− 7 -> do x1 <- get

1462+ 9 -> do x1 <- get

1448 x2 <- get

1463 x2 <- get

1449 x3 <- get

1464 x3 <- get

1450− return (PCase x1 x2 x3)

1465+ return (PAppBind x1 x2 x3)

1451− 8 -> do x1 <- get

1452− return (PTrue x1)

1453− 9 -> do x1 <- get

1454− return (PFalse x1)

1455 10 -> do x1 <- get

1466 10 -> do x1 <- get

1456 x2 <- get

1467 x2 <- get

1457− return (PRefl x1 x2)

1468+ return (PMatchApp x1 x2)

1458 11 -> do x1 <- get

1469 11 -> do x1 <- get

1470+ x2 <- get

1471+ x3 <- get

1459− return (PResolveTC x1)

1472+ return (PCase x1 x2 x3)

1460 12 -> do x1 <- get

1473 12 -> do x1 <- get

1474+ return (PTrue x1)

1475+ 13 -> do x1 <- get

1476+ return (PFalse x1)

1477+ 14 -> do x1 <- get

1478+ x2 <- get

1479+ return (PRefl x1 x2)

1480+ 15 -> do x1 <- get

1481+ return (PResolveTC x1)

1482+ 16 -> do x1 <- get

1461 x2 <- get

1483 x2 <- get

1462 x3 <- get

1484 x3 <- get

1463 return (PEq x1 x2 x3)

1485 return (PEq x1 x2 x3)

1486+ 17 -> do x1 <- get

1487+ x2 <- get

1488+ x3 <- get

1489+ x4 <- get

1490+ return (PRewrite x1 x2 x3 x4)

1464− 13 -> do x1 <- get

1491+ 18 -> do x1 <- get

1465 x2 <- get

1492 x2 <- get

1466 x3 <- get

1493 x3 <- get

1467 return (PPair x1 x2 x3)

1494 return (PPair x1 x2 x3)

1468− 14 -> do x1 <- get

1495+ 19 -> do x1 <- get

1469 x2 <- get

1496 x2 <- get

1470 x3 <- get

1497 x3 <- get

1471 x4 <- get

1498 x4 <- get

1472 return (PDPair x1 x2 x3 x4)

1499 return (PDPair x1 x2 x3 x4)

1473− 15 -> do x1 <- get

1500+ 20 -> do x1 <- get

1474 x2 <- get

1501 x2 <- get

1475 return (PAlternative x1 x2)

1502 return (PAlternative x1 x2)

1476− 16 -> do x1 <- get

1503+ 21 -> do x1 <- get

1477 return (PHidden x1)

1504 return (PHidden x1)

1478− 17 -> return PType

1505+ 22 -> return PType

1506+ 23 -> do x1 <- get

1507+ x2 <- get

1508+ x3 <- get

1509+ x4 <- get

1510+ return (PGoal x1 x2 x3 x4)

1479− 18 -> do x1 <- get

1511+ 24 -> do x1 <- get

1480 return (PConstant x1)

1512 return (PConstant x1)

1481− 19 -> return Placeholder

1513+ 25 -> return Placeholder

1482− 20 -> do x1 <- get

1514+ 26 -> do x1 <- get

1483 return (PDoBlock x1)

1515 return (PDoBlock x1)

1484− 21 -> do x1 <- get

1516+ 27 -> do x1 <- get

1485 x2 <- get

1517 x2 <- get

1486 return (PIdiom x1 x2)

1518 return (PIdiom x1 x2)

1487− 22 -> do x1 <- get

1488− return (PReturn x1)

1489− 23 -> do x1 <- get

1490− return (PMetavar x1)

1491− 24 -> do x1 <- get

1492− return (PProof x1)

1493− 25 -> do x1 <- get

1494− return (PTactics x1)

1495− 27 -> return PImpossible

1496 28 -> do x1 <- get

1519 28 -> do x1 <- get

1497− x2 <- get

1498− return (PPatvar x1 x2)

1520+ return (PReturn x1)

1499 29 -> do x1 <- get

1521 29 -> do x1 <- get

1500− x2 <- get

1501− return (PInferRef x1 x2)

1522+ return (PMetavar x1)

1502 30 -> do x1 <- get

1523 30 -> do x1 <- get

1503− x2 <- get

1504− x3 <- get

1505− x4 <- get

1506− return (PRewrite x1 x2 x3 x4)

1524+ return (PProof x1)

1507 31 -> do x1 <- get

1525 31 -> do x1 <- get

1508− x2 <- get

1526+ return (PTactics x1)

1509− x3 <- get

1527+ 33 -> return PImpossible

1510− x4 <- get

1528+ 34 -> do x1 <- get

1511− return (PGoal x1 x2 x3 x4)

1529+ return (PCoerced x1)

1512− 32 -> do x1 <- get

1530+ 35 -> do x1 <- get

1513− x2 <- get

1531+ return (PUnifyLog x1)

1514− x3 <- get

1532+ 36 -> do x1 <- get

1515− return (PAppBind x1 x2 x3)

1533+ return (PNoImplicits x1)

1516 _ -> error "Corrupted binary data for PTerm"

1534 _ -> error "Corrupted binary data for PTerm"

1517−

1535+

1518instance (Binary t) => Binary (PTactic' t) where

1536instance (Binary t) => Binary (PTactic' t) where

1519 put x

1537 put x

1520 = case x of

1538 = case x of