247b20c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some minor fiddling

247b20cEdwin Brady15 years ago

lib/prelude.idr+5−5

compare with master

unifiedsplit

@@ -49,11 +49,11 @@ instance (Show a, Show b) => Show (a, b) where

49 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

51instance Show a => Show (List a) where

52− show xs = "[" ++ show' xs ++ "]" where

52+ show xs = "[" ++ show' "" xs ++ "]" where

53− show' : Show a => List a -> String

53+ show' : Show a => String -> List a -> String

54− show' [] = ""

54+ show' acc [] = acc

55− show' [x] = show x

55+ show' acc [x] = acc ++ show x

56− show' (x :: xs) = show x ++ ", " ++ show' xs

56+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

58instance Show a => Show (Vect a n) where

59 show xs = "[" ++ show' xs ++ "]" where

lib/prelude/nat.idr+17−14

@@ -74,20 +74,6 @@ plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p

74plus_assoc O m p = refl

75plus_assoc (S k) m p = let ih = plus_assoc k m p in eqRespS ih

77−data Cmp : Nat -> Nat -> Set where

78− cmpLT : (y : Nat) -> Cmp x (x + S y)

79− cmpEQ : Cmp x x

80− cmpGT : (x : Nat) -> Cmp (y + S x) y

81−

82−cmp : (n, m : Nat) -> Cmp n m

83−cmp O O = cmpEQ

84−cmp (S n) O = cmpGT _

85−cmp O (S n) = cmpLT _

86−cmp (S x) (S y) with (cmp x y)

87− cmp (S x) (S x) | cmpEQ = cmpEQ

88− cmp (S (y + S x)) (S y) | cmpGT _ = cmpGT _

89− cmp (S x) (S (x + S y)) | cmpLT _ = cmpLT _

90−

91multnO : (n : Nat) -> (n * O) = O

77multnO : (n : Nat) -> (n * O) = O

92multnO O = refl

78multnO O = refl

93multnO (S k) = multnO k

79multnO (S k) = multnO k

@@ -122,3 +108,20 @@ multnSmSk = proof {

122 trivial;

108 trivial;

123}

109}

124

110

111+data Cmp : Nat -> Nat -> Set where

112+ cmpLT : (y : Nat) -> Cmp x (x + S y)

113+ cmpEQ : Cmp x x

114+ cmpGT : (x : Nat) -> Cmp (y + S x) y

115+

116+cmp : (n, m : Nat) -> Cmp n m

117+cmp O O = cmpEQ

118+cmp (S n) O = cmpGT _

119+cmp O (S n) = cmpLT _

120+cmp (S x) (S y) with (cmp x y)

121+ cmp (S x) (S x) | cmpEQ = cmpEQ

122+ cmp (S (y + S x)) (S y) | cmpGT _ = cmpGT _

123+ cmp (S x) (S (x + S y)) | cmpLT _ = cmpLT _

124+

125+ data LE : Nat -> Nat -> Set where

126+ leO : LE O n

127+ leS : LE x y -> LE (S x) (S y)

src/Idris/AbsSyntax.hs+19

@@ -434,6 +434,7 @@ data PTerm = PQuote Raw

434 | PLam Name PTerm PTerm

435 | PPi Plicity Name PTerm PTerm

436 | PLet Name PTerm PTerm PTerm

437+ | PTyped PTerm PTerm -- term with explicit type

437 | PApp FC PTerm [PArg]

438 | PApp FC PTerm [PArg]

438 | PCase FC PTerm [(PTerm, PTerm)]

439 | PCase FC PTerm [(PTerm, PTerm)]

439 | PTrue FC

440 | PTrue FC

@@ -469,6 +470,7 @@ mapPT f t = f (mpt t) where

469 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

470 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

470 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

471 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

471 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

472 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

473+ mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

472 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

474 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

473 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

475 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

474 mpt (PAlternative as) = PAlternative (map (mapPT f) as)

476 mpt (PAlternative as) = PAlternative (map (mapPT f) as)

@@ -714,6 +716,7 @@ showImp impl tm = se 10 tm where

714 se p (PTrue _) = "()"

716 se p (PTrue _) = "()"

715 se p (PFalse _) = "_|_"

717 se p (PFalse _) = "_|_"

716 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

718 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

719+ se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"

717 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

720 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

718 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

721 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

719 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

722 se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

@@ -751,6 +754,7 @@ allNamesIn tm = nub $ ni [] tm

751 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

754 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

752 ni env (PHidden tm) = ni env tm

755 ni env (PHidden tm) = ni env tm

753 ni env (PEq _ l r) = ni env l ++ ni env r

756 ni env (PEq _ l r) = ni env l ++ ni env r

757+ ni env (PTyped l r) = ni env l ++ ni env r

754 ni env (PPair _ l r) = ni env l ++ ni env r

758 ni env (PPair _ l r) = ni env l ++ ni env r

755 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

759 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

756 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

760 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

@@ -770,6 +774,7 @@ namesIn uvars ist tm = nub $ ni [] tm

770 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

774 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

771 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

775 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

772 ni env (PEq _ l r) = ni env l ++ ni env r

776 ni env (PEq _ l r) = ni env l ++ ni env r

777+ ni env (PTyped l r) = ni env l ++ ni env r

773 ni env (PPair _ l r) = ni env l ++ ni env r

778 ni env (PPair _ l r) = ni env l ++ ni env r

774 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

779 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

775 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

780 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

@@ -881,6 +886,7 @@ expandParams dec ps ns tm = en tm

881 PLet n' (en ty) (en v) (en (shadow n n' s))

886 PLet n' (en ty) (en v) (en (shadow n n' s))

882 | otherwise = PLet n (en ty) (en v) (en s)

887 | otherwise = PLet n (en ty) (en v) (en s)

883 en (PEq f l r) = PEq f (en l) (en r)

888 en (PEq f l r) = PEq f (en l) (en r)

889+ en (PTyped l r) = PTyped (en l) (en r)

884 en (PPair f l r) = PPair f (en l) (en r)

890 en (PPair f l r) = PPair f (en l) (en r)

885 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

891 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

886 en (PAlternative as) = PAlternative (map en as)

892 en (PAlternative as) = PAlternative (map en as)

@@ -956,6 +962,7 @@ getPriority i tm = pri tm

956 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

962 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

957 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

963 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

958 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

964 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

965+ pri (PTyped l r) = pri l

959 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

966 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

960 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

967 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

961 pri (PAlternative as) = maximum (map pri as)

968 pri (PAlternative as) = maximum (map pri as)

@@ -1028,6 +1035,8 @@ implicitise syn ist tm

1028 = do (decls, ns) <- get

1035 = do (decls, ns) <- get

1029 let isn = namesIn uvars ist l ++ namesIn uvars ist r

1036 let isn = namesIn uvars ist l ++ namesIn uvars ist r

1030 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1037 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1038+ imps top env (PTyped l r)

1039+ = imps top env l

1031 imps top env (PPair _ l r)

1040 imps top env (PPair _ l r)

1032 = do (decls, ns) <- get

1041 = do (decls, ns) <- get

1033 let isn = namesIn uvars ist l ++ namesIn uvars ist r

1042 let isn = namesIn uvars ist l ++ namesIn uvars ist r

@@ -1067,6 +1076,9 @@ addImpl ist ptm = ai [] ptm

1067 ai env (PEq fc l r) = let l' = ai env l

1076 ai env (PEq fc l r) = let l' = ai env l

1068 r' = ai env r in

1077 r' = ai env r in

1069 PEq fc l' r'

1078 PEq fc l' r'

1079+ ai env (PTyped l r) = let l' = ai env l

1080+ r' = ai env r in

1081+ PTyped l' r'

1070 ai env (PPair fc l r) = let l' = ai env l

1082 ai env (PPair fc l r) = let l' = ai env l

1071 r' = ai env r in

1083 r' = ai env r in

1072 PPair fc l' r'

1084 PPair fc l' r'

@@ -1236,6 +1248,11 @@ matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

1236 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1248 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1237 mr <- match' r r'

1249 mr <- match' r r'

1238 return (ml ++ mr)

1250 return (ml ++ mr)

1251+ match (PTyped l r) x = match l x

1252+ match x (PTyped l r) = match x l

1253+ match (PTyped l r) (PTyped l' r') = do ml <- match l l'

1254+ mr <- match r r'

1255+ return (ml ++ mr)

1239 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'

1256 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'

1240 mr <- match' r r'

1257 mr <- match' r r'

1241 return (ml ++ mr)

1258 return (ml ++ mr)

@@ -1299,6 +1316,7 @@ substMatch n tm t = sm t where

1299 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1316 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1300 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1317 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1301 sm (PEq f x y) = PEq f (sm x) (sm y)

1318 sm (PEq f x y) = PEq f (sm x) (sm y)

1319+ sm (PTyped x y) = PTyped (sm x) (sm y)

1302 sm (PPair f x y) = PPair f (sm x) (sm y)

1320 sm (PPair f x y) = PPair f (sm x) (sm y)

1303 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1321 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1304 sm (PAlternative as) = PAlternative (map sm as)

1322 sm (PAlternative as) = PAlternative (map sm as)

@@ -1313,6 +1331,7 @@ shadow n n' t = sm t where

1313 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1331 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1314 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1332 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1315 sm (PEq f x y) = PEq f (sm x) (sm y)

1333 sm (PEq f x y) = PEq f (sm x) (sm y)

1334+ sm (PTyped x y) = PTyped (sm x) (sm y)

1316 sm (PPair f x y) = PPair f (sm x) (sm y)

1335 sm (PPair f x y) = PPair f (sm x) (sm y)

1317 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1336 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1318 sm (PAlternative as) = PAlternative (map sm as)

1337 sm (PAlternative as) = PAlternative (map sm as)

src/Idris/Compiler.hs+1−1

@@ -34,7 +34,7 @@ compile f tm

34 Nothing ->

35 do m <- epicMain tm

36 let mainval = EpicFn (name "main") m

37− liftIO $ compileObjWith [Debug]

37+ liftIO $ compileObjWith []

38 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")

39 liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

40 where checkMVs = do i <- get

src/Idris/ElabTerm.hs+9

@@ -182,6 +182,15 @@ elab ist info pattern tcgen fn tm

182 elabE True val

183 elabE True sc

184 solve

185+-- elab' ina (PTyped val ty)

186+-- = do tyn <- unique_hole (MN 0 "castty")

187+-- claim tyn RSet

188+-- valn <- unique_hole (MN 0 "castval")

189+-- claim valn (Var tyn)

190+-- focus tyn

191+-- elabE True ty

192+-- focus valn

193+-- elabE True val

185 elab' ina (PApp fc (PRef _ f) args')

194 elab' ina (PApp fc (PRef _ f) args')

186 = do let args = {- case lookupCtxt f (inblock info) of

195 = do let args = {- case lookupCtxt f (inblock info) of

187 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

196 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

src/Idris/Parser.hs+3

@@ -651,6 +651,9 @@ pSimpleExpr syn =

651bracketed syn =

652 try (pPair syn)

653 <|> try (do e <- pExpr syn; lchar ')'; return e)

654+-- <|> try (do reserved "typed"

655+-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'

656+-- return (PTyped e t))

654 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'

657 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'

655 return $ PLam (MN 0 "x") Placeholder

658 return $ PLam (MN 0 "x") Placeholder

656 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),

659 (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),

tutorial/typesfuns.tex+7−3

@@ -328,9 +328,13 @@ data Fin : Nat -> Set where

328represents the number of elements in the set. Obviously we can't construct an

329element of an empty set, so neither constructor targets \texttt{Fin O}.

330

331−A useful application of the \tTC{Fin} family is to represent numbers with

331+A useful application of the \tTC{Fin} family is to represent bounded

332+natural numbers. Since the first \tTC{n} natural numbers form a finite

333+set of \tTC{n} elements, we can treat \tTC{Fin n} as the set of natural

334+numbers bounded by \tTC{n}.

335+

332−guaranteed bounds. For example, the following function which looks up an element in a \tTC{Vect}

336+For example, the following function which looks up an element in a \tTC{Vect},

333−is defined in the prelude:

337+by a bounded index given as a \tTC{Fin n}, is defined in the prelude:

334

338

335\begin{SaveVerbatim}{vlookup}

339\begin{SaveVerbatim}{vlookup}

336

340