dcb9ca0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

dcb9ca0Edwin Brady15 years ago

src/Core/CoreParser.hs+1−1

compare with master

unifiedsplit

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

25 "infix", "infixl", "infixr", "prefix",

26 "where", "with", "forall", "syntax", "proof",

27 "using", "params", "namespace", "class", "instance",

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

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

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

30 }

src/Idris/AbsSyntax.hs+17−17

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

537 | PEq FC PTerm PTerm

538 | PPair FC PTerm PTerm

539 | PDPair FC PTerm PTerm PTerm

540− | PAlternative [PTerm]

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

541 | PHidden PTerm -- irrelevant or hidden pattern

542 | PSet

543 | PConstant Const

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

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

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

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

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

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

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

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

964 prettySe 10 r <> rparen

965 else

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

967− prettySe p (PAlternative as) =

967+ prettySe p (PAlternative a as) =

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

969 where

970 prettyAs =

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

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

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

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

1060 se p PSet = "Set"

1061 se p (PConstant c) = show c

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

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

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

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

1131 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

1133 size (PHidden hidden) = size hidden

1134 size PSet = 1

1135 size (PConstant const) = 1 + size const

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

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

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

1159 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

1161 ni env _ = []

1162

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

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

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

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

1179 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

1181 ni env (PHidden tm) = ni env tm

1182 ni env _ = []

1183

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

1288 en (PTyped l r) = PTyped (en l) (en r)

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

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

1292 en (PHidden t) = PHidden (en t)

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

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

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

1364 pri (PTyped l r) = pri l

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

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

1368 pri (PConstant _) = 0

1369 pri Placeholder = 1

1370 pri _ = 3

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

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

1481 namesIn uvars ist r

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

1483− imps top env (PAlternative as)

1483+ imps top env (PAlternative a as)

1484 = do (decls, ns) <- get

1485 let isn = concatMap (namesIn uvars ist) as

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

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

1529 t' = ai env t

1530 r' = ai env r in

1531 PDPair fc l' t' r'

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

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

1533− PAlternative as'

1533+ PAlternative a as'

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

1535 | not (f `elem` env)

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

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

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

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

1584 alts -> Right $

1585− PAlternative $

1585+ PAlternative True $

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

1587 (insertImpl ns as)) alts

1588 where

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

1727 mt <- match' t t'

1728 mr <- match' r r'

1729 return (ml ++ mt ++ mr)

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

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

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

1732 return (concat ms)

1733− match a@(PAlternative as) b

1733+ match a@(PAlternative _ as) b

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

1735 case (rights (map toEither ms)) of

1736 (x: _) -> return x

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

1786 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

1790 sm (PHidden x) = PHidden (sm x)

1791 sm x = x

1792

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

1801 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

1805 sm (PHidden x) = PHidden (sm x)

1806 sm x = x

1807

src/Idris/DSL.hs+2−2

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

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

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

36 (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)

38expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

39expandDo dsl (PReturn fc) = dsl_return dsl

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

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

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

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

83 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

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

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

87 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

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

136 pimp (MN 0 "P") Placeholder,

137 pexp l, pexp r])

138− elab' ina (PAlternative as)

138+ elab' ina (PAlternative True as)

139 = let as' = pruneAlt as in

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

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

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

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

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

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

145 = do ctxt <- get_context

149 = do ctxt <- get_context

146 let iscon = isConName Nothing n ctxt

150 let iscon = isConName Nothing n ctxt

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

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

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

336 prune t = t

340 prune t = t

337

341

338− choose f (PAlternative as)

342+ choose f (PAlternative a as)

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

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

340 fs = filter (headIs f) as' in

344 fs = filter (headIs f) as' in

341 case fs of

345 case fs of

342 [a] -> a

346 [a] -> a

343− _ -> PAlternative as'

347+ _ -> PAlternative a as'

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

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

345 choose f t = t

349 choose f t = t

346

350

src/Idris/IBC.hs+5−3

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

849 put x2

850 put x3

851 put x4

852− PAlternative x1 -> do putWord8 13

852+ PAlternative x1 x2 -> do putWord8 13

853− put x1

853+ put x1

854+ put x2

854 PHidden x1 -> do putWord8 14

855 PHidden x1 -> do putWord8 14

855 put x1

856 put x1

856 PSet -> putWord8 15

857 PSet -> putWord8 15

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

918 x4 <- get

919 x4 <- get

919 return (PDPair x1 x2 x3 x4)

920 return (PDPair x1 x2 x3 x4)

920 13 -> do x1 <- get

921 13 -> do x1 <- get

922+ x2 <- get

921− return (PAlternative x1)

923+ return (PAlternative x1 x2)

922 14 -> do x1 <- get

924 14 -> do x1 <- get

923 return (PHidden x1)

925 return (PHidden x1)

924 15 -> return PSet

926 15 -> return PSet

src/Idris/Parser.hs+2−2

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

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

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

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

584 update ns (PHidden t) = PHidden (update ns t)

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

586 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

735pAlt syn = do symbol "(|";

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

737 symbol "|)"

738− return (PAlternative alts)

738+ return (PAlternative False alts)

739

740pHSimpleExpr syn

741 = do lchar '.'