4ae0450 · Idris-dev · git.iko.soy

papers/impl-paper/elaboration.tex+5−4

compare with master

unifiedsplit

@@ -902,9 +902,9 @@ are given explicitly, the application must be expanded.

902

903\subsection{Elaborating Expressions}

904

905−\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}

905+\newcommand{\piimp}[2]{\mbox{\texttt{\{$#1$ : $#2$\} -> }}}

906%\mathtt{\{}#1\mathtt{:}#2\mbox{\texttt{\} -> }}}

907−\newcommand{\piexp}[2]{\mbox{\texttt{( $#1$ : $#2$ ) -> }}}

907+\newcommand{\piexp}[2]{\mbox{\texttt{($#1$ : $#2$) -> }}}

908%\newcommand{\piexp}[2]{\mathtt{(}#1\mathtt{:}#2\mbox{\texttt{) -> }}}

909\newcommand{\piconst}[1]{\mbox{\texttt{$#1$ => }}}

910\newcommand{\icase}{\mathtt{case}}

@@ -992,8 +992,9 @@ are given explicitly, the application must be expanded.

992{\IdrisM{} declarations}

993{idrismd}

994

995+We will use a subset of full \Idris{}, which we call \IdrisM{}, to explain

995−We define a language \IdrisM{}, with expression syntax given in Figure \ref{idrism}

996+elaboration of expressions. \IdrisM{} expression syntax is given in Figure

996−and declaration syntax given in Figure \ref{idrismd}.

997+\ref{idrism} and declaration syntax given in Figure \ref{idrismd}.

997\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without

998\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without

998tuple syntax, \texttt{do}-notation or infix operators --- and with implicit

999tuple syntax, \texttt{do}-notation or infix operators --- and with implicit

999arguments in types bound explicitly

1000arguments 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

12

13\subsection{Preliminaries}

14

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

16\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for

17\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for

17text manipulation, and \tTC{Ptr} which represents foreign pointers.

18text manipulation, and \tTC{Ptr} which represents foreign pointers.

18There are also several data types declared in the library, including

19There are also several data types declared in the library, including

src/Idris/AbsSyntaxTree.hs+1

@@ -524,6 +524,7 @@ type PDo = PDo' PTerm

524-- The priority gives a hint as to elaboration order. Best to elaborate

525-- things early which will help give a more concrete type to other

526-- variables, e.g. a before (interpTy a).

527+-- TODO: priority no longer serves any purpose, drop it!

527

528

528data PArg' t = PImp { priority :: Int,

529data PArg' t = PImp { priority :: Int,

529 lazyarg :: Bool, pname :: Name, getTm :: t,

530 lazyarg :: Bool, pname :: Name, getTm :: t,

src/Idris/ElabTerm.hs+1−5

@@ -343,12 +343,8 @@ elab ist info pattern tcgen fn tm

343 ns <- apply (Var f) (map isph args)

344 ptm <- get_term

345 g <- goal

346− let (ns', eargs) = unzip $

347− sortBy (\(_,x) (_,y) ->

348− compare (priority x) (priority y))

349− (zip ns args)

350 elabArgs (ina || not isinf, guarded)

346 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)

352 mkSpecialised ist fc f (map getTm args') tm

348 mkSpecialised ist fc f (map getTm args') tm

353 solve

349 solve

354 ptm <- get_term

350 ptm <- get_term