git.iko.soy/Idris-dev
on master help sign in
More platform agnostic now

Cleaned up the paths, also added feof and ferror as functions (on mingw32 they're macros that expand incorrectly in the C based backend output. Conflicts: src/Pkg/Package.hs src/Util/System.hs

commitfd5cddb529d9003a66fc6049e369de79c1fbe98c authorChetan T <chetant@gmail.com> dateWed 28 Nov 2012, 22:31 (14 years ago) parent7fe382d
9 files changed+399−405
compare with master
unifiedsplit
Setup.hs+6−3 contribs/lib/simpleparser.idr+139−139 idris.cabal+1−1 lib/Prelude.idr+10−2 papers/impl-paper/impldtp.tex+155−155 rts/idris_stdfgn.c+10−1 src/Core/Constraints.hs+61−61 src/Pkg/Package.hs+8−14 src/Util/System.hs+9−29
Setup.hs+6−3
@@ -7,7 +7,8 @@ import qualified Distribution.Simple.Program as P
77import Distribution.PackageDescription
88
99import System.Exit
10−import System.FilePath ((</>))
10+import System.FilePath ((</>), splitDirectories)
11+import qualified System.FilePath.Posix as Px
1112import System.Process
1213
1314-- 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
1617
1718#ifdef mingw32_HOST_OS
1819-- 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"
2023#else
21−idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
24+idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
2225#endif
2326
2427cleanStdLib verbosity
contribs/lib/simpleparser.idr+139−139
@@ -1,153 +1,153 @@
1−module Parsing
2−
3−import prelude
4−import builtins
5−
6−infixr 5 |||
7−
8−{-
9−The monad of parsers
10−--------------------
11−-}
12−
13−data Parser a = P (String -> Either String (a,String))
14−
15−parse : Parser a -> String ->Either String (a,String)
16−parse (P p) inp = p inp
17−
18−instance Monad Parser where
19− return v = P (\inp => Right (v,inp))
20− p >>= f = P (\inp => case parse p inp of
21− Left err => Left err
22− Right (v,rest) => parse (f v) rest)
23−
24−
25−instance MonadPlus Parser where
26− mzero = P (\inp => Left "Parse Error")
27− mplus p q = P (\inp => case parse p inp of
28− Left msg => parse q inp
1+module Parsing
2+
3+import prelude
4+import builtins
5+
6+infixr 5 |||
7+
8+{-
9+The monad of parsers
10+--------------------
11+-}
12+
13+data Parser a = P (String -> Either String (a,String))
14+
15+parse : Parser a -> String ->Either String (a,String)
16+parse (P p) inp = p inp
17+
18+instance Monad Parser where
19+ return v = P (\inp => Right (v,inp))
20+ p >>= f = P (\inp => case parse p inp of
21+ Left err => Left err
22+ Right (v,rest) => parse (f v) rest)
23+
24+
25+instance MonadPlus Parser where
26+ mzero = P (\inp => Left "Parse Error")
27+ mplus p q = P (\inp => case parse p inp of
28+ Left msg => parse q inp
2929 Right (v,out) => Right(v,out))
3030
31−
32−{-
33−Basic parsers
34−-------------
35−-}
36−
37−failure : String -> Parser a
38−failure msg = P (\inp => Left msg)
39−
40−item : Parser Char
41−item = P (\inp => case unpack inp of
42− [] => Left "Error! Parsing empty list."
31+
32+{-
33+Basic parsers
34+-------------
35+-}
36+
37+failure : String -> Parser a
38+failure msg = P (\inp => Left msg)
39+
40+item : Parser Char
41+item = P (\inp => case unpack inp of
42+ [] => Left "Error! Parsing empty list."
4343 (x::xs) => Right (x, pack xs))
4444
45−
45+
4646{-
47−Choice
48−--------
49−---}
50−
51−(|||) : Parser a -> Parser a -> Parser a
52−p ||| q = p `mplus` q
53−
54−
55−--{-
56−--Derived primitives
57−---}
58−
59−sat : (Char -> Bool) -> Parser Char
47+Choice
48+--------
49+---}
50+
51+(|||) : Parser a -> Parser a -> Parser a
52+p ||| q = p `mplus` q
53+
54+
55+--{-
56+--Derived primitives
57+---}
58+
59+sat : (Char -> Bool) -> Parser Char
6060sat p = item >>= (\x => if p x then return x else failure "failed")
61−
62−oneof : List Char -> Parser Char
63−oneof xs = sat (\x => elem x xs)
64−
65−digit : Parser Char
66−digit = sat isDigit
67−
68−lower : Parser Char
69−lower = sat isLower
70−
71−upper : Parser Char
72−upper = sat isUpper
73−
74−letter : Parser Char
75−letter = sat isAlpha
76−
77−alphanum : Parser Char
78−alphanum = sat isAlphaNum
79−
80−char : Char -> Parser Char
81−char x = sat (== x)
82−
83−string : String -> Parser String
84−helper : List Char -> Parser (List Char)
85−string s = do result <- helper (unpack s)
86− return (pack result)
87−
88−helper [] = return []
89−helper (x::xs) = do char x
90− string (cast xs)
91− return (x :: xs)
92−
93−many1 : Parser a -> Parser (List a)
94−many : Parser a -> Parser (List a)
95−many1 p = do v <- p
96− vs <- many p
97− return (v::vs)
98−
99−
100−many p = many1 p `mplus` return []
101−
102−
103−
104−ident : Parser String
105−ident = do x <- letter
106− xs <- many1 alphanum
107− return (pack(x::xs))
108−
109−
110−nat : Parser Int
111−nat = do xs <- many digit
112− return (cast (cast xs))
113−
114−
115−int : Parser Int
116−int = do char '-'
117− n <- nat
118− return (-n)
119− `mplus` nat
120−
121−space : Parser ()
122−space = do many (sat isSpace)
123− return ()
124−--{-
125−--Ignoring spacing
126−---}
127−
128−token : Parser a -> Parser a
129−token p = do space
130− v <- p
131− space
132− return v
133−
134−identifier : Parser String
135−identifier = token ident
136−
137−natural : Parser Int
138−natural = token nat
139−
140−integer : Parser Int
141−integer = token int
142−
143−symbol : String -> Parser String
144−symbol xs = token (string xs)
61+
62+oneof : List Char -> Parser Char
63+oneof xs = sat (\x => elem x xs)
64+
65+digit : Parser Char
66+digit = sat isDigit
67+
68+lower : Parser Char
69+lower = sat isLower
70+
71+upper : Parser Char
72+upper = sat isUpper
73+
74+letter : Parser Char
75+letter = sat isAlpha
76+
77+alphanum : Parser Char
78+alphanum = sat isAlphaNum
79+
80+char : Char -> Parser Char
81+char x = sat (== x)
82+
83+string : String -> Parser String
84+helper : List Char -> Parser (List Char)
85+string s = do result <- helper (unpack s)
86+ return (pack result)
87+
88+helper [] = return []
89+helper (x::xs) = do char x
90+ string (cast xs)
91+ return (x :: xs)
92+
93+many1 : Parser a -> Parser (List a)
94+many : Parser a -> Parser (List a)
95+many1 p = do v <- p
96+ vs <- many p
97+ return (v::vs)
98+
99+
100+many p = many1 p `mplus` return []
101+
102+
103+
104+ident : Parser String
105+ident = do x <- letter
106+ xs <- many1 alphanum
107+ return (pack(x::xs))
108+
109+
110+nat : Parser Int
111+nat = do xs <- many digit
112+ return (cast (cast xs))
113+
114+
115+int : Parser Int
116+int = do char '-'
117+ n <- nat
118+ return (-n)
119+ `mplus` nat
120+
121+space : Parser ()
122+space = do many (sat isSpace)
123+ return ()
124+--{-
125+--Ignoring spacing
126+---}
127+
128+token : Parser a -> Parser a
129+token p = do space
130+ v <- p
131+ space
132+ return v
133+
134+identifier : Parser String
135+identifier = token ident
136+
137+natural : Parser Int
138+natural = token nat
139+
140+integer : Parser Int
141+integer = token int
142+
143+symbol : String -> Parser String
144+symbol xs = token (string xs)
145145
146146--apply : Parser a -> String -> List (a,String)
147147--apply p = parse (space >>= (\_ => p))
148148
149149--{-
150−-- Expressions
150+-- Expressions
151151---}
152152
153153factor : Parser Int
idris.cabal+1−1
@@ -89,7 +89,7 @@ Executable idris
8989 Paths_idris
9090
9191 Build-depends: base>=4 && <5, parsec, mtl, Cabal,
92− haskeline>=0.7, split,
92+ haskeline>=0.7, split, directory,
9393 containers, process, transformers, filepath,
9494 directory, binary, bytestring, pretty
9595
lib/Prelude.idr+10−2
@@ -289,11 +289,19 @@ fwrite (FHandle h) s = do_fwrite h s
289289
290290partial
291291do_feof : Ptr -> IO Int
292−do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
292+do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
293293
294294feof : File -> IO Bool
295295feof (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))
297305
298306partial
299307nullPtr : Ptr -> IO Bool
papers/impl-paper/impldtp.tex+155−155
@@ -1,155 +1,155 @@
1−\documentclass{jfp1}
2−%\documentclass[acmtoplas]{acmtrans2m}
3−
4−\usepackage[draft]{comments}
5−%\usepackage[final]{comments}
6−% \newcommand{\comment}[2]{[#1: #2]}
7−\newcommand{\khcomment}[1]{\comment{KH}{#1}}
8−\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
9−
10−\usepackage{epsfig}
11−%\usepackage{path}
12−\usepackage{url}
13−%\usepackage{amsmath,amssymb}
14−\usepackage{fancyvrb}
15−\usepackage{todonotes}
16−
17−\newenvironment{template}{\sffamily}
18−
19−\usepackage{graphics,epsfig}
20−\usepackage{stmaryrd}
21−
22−\input{./macros.ltx}
23−\input{./library.ltx}
24−
25−\NatPackage
26−\FinPackage
27−
28−\newcounter{per}
29−\setcounter{per}{1}
30−
31−\newcommand{\Ivor}{\textsc{Ivor}}
32−\newcommand{\Idris}{\textsc{Idris}}
33−\newcommand{\IdrisM}{\textsc{Idris}$^-$}
34−\newcommand{\TT}{\textsf{TT}}
35−\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
36−\newcommand{\Funl}{\textsc{Funl}}
37−\newcommand{\Agda}{\textsc{Agda}}
38−\newcommand{\LamPi}{$\lambda_\Pi$}
39−
40−\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
41−\begin{center}
42−\fbox{
43−\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
44−\end{minipage}}
45−\end{center}
46−\vspace*{0.1cm}
47−}
48−
49−\newcommand{\mysubsubsection}[1]{
50−\noindent
51−\textbf{#1}
52−}
53−\newcommand{\hdecl}[1]{\texttt{#1}}
54−
55−
56−\title
57− {Implementing General Purpose Dependently Typed Programming Languages}
58−%\subtitle{Implementing Domain Specific Languages by Overloading}
59−
60−\author[Edwin Brady]
61−{EDWIN BRADY\\
62−School of Computer Science, University of St Andrews, St Andrews,
63−KY16 9SX, UK}
64−
65−\begin{document}
66−
67−\maketitle
68−
69−\begin{abstract}
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
72−evaluation. How to combine these components into a realistic and usable high
73−level language is, however, folklore, discovered anew by successive
74−language implementations. In this paper, I describe the implementation of a
75−new dependently typed functional programming language, \Idris{}.
76−\Idris{} is intended to be a \emph{general purpose} programming language
77−and as such provides high level concepts such as implicit syntax,
78−type classes and \texttt{do} notation.
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
81−arguments and type classes into a fully explicit type theory. Furthermore,
82−I show how this method,
83−based on a domain specific language embedded in Haskell, facilitates the
84−implementation of new high level language constructs.
85−
86−%I describe the implementation of a dependently typed functional
87−%programming language, \Idris{}. Much has been written about various
88−%aspects of dependently typed language implementation (e.g. checking
89−%dependent types, unification, optimisation) but nothing yet about how
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
92−%concrete syntax with implicit arguments into fully elaborated type
93−%theory, using unification and a tactic engine.
94−\end{abstract}
95−
96−
97−%\category{D.3.2}{Programming Languages}{Language
98−% Classifications}[Applicative (functional) Languages]
99−%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
100−%\terms{Languages, Verification, Performance}
101−%\keywords{Dependent Types, Typechecking}
102−
103−
104−%\begin{bottomstuff}
105−%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
106−%KY16 9SX
107−%\end{bottomstuff}
108−
109−\input{intro.tex}
110−
111−%\input{overview.tex}
112−
113−\input{hll.tex}
114−
115−\input{typechecking.tex}
116−
117−%\input{proofstate.tex}
118−
119−\input{elaboration.tex}
120−
121−\input{delab.tex}
122−
123−%\input{compiling.tex}
124−
125−%\input{syntax.tex}
126−
127−\input{conclusions.tex}
128−
129−\section*{Acknowledgements}
130−
131−This work was funded by the Scottish Informatics and Computer Science
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
134−on an earlier draft of this paper.
135−
136−\bibliographystyle{jfp}
137−\bibliography{library.bib}
138−
139−\appendix
140−
141−%\section{TODOs}
142−%\listoftodos{}
143−
144−%\section{Elaboration meta-operations}
145−
146−%It's possible that it would be useful to have a quick reference of meta-operations
147−%used by the elaborator here.
148−
149−%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
150−%$\MO{NewProof}$, $\MO{NewTerm}$,
151−%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
152−
153−%\input{code}
154−
155−\end{document}
1+\documentclass{jfp1}
2+%\documentclass[acmtoplas]{acmtrans2m}
3+
4+\usepackage[draft]{comments}
5+%\usepackage[final]{comments}
6+% \newcommand{\comment}[2]{[#1: #2]}
7+\newcommand{\khcomment}[1]{\comment{KH}{#1}}
8+\newcommand{\ebcomment}[1]{\comment{EB}{#1}}
9+
10+\usepackage{epsfig}
11+%\usepackage{path}
12+\usepackage{url}
13+%\usepackage{amsmath,amssymb}
14+\usepackage{fancyvrb}
15+\usepackage{todonotes}
16+
17+\newenvironment{template}{\sffamily}
18+
19+\usepackage{graphics,epsfig}
20+\usepackage{stmaryrd}
21+
22+\input{./macros.ltx}
23+\input{./library.ltx}
24+
25+\NatPackage
26+\FinPackage
27+
28+\newcounter{per}
29+\setcounter{per}{1}
30+
31+\newcommand{\Ivor}{\textsc{Ivor}}
32+\newcommand{\Idris}{\textsc{Idris}}
33+\newcommand{\IdrisM}{\textsc{Idris}$^-$}
34+\newcommand{\TT}{\textsf{TT}}
35+\newcommand{\TTdev}{\textsf{TT$_{dev}$}}
36+\newcommand{\Funl}{\textsc{Funl}}
37+\newcommand{\Agda}{\textsc{Agda}}
38+\newcommand{\LamPi}{$\lambda_\Pi$}
39+
40+\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
41+\begin{center}
42+\fbox{
43+\begin{minipage}{7.5cm}\textbf{Rule \theper:} #1\addtocounter{per}{1}
44+\end{minipage}}
45+\end{center}
46+\vspace*{0.1cm}
47+}
48+
49+\newcommand{\mysubsubsection}[1]{
50+\noindent
51+\textbf{#1}
52+}
53+\newcommand{\hdecl}[1]{\texttt{#1}}
54+
55+
56+\title
57+ {Implementing General Purpose Dependently Typed Programming Languages}
58+%\subtitle{Implementing Domain Specific Languages by Overloading}
59+
60+\author[Edwin Brady]
61+{EDWIN BRADY\\
62+School of Computer Science, University of St Andrews, St Andrews,
63+KY16 9SX, UK}
64+
65+\begin{document}
66+
67+\maketitle
68+
69+\begin{abstract}
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
72+evaluation. How to combine these components into a realistic and usable high
73+level language is, however, folklore, discovered anew by successive
74+language implementations. In this paper, I describe the implementation of a
75+new dependently typed functional programming language, \Idris{}.
76+\Idris{} is intended to be a \emph{general purpose} programming language
77+and as such provides high level concepts such as implicit syntax,
78+type classes and \texttt{do} notation.
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
81+arguments and type classes into a fully explicit type theory. Furthermore,
82+I show how this method,
83+based on a domain specific language embedded in Haskell, facilitates the
84+implementation of new high level language constructs.
85+
86+%I describe the implementation of a dependently typed functional
87+%programming language, \Idris{}. Much has been written about various
88+%aspects of dependently typed language implementation (e.g. checking
89+%dependent types, unification, optimisation) but nothing yet about how
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
92+%concrete syntax with implicit arguments into fully elaborated type
93+%theory, using unification and a tactic engine.
94+\end{abstract}
95+
96+
97+%\category{D.3.2}{Programming Languages}{Language
98+% Classifications}[Applicative (functional) Languages]
99+%\category{D.3.4}{Programming Languages}{Processors}[Compilers]
100+%\terms{Languages, Verification, Performance}
101+%\keywords{Dependent Types, Typechecking}
102+
103+
104+%\begin{bottomstuff}
105+%Author's address: Edwin Brady, School of Computer Science, North Haugh, St Andrews,
106+%KY16 9SX
107+%\end{bottomstuff}
108+
109+\input{intro.tex}
110+
111+%\input{overview.tex}
112+
113+\input{hll.tex}
114+
115+\input{typechecking.tex}
116+
117+%\input{proofstate.tex}
118+
119+\input{elaboration.tex}
120+
121+\input{delab.tex}
122+
123+%\input{compiling.tex}
124+
125+%\input{syntax.tex}
126+
127+\input{conclusions.tex}
128+
129+\section*{Acknowledgements}
130+
131+This work was funded by the Scottish Informatics and Computer Science
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
134+on an earlier draft of this paper.
135+
136+\bibliographystyle{jfp}
137+\bibliography{library.bib}
138+
139+\appendix
140+
141+%\section{TODOs}
142+%\listoftodos{}
143+
144+%\section{Elaboration meta-operations}
145+
146+%It's possible that it would be useful to have a quick reference of meta-operations
147+%used by the elaborator here.
148+
149+%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
150+%$\MO{NewProof}$, $\MO{NewTerm}$,
151+%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
152+
153+%\input{code}
154+
155+\end{document}
rts/idris_stdfgn.c+10−1
@@ -15,6 +15,16 @@ void fileClose(void* h) {
1515 fclose(f);
1616}
1717
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+
1828void fputStr(void* h, char* str) {
1929 FILE* f = (FILE*)h;
2030 fputs(str, f);
@@ -27,4 +37,3 @@ int isNull(void* ptr) {
2737void* idris_stdin() {
2838 return (void*)stdin;
2939}
30−
src/Core/Constraints.hs+61−61
@@ -1,61 +1,61 @@
1−module Core.Constraints(ucheck) where
2−
3−import Core.TT
4−
5−import Control.Applicative
6−import Control.Arrow
7−import Control.Monad.Error
8−import Control.Monad.RWS
9−import Control.Monad.State
10−import Data.List
11−import Data.Maybe
12−import qualified Data.Map as M
13−
14−import Debug.Trace
15−
16−ucheck :: [(UConstraint, FC)] -> TC ()
17−ucheck cs = acyclic rels (map fst (M.toList rels))
18− where lhs (ULT l _) = l
19− lhs (ULE l _) = l
20− rels = mkRels cs M.empty
21−
22−type Relations = M.Map UExp [(UConstraint, FC)]
23−
24−mkRels :: [(UConstraint, FC)] -> Relations -> Relations
25−mkRels [] acc = acc
26−mkRels ((c, f) : cs) acc
27− | not (ignore c)
28− = case M.lookup (lhs c) acc of
29− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
30− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
31− | otherwise = mkRels cs acc
32− where lhs (ULT l _) = l
33− lhs (ULE l _) = l
34− ignore (ULE l r) = l == r
35− ignore _ = False
36−
37−
38−acyclic :: Relations -> [UExp] -> TC ()
39−acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
40− where
41− checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
42− checkCycle fc r path inc [] = return ()
43− checkCycle fc r path inc (c : cs)
44− = do check fc path inc c
45− -- Remove c from r since we know there's no cycles now
46− let r' = M.insert c [] r
47− checkCycle fc r' path inc cs
48−
49− check fc path inc (UVar x) | x < 0 = return ()
50− check fc path inc cv
51− | inc > 0 && cv `elem` map fst path
52− = Error $ At fc UniverseError
53− -- FIXME: Make informative
54− -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
55− | otherwise = case M.lookup cv r of
56− Nothing -> return ()
57− Just cs -> mapM_ (next ((cv, fc):path) inc) cs
58−
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
61−
1+module Core.Constraints(ucheck) where
2+
3+import Core.TT
4+
5+import Control.Applicative
6+import Control.Arrow
7+import Control.Monad.Error
8+import Control.Monad.RWS
9+import Control.Monad.State
10+import Data.List
11+import Data.Maybe
12+import qualified Data.Map as M
13+
14+import Debug.Trace
15+
16+ucheck :: [(UConstraint, FC)] -> TC ()
17+ucheck cs = acyclic rels (map fst (M.toList rels))
18+ where lhs (ULT l _) = l
19+ lhs (ULE l _) = l
20+ rels = mkRels cs M.empty
21+
22+type Relations = M.Map UExp [(UConstraint, FC)]
23+
24+mkRels :: [(UConstraint, FC)] -> Relations -> Relations
25+mkRels [] acc = acc
26+mkRels ((c, f) : cs) acc
27+ | not (ignore c)
28+ = case M.lookup (lhs c) acc of
29+ Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
30+ Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
31+ | otherwise = mkRels cs acc
32+ where lhs (ULT l _) = l
33+ lhs (ULE l _) = l
34+ ignore (ULE l r) = l == r
35+ ignore _ = False
36+
37+
38+acyclic :: Relations -> [UExp] -> TC ()
39+acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
40+ where
41+ checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
42+ checkCycle fc r path inc [] = return ()
43+ checkCycle fc r path inc (c : cs)
44+ = do check fc path inc c
45+ -- Remove c from r since we know there's no cycles now
46+ let r' = M.insert c [] r
47+ checkCycle fc r' path inc cs
48+
49+ check fc path inc (UVar x) | x < 0 = return ()
50+ check fc path inc cv
51+ | inc > 0 && cv `elem` map fst path
52+ = Error $ At fc UniverseError
53+ -- FIXME: Make informative
54+ -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
55+ | otherwise = case M.lookup cv r of
56+ Nothing -> return ()
57+ Just cs -> mapM_ (next ((cv, fc):path) inc) cs
58+
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
61+
src/Pkg/Package.hs+8−14
@@ -5,7 +5,8 @@ import System.Process
55import System.Directory
66import System.Exit
77import System.IO
8−import System.FilePath ((</>), addTrailingPathSeparator)
8+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName)
9+import System.Directory (createDirectoryIfMissing, copyFile)
910
1011import Util.System
1112
@@ -55,10 +56,7 @@ cleanPkg fp
5556 mapM_ rmIBC (modules pkgdesc)
5657 case execout pkgdesc of
5758 Nothing -> return ()
58− Just s -> do let exec = dir </> s
59− putStrLn $ "Removing " ++ exec
60− system $ "rm -f " ++ exec
61− return ()
59+ Just s -> rmFile $ dir </> s
6260
6361installPkg :: PkgDesc -> IO ()
6462installPkg pkgdesc
@@ -92,10 +90,7 @@ testLib warn p f
9290 else fail $ "Missing library " ++ f
9391
9492rmIBC :: Name -> IO ()
95−rmIBC m = do let f = toIBCFile m
96− putStrLn $ "Removing " ++ f
97− system $ "rm -f " ++ f
98− return ()
93+rmIBC m = rmFile $ toIBCFile m
9994
10095toIBCFile (UN n) = n ++ ".ibc"
10196toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))
@@ -106,8 +101,8 @@ installIBC p m = do let f = toIBCFile m
106101 d <- maybe getDataDir return target
107102 let destdir = d </> p </> getDest m
108103 putStrLn $ "Installing " ++ f ++ " to " ++ destdir
109− system $ mkDirCmd ++ destdir
110− system $ "install " ++ f ++ " " ++ destdir
104+ createDirectoryIfMissing True destdir
105+ copyFile f (destdir </> takeFileName f)
111106 return ()
112107 where getDest (UN n) = ""
113108 getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))
@@ -116,8 +111,8 @@ installObj :: String -> String -> IO ()
116111installObj p o = do d <- getDataDir
117112 let destdir = addTrailingPathSeparator (d </> p)
118113 putStrLn $ "Installing " ++ o ++ " to " ++ destdir
119− system $ mkDirCmd ++ destdir
120− system $ "install " ++ o ++ " " ++ destdir
114+ createDirectoryIfMissing True destdir
115+ copyFile o (destdir </> takeFileName o)
121116 return ()
122117
123118#ifdef mingw32_HOST_OS
@@ -135,4 +130,3 @@ clean :: Maybe String -> IO ()
135130clean Nothing = return ()
136131clean (Just s) = do system $ "make -f " ++ s ++ " clean"
137132 return ()
138−
src/Util/System.hs+9−29
@@ -1,8 +1,9 @@
11{-# 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
33
44-- System helper functions.
55
6+import System.Directory (getTemporaryDirectory, removeFile)
67import System.FilePath ((</>), addTrailingPathSeparator, normalise)
78import System.Environment
89import System.IO
@@ -10,11 +11,6 @@ import System.IO
1011import Control.Exception as CE
1112#endif
1213
13−-- import Data.List
14−import Data.List.Split(splitOn)
15−
16−import Paths_idris
17−
1814#if MIN_VERSION_base(4,0,0)
1915catchIO :: IO a -> (IOError -> IO a) -> IO a
2016catchIO = CE.catch
@@ -29,32 +25,16 @@ getCC = do env <- environment "IDRIS_CC"
2925 Just cc -> return cc
3026
3127tempfile :: IO (FilePath, Handle)
32−tempfile = do env <- environment tempDirEnvVar
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
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
28+tempfile = do dir <- getTemporaryDirectory
29+ openTempFile (normalise dir) "idris"
4730
4831environment :: String -> IO (Maybe String)
4932environment x = catchIO (do e <- getEnv x
5033 return (Just e))
5134 (\_ -> return Nothing)
5235
53−getLibFlags = do dir <- getDataDir
54− return $ "-L" ++ (dir </> "rts") ++ " -lidris_rts -lgmp -lpthread"
55−
56−getIdrisLibDir = do dir <- getDataDir
57− return $ addTrailingPathSeparator dir
58−
59−getIncFlags = do dir <- getDataDir
60− return $ "-I" ++ dir </> "rts"
36+rmFile :: FilePath -> IO ()
37+rmFile f = do putStrLn $ "Removing " ++ f
38+ catchIO (removeFile f)
39+ (\ioerr -> putStrLn $ "WARNING: Cannot remove file "
40+ ++ f ++ ", Error msg:" ++ show ioerr)