git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of https://github.com/edwinb/Idris-dev into JavaRepairs
9991ac2Jan Bessai
README+5−1
compare with master
unifiedsplit
@@ -7,4 +7,8 @@ To install, type 'make'. This will install everything using cabal and
7typecheck the libraries.
7typecheck the libraries.
8
8
9To run the tests, type 'make test' which will execute the test suite, and
9To run the tests, type 'make test' which will execute the test suite, and
10−'make relib', which will typecheck and recompile the standard library.
10+'make relib', which will typecheck and recompile the standard library.
11+
12+Idris has buildtime dependencies on the C libraries llvm-3.3 and libffi. Be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc).
13+
14+Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).
contribs/lib/SimpleParser/SimpleParser.idr+106−156
@@ -1,5 +1,5 @@
1{-
1{-
2− Simple monadic parser module, based heavily on that by
2+ Simple monadic parser module, based heavily on that by
3 Graham Hutton.
3 Graham Hutton.
4-}
4-}
5
5
@@ -13,119 +13,94 @@ import Builtins
13
13
14%access public
14%access public
15
15
16−infixr 5 |||
17
16
18−{-
17+--------------------------------------------------------------------------------
19−The monad of parsers
18+-- The monad of parsers
20−--------------------
19+--------------------------------------------------------------------------------
21−-}
22
20
23−data Parser a = P (String -> Either String (a, String))
21+data Parser a = P (String -> Either String (a, String))
24
22
25−parse : Parser a -> String -> Either String (a, String)
23+parse : Parser a -> String -> Either String (a, String)
26−parse (P p) inp = p inp
24+parse (P p) inp = p inp
27
25
28−instance Functor Parser where
26+instance Functor Parser where
29− -- fmap : (a -> b) -> f a -> f b
30− -- fmap : (a -> b) -> Parser a -> Parser b
31− -- Given a function (a -> b), and a parser a, make a parser b
32− fmap f p = P (\inp => case parse p inp of
27+ fmap f p = P (\inp => case parse p inp of
33− (Left err) => Left err
28+ Left err => Left err
34− -- Apply f to the v that we got from parsing
35− (Right (v, rest)) => Right ((f v), rest))
29+ Right (v, rest) => Right ((f v), rest))
36−
37
30
38−instance Applicative Parser where
31+instance Applicative Parser where
39− pure v = P (\inp => Right (v, inp))
32+ pure v = P (\inp => Right (v, inp))
40− -- Parse to get the function, then parse to get the first argument
41− a <$> b = P (\inp => do (f, rest) <- parse a inp
33+ a <$> b = P (\inp => do (f, rest) <- parse a inp
42− (x, rest') <- parse b rest
34+ (x, rest') <- parse b rest
43− pure ((f x), rest'))
35+ pure ((f x), rest'))
44
36
45instance Monad Parser where
37instance Monad Parser where
46−-- pure v = P (\inp => Right (v,inp))
47− -- m a -> (a -> m b) -> m b
48− p >>= f = P (\inp => case parse p inp of
38+ p >>= f = P (\inp => case parse p inp of
49− (Left err) => Left err
39+ Left err => Left err
50− (Right (v,rest)) => parse (f v) rest)
40+ Right (v,rest) => parse (f v) rest)
51−
52−--mplus : Monad m => m a -> m a -> m a
53−mplus : Parser a -> Parser a -> Parser a
54−mplus p q = P (\inp => case parse p inp of
55− Left msg => parse q inp
56− Right (v,out) => Right(v,out))
57
41
42+instance Alternative Parser where
43+ empty = P (const (Left "empty"))
44+ p <|> q = P (\inp => case parse p inp of
45+ Left msg => parse q inp
46+ Right (v,out) => Right (v,out))
58
47
59−{-
60−Basic parsers
61−-------------
62−-}
63
48
64−failure : String -> Parser a
49+--------------------------------------------------------------------------------
65−failure msg = P (\inp => Left msg)
50+-- Basic parsers
51+--------------------------------------------------------------------------------
66
52
67−item : Parser Char
53+failure : String -> Parser a
68−item = P (\inp => case unpack inp of
54+failure msg = P (\inp => Left msg)
69− [] => Left "Error! Parsing empty list."
70− (x::xs) => Right (x, pack xs))
71−
72
55
73−{-
56+item : Parser Char
74−Choice
57+item = P (\inp => case unpack inp of
75−--------
58+ [] => Left "Error! Parsing empty list."
76−---}
59+ (x::xs) => Right (x, pack xs))
77
60
78−(|||) : Parser a -> Parser a -> Parser a
79−p ||| q = p `mplus` q
80
61
62+--------------------------------------------------------------------------------
63+-- Derived primitives
64+--------------------------------------------------------------------------------
81
65
82−--{-
66+sat : (Char -> Bool) -> Parser Char
83−--Derived primitives
67+sat p = do x <- item
84−---}
68+ guard (p x)
69+ pure x
85
70
86−sat : (Char -> Bool) -> Parser Char
87−sat p = item >>= (\x => if p x then pure x else failure "failed")
88−
89−oneof : List Char -> Parser Char
71+oneof : List Char -> Parser Char
90−oneof xs = sat (\x => elem x xs)
72+oneof xs = sat (\x => elem x xs)
91
73
92−digit : Parser Char
74+digit : Parser Char
93−digit = sat isDigit
75+digit = sat isDigit
94
76
95−lower : Parser Char
77+lower : Parser Char
96−lower = sat isLower
78+lower = sat isLower
97
79
98−upper : Parser Char
80+upper : Parser Char
99−upper = sat isUpper
81+upper = sat isUpper
100
82
101−letter : Parser Char
83+letter : Parser Char
102−letter = sat isAlpha
84+letter = sat isAlpha
103
85
104−alphanum : Parser Char
86+alphanum : Parser Char
105−alphanum = sat isAlphaNum
87+alphanum = sat isAlphaNum
106
88
107−char : Char -> Parser Char
89+char : Char -> Parser Char
108−char x = sat (== x)
90+char x = sat (== x)
109
91
110−helper : List Char -> Parser (List Char)
111−string : String -> Parser String
92+string : String -> Parser String
112−string s = do result <- helper (unpack s)
93+string s = fmap pack (traverse char (unpack s))
113− pure (pack result)
114−
115−helper [] = pure Prelude.List.Nil
116−helper (x::xs) = do char x
117− string (cast xs)
118− pure (x :: xs)
119
94
120−many : Parser a -> Parser (List a)
95+many1 : Parser a -> Parser (List a)
121−many1 : Parser a -> Parser (List a)
96+many : Parser a -> Parser (List a)
122−many1 p = do v <- p
123− vs <- many p
124− pure $ Prelude.List.(::) v vs
125
97
98+many1 p = [| p :: many p |]
99+
100+many p = many1 p <|> pure []
126
101
127bool : Parser Bool
102bool : Parser Bool
128−bool = parseTrue ||| parseFalse
103+bool = parseTrue <|> parseFalse
129 where parseTrue : Parser Bool
104 where parseTrue : Parser Bool
130 parseTrue = do oneof ['T', 't']
105 parseTrue = do oneof ['T', 't']
131 string "rue"
106 string "rue"
@@ -134,90 +109,65 @@ bool = parseTrue ||| parseFalse
134 string "alse"
109 string "alse"
135 pure False
110 pure False
136
111
112+ident : Parser String
113+ident = fmap pack [| letter :: many1 alphanum |]
137
114
115+nat : Parser Int
116+nat = do xs <- many digit
117+ pure (cast (cast xs))
138
118
139−
140−many p = many1 p `mplus` pure Prelude.List.Nil
141−
142−
143−
144−ident : Parser String
145−ident = do x <- letter
146− xs <- many1 alphanum
147− pure (pack(x::xs))
148−
149−nat : Parser Int
119+int : Parser Int
150−nat = do xs <- many digit
151− pure (cast (cast xs))
152−
153−
154−int : Parser Int
155−int = neg ||| nat
120+int = neg <|> nat
156 where neg : Parser Int
121 where neg : Parser Int
157 neg = do char '-'
122 neg = do char '-'
158 n <- nat
123 n <- nat
159 pure (-n)
124 pure (-n)
160
125
161−space : Parser ()
126+space : Parser ()
162−space = do many (sat isSpace)
127+space = do many (sat isSpace)
163− pure ()
128+ pure ()
164−--{-
129+
165−--Ignoring spacing
166−---}
167
130
168−token : Parser a -> Parser a
131+--------------------------------------------------------------------------------
169−token p = do space
132+-- Ignoring spacing
170− v <- p
133+--------------------------------------------------------------------------------
171− space
172− pure v
173
134
174−identifier : Parser String
135+token : Parser a -> Parser a
175−identifier = token ident
136+token p = space $> p <$ space
176
137
177−natural : Parser Int
138+identifier : Parser String
178−natural = token nat
139+identifier = token ident
179
140
180−integer : Parser Int
141+natural : Parser Int
181−integer = token int
142+natural = token nat
182
143
144+integer : Parser Int
145+integer = token int
146+
183−symbol : String -> Parser String
147+symbol : String -> Parser String
184−symbol xs = token (string xs)
148+symbol xs = token (string xs)
185
149
186strToken : Parser String
150strToken : Parser String
187strToken = fmap pack (token (many1 alphanum))
151strToken = fmap pack (token (many1 alphanum))
188
152
189−--apply : Parser a -> String -> List (a,String)
190−--apply p = parse (space >>= (\_ => p))
191
153
192−--{-
154+--------------------------------------------------------------------------------
193-- Expressions
155-- Expressions
194−---}
156+--------------------------------------------------------------------------------
195−
157+
196−factor : Parser Int
158+expr : Parser Int
197−term : Parser Int
159+factor : Parser Int
198−expr : Parser Int
160+term : Parser Int
161+
199−expr = do t <- term
162+expr = do t <- term
200− do symbol "+"
163+ fmap (t+) (symbol "+" $> expr) <|> pure t
201− e <- expr
164+
202− pure $ t + e
203− `mplus` pure t
204−
205−
206−factor = do symbol "("
165+factor = (symbol "(" $> expr <$ symbol ")") <|> natural
207− do e <- expr
166+
208− symbol ")"
209− pure e
210− `mplus` natural
211−
212−term = do f <- factor
167+term = do f <- factor
213− do symbol "*"
168+ fmap (f*) (symbol "*" $> term) <|> pure f
214− t <- term
169+
215− pure (f * t)
216− `mplus` pure f
217−
218−
219−
220−eval : String -> Maybe Int
170+eval : String -> Maybe Int
221−eval xs = case (parse expr xs) of
171+eval xs = case (parse expr xs) of
222− Right (n,rest) => if rest == "" then Just n else Nothing
172+ Right (n,rest) => if rest == "" then Just n else Nothing
223− Left msg => Nothing
173+ Left msg => Nothing
src/Core/Elaborate.hs+10−13
@@ -501,8 +501,8 @@ checkPiGoal n
501 solve
501 solve
502 focus f
502 focus f
503
503
504−simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
504+simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
505−simple_app fun arg =
505+simple_app fun arg appstr =
506 do a <- unique_hole (MN 0 "argTy")
506 do a <- unique_hole (MN 0 "argTy")
507 b <- unique_hole (MN 0 "retTy")
507 b <- unique_hole (MN 0 "retTy")
508 f <- unique_hole (MN 0 "f")
508 f <- unique_hole (MN 0 "f")
@@ -514,24 +514,21 @@ simple_app fun arg =
514 start_unify s
514 start_unify s
515 claim s (Var a)
515 claim s (Var a)
516 prep_fill f [s]
516 prep_fill f [s]
517− -- try elaborating in both orders, since we might learn something useful
518− -- either way
519−-- try (do focus s; arg
520−-- focus f; fun)
521−-- (do focus f; fun
522−-- focus s; arg)
523 focus f; fun
517 focus f; fun
524 focus s; arg
518 focus s; arg
525 tm <- get_term
519 tm <- get_term
526 ps <- get_probs
520 ps <- get_probs
527 complete_fill
521 complete_fill
528 hs <- get_holes
522 hs <- get_holes
523+ env <- get_env
529− -- We don't need a and b in the hole queue any more since they were just for
524+ -- We don't need a and b in the hole queue any more since they were
530− -- checking f, so discard them if they are still there. If they haven't been solved,
525+ -- just for checking f, so discard them if they are still there.
531− -- regret will fail
526+ -- If they haven't been solved, regret will fail
532− when (a `elem` hs) $ do focus a; regret
527+ when (a `elem` hs) $ do focus a; regretWith (CantInferType appstr)
533− when (b `elem` hs) $ do focus b; regret
528+ when (b `elem` hs) $ do focus b; regretWith (CantInferType appstr)
534 end_unify
529 end_unify
530+ where regretWith err = try regret
531+ (lift $ tfail err)
535
532
536-- Abstract over an argument of unknown type, giving a name for the hole
533-- Abstract over an argument of unknown type, giving a name for the hole
537-- which we'll fill with the argument type too.
534-- which we'll fill with the argument type too.
src/Core/ProofState.hs+2−1
@@ -363,7 +363,8 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
363 do action (\ps -> let hs = holes ps in
363 do action (\ps -> let hs = holes ps in
364 ps { holes = hs \\ [x] })
364 ps { holes = hs \\ [x] })
365 return sc
365 return sc
366+regret ctxt env (Bind x (Hole t) _)
366−regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
367+ = fail $ show x ++ " : " ++ show t ++ " is not solved..."
367
368
368exact :: Raw -> RunTactic
369exact :: Raw -> RunTactic
369exact guess ctxt env (Bind x (Hole ty) sc) =
370exact guess ctxt env (Bind x (Hole ty) sc) =
src/Core/TT.hs+2
@@ -60,6 +60,7 @@ data Err = Msg String
60 -- unification succeed
60 -- unification succeed
61 | InfiniteUnify Name Term [(Name, Type)]
61 | InfiniteUnify Name Term [(Name, Type)]
62 | CantConvert Term Term [(Name, Type)]
62 | CantConvert Term Term [(Name, Type)]
63+ | CantInferType String
63 | NonFunctionType Term Term
64 | NonFunctionType Term Term
64 | CantIntroduce Term
65 | CantIntroduce Term
65 | NoSuchVariable Name
66 | NoSuchVariable Name
@@ -103,6 +104,7 @@ score (CantUnify _ _ _ m _ s) = s + score m
103score (CantResolve _) = 20
104score (CantResolve _) = 20
104score (NoSuchVariable _) = 1000
105score (NoSuchVariable _) = 1000
105score (ProofSearchFail _) = 10000
106score (ProofSearchFail _) = 10000
107+score (InternalMsg _) = -1
106score _ = 0
108score _ = 0
107
109
108instance Show Err where
110instance Show Err where
src/Idris/Delaborate.hs+2
@@ -112,6 +112,8 @@ pshow i (CantConvert x y env)
112 "Can't convert " ++ showImp imps (delab i x) ++ " with "
112 "Can't convert " ++ showImp imps (delab i x) ++ " with "
113 ++ showImp imps (delab i y) ++
113 ++ showImp imps (delab i y) ++
114 if (opt_errContext (idris_options i)) then showSc i env else ""
114 if (opt_errContext (idris_options i)) then showSc i env else ""
115+pshow i (CantInferType t)
116+ = "Can't infer type for " ++ t
115pshow i (NonFunctionType f ty)
117pshow i (NonFunctionType f ty)
116 = let imps = opt_showimp (idris_options i) in
118 = let imps = opt_showimp (idris_options i) in
117 showImp imps (delab i f) ++ " does not have a function type ("
119 showImp imps (delab i f) ++ " does not have a function type ("
src/Idris/ElabTerm.hs+3−1
@@ -349,6 +349,7 @@ elab ist info pattern tcgen fn tm
349 then -- simple app, as below
349 then -- simple app, as below
350 do simple_app (elabE (ina, g) (PRef fc f))
350 do simple_app (elabE (ina, g) (PRef fc f))
351 (elabE (True, g) (getTm (head args')))
351 (elabE (True, g) (getTm (head args')))
352+ (show tm)
352 solve
353 solve
353 else
354 else
354 do ivs <- get_instances
355 do ivs <- get_instances
@@ -401,9 +402,10 @@ elab ist info pattern tcgen fn tm
401 setInjective (PApp _ (PRef _ n) _) = setinj n
402 setInjective (PApp _ (PRef _ n) _) = setinj n
402 setInjective _ = return ()
403 setInjective _ = return ()
403
404
404− elab' ina@(_, a) (PApp fc f [arg])
405+ elab' ina@(_, a) tm@(PApp fc f [arg])
405 = erun fc $
406 = erun fc $
406 do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
407 do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
408+ (show tm)
407 solve
409 solve
408 elab' ina Placeholder = do (h : hs) <- get_holes
410 elab' ina Placeholder = do (h : hs) <- get_holes
409 movelast h
411 movelast h