e89453f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow type labels on sigma bindings

commite89453fc7bcdfa0f995aa056b9486c538745841a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 12:42 (15 years ago) parent1c49219

3 files changed+37−28

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+20−18 src/Idris/ElabDecls.hs+5−5 src/Idris/Parser.hs+12−5

src/Idris/AbsSyntax.hs+20−18

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

286286 | PResolveTC FC

287287 | PEq FC PTerm PTerm

288288 | PPair FC PTerm PTerm

289− | PDPair FC PTerm PTerm

289+ | PDPair FC PTerm PTerm PTerm

290290 | PHidden PTerm -- irrelevant or hidden pattern

291291 | PSet

292292 | PConstant Const

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

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

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

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

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

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

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

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

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

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

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

493493 se p PSet = "Set"

494494 se p (PConstant c) = show c

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

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

519519 ni env (PHidden tm) = ni env tm

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

521521 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

523523 ni env _ = []

524524

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

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

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

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

537537 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

539539 ni env (PHidden tm) = ni env tm

540540 ni env _ = []

541541

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

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

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

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

622622 en (PHidden t) = PHidden (en t)

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

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

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

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

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

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

694694 pri (PConstant _) = 0

695695 pri Placeholder = 1

696696 pri _ = 3

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

761761 = do (decls, ns) <- get

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

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

765765 = do (decls, ns) <- get

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

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

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

769769 = 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

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

772772 imps top env (PLam n ty sc)

773773 = do imps False env ty

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

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

794794 r' = ai env r in

795795 PPair fc l' r'

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

797− r' = ai env r in

798− PDPair fc l' r'

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

797+ t' = ai env t

798+ r' = ai env r in

799+ PDPair fc l' t' r'

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

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

801802 aiFn ist fc f as'

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

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

923924 mr <- match r r'

924925 return (ml ++ mr)

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

926− mr <- match r r'

927− return (ml ++ mr)

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

927+ mt <- match t t'

928+ mr <- match r r'

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

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

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

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

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

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

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

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

956958 sm (PHidden x) = PHidden (sm x)

957959 sm x = x

958960

src/Idris/ElabDecls.hs+5−5

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

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

524524 pimp (MN 0 "B") Placeholder,

525525 pexp l, pexp r]))

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

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

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

528− [pexp Placeholder,

528+ [pexp t,

529529 pexp (PLam n Placeholder r)]))

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

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

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

532532 pimp (MN 0 "P") Placeholder,

533533 pexp l, pexp r]))

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

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

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

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

536536 pimp (MN 0 "P") Placeholder,

537537 pexp l, pexp r])

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

src/Idris/Parser.hs+12−5

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

383383 (update (dropn n ns) sc)

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

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

387387 update ns (PHidden t) = PHidden (update ns t)

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

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

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

433433modifyConst syn fc x = x

434434

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 "**";

436441 fc <- pfc

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

438− return (op fc l r)

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

439444 where

440445 pairOp = do lchar ','; return PPair

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

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

447+

442448

443449pHSimpleExpr syn

444450 = do lchar '.'

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

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

780786 (map (fmap (expandDo dsl)) args)

781787expandDo 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)

783790expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

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

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