@@ -313,6 +313,7 @@ data PTerm = PQuote Raw
313313 | PEq FC PTerm PTerm
314314 | PPair FC PTerm PTerm
315315 | PDPair FC PTerm PTerm PTerm
316+ | PAlternative [PTerm]
316317 | PHidden PTerm -- irrelevant or hidden pattern
317318 | PSet
318319 | PConstant Const
@@ -334,6 +335,7 @@ mapPT f t = f (mpt t) where
334335 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
335336 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
336337 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
338+ mpt (PAlternative as) = PAlternative (map (mapPT f) as)
337339 mpt (PHidden t) = PHidden (mapPT f t)
338340 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
339341 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
@@ -516,6 +518,7 @@ showImp impl tm = se 10 tm where
516518 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
517519 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
518520 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
521+ se p (PAlternative as) = "(" ++ showSep " ||| " (map (se 10) as) ++ ")"
519522 se p PSet = "Set"
520523 se p (PConstant c) = show c
521524 se p (PProof ts) = "proof { " ++ show ts ++ "}"
@@ -547,6 +550,7 @@ allNamesIn tm = nub $ ni [] tm
547550 ni env (PPair _ l r) = ni env l ++ ni env r
548551 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
549552 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
553+ ni env (PAlternative ls) = concatMap (ni env) ls
550554 ni env _ = []
551555
552556namesIn :: IState -> PTerm -> [Name]
@@ -564,6 +568,7 @@ namesIn ist tm = nub $ ni [] tm
564568 ni env (PPair _ l r) = ni env l ++ ni env r
565569 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
566570 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
571+ ni env (PAlternative as) = concatMap (ni env) as
567572 ni env (PHidden tm) = ni env tm
568573 ni env _ = []
569574
@@ -647,6 +652,7 @@ expandParams dec ps ns tm = en tm
647652 en (PEq f l r) = PEq f (en l) (en r)
648653 en (PPair f l r) = PPair f (en l) (en r)
649654 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
655+ en (PAlternative as) = PAlternative (map en as)
650656 en (PHidden t) = PHidden (en t)
651657 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
652658 en (PProof ts) = PProof (map (fmap en) ts)
@@ -719,6 +725,7 @@ getPriority i tm = pri tm
719725 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
720726 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
721727 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
728+ pri (PAlternative as) = maximum (map pri as)
722729 pri (PConstant _) = 0
723730 pri Placeholder = 1
724731 pri _ = 3
@@ -797,6 +804,10 @@ implicitise syn ist tm
797804 = do (decls, ns) <- get
798805 let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
799806 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
807+ imps top env (PAlternative as)
808+ = do (decls, ns) <- get
809+ let isn = concatMap (namesIn ist) as
810+ put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
800811 imps top env (PLam n ty sc)
801812 = do imps False env ty
802813 imps False (n:env) sc
@@ -825,6 +836,8 @@ addImpl ist ptm = ai [] ptm
825836 t' = ai env t
826837 r' = ai env r in
827838 PDPair fc l' t' r'
839+ ai env (PAlternative as) = let as' = map (ai env) as in
840+ PAlternative as'
828841 ai env (PApp fc (PRef _ f) as)
829842 = let as' = map (fmap (ai env)) as in
830843 aiFn ist fc f as'
@@ -955,6 +968,9 @@ matchClause x y = match x y where
955968 mt <- match t t'
956969 mr <- match r r'
957970 return (ml ++ mt ++ mr)
971+ match (PAlternative as) (PAlternative as')
972+ = do ms <- zipWithM match as as'
973+ return (concat ms)
958974 match (PRefl _) (PRefl _) = return []
959975 match (PResolveTC _) (PResolveTC _) = return []
960976 match (PTrue _) (PTrue _) = return []
@@ -983,6 +999,7 @@ substMatch n tm t = sm t where
983999 sm (PEq f x y) = PEq f (sm x) (sm y)
9841000 sm (PPair f x y) = PPair f (sm x) (sm y)
9851001 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1002+ sm (PAlternative as) = PAlternative (map sm as)
9861003 sm (PHidden x) = PHidden (sm x)
9871004 sm x = x
9881005