e2807a1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Verified numbers

commite2807a15b4922a8899176ffc0abd37151776d5b8 authorBenjamin Saunders <besaunde@sfu.ca> dateThu 20 Dec 2012, 14:13 (14 years ago) parentb3ba46e

2 files changed+7−6

unifiedsplit

src/Core/CaseTree.hs+2−2

@@ -226,10 +226,10 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

226226 toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

227227 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

228228 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

229− toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

229+ toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

230230 toPat' (Constant B8Type) [] | tc = return $ PCon (UN "Bits8") 7 []

231231 toPat' (Constant B16Type) [] | tc = return $ PCon (UN "Bits16") 8 []

232− toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 [] -- TODO: Verify numbers

232+ toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 []

233233 toPat' (Constant B64Type) [] | tc = return $ PCon (UN "Bits64") 10 []

234234

235235 toPat' (P Bound n _) [] = do ns <- get

src/Core/Evaluate.hs+5−4

@@ -526,10 +526,11 @@ eval_hnf ctxt statics genv tm = ev [] tm where

526526 findConst ChType (ConCase n 3 [] v : xs) = Just v

527527 findConst StrType (ConCase n 4 [] v : xs) = Just v

528528 findConst PtrType (ConCase n 5 [] v : xs) = Just v

529− findConst B8Type (ConCase n 6 [] v : xs) = Just v

530− findConst B16Type (ConCase n 7 [] v : xs) = Just v

531− findConst B32Type (ConCase n 8 [] v : xs) = Just v

532− findConst B64Type (ConCase n 9 [] v : xs) = Just v -- TODO: Verify numbers

529+ findConst BIType (ConCase n 6 [] v : xs) = Just v

530+ findConst B8Type (ConCase n 7 [] v : xs) = Just v

531+ findConst B16Type (ConCase n 8 [] v : xs) = Just v

532+ findConst B32Type (ConCase n 9 [] v : xs) = Just v

533+ findConst B64Type (ConCase n 10 [] v : xs) = Just v

533534 findConst c (_ : xs) = findConst c xs

534535

535536 getValArgs (HApp t env args) = (t, env, args)