01dc619 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

New way of generating default definitions

commit01dc6193072bb01ee11dfd29818e56c52a8a2c1a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 1 May 2012, 15:04 (14 years ago) parent9c6546e

3 files changed+284−55

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+13−1 src/Idris/ElabDecls.hs+17−11 src/Idris/IBC.hs+254−43

src/Idris/AbsSyntax.hs+13−1

@@ -472,17 +472,26 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

472472 | PSyntax FC Syntax

473473 | PDirective (Idris ())

474474 deriving Functor

475+{-!

476+deriving instance Binary PDecl'

477+!-}

475478

476479data PClause' t = PClause FC Name t [t] t [PDecl' t]

477480 | PWith FC Name t [t] t [PDecl' t]

478481 | PClauseR FC [t] t [PDecl' t]

479482 | PWithR FC [t] t [PDecl' t]

480483 deriving Functor

484+{-!

485+deriving instance Binary PClause'

486+!-}

481487

482488data PData' t = PDatadecl { d_name :: Name,

483489 d_tcon :: t,

484490 d_cons :: [(Name, t, FC)] }

485491 deriving Functor

492+{-!

493+deriving instance Binary PData'

494+!-}

486495

487496-- Handy to get a free function for applying PTerm -> PTerm functions

488497-- across a program, by deriving Functor

@@ -680,7 +689,7 @@ type PArg = PArg' PTerm

680689

681690data ClassInfo = CI { instanceName :: Name,

682691 class_methods :: [(Name, (FnOpts, PTerm))],

683− class_defaults :: [(Name, Name)], -- method name -> default impl

692+ class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

684693 class_params :: [Name],

685694 class_instances :: [Name] }

686695 deriving Show

@@ -762,6 +771,9 @@ data SyntaxInfo = Syn { using :: [(Name, PTerm)],

762771 inPattern :: Bool,

763772 dsl_info :: DSL }

764773 deriving Show

774+{-!

775+deriving instance Binary SyntaxInfo

776+!-}

765777

766778defaultSyntax = Syn [] [] [] [] id False initDSL

767779

src/Idris/ElabDecls.hs+17−11

@@ -586,7 +586,7 @@ elabClass info syn fc constraints tn ps ds

586586 [PTy syn fc [] n ty',

587587 PClauses fc (TCGen:o ++ opts) n cs]

588588 iLOG (show ds)

589− return (n, (defaultdec n, ds))

589+ return (n, ((defaultdec n, ds!!1), ds))

590590 _ -> fail $ show n ++ " is not a method"

591591 defdecl _ _ _ = fail "Can't happen (defdecl)"

592592

@@ -689,7 +689,7 @@ elabInstance info syn fc cs n ps t ds

689689 (decorate ns n, op, coninsert cs t', t'))

690690 (class_methods ci)

691691 logLvl 3 (show (mtys, ips))

692− let ds' = insertDefaults (class_defaults ci) ns ds

692+ let ds' = insertDefaults i (class_defaults ci) ns ds

693693 iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

694694 mapM_ (warnMissing ds' ns) (map fst (class_methods ci))

695695 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

@@ -770,16 +770,20 @@ elabInstance info syn fc cs n ps t ds

770770 coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc)

771771 coninsert cs sc = conbind cs sc

772772

773− insertDefaults :: [(Name, Name)] -> [String] -> [PDecl] -> [PDecl]

774− insertDefaults [] ns ds = ds

775− insertDefaults ((n,dn) : defs) ns ds

776− = insertDefaults defs ns (insertDef n dn ns ds)

773+ insertDefaults :: IState -> [(Name, (Name, PDecl))] -> [String] -> [PDecl] -> [PDecl]

774+ insertDefaults i [] ns ds = ds

775+ insertDefaults i ((n,(dn, clauses)) : defs) ns ds

776+ = insertDefaults i defs ns (insertDef i n dn clauses ns ds)

777777

778− insertDef meth def ns decls

778+ insertDef i meth def clauses ns decls

779779 | null $ filter (clauseFor meth ns) decls

780− = decls ++ [PClauses fc [Inlinable,TCGen] meth

781− [PClause fc meth (PApp fc (PRef fc meth) []) []

782− (PApp fc (PRef fc def) []) []]]

780+ = let newd = expandParamsD i (\n -> meth) [] [def] clauses in

781+ -- trace (show newd) $

782+ decls ++ [newd]

783+

784+-- [PClauses fc [Inlinable,TCGen] meth

785+-- [PClause fc meth (PApp fc (PRef fc meth) []) []

786+-- (PApp fc (PRef fc def) []) []]]

783787 | otherwise = decls

784788

785789 warnMissing decls ns meth

@@ -883,14 +887,16 @@ elabCaseBlock info d@(PClauses f o n ps)

883887

884888checkInferred :: FC -> PTerm -> PTerm -> Idris ()

885889checkInferred fc inf user =

886− do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

890+ do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++

887891 showImp True user

892+ logLvl 10 $ "Checking match"

888893 i <- get

889894 tclift $ case matchClause' True i user inf of

890895 Right vs -> return ()

891896 Left (x, y) -> tfail $ At fc

892897 (Msg $ "The type-checked term and given term do not match: "

893898 ++ show x ++ " and " ++ show y)

899+ logLvl 10 $ "Checked match"

894900-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

895901

896902-- Return whether inferred term is different from given term

src/Idris/IBC.hs+254−43

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

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 17

24+ibcVersion = 18

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -802,6 +802,202 @@ instance Binary Plicity where

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

803803

804804

805+instance (Binary t) => Binary (PDecl' t) where

806+ put x

807+ = case x of

808+ PFix x1 x2 x3 -> do putWord8 0

809+ put x1

810+ put x2

811+ put x3

812+ PTy x1 x2 x3 x4 x5 -> do putWord8 1

813+ put x1

814+ put x2

815+ put x3

816+ put x4

817+ put x5

818+ PClauses x1 x2 x3 x4 -> do putWord8 2

819+ put x1

820+ put x2

821+ put x3

822+ put x4

823+ PData x1 x2 x3 -> do putWord8 3

824+ put x1

825+ put x2

826+ put x3

827+ PParams x1 x2 x3 -> do putWord8 4

828+ put x1

829+ put x2

830+ put x3

831+ PNamespace x1 x2 -> do putWord8 5

832+ put x1

833+ put x2

834+ PRecord x1 x2 x3 x4 x5 x6 -> do putWord8 6

835+ put x1

836+ put x2

837+ put x3

838+ put x4

839+ put x5

840+ put x6

841+ PClass x1 x2 x3 x4 x5 x6 -> do putWord8 7

842+ put x1

843+ put x2

844+ put x3

845+ put x4

846+ put x5

847+ put x6

848+ PInstance x1 x2 x3 x4 x5 x6 x7 -> do putWord8 8

849+ put x1

850+ put x2

851+ put x3

852+ put x4

853+ put x5

854+ put x6

855+ put x7

856+ PDSL x1 x2 -> do putWord8 9

857+ put x1

858+ put x2

859+ get

860+ = do i <- getWord8

861+ case i of

862+ 0 -> do x1 <- get

863+ x2 <- get

864+ x3 <- get

865+ return (PFix x1 x2 x3)

866+ 1 -> do x1 <- get

867+ x2 <- get

868+ x3 <- get

869+ x4 <- get

870+ x5 <- get

871+ return (PTy x1 x2 x3 x4 x5)

872+ 2 -> do x1 <- get

873+ x2 <- get

874+ x3 <- get

875+ x4 <- get

876+ return (PClauses x1 x2 x3 x4)

877+ 3 -> do x1 <- get

878+ x2 <- get

879+ x3 <- get

880+ return (PData x1 x2 x3)

881+ 4 -> do x1 <- get

882+ x2 <- get

883+ x3 <- get

884+ return (PParams x1 x2 x3)

885+ 5 -> do x1 <- get

886+ x2 <- get

887+ return (PNamespace x1 x2)

888+ 6 -> do x1 <- get

889+ x2 <- get

890+ x3 <- get

891+ x4 <- get

892+ x5 <- get

893+ x6 <- get

894+ return (PRecord x1 x2 x3 x4 x5 x6)

895+ 7 -> do x1 <- get

896+ x2 <- get

897+ x3 <- get

898+ x4 <- get

899+ x5 <- get

900+ x6 <- get

901+ return (PClass x1 x2 x3 x4 x5 x6)

902+ 8 -> do x1 <- get

903+ x2 <- get

904+ x3 <- get

905+ x4 <- get

906+ x5 <- get

907+ x6 <- get

908+ x7 <- get

909+ return (PInstance x1 x2 x3 x4 x5 x6 x7)

910+ 9 -> do x1 <- get

911+ x2 <- get

912+ return (PDSL x1 x2)

913+ _ -> error "Corrupted binary data for PDecl'"

914+

915+instance Binary SyntaxInfo where

916+ put (Syn x1 x2 x3 x4 x5 x6 x7)

917+ = do put x1

918+ put x2

919+ put x3

920+ put x4

921+ put x5

922+ put x6

923+ put x7

924+ get

925+ = do x1 <- get

926+ x2 <- get

927+ x3 <- get

928+ x4 <- get

929+ x5 <- get

930+ x6 <- get

931+ x7 <- get

932+ return (Syn x1 x2 x3 x4 x5 x6 x7)

933+

934+instance (Binary t) => Binary (PClause' t) where

935+ put x

936+ = case x of

937+ PClause x1 x2 x3 x4 x5 x6 -> do putWord8 0

938+ put x1

939+ put x2

940+ put x3

941+ put x4

942+ put x5

943+ put x6

944+ PWith x1 x2 x3 x4 x5 x6 -> do putWord8 1

945+ put x1

946+ put x2

947+ put x3

948+ put x4

949+ put x5

950+ put x6

951+ PClauseR x1 x2 x3 x4 -> do putWord8 2

952+ put x1

953+ put x2

954+ put x3

955+ put x4

956+ PWithR x1 x2 x3 x4 -> do putWord8 3

957+ put x1

958+ put x2

959+ put x3

960+ put x4

961+ get

962+ = do i <- getWord8

963+ case i of

964+ 0 -> do x1 <- get

965+ x2 <- get

966+ x3 <- get

967+ x4 <- get

968+ x5 <- get

969+ x6 <- get

970+ return (PClause x1 x2 x3 x4 x5 x6)

971+ 1 -> do x1 <- get

972+ x2 <- get

973+ x3 <- get

974+ x4 <- get

975+ x5 <- get

976+ x6 <- get

977+ return (PWith x1 x2 x3 x4 x5 x6)

978+ 2 -> do x1 <- get

979+ x2 <- get

980+ x3 <- get

981+ x4 <- get

982+ return (PClauseR x1 x2 x3 x4)

983+ 3 -> do x1 <- get

984+ x2 <- get

985+ x3 <- get

986+ x4 <- get

987+ return (PWithR x1 x2 x3 x4)

988+ _ -> error "Corrupted binary data for PClause'"

989+

990+instance (Binary t) => Binary (PData' t) where

991+ put (PDatadecl x1 x2 x3)

992+ = do put x1

993+ put x2

994+ put x3

995+ get

996+ = do x1 <- get

997+ x2 <- get

998+ x3 <- get

999+ return (PDatadecl x1 x2 x3)

1000+

8051001instance Binary PTerm where

8061002 put x

8071003 = case x of

@@ -824,53 +1020,61 @@ instance Binary PTerm where

8241020 put x2

8251021 put x3

8261022 put x4

827− PApp x1 x2 x3 -> do putWord8 5

1023+ PTyped x1 x2 -> do putWord8 5

1024+ put x1

1025+ put x2

1026+ PApp x1 x2 x3 -> do putWord8 6

8281027 put x1

8291028 put x2

8301029 put x3

831− PTrue x1 -> do putWord8 6

1030+ PCase x1 x2 x3 -> do putWord8 7

1031+ put x1

1032+ put x2

1033+ put x3

1034+ PTrue x1 -> do putWord8 8

8321035 put x1

833− PFalse x1 -> do putWord8 7

1036+ PFalse x1 -> do putWord8 9

8341037 put x1

835− PRefl x1 -> do putWord8 8

1038+ PRefl x1 -> do putWord8 10

8361039 put x1

837− PResolveTC x1 -> do putWord8 9

1040+ PResolveTC x1 -> do putWord8 11

8381041 put x1

839− PEq x1 x2 x3 -> do putWord8 10

1042+ PEq x1 x2 x3 -> do putWord8 12

8401043 put x1

8411044 put x2

8421045 put x3

843− PPair x1 x2 x3 -> do putWord8 11

1046+ PPair x1 x2 x3 -> do putWord8 13

8441047 put x1

8451048 put x2

8461049 put x3

847− PDPair x1 x2 x3 x4 -> do putWord8 12

1050+ PDPair x1 x2 x3 x4 -> do putWord8 14

8481051 put x1

8491052 put x2

8501053 put x3

8511054 put x4

852− PAlternative x1 x2 -> do putWord8 13

1055+ PAlternative x1 x2 -> do putWord8 15

8531056 put x1

8541057 put x2

855− PHidden x1 -> do putWord8 14

1058+ PHidden x1 -> do putWord8 16

8561059 put x1

857− PSet -> putWord8 15

858− PConstant x1 -> do putWord8 16

1060+ PSet -> putWord8 17

1061+ PConstant x1 -> do putWord8 18

8591062 put x1

860− Placeholder -> putWord8 17

861− PDoBlock x1 -> do putWord8 18

1063+ Placeholder -> putWord8 19

1064+ PDoBlock x1 -> do putWord8 20

8621065 put x1

863− PReturn x1 -> do putWord8 19

1066+ PIdiom x1 x2 -> do putWord8 21

1067+ put x1

1068+ put x2

1069+ PReturn x1 -> do putWord8 22

8641070 put x1

865− PMetavar x1 -> do putWord8 20

1071+ PMetavar x1 -> do putWord8 23

8661072 put x1

867− PProof x1 -> do putWord8 21

1073+ PProof x1 -> do putWord8 24

8681074 put x1

869− PTactics x1 -> do putWord8 22

1075+ PTactics x1 -> do putWord8 25

8701076 put x1

871−-- PElabError x1 -> do putWord8 23

872−-- put x1

873− PImpossible -> putWord8 24

1077+ PImpossible -> putWord8 27

8741078 get

8751079 = do i <- getWord8

8761080 case i of

@@ -894,54 +1098,61 @@ instance Binary PTerm where

8941098 x4 <- get

8951099 return (PLet x1 x2 x3 x4)

8961100 5 -> do x1 <- get

1101+ x2 <- get

1102+ return (PTyped x1 x2)

1103+ 6 -> do x1 <- get

8971104 x2 <- get

8981105 x3 <- get

8991106 return (PApp x1 x2 x3)

900− 6 -> do x1 <- get

901− return (PTrue x1)

9021107 7 -> do x1 <- get

903− return (PFalse x1)

1108+ x2 <- get

1109+ x3 <- get

1110+ return (PCase x1 x2 x3)

9041111 8 -> do x1 <- get

905− return (PRefl x1)

1112+ return (PTrue x1)

9061113 9 -> do x1 <- get

907− return (PResolveTC x1)

1114+ return (PFalse x1)

9081115 10 -> do x1 <- get

1116+ return (PRefl x1)

1117+ 11 -> do x1 <- get

1118+ return (PResolveTC x1)

1119+ 12 -> do x1 <- get

9091120 x2 <- get

9101121 x3 <- get

9111122 return (PEq x1 x2 x3)

912− 11 -> do x1 <- get

1123+ 13 -> do x1 <- get

9131124 x2 <- get

9141125 x3 <- get

9151126 return (PPair x1 x2 x3)

916− 12 -> do x1 <- get

1127+ 14 -> do x1 <- get

9171128 x2 <- get

9181129 x3 <- get

9191130 x4 <- get

9201131 return (PDPair x1 x2 x3 x4)

921− 13 -> do x1 <- get

1132+ 15 -> do x1 <- get

9221133 x2 <- get

9231134 return (PAlternative x1 x2)

924− 14 -> do x1 <- get

925− return (PHidden x1)

926− 15 -> return PSet

9271135 16 -> do x1 <- get

928− return (PConstant x1)

929− 17 -> return Placeholder

1136+ return (PHidden x1)

1137+ 17 -> return PSet

9301138 18 -> do x1 <- get

1139+ return (PConstant x1)

1140+ 19 -> return Placeholder

1141+ 20 -> do x1 <- get

9311142 return (PDoBlock x1)

932− 19 -> do x1 <- get

1143+ 21 -> do x1 <- get

1144+ x2 <- get

1145+ return (PIdiom x1 x2)

1146+ 22 -> do x1 <- get

9331147 return (PReturn x1)

934− 20 -> do x1 <- get

1148+ 23 -> do x1 <- get

9351149 return (PMetavar x1)

936− 21 -> do x1 <- get

1150+ 24 -> do x1 <- get

9371151 return (PProof x1)

938− 22 -> do x1 <- get

1152+ 25 -> do x1 <- get

9391153 return (PTactics x1)

940−-- 23 -> do x1 <- get

941−-- return (PElabError x1)

942− 24 -> return PImpossible

1154+ 27 -> return PImpossible

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

944−

9451156

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

9471158 put x