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

lib/Builtins.idr+1−1

compare with master

unifiedsplit

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

63

64data Bool = False | True

65

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

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

67boolElim True t e = t

68boolElim False t e = e

69

lib/Network/Cgi.idr+2−2

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

102 getC : Int -> String -> IO String

103 getC 0 acc = return $ reverse acc

104 getC n acc = if (n > 0)

105− then do x' <- getChar

105+ then do x <- getChar

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

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

107 else (return "")

108

109abstract

src/Core/Elaborate.hs+1−1

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

305 when i (movelast n)

306

307 mkMN n@(MN _ _) = n

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

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

309 mkMN (NS n xs) = NS (mkMN n) xs

310

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

src/Idris/ElabTerm.hs+5−1

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

172 _ -> True

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

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

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

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

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

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

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

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

177 = do hsin <- get_holes

181 = do hsin <- get_holes

178 ptmin <- get_term

182 ptmin <- get_term

src/Idris/IBC.hs+2

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

763 Specialise x -> do putWord8 4

764 put x

765 Coinductive -> putWord8 5

766+ PartialFn -> putWord8 6

766 get

767 get

767 = do i <- getWord8

768 = do i <- getWord8

768 case i of

769 case i of

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

773 4 -> do x <- get

774 4 -> do x <- get

774 return (Specialise x)

775 return (Specialise x)

775 5 -> return Coinductive

776 5 -> return Coinductive

777+ 6 -> return PartialFn

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

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

777

779

778instance Binary Fixity where

780instance Binary Fixity where

src/Idris/Parser.hs+4−4

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

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

724-- return (PTyped e t))

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

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

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

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

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

728 pexp e]))

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

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

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

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

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

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

733

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

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

src/Idris/REPLParser.hs+1−1

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

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

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

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

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

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

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

28 return (ModImport (map dot f)))

27 return (ModImport (map dot f)))

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

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

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

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

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

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

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

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

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

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

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

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

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