git.iko.soy/Idris-dev
on master help sign in
Fixes some string comparison that made sigma show incorrectly.

Showing types of first component of sigma type.

commit2f6e7362604f2d18ebf4e4a61649cee722eadac9 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSat 9 May 2015, 15:25 (11 years ago) parent23b36da
4 files changed+10−10
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Apropos.hs+1−1 src/Idris/Delaborate.hs+4−4 src/Idris/Elab/Term.hs+2−2
src/Idris/AbsSyntaxTree.hs+3−3
@@ -1346,7 +1346,7 @@ modDocName = sMN 0 "ModuleDocs"
13461346
13471347-- Defined in builtins.idr
13481348sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1349−existsCon = sNS (sUN "MkSigma") ["Builtins"]
1349+sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
13501350
13511351piBind :: [(Name, PTerm)] -> PTerm -> PTerm
13521352piBind = piBindp expl
@@ -1597,10 +1597,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
15971597 annotated rparen
15981598 where annotated = case pun of
15991599 IsType -> annName sigmaTy
1600− IsTerm -> annName existsCon
1600+ IsTerm -> annName sigmaCon
16011601 TypeOrTerm -> id
16021602 (left, addBinding) = case (l, pun) of
1603− (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1603+ (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe startPrec bnd t, ((n, False) :))
16041604 _ -> (prettySe startPrec bnd l, id )
16051605 prettySe p bnd (PAlternative a as) =
16061606 lparen <> text "|" <> prettyAs <> text "|" <> rparen
src/Idris/Apropos.hs+1−1
@@ -55,7 +55,7 @@ instance Apropos Name where
5555 | (n == pairTy || n == pairCon) && str == T.pack "," = True
5656 | n == eqTy && str == T.pack "=" = True
5757 | n == eqCon && (T.toLower str) == T.pack "Refl" = True
58− | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True
58+ | (n == sigmaTy || n == sigmaCon) && str == T.pack "**" = True
5959 isApropos _ _ = False -- we don't care about case blocks, MNs, etc
6060
6161instance Apropos Def where
src/Idris/Delaborate.hs+4−4
@@ -108,17 +108,17 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
108108 deFn env (P _ n _) [l,r]
109109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)
110110 | n == eqCon = PRefl un (de env [] r)
111− | n == sUN "lazy" = de env [] r
111+ | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching
112112 deFn env (P _ n _) [ty, Bind x (Lam _) r]
113− | n == sUN "Sigma"
113+ | n == sigmaTy
114114 = PDPair un IsType (PRef un x) (de env [] ty)
115115 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
116116 deFn env (P _ n _) [lt,rt,l,r]
117117 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
118118 | n == eqTy = PEq un (de env [] lt) (de env [] rt)
119119 (de env [] l) (de env [] r)
120− | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder
121− (de env [] r)
120+ | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder
121+ (de env [] r)
122122 deFn env f@(P _ n _) args
123123 | n `elem` map snd env
124124 = PApp un (de env [] f) (map pexp (map (de env []) args))
src/Idris/Elab/Term.hs+2−2
@@ -410,11 +410,11 @@ elab ist info emode opts fn tm
410410 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
411411 [pexp t,
412412 pexp (PLam fc n Placeholder r)])
413− asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)
413+ asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)
414414 [pimp (sMN 0 "a") t False,
415415 pimp (sMN 0 "P") Placeholder True,
416416 pexp l, pexp r])
417− elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc existsCon)
417+ elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)
418418 [pimp (sMN 0 "a") t False,
419419 pimp (sMN 0 "P") Placeholder True,
420420 pexp l, pexp r])