671d39a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix name clashes between holes and bound variables

commit671d39a0f255a5d612295bb449b2126126ee90f7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 29 Oct 2012, 11:44 (14 years ago) parent74cd49e

7 files changed+16−10

compare with master

unifiedsplit

lib/Builtins.idr+1−1 lib/Network/Cgi.idr+2−2 src/Core/Elaborate.hs+1−1 src/Idris/ElabTerm.hs+5−1 src/Idris/IBC.hs+2 src/Idris/Parser.hs+4−4 src/Idris/REPLParser.hs+1−1

lib/Builtins.idr+1−1

@@ -63,7 +63,7 @@ cong refl = refl

6363

6464data Bool = False | True

6565

66−boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a

66+boolElim : Bool -> |(t : a) -> |(f : a) -> a

6767boolElim True t e = t

6868boolElim False t e = e

6969

lib/Network/Cgi.idr+2−2

@@ -102,8 +102,8 @@ getContent x = getC x "" where

102102 getC : Int -> String -> IO String

103103 getC 0 acc = return $ reverse acc

104104 getC n acc = if (n > 0)

105− then do x' <- getChar

106− getC (n-1) (strCons x' acc)

105+ then do x <- getChar

106+ getC (n-1) (strCons x acc)

107107 else (return "")

108108

109109abstract

src/Core/Elaborate.hs+1−1

@@ -305,7 +305,7 @@ prepare_apply fn imps =

305305 when i (movelast n)

306306

307307 mkMN n@(MN _ _) = n

308− mkMN n@(UN x) = MN 0 x

308+ mkMN n@(UN x) = MN 1000 x

309309 mkMN (NS n xs) = NS (mkMN n) xs

310310

311311apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

src/Idris/ElabTerm.hs+5−1

@@ -172,7 +172,11 @@ elab ist info pattern tcgen fn tm

172172 _ -> True

173173 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

174174 elab' ina@(_, a) (PLam n Placeholder sc)

175− = do attack; intro (Just n); elabE (True, a) sc; solve

175+ = do -- n' <- unique_hole n

176+ -- let sc' = mapPT (repN n n') sc

177+ attack; intro (Just n); elabE (True, a) sc; solve

178+ where repN n n' (PRef fc x) | x == n' = PRef fc n'

179+ repN _ _ t = t

176180 elab' ina@(_, a) (PLam n ty sc)

177181 = do hsin <- get_holes

178182 ptmin <- get_term

src/Idris/IBC.hs+2

@@ -763,6 +763,7 @@ instance Binary FnOpt where

763763 Specialise x -> do putWord8 4

764764 put x

765765 Coinductive -> putWord8 5

766+ PartialFn -> putWord8 6

766767 get

767768 = do i <- getWord8

768769 case i of

@@ -773,6 +774,7 @@ instance Binary FnOpt where

773774 4 -> do x <- get

774775 return (Specialise x)

775776 5 -> return Coinductive

777+ 6 -> return PartialFn

776778 _ -> error "Corrupted binary data for FnOpt"

777779

778780instance Binary Fixity where

src/Idris/Parser.hs+4−4

@@ -723,13 +723,13 @@ bracketed syn =

723723-- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'

724724-- return (PTyped e t))

725725 <|> try (do fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'

726− return $ PLam (MN 0 "x") Placeholder

727− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 0 "x")),

726+ return $ PLam (MN 1000 "ARG") Placeholder

727+ (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),

728728 pexp e]))

729729 <|> try (do fc <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'

730− return $ PLam (MN 0 "x") Placeholder

730+ return $ PLam (MN 1000 "ARG") Placeholder

731731 (PApp fc (PRef fc (UN o)) [pexp e,

732− pexp (PRef fc (MN 0 "x"))]))

732+ pexp (PRef fc (MN 1000 "ARG"))]))

733733

734734pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

735735pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn

src/Idris/REPLParser.hs+1−1

@@ -23,7 +23,6 @@ pCmd :: IParser Command

2323pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

2424 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

2525 <|> try (do cmd ["r", "reload"]; eof; return Reload)

26− <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

2726 <|> try (do cmd ["m", "module"]; f <- identifier; eof;

2827 return (ModImport (map dot f)))

2928 <|> try (do cmd ["e", "edit"]; eof; return Edit)

@@ -41,6 +40,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

4140 <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))

4241 <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))

4342 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

43+ <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

4444 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

4545 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

4646 <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))