1d97fa7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Propagate default totality to instances

Fixes #2962

commit1d97fa71156835112427a0a42861156ae901e83d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Feb 2016, 12:35 (11 years ago) parent6c682f3

4 files changed+19−11

compare with master

unifiedsplit

libs/prelude/Prelude/File.idr+2 libs/prelude/Prelude/Nat.idr+3 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Instance.hs+13−10

libs/prelude/Prelude/File.idr+2

@@ -44,6 +44,8 @@ getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

4444 return err

4545

4646Show FileError where

47+ show FileReadError = "File Read Error"

48+ show FileWriteError = "File Write Error"

4749 show FileNotFound = "File Not Found"

4850 show PermissionDenied = "Permission Denied"

4951 show (GenericFileError errno) = strError errno

libs/prelude/Prelude/Nat.idr+3

@@ -341,9 +341,12 @@ partial

341341divCeil : Nat -> Nat -> Nat

342342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ

343343

344+-- TMP HACK until it's possible to set flags on instances

345+%default partial

344346Integral Nat where

345347 div = divNat

346348 mod = modNat

349+%default total

347350

348351log2NZ : (x: Nat) -> Not (x = Z) -> Nat

349352log2NZ Z p = void (p Refl)

src/Idris/Elab/Clause.hs+1−1

@@ -581,7 +581,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

581581-- let lhs = mkLHSapp $

582582-- propagateParams i params fn_ty (addImplPat i lhs_in)

583583 logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

584− logElab 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

584+ logElab 5 ("LHS: " ++ show opts ++ "\n" ++ show fc ++ " " ++ showTmImpls lhs)

585585 logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

586586 "\n" ++ show (fn_ty, fn_is))

587587

src/Idris/Elab/Instance.hs+13−10

@@ -63,24 +63,27 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

6363 Maybe Name -> -- explicit name

6464 [PDecl] -> Idris ()

6565elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

66− i <- getIState

67− (n, ci) <- case lookupCtxtName n (idris_classes i) of

66+ ist <- getIState

67+ (n, ci) <- case lookupCtxtName n (idris_classes ist) of

6868 [c] -> return c

6969 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

7070 cs -> tclift $ tfail $ At fc

7171 (CantResolveAlts (map fst cs))

7272 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

7373 let iname = mkiname n (namespace info) ps expn

74− putIState (i { hide_list = addDef iname acc (hide_list i) })

75− i <- getIState

74+ putIState (ist { hide_list = addDef iname acc (hide_list ist) })

75+ ist <- getIState

76+

77+ let totopts = if default_total ist then [TotalFn, Dictionary]

78+ else [Dictionary]

7679

7780 let emptyclass = null (class_methods ci)

7881 when (what /= EDefns) $ do

79− nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

82+ nty <- elabType' True info syn doc argDocs fc totopts iname NoFC t

8083 -- if the instance type matches any of the instances we have already,

8184 -- and it's not a named instance, then it's overlapping, so report an error

8285 case expn of

83− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))

86+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (class_determiners ci) (delab ist nty))

8487 (map fst $ class_instances ci)

8588 addInstance intInst True n iname

8689 Just _ -> addInstance intInst False n iname

@@ -99,7 +102,7 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

99102 let pnames = nub $ map pname (concat (nub wparams)) ++

100103 concatMap (namesIn [] ist) ps

101104 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

102− undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances

105+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

103106 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

104107 let all_meths = map (nsroot . fst) (class_methods ci)

105108 let mtys = map (\ (n, (op, t)) ->

@@ -112,7 +115,7 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

112115 (class_methods ci)

113116 logElab 3 (show (mtys, ips))

114117 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

115− let ds_defs = insertDefaults i iname (class_defaults ci) ns ds

118+ let ds_defs = insertDefaults ist iname (class_defaults ci) ns ds

116119 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

117120 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

118121 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

@@ -138,10 +141,10 @@ elabInstance info syn doc argDocs what fc cs acc n nfc ps t expn ds = do

138141 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

139142 (map (pexp . mkMethApp) mtys)

140143

141− logElab 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

144+ logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ show lhs ++ " " ++ show headVars

142145 logElab 5 $ "Instance RHS " ++ show rhs

143146

144− let idecls = [PClauses fc [Dictionary] iname

147+ let idecls = [PClauses fc totopts iname

145148 [PClause fc iname lhs [] rhs wb]]

146149 logElab 1 (show idecls)

147150 push_estack iname True