e89453f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow type labels on sigma bindings

e89453fEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+20−18

compare with master

unifiedsplit

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

286 | PResolveTC FC

287 | PEq FC PTerm PTerm

288 | PPair FC PTerm PTerm

289− | PDPair FC PTerm PTerm

289+ | PDPair FC PTerm PTerm PTerm

290 | PHidden PTerm -- irrelevant or hidden pattern

291 | PSet

292 | PConstant Const

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

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

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

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

310− mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)

310+ mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

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

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

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

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

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

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

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

492− se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

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

493 se p PSet = "Set"

494 se p (PConstant c) = show c

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

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

519 ni env (PHidden tm) = ni env tm

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

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

522− ni env (PDPair _ l r) = ni env l ++ ni env r

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

523 ni env _ = []

524

525namesIn :: IState -> PTerm -> [Name]

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

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

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

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

538− ni env (PDPair _ l r) = ni env l ++ ni env r

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

539 ni env (PHidden tm) = ni env tm

540 ni env _ = []

541

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

618 en (PLet n ty v s) = PLet n (en ty) (en v) (en s)

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

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

621− en (PDPair f l r) = PDPair f (en l) (en r)

621+ en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

622 en (PHidden t) = PHidden (en t)

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

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

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

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

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

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

693− pri (PDPair _ l r) = max 1 (max (pri l) (pri r))

693+ pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

694 pri (PConstant _) = 0

695 pri Placeholder = 1

696 pri _ = 3

@@ -761,13 +761,13 @@ implicitise syn ist tm

761 = do (decls, ns) <- get

762 let isn = namesIn ist l ++ namesIn ist r

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

764− imps top env (PDPair _ (PRef _ n) r)

764+ imps top env (PDPair _ (PRef _ n) t r)

765 = do (decls, ns) <- get

766− let isn = nub (namesIn ist r) \\ [n]

766+ let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]

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

768− imps top env (PDPair _ l r)

768+ imps top env (PDPair _ l t r)

769 = do (decls, ns) <- get

770− let isn = namesIn ist l ++ namesIn ist r

770+ let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r

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

772 imps top env (PLam n ty sc)

773 = do imps False env ty

@@ -793,9 +793,10 @@ addImpl ist ptm = ai [] ptm

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

794 r' = ai env r in

795 PPair fc l' r'

796− ai env (PDPair fc l r) = let l' = ai env l

796+ ai env (PDPair fc l t r) = let l' = ai env l

797+ t' = ai env t

797− r' = ai env r in

798+ r' = ai env r in

798− PDPair fc l' r'

799+ PDPair fc l' t' r'

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

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

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

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

801 aiFn ist fc f as'

802 aiFn ist fc f as'

@@ -922,9 +923,10 @@ matchClause x y = match x y where

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

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

923 mr <- match r r'

924 mr <- match r r'

924 return (ml ++ mr)

925 return (ml ++ mr)

925− match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'

926+ match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match l l'

927+ mt <- match t t'

926− mr <- match r r'

928+ mr <- match r r'

927− return (ml ++ mr)

929+ return (ml ++ mt ++ mr)

928 match (PRefl _) (PRefl _) = return []

930 match (PRefl _) (PRefl _) = return []

929 match (PResolveTC _) (PResolveTC _) = return []

931 match (PResolveTC _) (PResolveTC _) = return []

930 match (PTrue _) (PTrue _) = return []

932 match (PTrue _) (PTrue _) = return []

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

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

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

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

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

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

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

955− sm (PDPair f x y) = PDPair f (sm x) (sm y)

957+ sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

956 sm (PHidden x) = PHidden (sm x)

958 sm (PHidden x) = PHidden (sm x)

957 sm x = x

959 sm x = x

958

960

src/Idris/ElabDecls.hs+5−5

@@ -523,16 +523,16 @@ elab ist info pattern tm

523 [pimp (MN 0 "A") Placeholder,

524 pimp (MN 0 "B") Placeholder,

525 pexp l, pexp r]))

526− elab' (PDPair fc l@(PRef _ n) r)

526+ elab' (PDPair fc l@(PRef _ n) t r)

527 = try (elab' (PApp fc (PRef fc sigmaTy)

528− [pexp Placeholder,

528+ [pexp t,

529 pexp (PLam n Placeholder r)]))

530 (elab' (PApp fc (PRef fc existsCon)

531− [pimp (MN 0 "a") Placeholder,

531+ [pimp (MN 0 "a") t,

532 pimp (MN 0 "P") Placeholder,

533 pexp l, pexp r]))

534− elab' (PDPair fc l r) = elab' (PApp fc (PRef fc existsCon)

534+ elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)

535− [pimp (MN 0 "a") Placeholder,

535+ [pimp (MN 0 "a") t,

536 pimp (MN 0 "P") Placeholder,

537 pexp l, pexp r])

538 elab' (PRef fc n) | pattern && not (inparamBlock n)

src/Idris/Parser.hs+12−5

@@ -383,7 +383,7 @@ pExt syn (Rule (s:ssym) ptm _)

383 (update (dropn n ns) sc)

384 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

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

386− update ns (PDPair fc l r) = PDPair fc (update ns l) (update ns r)

386+ update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

387 update ns (PHidden t) = PHidden (update ns t)

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

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

@@ -432,13 +432,19 @@ modifyConst syn fc (PConstant (I x))

432 = PApp fc (PRef fc (UN ["fromInteger"])) [pexp (PConstant (I x))]

433modifyConst syn fc x = x

434

435−pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp

435+pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp

436+ fc <- pfc

437+ r <- pExpr syn; lchar ')';

438+ return (op fc l r))

439+ <|> do lchar '('; ln <- pName; lchar ':'; lty <- pExpr syn;

440+ reservedOp "**";

436 fc <- pfc

441 fc <- pfc

437 r <- pExpr syn; lchar ')';

442 r <- pExpr syn; lchar ')';

438− return (op fc l r)

443+ return (PDPair fc (PRef fc ln) lty r)

439 where

444 where

440 pairOp = do lchar ','; return PPair

445 pairOp = do lchar ','; return PPair

441− <|> do reservedOp "**"; return PDPair

446+ <|> do reservedOp "**"; return (\f x y -> PDPair f x Placeholder y)

447+

442

448

443pHSimpleExpr syn

449pHSimpleExpr syn

444 = do lchar '.'

450 = do lchar '.'

@@ -779,7 +785,8 @@ expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

779expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

785expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

780 (map (fmap (expandDo dsl)) args)

786 (map (fmap (expandDo dsl)) args)

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

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

782−expandDo dsl (PDPair fc l r) = PDPair fc (expandDo dsl l) (expandDo dsl r)

788+expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

789+ (expandDo dsl r)

783expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

790expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

784expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

791expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

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

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