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

git.iko.soy/Idris-dev

Some minor fiddling

commit247b20c525a39ea0ee33536d82dff119b37a754a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 19 Jan 2012, 14:49 (15 years ago) parente39254c

7 files changed+61−23

compare with master

unifiedsplit

lib/prelude.idr+5−5 lib/prelude/nat.idr+17−14 src/Idris/AbsSyntax.hs+19 src/Idris/Compiler.hs+1−1 src/Idris/ElabTerm.hs+9 src/Idris/Parser.hs+3 tutorial/typesfuns.tex+7−3

lib/prelude.idr+5−5

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

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

5050

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

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

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

54− show' [] = ""

55− show' [x] = show x

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

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

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

54+ show' acc [] = acc

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

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

5757

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

5959 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

7474plus_assoc O m p = refl

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

7676

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−

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

9278multnO O = refl

9379multnO (S k) = multnO k

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

122108 trivial;

123109}

124110

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

434434 | PLam Name PTerm PTerm

435435 | PPi Plicity Name PTerm PTerm

436436 | PLet Name PTerm PTerm PTerm

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

437438 | PApp FC PTerm [PArg]

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

439440 | PTrue FC

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

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

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

471472 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)

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

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

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

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

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

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

716718 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 ++ ")"

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

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

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

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

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

752755 ni env (PHidden tm) = ni env tm

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

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

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

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

756760 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

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

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

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

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

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

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

775780 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

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

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

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

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

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

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

886892 en (PAlternative as) = PAlternative (map en as)

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

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

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

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

965+ pri (PTyped l r) = pri l

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

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

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

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

10281035 = do (decls, ns) <- get

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

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

1038+ imps top env (PTyped l r)

1039+ = imps top env l

10311040 imps top env (PPair _ l r)

10321041 = do (decls, ns) <- get

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

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

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

10681077 r' = ai env r in

10691078 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'

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

10711083 r' = ai env r in

10721084 PPair fc l' r'

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

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

12371249 mr <- match' r r'

12381250 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)

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

12401257 mr <- match' r r'

12411258 return (ml ++ mr)

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

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

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

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

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

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

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

13041322 sm (PAlternative as) = PAlternative (map sm as)

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

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

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

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

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

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

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

13181337 sm (PAlternative as) = PAlternative (map sm as)

src/Idris/Compiler.hs+1−1

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

3434 Nothing ->

3535 do m <- epicMain tm

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

37− liftIO $ compileObjWith [Debug]

37+ liftIO $ compileObjWith []

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

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

4040 where checkMVs = do i <- get

src/Idris/ElabTerm.hs+9

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

182182 elabE True val

183183 elabE True sc

184184 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

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

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

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

src/Idris/Parser.hs+3

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

651651bracketed syn =

652652 try (pPair syn)

653653 <|> 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))

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

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

656659 (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

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

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

330330

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

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

333−is defined in the prelude:

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+

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

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

334338

335339\begin{SaveVerbatim}{vlookup}

336340