dcb9ca0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change meaning of alternative syntax (| a , b , ... |)

Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.

commitdcb9ca0f0381425bb1bc8b6a8465e2b88b3b6f89 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 17 Apr 2012, 13:47 (15 years ago) parent923e19a

6 files changed+34−28

compare with master

unifiedsplit

src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+17−17 src/Idris/DSL.hs+2−2 src/Idris/ElabTerm.hs+7−3 src/Idris/IBC.hs+5−3 src/Idris/Parser.hs+2−2

src/Core/CoreParser.hs+1−1

@@ -25,7 +25,7 @@ idrisDef = haskellDef {

2525 "infix", "infixl", "infixr", "prefix",

2626 "where", "with", "forall", "syntax", "proof",

2727 "using", "params", "namespace", "class", "instance",

28− "public", "private", "abstract",

28+ "public", "private", "abstract",

2929 "Int", "Integer", "Float", "Char", "String", "Ptr"]

3030 }

3131

src/Idris/AbsSyntax.hs+17−17

@@ -537,7 +537,7 @@ data PTerm = PQuote Raw

537537 | PEq FC PTerm PTerm

538538 | PPair FC PTerm PTerm

539539 | PDPair FC PTerm PTerm PTerm

540− | PAlternative [PTerm]

540+ | PAlternative Bool [PTerm] -- True if only one may work

541541 | PHidden PTerm -- irrelevant or hidden pattern

542542 | PSet

543543 | PConstant Const

@@ -566,7 +566,7 @@ mapPT f t = f (mpt t) where

566566 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

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

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

569− mpt (PAlternative as) = PAlternative (map (mapPT f) as)

569+ mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)

570570 mpt (PHidden t) = PHidden (mapPT f t)

571571 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

572572 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

@@ -964,7 +964,7 @@ prettyImp impl = prettySe 10

964964 prettySe 10 r <> rparen

965965 else

966966 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen

967− prettySe p (PAlternative as) =

967+ prettySe p (PAlternative a as) =

968968 lparen <> text "|" <> prettyAs <> text "|" <> rparen

969969 where

970970 prettyAs =

@@ -1056,7 +1056,7 @@ showImp impl tm = se 10 tm where

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

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

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

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

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

10601060 se p PSet = "Set"

10611061 se p (PConstant c) = show c

10621062 se p (PProof ts) = "proof { " ++ show ts ++ "}"

@@ -1129,7 +1129,7 @@ instance Sized PTerm where

11291129 size (PEq fc left right) = 1 + size left + size right

11301130 size (PPair fc left right) = 1 + size left + size right

11311131 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1132− size (PAlternative alts) = 1 + size alts

1132+ size (PAlternative a alts) = 1 + size alts

11331133 size (PHidden hidden) = size hidden

11341134 size PSet = 1

11351135 size (PConstant const) = 1 + size const

@@ -1157,7 +1157,7 @@ allNamesIn tm = nub $ ni [] tm

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

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

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

1160− ni env (PAlternative ls) = concatMap (ni env) ls

1160+ ni env (PAlternative a ls) = concatMap (ni env) ls

11611161 ni env _ = []

11621162

11631163namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

@@ -1177,7 +1177,7 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

1180− ni env (PAlternative as) = concatMap (ni env) as

1180+ ni env (PAlternative a as) = concatMap (ni env) as

11811181 ni env (PHidden tm) = ni env tm

11821182 ni env _ = []

11831183

@@ -1288,7 +1288,7 @@ expandParams dec ps ns tm = en tm

12881288 en (PTyped l r) = PTyped (en l) (en r)

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

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

1291− en (PAlternative as) = PAlternative (map en as)

1291+ en (PAlternative a as) = PAlternative a (map en as)

12921292 en (PHidden t) = PHidden (en t)

12931293 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

12941294 en (PProof ts) = PProof (map (fmap en) ts)

@@ -1364,7 +1364,7 @@ getPriority i tm = pri tm

13641364 pri (PTyped l r) = pri l

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

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

1367− pri (PAlternative as) = maximum (map pri as)

1367+ pri (PAlternative a as) = maximum (map pri as)

13681368 pri (PConstant _) = 0

13691369 pri Placeholder = 1

13701370 pri _ = 3

@@ -1480,7 +1480,7 @@ implicitise syn ist tm

14801480 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++

14811481 namesIn uvars ist r

14821482 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

1483− imps top env (PAlternative as)

1483+ imps top env (PAlternative a as)

14841484 = do (decls, ns) <- get

14851485 let isn = concatMap (namesIn uvars ist) as

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

@@ -1529,8 +1529,8 @@ addImpl' inpat env ist ptm = ai env ptm

15291529 t' = ai env t

15301530 r' = ai env r in

15311531 PDPair fc l' t' r'

1532− ai env (PAlternative as) = let as' = map (ai env) as in

1533− PAlternative as'

1532+ ai env (PAlternative a as) = let as' = map (ai env) as in

1533+ PAlternative a as'

15341534 ai env (PApp fc (PRef _ f) as)

15351535 | not (f `elem` env)

15361536 = let as' = map (fmap (ai env)) as in

@@ -1582,7 +1582,7 @@ aiFn inpat ist fc f as

15821582 then Right $ PApp fc (PRef fc f) as

15831583 else Right $ mkPApp fc (length as) (PRef fc f) as

15841584 alts -> Right $

1585− PAlternative $

1585+ PAlternative True $

15861586 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

15871587 (insertImpl ns as)) alts

15881588 where

@@ -1727,10 +1727,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

17271727 mt <- match' t t'

17281728 mr <- match' r r'

17291729 return (ml ++ mt ++ mr)

1730− match (PAlternative as) (PAlternative as')

1730+ match (PAlternative a as) (PAlternative a' as')

17311731 = do ms <- zipWithM match' as as'

17321732 return (concat ms)

1733− match a@(PAlternative as) b

1733+ match a@(PAlternative _ as) b

17341734 = do let ms = zipWith match' as (repeat b)

17351735 case (rights (map toEither ms)) of

17361736 (x: _) -> return x

@@ -1786,7 +1786,7 @@ substMatch n tm t = sm t where

17861786 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

1789− sm (PAlternative as) = PAlternative (map sm as)

1789+ sm (PAlternative a as) = PAlternative a (map sm as)

17901790 sm (PHidden x) = PHidden (sm x)

17911791 sm x = x

17921792

@@ -1801,7 +1801,7 @@ shadow n n' t = sm t where

18011801 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

1804− sm (PAlternative as) = PAlternative (map sm as)

1804+ sm (PAlternative a as) = PAlternative a (map sm as)

18051805 sm (PHidden x) = PHidden (sm x)

18061806 sm x = x

18071807

src/Idris/DSL.hs+2−2

@@ -34,7 +34,7 @@ expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

3434expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

3535expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

3636 (expandDo dsl r)

37−expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)

37+expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

3838expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

3939expandDo dsl (PReturn fc) = dsl_return dsl

4040expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

@@ -81,7 +81,7 @@ var dsl n t i = v' i t where

8181 v' i (PEq f l r) = PEq f (v' i l) (v' i r)

8282 v' i (PPair f l r) = PPair f (v' i l) (v' i r)

8383 v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)

84− v' i (PAlternative as) = PAlternative $ map (v' i) as

84+ v' i (PAlternative a as) = PAlternative a $ map (v' i) as

8585 v' i (PHidden t) = PHidden (v' i t)

8686 v' i (PIdiom f t) = PIdiom f (v' i t)

8787 v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)

src/Idris/ElabTerm.hs+7−3

@@ -135,12 +135,16 @@ elab ist info pattern tcgen fn tm

135135 [pimp (MN 0 "a") t,

136136 pimp (MN 0 "P") Placeholder,

137137 pexp l, pexp r])

138− elab' ina (PAlternative as)

138+ elab' ina (PAlternative True as)

139139 = let as' = pruneAlt as in

140140 try (tryAll (zip (map (elab' ina) as') (map showHd as')))

141141 (tryAll (zip (map (elab' ina) as) (map showHd as)))

142142 where showHd (PApp _ h _) = show h

143143 showHd x = show x

144+ elab' ina (PAlternative False as)

145+ = trySeq as

146+ where trySeq [] = fail "All alternatives fail to elaborate"

147+ trySeq (x : xs) = try (elab' ina x) (trySeq xs)

144148 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

145149 = do ctxt <- get_context

146150 let iscon = isConName Nothing n ctxt

@@ -335,12 +339,12 @@ pruneAlt xs = map prune xs

335339 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

336340 prune t = t

337341

338− choose f (PAlternative as)

342+ choose f (PAlternative a as)

339343 = let as' = fmap (choose f) as

340344 fs = filter (headIs f) as' in

341345 case fs of

342346 [a] -> a

343− _ -> PAlternative as'

347+ _ -> PAlternative a as'

344348 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

345349 choose f t = t

346350

src/Idris/IBC.hs+5−3

@@ -849,8 +849,9 @@ instance Binary PTerm where

849849 put x2

850850 put x3

851851 put x4

852− PAlternative x1 -> do putWord8 13

853− put x1

852+ PAlternative x1 x2 -> do putWord8 13

853+ put x1

854+ put x2

854855 PHidden x1 -> do putWord8 14

855856 put x1

856857 PSet -> putWord8 15

@@ -918,7 +919,8 @@ instance Binary PTerm where

918919 x4 <- get

919920 return (PDPair x1 x2 x3 x4)

920921 13 -> do x1 <- get

921− return (PAlternative x1)

922+ x2 <- get

923+ return (PAlternative x1 x2)

922924 14 -> do x1 <- get

923925 return (PHidden x1)

924926 15 -> return PSet

src/Idris/Parser.hs+2−2

@@ -580,7 +580,7 @@ pExt syn (Rule ssym ptm _)

580580 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

581581 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

582582 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

583− update ns (PAlternative as) = PAlternative (map (update ns) as)

583+ update ns (PAlternative a as) = PAlternative a (map (update ns) as)

584584 update ns (PHidden t) = PHidden (update ns t)

585585 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

586586 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

@@ -735,7 +735,7 @@ pPair syn = try (do l <- pExpr syn

735735pAlt syn = do symbol "(|";

736736 alts <- sepBy1 (pExpr' syn) (lchar ',')

737737 symbol "|)"

738− return (PAlternative alts)

738+ return (PAlternative False alts)

739739

740740pHSimpleExpr syn

741741 = do lchar '.'