git.iko.soy/Idris-dev
on master help sign in
Fixes some string comparison that made sigma show incorrectly.
2f6e736Ahmad Salim Al-Sibahi
src/Idris/AbsSyntaxTree.hs+3−3
compare with master
unifiedsplit
@@ -1346,7 +1346,7 @@ modDocName = sMN 0 "ModuleDocs"
1346
1346
1347-- Defined in builtins.idr
1347-- Defined in builtins.idr
1348sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1348sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1349−existsCon = sNS (sUN "MkSigma") ["Builtins"]
1349+sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1350
1350
1351piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1351piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1352piBind = piBindp expl
1352piBind = piBindp expl
@@ -1597,10 +1597,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1597 annotated rparen
1597 annotated rparen
1598 where annotated = case pun of
1598 where annotated = case pun of
1599 IsType -> annName sigmaTy
1599 IsType -> annName sigmaTy
1600− IsTerm -> annName existsCon
1600+ IsTerm -> annName sigmaCon
1601 TypeOrTerm -> id
1601 TypeOrTerm -> id
1602 (left, addBinding) = case (l, pun) of
1602 (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) :))
1604 _ -> (prettySe startPrec bnd l, id )
1604 _ -> (prettySe startPrec bnd l, id )
1605 prettySe p bnd (PAlternative a as) =
1605 prettySe p bnd (PAlternative a as) =
1606 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1606 lparen <> text "|" <> prettyAs <> text "|" <> rparen
src/Idris/Apropos.hs+1−1
@@ -55,7 +55,7 @@ instance Apropos Name where
55 | (n == pairTy || n == pairCon) && str == T.pack "," = True
55 | (n == pairTy || n == pairCon) && str == T.pack "," = True
56 | n == eqTy && str == T.pack "=" = True
56 | n == eqTy && str == T.pack "=" = True
57 | n == eqCon && (T.toLower str) == T.pack "Refl" = True
57 | 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
59 isApropos _ _ = False -- we don't care about case blocks, MNs, etc
59 isApropos _ _ = False -- we don't care about case blocks, MNs, etc
60
60
61instance Apropos Def where
61instance Apropos Def where
src/Idris/Delaborate.hs+4−4
@@ -108,17 +108,17 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
108 deFn env (P _ n _) [l,r]
108 deFn env (P _ n _) [l,r]
109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)
109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)
110 | n == eqCon = PRefl un (de env [] r)
110 | 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
112 deFn env (P _ n _) [ty, Bind x (Lam _) r]
112 deFn env (P _ n _) [ty, Bind x (Lam _) r]
113− | n == sUN "Sigma"
113+ | n == sigmaTy
114 = PDPair un IsType (PRef un x) (de env [] ty)
114 = PDPair un IsType (PRef un x) (de env [] ty)
115 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
115 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
116 deFn env (P _ n _) [lt,rt,l,r]
116 deFn env (P _ n _) [lt,rt,l,r]
117 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
117 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
118 | n == eqTy = PEq un (de env [] lt) (de env [] rt)
118 | n == eqTy = PEq un (de env [] lt) (de env [] rt)
119 (de env [] l) (de env [] r)
119 (de env [] l) (de env [] r)
120− | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder
120+ | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder
121− (de env [] r)
121+ (de env [] r)
122 deFn env f@(P _ n _) args
122 deFn env f@(P _ n _) args
123 | n `elem` map snd env
123 | n `elem` map snd env
124 = PApp un (de env [] f) (map pexp (map (de env []) args))
124 = 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
410 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
410 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
411 [pexp t,
411 [pexp t,
412 pexp (PLam fc n Placeholder r)])
412 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)
414 [pimp (sMN 0 "a") t False,
414 [pimp (sMN 0 "a") t False,
415 pimp (sMN 0 "P") Placeholder True,
415 pimp (sMN 0 "P") Placeholder True,
416 pexp l, pexp r])
416 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)
418 [pimp (sMN 0 "a") t False,
418 [pimp (sMN 0 "a") t False,
419 pimp (sMN 0 "P") Placeholder True,
419 pimp (sMN 0 "P") Placeholder True,
420 pexp l, pexp r])
420 pexp l, pexp r])