git.iko.soy/Idris-dev
on master help sign in
Remove old code, tinker with section 4
commit4ae0450580d11f6b4f251465fdc47a4e70957071 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Feb 2013, 18:26 (14 years ago) parent2b3634a
4 files changed+9−10
compare with master
unifiedsplit
papers/impl-paper/elaboration.tex+5−4 papers/impl-paper/hll.tex+2−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+1−5
papers/impl-paper/elaboration.tex+5−4
@@ -902,9 +902,9 @@ are given explicitly, the application must be expanded.
902902
903903\subsection{Elaborating Expressions}
904904
905−\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}
905+\newcommand{\piimp}[2]{\mbox{\texttt{\{$#1$ : $#2$\} -> }}}
906906%\mathtt{\{}#1\mathtt{:}#2\mbox{\texttt{\} -> }}}
907−\newcommand{\piexp}[2]{\mbox{\texttt{( $#1$ : $#2$ ) -> }}}
907+\newcommand{\piexp}[2]{\mbox{\texttt{($#1$ : $#2$) -> }}}
908908%\newcommand{\piexp}[2]{\mathtt{(}#1\mathtt{:}#2\mbox{\texttt{) -> }}}
909909\newcommand{\piconst}[1]{\mbox{\texttt{$#1$ => }}}
910910\newcommand{\icase}{\mathtt{case}}
@@ -992,8 +992,9 @@ are given explicitly, the application must be expanded.
992992{\IdrisM{} declarations}
993993{idrismd}
994994
995−We define a language \IdrisM{}, with expression syntax given in Figure \ref{idrism}
996−and declaration syntax given in Figure \ref{idrismd}.
995+We will use a subset of full \Idris{}, which we call \IdrisM{}, to explain
996+elaboration of expressions. \IdrisM{} expression syntax is given in Figure
997+\ref{idrism} and declaration syntax given in Figure \ref{idrismd}.
997998\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
998999tuple syntax, \texttt{do}-notation or infix operators --- and with implicit
9991000arguments in types bound explicitly
papers/impl-paper/hll.tex+2−1
@@ -12,7 +12,8 @@ covering the most important features. A full tutorial is available elsewhere
1212
1313\subsection{Preliminaries}
1414
15−\Idris{} defines several primitive types: \tTC{Int}, \tTC{Integer} and
15+\Idris{} defines several primitive types: fixed width integers
16+\tTC{Int}, arbitrary width integers \tTC{Integer}, and
1617\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for
1718text manipulation, and \tTC{Ptr} which represents foreign pointers.
1819There are also several data types declared in the library, including
src/Idris/AbsSyntaxTree.hs+1
@@ -524,6 +524,7 @@ type PDo = PDo' PTerm
524524-- The priority gives a hint as to elaboration order. Best to elaborate
525525-- things early which will help give a more concrete type to other
526526-- variables, e.g. a before (interpTy a).
527+-- TODO: priority no longer serves any purpose, drop it!
527528
528529data PArg' t = PImp { priority :: Int,
529530 lazyarg :: Bool, pname :: Name, getTm :: t,
src/Idris/ElabTerm.hs+1−5
@@ -343,12 +343,8 @@ elab ist info pattern tcgen fn tm
343343 ns <- apply (Var f) (map isph args)
344344 ptm <- get_term
345345 g <- goal
346− let (ns', eargs) = unzip $
347− sortBy (\(_,x) (_,y) ->
348− compare (priority x) (priority y))
349− (zip ns args)
350346 elabArgs (ina || not isinf, guarded)
351− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
347+ [] False ns (map (\x -> (lazyarg x, getTm x)) args)
352348 mkSpecialised ist fc f (map getTm args') tm
353349 solve
354350 ptm <- get_term