git.iko.soy/Idris-dev
on master help sign in
More platform agnostic now
fd5cddbChetan T
Setup.hs+6−3
compare with master
unifiedsplit
@@ -7,7 +7,8 @@ import qualified Distribution.Simple.Program as P
7import Distribution.PackageDescription
7import Distribution.PackageDescription
8
8
9import System.Exit
9import System.Exit
10−import System.FilePath ((</>))
10+import System.FilePath ((</>), splitDirectories)
11+import qualified System.FilePath.Posix as Px
11import System.Process
12import System.Process
12
13
13-- After Idris is built, we need to check and install the prelude and other libs
14-- After Idris is built, we need to check and install the prelude and other libs
@@ -16,9 +17,11 @@ make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "m
16
17
17#ifdef mingw32_HOST_OS
18#ifdef mingw32_HOST_OS
18-- make on mingw32 exepects unix style separators
19-- make on mingw32 exepects unix style separators
19−idrisCmd local = "../dist/build/idris/idris"
20+(<//>) = (Px.</>)
21+idrisCmd local = Px.joinPath $ splitDirectories $
22+ ".." <//> buildDir local <//> "idris" <//> "idris"
20#else
23#else
21−idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
24+idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
22#endif
25#endif
23
26
24cleanStdLib verbosity
27cleanStdLib verbosity
contribs/lib/simpleparser.idr+139−139
@@ -1,153 +1,153 @@
1−module Parsing
1+module Parsing
2−
2+
3−import prelude
3+import prelude
4−import builtins
4+import builtins
5−
5+
6−infixr 5 |||
6+infixr 5 |||
7−
7+
8−{-
8+{-
9−The monad of parsers
9+The monad of parsers
10−--------------------
10+--------------------
11−-}
11+-}
12−
12+
13−data Parser a = P (String -> Either String (a,String))
13+data Parser a = P (String -> Either String (a,String))
14−
14+
15−parse : Parser a -> String ->Either String (a,String)
15+parse : Parser a -> String ->Either String (a,String)
16−parse (P p) inp = p inp
16+parse (P p) inp = p inp
17−
17+
18−instance Monad Parser where
18+instance Monad Parser where
19− return v = P (\inp => Right (v,inp))
19+ return v = P (\inp => Right (v,inp))
20− p >>= f = P (\inp => case parse p inp of
20+ p >>= f = P (\inp => case parse p inp of
21− Left err => Left err
21+ Left err => Left err
22− Right (v,rest) => parse (f v) rest)
22+ Right (v,rest) => parse (f v) rest)
23−
23+
24−
24+
25−instance MonadPlus Parser where
25+instance MonadPlus Parser where
26− mzero = P (\inp => Left "Parse Error")
26+ mzero = P (\inp => Left "Parse Error")
27− mplus p q = P (\inp => case parse p inp of
27+ mplus p q = P (\inp => case parse p inp of
28− Left msg => parse q inp
28+ Left msg => parse q inp
29 Right (v,out) => Right(v,out))
29 Right (v,out) => Right(v,out))
30
30
31−
31+
32−{-
32+{-
33−Basic parsers
33+Basic parsers
34−-------------
34+-------------
35−-}
35+-}
36−
36+
37−failure : String -> Parser a
37+failure : String -> Parser a
38−failure msg = P (\inp => Left msg)
38+failure msg = P (\inp => Left msg)
39−
39+
40−item : Parser Char
40+item : Parser Char
41−item = P (\inp => case unpack inp of
41+item = P (\inp => case unpack inp of
42− [] => Left "Error! Parsing empty list."
42+ [] => Left "Error! Parsing empty list."
43 (x::xs) => Right (x, pack xs))
43 (x::xs) => Right (x, pack xs))
44
44
45−
45+
46{-
46{-
47−Choice
47+Choice
48−--------
48+--------
49−---}
49+---}
50−
50+
51−(|||) : Parser a -> Parser a -> Parser a
51+(|||) : Parser a -> Parser a -> Parser a
52−p ||| q = p `mplus` q
52+p ||| q = p `mplus` q
53−
53+
54−
54+
55−--{-
55+--{-
56−--Derived primitives
56+--Derived primitives
57−---}
57+---}
58−
58+
59−sat : (Char -> Bool) -> Parser Char
59+sat : (Char -> Bool) -> Parser Char
60sat p = item >>= (\x => if p x then return x else failure "failed")
60sat p = item >>= (\x => if p x then return x else failure "failed")
61−
61+
62−oneof : List Char -> Parser Char
62+oneof : List Char -> Parser Char
63−oneof xs = sat (\x => elem x xs)
63+oneof xs = sat (\x => elem x xs)
64−
64+
65−digit : Parser Char
65+digit : Parser Char
66−digit = sat isDigit
66+digit = sat isDigit
67−
67+
68−lower : Parser Char
68+lower : Parser Char
69−lower = sat isLower
69+lower = sat isLower
70−
70+
71−upper : Parser Char
71+upper : Parser Char
72−upper = sat isUpper
72+upper = sat isUpper
73−
73+
74−letter : Parser Char
74+letter : Parser Char
75−letter = sat isAlpha
75+letter = sat isAlpha
76−
76+
77−alphanum : Parser Char
77+alphanum : Parser Char
78−alphanum = sat isAlphaNum
78+alphanum = sat isAlphaNum
79−
79+
80−char : Char -> Parser Char
80+char : Char -> Parser Char
81−char x = sat (== x)
81+char x = sat (== x)
82−
82+
83−string : String -> Parser String
83+string : String -> Parser String
84−helper : List Char -> Parser (List Char)
84+helper : List Char -> Parser (List Char)
85−string s = do result <- helper (unpack s)
85+string s = do result <- helper (unpack s)
86− return (pack result)
86+ return (pack result)
87−
87+
88−helper [] = return []
88+helper [] = return []
89−helper (x::xs) = do char x
89+helper (x::xs) = do char x
90− string (cast xs)
90+ string (cast xs)
91− return (x :: xs)
91+ return (x :: xs)
92−
92+
93−many1 : Parser a -> Parser (List a)
93+many1 : Parser a -> Parser (List a)
94−many : Parser a -> Parser (List a)
94+many : Parser a -> Parser (List a)
95−many1 p = do v <- p
95+many1 p = do v <- p
96− vs <- many p
96+ vs <- many p
97− return (v::vs)
97+ return (v::vs)
98−
98+
99−
99+
100−many p = many1 p `mplus` return []
100+many p = many1 p `mplus` return []
101−
101+
102−
102+
103−
103+
104−ident : Parser String
104+ident : Parser String
105−ident = do x <- letter
105+ident = do x <- letter
106− xs <- many1 alphanum
106+ xs <- many1 alphanum
107− return (pack(x::xs))
107+ return (pack(x::xs))
108−
108+
109−
109+
110−nat : Parser Int
110+nat : Parser Int
111−nat = do xs <- many digit
111+nat = do xs <- many digit
112− return (cast (cast xs))
112+ return (cast (cast xs))
113−
113+
114−
114+
115−int : Parser Int
115+int : Parser Int
116−int = do char '-'
116+int = do char '-'
117− n <- nat
117+ n <- nat
118− return (-n)
118+ return (-n)
119− `mplus` nat
119+ `mplus` nat
120−
120+
121−space : Parser ()
121+space : Parser ()
122−space = do many (sat isSpace)
122+space = do many (sat isSpace)
123− return ()
123+ return ()
124−--{-
124+--{-
125−--Ignoring spacing
125+--Ignoring spacing
126−---}
126+---}
127−
127+
128−token : Parser a -> Parser a
128+token : Parser a -> Parser a
129−token p = do space
129+token p = do space
130− v <- p
130+ v <- p
131− space
131+ space
132− return v
132+ return v
133−
133+
134−identifier : Parser String
134+identifier : Parser String
135−identifier = token ident
135+identifier = token ident
136−
136+
137−natural : Parser Int
137+natural : Parser Int
138−natural = token nat
138+natural = token nat
139−
139+
140−integer : Parser Int
140+integer : Parser Int
141−integer = token int
141+integer = token int
142−
142+
143−symbol : String -> Parser String
143+symbol : String -> Parser String
144−symbol xs = token (string xs)
144+symbol xs = token (string xs)
145
145
146--apply : Parser a -> String -> List (a,String)
146--apply : Parser a -> String -> List (a,String)
147--apply p = parse (space >>= (\_ => p))
147--apply p = parse (space >>= (\_ => p))
148
148
149--{-
149--{-
150−-- Expressions
150+-- Expressions
151---}
151---}
152
152
153factor : Parser Int
153factor : Parser Int
idris.cabal+1−1
@@ -89,7 +89,7 @@ Executable idris
89 Paths_idris
89 Paths_idris
90
90
91 Build-depends: base>=4 && <5, parsec, mtl, Cabal,
91 Build-depends: base>=4 && <5, parsec, mtl, Cabal,
92− haskeline>=0.7, split,
92+ haskeline>=0.7, split, directory,
93 containers, process, transformers, filepath,
93 containers, process, transformers, filepath,
94 directory, binary, bytestring, pretty
94 directory, binary, bytestring, pretty
95
95
lib/Prelude.idr+10−2
@@ -289,11 +289,19 @@ fwrite (FHandle h) s = do_fwrite h s
289
289
290partial
290partial
291do_feof : Ptr -> IO Int
291do_feof : Ptr -> IO Int
292−do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
292+do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
293
293
294feof : File -> IO Bool
294feof : File -> IO Bool
295feof (FHandle h) = do eof <- do_feof h
295feof (FHandle h) = do eof <- do_feof h
296− return (not (eof == 0))
296+ return (not (eof == 0))
297+
298+partial
299+do_ferror : Ptr -> IO Int
300+do_ferror h = mkForeign (FFun "fileError" [FPtr] FInt) h
301+
302+ferror : File -> IO Bool
303+ferror (FHandle h) = do err <- do_ferror h
304+ return (not (err == 0))
297
305
298partial
306partial
299nullPtr : Ptr -> IO Bool
307nullPtr : Ptr -> IO Bool
papers/impl-paper/impldtp.tex+155−155
@@ -1,155 +1,155 @@
1−\documentclass{jfp1}
1+\documentclass{jfp1}
2−%\documentclass[acmtoplas]{acmtrans2m}
2+%\documentclass[acmtoplas]{acmtrans2m}
3−
3+
4−\usepackage[draft]{comments}
4+\usepackage[draft]{comments}
5−%\usepackage[final]{comments}
5+%\usepackage[final]{comments}
6−% \newcommand{\comment}[2]{[#1: #2]}
6+% \newcommand{\comment}[2]{[#1: #2]}
7−\newcommand{\khcomment}[1]{\comment{KH}{#1}}
7+\newcommand{\khcomment}[1]{\comment{KH}{#1}}
8−\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
8+\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
9−
9+
10−\usepackage{epsfig}
10+\usepackage{epsfig}
11−%\usepackage{path}
11+%\usepackage{path}
12−\usepackage{url}
12+\usepackage{url}
13−%\usepackage{amsmath,amssymb}
13+%\usepackage{amsmath,amssymb}
14−\usepackage{fancyvrb}
14+\usepackage{fancyvrb}
15−\usepackage{todonotes}
15+\usepackage{todonotes}
16−
16+
17−\newenvironment{template}{\sffamily}
17+\newenvironment{template}{\sffamily}
18−
18+
19−\usepackage{graphics,epsfig}
19+\usepackage{graphics,epsfig}
20−\usepackage{stmaryrd}
20+\usepackage{stmaryrd}
21−
21+
22−\input{./macros.ltx}
22+\input{./macros.ltx}
23−\input{./library.ltx}
23+\input{./library.ltx}
24−
24+
25−\NatPackage
25+\NatPackage
26−\FinPackage
26+\FinPackage
27−
27+
28−\newcounter{per}
28+\newcounter{per}
29−\setcounter{per}{1}
29+\setcounter{per}{1}
30−
30+
31−\newcommand{\Ivor}{\textsc{Ivor}}
31+\newcommand{\Ivor}{\textsc{Ivor}}
32−\newcommand{\Idris}{\textsc{Idris}}
32+\newcommand{\Idris}{\textsc{Idris}}
33−\newcommand{\IdrisM}{\textsc{Idris}$^-$}
33+\newcommand{\IdrisM}{\textsc{Idris}$^-$}
34−\newcommand{\TT}{\textsf{TT}}
34+\newcommand{\TT}{\textsf{TT}}
35−\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
35+\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
36−\newcommand{\Funl}{\textsc{Funl}}
36+\newcommand{\Funl}{\textsc{Funl}}
37−\newcommand{\Agda}{\textsc{Agda}}
37+\newcommand{\Agda}{\textsc{Agda}}
38−\newcommand{\LamPi}{$\lambda_\Pi$}
38+\newcommand{\LamPi}{$\lambda_\Pi$}
39−
39+
40−\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
40+\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
41−\begin{center}
41+\begin{center}
42−\fbox{
42+\fbox{
43−\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
43+\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
44−\end{minipage}}
44+\end{minipage}}
45−\end{center}
45+\end{center}
46−\vspace*{0.1cm}
46+\vspace*{0.1cm}
47−}
47+}
48−
48+
49−\newcommand{\mysubsubsection}[1]{
49+\newcommand{\mysubsubsection}[1]{
50−\noindent
50+\noindent
51−\textbf{#1}
51+\textbf{#1}
52−}
52+}
53−\newcommand{\hdecl}[1]{\texttt{#1}}
53+\newcommand{\hdecl}[1]{\texttt{#1}}
54−
54+
55−
55+
56−\title
56+\title
57− {Implementing General Purpose Dependently Typed Programming Languages}
57+ {Implementing General Purpose Dependently Typed Programming Languages}
58−%\subtitle{Implementing Domain Specific Languages by Overloading}
58+%\subtitle{Implementing Domain Specific Languages by Overloading}
59−
59+
60−\author[Edwin Brady]
60+\author[Edwin Brady]
61−{EDWIN BRADY\\
61+{EDWIN BRADY\\
62−School of Computer Science, University of St Andrews, St Andrews,
62+School of Computer Science, University of St Andrews, St Andrews,
63−KY16 9SX, UK}
63+KY16 9SX, UK}
64−
64+
65−\begin{document}
65+\begin{document}
66−
66+
67−\maketitle
67+\maketitle
68−
68+
69−\begin{abstract}
69+\begin{abstract}
70−Many components of a dependently typed programming language are by now well
70+Many components of a dependently typed programming language are by now well
71−understood, for example the underlying type theory, type checking, unification and
71+understood, for example the underlying type theory, type checking, unification and
72−evaluation. How to combine these components into a realistic and usable high
72+evaluation. How to combine these components into a realistic and usable high
73−level language is, however, folklore, discovered anew by successive
73+level language is, however, folklore, discovered anew by successive
74−language implementations. In this paper, I describe the implementation of a
74+language implementations. In this paper, I describe the implementation of a
75−new dependently typed functional programming language, \Idris{}.
75+new dependently typed functional programming language, \Idris{}.
76−\Idris{} is intended to be a \emph{general purpose} programming language
76+\Idris{} is intended to be a \emph{general purpose} programming language
77−and as such provides high level concepts such as implicit syntax,
77+and as such provides high level concepts such as implicit syntax,
78−type classes and \texttt{do} notation.
78+type classes and \texttt{do} notation.
79−I describe the high level language and the underlying type theory, and present
79+I describe the high level language and the underlying type theory, and present
80−a method for \emph{elaborating} concrete high level syntax with implicit
80+a method for \emph{elaborating} concrete high level syntax with implicit
81−arguments and type classes into a fully explicit type theory. Furthermore,
81+arguments and type classes into a fully explicit type theory. Furthermore,
82−I show how this method,
82+I show how this method,
83−based on a domain specific language embedded in Haskell, facilitates the
83+based on a domain specific language embedded in Haskell, facilitates the
84−implementation of new high level language constructs.
84+implementation of new high level language constructs.
85−
85+
86−%I describe the implementation of a dependently typed functional
86+%I describe the implementation of a dependently typed functional
87−%programming language, \Idris{}. Much has been written about various
87+%programming language, \Idris{}. Much has been written about various
88−%aspects of dependently typed language implementation (e.g. checking
88+%aspects of dependently typed language implementation (e.g. checking
89−%dependent types, unification, optimisation) but nothing yet about how
89+%dependent types, unification, optimisation) but nothing yet about how
90−%to bring it all together into a complete, practical, usable tool. This paper
90+%to bring it all together into a complete, practical, usable tool. This paper
91−%attempts to do so. In particular, I explain what is needed to turn
91+%attempts to do so. In particular, I explain what is needed to turn
92−%concrete syntax with implicit arguments into fully elaborated type
92+%concrete syntax with implicit arguments into fully elaborated type
93−%theory, using unification and a tactic engine.
93+%theory, using unification and a tactic engine.
94−\end{abstract}
94+\end{abstract}
95−
95+
96−
96+
97−%\category{D.3.2}{Programming Languages}{Language
97+%\category{D.3.2}{Programming Languages}{Language
98−% Classifications}[Applicative (functional) Languages]
98+% Classifications}[Applicative (functional) Languages]
99−%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
99+%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
100−%\terms{Languages, Verification, Performance}
100+%\terms{Languages, Verification, Performance}
101−%\keywords{Dependent Types, Typechecking}
101+%\keywords{Dependent Types, Typechecking}
102−
102+
103−
103+
104−%\begin{bottomstuff}
104+%\begin{bottomstuff}
105−%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
105+%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
106−%KY16 9SX
106+%KY16 9SX
107−%\end{bottomstuff}
107+%\end{bottomstuff}
108−
108+
109−\input{intro.tex}
109+\input{intro.tex}
110−
110+
111−%\input{overview.tex}
111+%\input{overview.tex}
112−
112+
113−\input{hll.tex}
113+\input{hll.tex}
114−
114+
115−\input{typechecking.tex}
115+\input{typechecking.tex}
116−
116+
117−%\input{proofstate.tex}
117+%\input{proofstate.tex}
118−
118+
119−\input{elaboration.tex}
119+\input{elaboration.tex}
120−
120+
121−\input{delab.tex}
121+\input{delab.tex}
122−
122+
123−%\input{compiling.tex}
123+%\input{compiling.tex}
124−
124+
125−%\input{syntax.tex}
125+%\input{syntax.tex}
126−
126+
127−\input{conclusions.tex}
127+\input{conclusions.tex}
128−
128+
129−\section*{Acknowledgements}
129+\section*{Acknowledgements}
130−
130+
131−This work was funded by the Scottish Informatics and Computer Science
131+This work was funded by the Scottish Informatics and Computer Science
132−Alliance (SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE).
132+Alliance (SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE).
133−My thanks to Kevin Hammond and Vilhelm Sj\"{o}berg for their comments
133+My thanks to Kevin Hammond and Vilhelm Sj\"{o}berg for their comments
134−on an earlier draft of this paper.
134+on an earlier draft of this paper.
135−
135+
136−\bibliographystyle{jfp}
136+\bibliographystyle{jfp}
137−\bibliography{library.bib}
137+\bibliography{library.bib}
138−
138+
139−\appendix
139+\appendix
140−
140+
141−%\section{TODOs}
141+%\section{TODOs}
142−%\listoftodos{}
142+%\listoftodos{}
143−
143+
144−%\section{Elaboration meta-operations}
144+%\section{Elaboration meta-operations}
145−
145+
146−%It's possible that it would be useful to have a quick reference of meta-operations
146+%It's possible that it would be useful to have a quick reference of meta-operations
147−%used by the elaborator here.
147+%used by the elaborator here.
148−
148+
149−%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
149+%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
150−%$\MO{NewProof}$, $\MO{NewTerm}$,
150+%$\MO{NewProof}$, $\MO{NewTerm}$,
151−%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
151+%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
152−
152+
153−%\input{code}
153+%\input{code}
154−
154+
155−\end{document}
155+\end{document}
rts/idris_stdfgn.c+10−1
@@ -15,6 +15,16 @@ void fileClose(void* h) {
15 fclose(f);
15 fclose(f);
16}
16}
17
17
18+int fileEOF(void* h) {
19+ FILE* f = (FILE*)h;
20+ return feof(f);
21+}
22+
23+int fileError(void* h) {
24+ FILE* f = (FILE*)h;
25+ return ferror(f);
26+}
27+
18void fputStr(void* h, char* str) {
28void fputStr(void* h, char* str) {
19 FILE* f = (FILE*)h;
29 FILE* f = (FILE*)h;
20 fputs(str, f);
30 fputs(str, f);
@@ -27,4 +37,3 @@ int isNull(void* ptr) {
27void* idris_stdin() {
37void* idris_stdin() {
28 return (void*)stdin;
38 return (void*)stdin;
29}
39}
30−
src/Core/Constraints.hs+61−61
@@ -1,61 +1,61 @@
1−module Core.Constraints(ucheck) where
1+module Core.Constraints(ucheck) where
2−
2+
3−import Core.TT
3+import Core.TT
4−
4+
5−import Control.Applicative
5+import Control.Applicative
6−import Control.Arrow
6+import Control.Arrow
7−import Control.Monad.Error
7+import Control.Monad.Error
8−import Control.Monad.RWS
8+import Control.Monad.RWS
9−import Control.Monad.State
9+import Control.Monad.State
10−import Data.List
10+import Data.List
11−import Data.Maybe
11+import Data.Maybe
12−import qualified Data.Map as M
12+import qualified Data.Map as M
13−
13+
14−import Debug.Trace
14+import Debug.Trace
15−
15+
16−ucheck :: [(UConstraint, FC)] -> TC ()
16+ucheck :: [(UConstraint, FC)] -> TC ()
17−ucheck cs = acyclic rels (map fst (M.toList rels))
17+ucheck cs = acyclic rels (map fst (M.toList rels))
18− where lhs (ULT l _) = l
18+ where lhs (ULT l _) = l
19− lhs (ULE l _) = l
19+ lhs (ULE l _) = l
20− rels = mkRels cs M.empty
20+ rels = mkRels cs M.empty
21−
21+
22−type Relations = M.Map UExp [(UConstraint, FC)]
22+type Relations = M.Map UExp [(UConstraint, FC)]
23−
23+
24−mkRels :: [(UConstraint, FC)] -> Relations -> Relations
24+mkRels :: [(UConstraint, FC)] -> Relations -> Relations
25−mkRels [] acc = acc
25+mkRels [] acc = acc
26−mkRels ((c, f) : cs) acc
26+mkRels ((c, f) : cs) acc
27− | not (ignore c)
27+ | not (ignore c)
28− = case M.lookup (lhs c) acc of
28+ = case M.lookup (lhs c) acc of
29− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
29+ Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
30− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
30+ Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
31− | otherwise = mkRels cs acc
31+ | otherwise = mkRels cs acc
32− where lhs (ULT l _) = l
32+ where lhs (ULT l _) = l
33− lhs (ULE l _) = l
33+ lhs (ULE l _) = l
34− ignore (ULE l r) = l == r
34+ ignore (ULE l r) = l == r
35− ignore _ = False
35+ ignore _ = False
36−
36+
37−
37+
38−acyclic :: Relations -> [UExp] -> TC ()
38+acyclic :: Relations -> [UExp] -> TC ()
39−acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
39+acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
40− where
40+ where
41− checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
41+ checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
42− checkCycle fc r path inc [] = return ()
42+ checkCycle fc r path inc [] = return ()
43− checkCycle fc r path inc (c : cs)
43+ checkCycle fc r path inc (c : cs)
44− = do check fc path inc c
44+ = do check fc path inc c
45− -- Remove c from r since we know there's no cycles now
45+ -- Remove c from r since we know there's no cycles now
46− let r' = M.insert c [] r
46+ let r' = M.insert c [] r
47− checkCycle fc r' path inc cs
47+ checkCycle fc r' path inc cs
48−
48+
49− check fc path inc (UVar x) | x < 0 = return ()
49+ check fc path inc (UVar x) | x < 0 = return ()
50− check fc path inc cv
50+ check fc path inc cv
51− | inc > 0 && cv `elem` map fst path
51+ | inc > 0 && cv `elem` map fst path
52− = Error $ At fc UniverseError
52+ = Error $ At fc UniverseError
53− -- FIXME: Make informative
53+ -- FIXME: Make informative
54− -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
54+ -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
55− | otherwise = case M.lookup cv r of
55+ | otherwise = case M.lookup cv r of
56− Nothing -> return ()
56+ Nothing -> return ()
57− Just cs -> mapM_ (next ((cv, fc):path) inc) cs
57+ Just cs -> mapM_ (next ((cv, fc):path) inc) cs
58−
58+
59− next path inc (ULT l r, fc) = check fc path (inc + 1) r
59+ next path inc (ULT l r, fc) = check fc path (inc + 1) r
60− next path inc (ULE l r, fc) = check fc path inc r
60+ next path inc (ULE l r, fc) = check fc path inc r
61−
61+
src/Pkg/Package.hs+8−14
@@ -5,7 +5,8 @@ import System.Process
5import System.Directory
5import System.Directory
6import System.Exit
6import System.Exit
7import System.IO
7import System.IO
8−import System.FilePath ((</>), addTrailingPathSeparator)
8+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName)
9+import System.Directory (createDirectoryIfMissing, copyFile)
9
10
10import Util.System
11import Util.System
11
12
@@ -55,10 +56,7 @@ cleanPkg fp
55 mapM_ rmIBC (modules pkgdesc)
56 mapM_ rmIBC (modules pkgdesc)
56 case execout pkgdesc of
57 case execout pkgdesc of
57 Nothing -> return ()
58 Nothing -> return ()
58− Just s -> do let exec = dir </> s
59+ Just s -> rmFile $ dir </> s
59− putStrLn $ "Removing " ++ exec
60− system $ "rm -f " ++ exec
61− return ()
62
60
63installPkg :: PkgDesc -> IO ()
61installPkg :: PkgDesc -> IO ()
64installPkg pkgdesc
62installPkg pkgdesc
@@ -92,10 +90,7 @@ testLib warn p f
92 else fail $ "Missing library " ++ f
90 else fail $ "Missing library " ++ f
93
91
94rmIBC :: Name -> IO ()
92rmIBC :: Name -> IO ()
95−rmIBC m = do let f = toIBCFile m
93+rmIBC m = rmFile $ toIBCFile m
96− putStrLn $ "Removing " ++ f
97− system $ "rm -f " ++ f
98− return ()
99
94
100toIBCFile (UN n) = n ++ ".ibc"
95toIBCFile (UN n) = n ++ ".ibc"
101toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))
96toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))
@@ -106,8 +101,8 @@ installIBC p m = do let f = toIBCFile m
106 d <- maybe getDataDir return target
101 d <- maybe getDataDir return target
107 let destdir = d </> p </> getDest m
102 let destdir = d </> p </> getDest m
108 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
103 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
109− system $ mkDirCmd ++ destdir
104+ createDirectoryIfMissing True destdir
110− system $ "install " ++ f ++ " " ++ destdir
105+ copyFile f (destdir </> takeFileName f)
111 return ()
106 return ()
112 where getDest (UN n) = ""
107 where getDest (UN n) = ""
113 getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))
108 getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))
@@ -116,8 +111,8 @@ installObj :: String -> String -> IO ()
116installObj p o = do d <- getDataDir
111installObj p o = do d <- getDataDir
117 let destdir = addTrailingPathSeparator (d </> p)
112 let destdir = addTrailingPathSeparator (d </> p)
118 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
113 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
119− system $ mkDirCmd ++ destdir
114+ createDirectoryIfMissing True destdir
120− system $ "install " ++ o ++ " " ++ destdir
115+ copyFile o (destdir </> takeFileName o)
121 return ()
116 return ()
122
117
123#ifdef mingw32_HOST_OS
118#ifdef mingw32_HOST_OS
@@ -135,4 +130,3 @@ clean :: Maybe String -> IO ()
135clean Nothing = return ()
130clean Nothing = return ()
136clean (Just s) = do system $ "make -f " ++ s ++ " clean"
131clean (Just s) = do system $ "make -f " ++ s ++ " clean"
137 return ()
132 return ()
138−
src/Util/System.hs+9−29
@@ -1,8 +1,9 @@
1{-# LANGUAGE CPP #-}
1{-# LANGUAGE CPP #-}
2−module Util.System(tempfile,environment,getCC,getLibFlags,getIdrisLibDir,getIncFlags) where
2+module Util.System(tempfile,environment,getCC,getLibFlags,getIdrisLibDir,getIncFlags,rmFile) where
3
3
4-- System helper functions.
4-- System helper functions.
5
5
6+import System.Directory (getTemporaryDirectory, removeFile)
6import System.FilePath ((</>), addTrailingPathSeparator, normalise)
7import System.FilePath ((</>), addTrailingPathSeparator, normalise)
7import System.Environment
8import System.Environment
8import System.IO
9import System.IO
@@ -10,11 +11,6 @@ import System.IO
10import Control.Exception as CE
11import Control.Exception as CE
11#endif
12#endif
12
13
13−-- import Data.List
14−import Data.List.Split(splitOn)
15−
16−import Paths_idris
17−
18#if MIN_VERSION_base(4,0,0)
14#if MIN_VERSION_base(4,0,0)
19catchIO :: IO a -> (IOError -> IO a) -> IO a
15catchIO :: IO a -> (IOError -> IO a) -> IO a
20catchIO = CE.catch
16catchIO = CE.catch
@@ -29,32 +25,16 @@ getCC = do env <- environment "IDRIS_CC"
29 Just cc -> return cc
25 Just cc -> return cc
30
26
31tempfile :: IO (FilePath, Handle)
27tempfile :: IO (FilePath, Handle)
32−tempfile = do env <- environment tempDirEnvVar
28+tempfile = do dir <- getTemporaryDirectory
33− let dir = case env of
34− Nothing -> "/tmp"
35−#ifdef mingw32_HOST_OS
36− -- ghc changes the path separators if we start program in a *nix shell
37− (Just d) -> normalise d
29+ openTempFile (normalise dir) "idris"
38−#else
39− (Just d) -> d
40−#endif
41− openTempFile dir "idris"
42−#ifdef mingw32_HOST_OS
43− where tempDirEnvVar = "TMP"
44−#else
45− where tempDirEnvVar = "TMPDIR"
46−#endif
47
30
48environment :: String -> IO (Maybe String)
31environment :: String -> IO (Maybe String)
49environment x = catchIO (do e <- getEnv x
32environment x = catchIO (do e <- getEnv x
50 return (Just e))
33 return (Just e))
51 (\_ -> return Nothing)
34 (\_ -> return Nothing)
52
35
53−getLibFlags = do dir <- getDataDir
36+rmFile :: FilePath -> IO ()
54− return $ "-L" ++ (dir </> "rts") ++ " -lidris_rts -lgmp -lpthread"
37+rmFile f = do putStrLn $ "Removing " ++ f
55−
38+ catchIO (removeFile f)
56−getIdrisLibDir = do dir <- getDataDir
39+ (\ioerr -> putStrLn $ "WARNING: Cannot remove file "
57− return $ addTrailingPathSeparator dir
40+ ++ f ++ ", Error msg:" ++ show ioerr)
58−
59−getIncFlags = do dir <- getDataDir
60− return $ "-I" ++ dir </> "rts"