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

git.iko.soy/Idris-dev

on master help sign in

New way of generating default definitions

01dc619Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+13−1

compare with master

unifiedsplit

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

472 | PSyntax FC Syntax

473 | PDirective (Idris ())

474 deriving Functor

475+{-!

476+deriving instance Binary PDecl'

477+!-}

475

478

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

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

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

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

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

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

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

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

480 deriving Functor

483 deriving Functor

484+{-!

485+deriving instance Binary PClause'

486+!-}

481

487

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

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

483 d_tcon :: t,

489 d_tcon :: t,

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

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

485 deriving Functor

491 deriving Functor

492+{-!

493+deriving instance Binary PData'

494+!-}

486

495

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

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

488-- across a program, by deriving Functor

497-- across a program, by deriving Functor

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

680

689

681data ClassInfo = CI { instanceName :: Name,

690data ClassInfo = CI { instanceName :: Name,

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

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

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

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

684 class_params :: [Name],

693 class_params :: [Name],

685 class_instances :: [Name] }

694 class_instances :: [Name] }

686 deriving Show

695 deriving Show

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

762 inPattern :: Bool,

771 inPattern :: Bool,

763 dsl_info :: DSL }

772 dsl_info :: DSL }

764 deriving Show

773 deriving Show

774+{-!

775+deriving instance Binary SyntaxInfo

776+!-}

765

777

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

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

767

779

src/Idris/ElabDecls.hs+17−11

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

586 [PTy syn fc [] n ty',

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

588 iLOG (show ds)

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

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

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

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

592

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

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

690 (class_methods ci)

691 logLvl 3 (show (mtys, ips))

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

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

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

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

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

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

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

771 coninsert cs sc = conbind cs sc

772

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

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

774− insertDefaults [] ns ds = ds

774+ insertDefaults i [] ns ds = ds

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

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

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

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

777

778− insertDef meth def ns decls

778+ insertDef i meth def clauses ns decls

779 | null $ filter (clauseFor meth ns) decls

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

781+ -- trace (show newd) $

782+ decls ++ [newd]

783+

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

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

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

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

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

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

783 | otherwise = decls

787 | otherwise = decls

784

788

785 warnMissing decls ns meth

789 warnMissing decls ns meth

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

883

887

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

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

885checkInferred fc inf user =

889checkInferred 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" ++

887 showImp True user

891 showImp True user

892+ logLvl 10 $ "Checking match"

888 i <- get

893 i <- get

889 tclift $ case matchClause' True i user inf of

894 tclift $ case matchClause' True i user inf of

890 Right vs -> return ()

895 Right vs -> return ()

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

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

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

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

893 ++ show x ++ " and " ++ show y)

898 ++ show x ++ " and " ++ show y)

899+ logLvl 10 $ "Checked match"

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

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

895

901

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

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

src/Idris/IBC.hs+254−43

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

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 17

24+ibcVersion = 18

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

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

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

803

804

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+

805instance Binary PTerm where

1001instance Binary PTerm where

806 put x

1002 put x

807 = case x of

1003 = case x of

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

824 put x2

1020 put x2

825 put x3

1021 put x3

826 put x4

1022 put x4

1023+ PTyped x1 x2 -> do putWord8 5

1024+ put x1

1025+ put x2

827− PApp x1 x2 x3 -> do putWord8 5

1026+ PApp x1 x2 x3 -> do putWord8 6

828 put x1

1027 put x1

829 put x2

1028 put x2

830 put x3

1029 put x3

1030+ PCase x1 x2 x3 -> do putWord8 7

1031+ put x1

1032+ put x2

1033+ put x3

831− PTrue x1 -> do putWord8 6

1034+ PTrue x1 -> do putWord8 8

832 put x1

1035 put x1

833− PFalse x1 -> do putWord8 7

1036+ PFalse x1 -> do putWord8 9

834 put x1

1037 put x1

835− PRefl x1 -> do putWord8 8

1038+ PRefl x1 -> do putWord8 10

836 put x1

1039 put x1

837− PResolveTC x1 -> do putWord8 9

1040+ PResolveTC x1 -> do putWord8 11

838 put x1

1041 put x1

839− PEq x1 x2 x3 -> do putWord8 10

1042+ PEq x1 x2 x3 -> do putWord8 12

840 put x1

1043 put x1

841 put x2

1044 put x2

842 put x3

1045 put x3

843− PPair x1 x2 x3 -> do putWord8 11

1046+ PPair x1 x2 x3 -> do putWord8 13

844 put x1

1047 put x1

845 put x2

1048 put x2

846 put x3

1049 put x3

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

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

848 put x1

1051 put x1

849 put x2

1052 put x2

850 put x3

1053 put x3

851 put x4

1054 put x4

852− PAlternative x1 x2 -> do putWord8 13

1055+ PAlternative x1 x2 -> do putWord8 15

853 put x1

1056 put x1

854 put x2

1057 put x2

855− PHidden x1 -> do putWord8 14

1058+ PHidden x1 -> do putWord8 16

856 put x1

1059 put x1

857− PSet -> putWord8 15

1060+ PSet -> putWord8 17

858− PConstant x1 -> do putWord8 16

1061+ PConstant x1 -> do putWord8 18

859 put x1

1062 put x1

860− Placeholder -> putWord8 17

1063+ Placeholder -> putWord8 19

861− PDoBlock x1 -> do putWord8 18

1064+ PDoBlock x1 -> do putWord8 20

862 put x1

1065 put x1

1066+ PIdiom x1 x2 -> do putWord8 21

1067+ put x1

1068+ put x2

863− PReturn x1 -> do putWord8 19

1069+ PReturn x1 -> do putWord8 22

864 put x1

1070 put x1

865− PMetavar x1 -> do putWord8 20

1071+ PMetavar x1 -> do putWord8 23

866 put x1

1072 put x1

867− PProof x1 -> do putWord8 21

1073+ PProof x1 -> do putWord8 24

868 put x1

1074 put x1

869− PTactics x1 -> do putWord8 22

1075+ PTactics x1 -> do putWord8 25

870 put x1

1076 put x1

871−-- PElabError x1 -> do putWord8 23

872−-- put x1

873− PImpossible -> putWord8 24

1077+ PImpossible -> putWord8 27

874 get

1078 get

875 = do i <- getWord8

1079 = do i <- getWord8

876 case i of

1080 case i of

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

894 x4 <- get

1098 x4 <- get

895 return (PLet x1 x2 x3 x4)

1099 return (PLet x1 x2 x3 x4)

896 5 -> do x1 <- get

1100 5 -> do x1 <- get

1101+ x2 <- get

1102+ return (PTyped x1 x2)

1103+ 6 -> do x1 <- get

897 x2 <- get

1104 x2 <- get

898 x3 <- get

1105 x3 <- get

899 return (PApp x1 x2 x3)

1106 return (PApp x1 x2 x3)

900− 6 -> do x1 <- get

901− return (PTrue x1)

902 7 -> do x1 <- get

1107 7 -> do x1 <- get

1108+ x2 <- get

1109+ x3 <- get

903− return (PFalse x1)

1110+ return (PCase x1 x2 x3)

904 8 -> do x1 <- get

1111 8 -> do x1 <- get

905− return (PRefl x1)

1112+ return (PTrue x1)

906 9 -> do x1 <- get

1113 9 -> do x1 <- get

907− return (PResolveTC x1)

1114+ return (PFalse x1)

908 10 -> do x1 <- get

1115 10 -> do x1 <- get

1116+ return (PRefl x1)

1117+ 11 -> do x1 <- get

1118+ return (PResolveTC x1)

1119+ 12 -> do x1 <- get

909 x2 <- get

1120 x2 <- get

910 x3 <- get

1121 x3 <- get

911 return (PEq x1 x2 x3)

1122 return (PEq x1 x2 x3)

912− 11 -> do x1 <- get

1123+ 13 -> do x1 <- get

913 x2 <- get

1124 x2 <- get

914 x3 <- get

1125 x3 <- get

915 return (PPair x1 x2 x3)

1126 return (PPair x1 x2 x3)

916− 12 -> do x1 <- get

1127+ 14 -> do x1 <- get

917 x2 <- get

1128 x2 <- get

918 x3 <- get

1129 x3 <- get

919 x4 <- get

1130 x4 <- get

920 return (PDPair x1 x2 x3 x4)

1131 return (PDPair x1 x2 x3 x4)

921− 13 -> do x1 <- get

1132+ 15 -> do x1 <- get

922 x2 <- get

1133 x2 <- get

923 return (PAlternative x1 x2)

1134 return (PAlternative x1 x2)

924− 14 -> do x1 <- get

925− return (PHidden x1)

926− 15 -> return PSet

927 16 -> do x1 <- get

1135 16 -> do x1 <- get

928− return (PConstant x1)

1136+ return (PHidden x1)

929− 17 -> return Placeholder

1137+ 17 -> return PSet

930 18 -> do x1 <- get

1138 18 -> do x1 <- get

1139+ return (PConstant x1)

1140+ 19 -> return Placeholder

1141+ 20 -> do x1 <- get

931 return (PDoBlock x1)

1142 return (PDoBlock x1)

1143+ 21 -> do x1 <- get

1144+ x2 <- get

1145+ return (PIdiom x1 x2)

932− 19 -> do x1 <- get

1146+ 22 -> do x1 <- get

933 return (PReturn x1)

1147 return (PReturn x1)

934− 20 -> do x1 <- get

1148+ 23 -> do x1 <- get

935 return (PMetavar x1)

1149 return (PMetavar x1)

936− 21 -> do x1 <- get

1150+ 24 -> do x1 <- get

937 return (PProof x1)

1151 return (PProof x1)

938− 22 -> do x1 <- get

1152+ 25 -> do x1 <- get

939 return (PTactics x1)

1153 return (PTactics x1)

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

941−-- return (PElabError x1)

942− 24 -> return PImpossible

1154+ 27 -> return PImpossible

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

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

944−

945

1156

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

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

947 put x

1158 put x