Juillet 2018 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][graveline] Add function syntax support in `plain-let`
by Jonathan Graveline 01 Aoû '18

01 Aoû '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 5c4ba829 by Jonathan Graveline at 2018-07-31T22:47:13Z Add function syntax support in `plain-let` - - - - - 1 changed file: - btl/plain-let.typer Changes: ===================================== btl/plain-let.typer ===================================== @@ -3,6 +3,9 @@ %%%% %%%% normal `let` but not recursive nor sequential %%%% +%%%% (currently handle definition with `_=_`) +%%%% (would declaration be useful ? (e.g. `_:_`)) +%%%% %% List_nth = list.nth; %% List_fold2 = list.fold2; @@ -20,10 +23,19 @@ impl args = let gen-sym arg = let io-serr = lambda _ -> IO_return Sexp_error; + + rename : Sexp -> IO Sexp; + rename sexp = Sexp_dispatch sexp + (lambda _ ss -> do { + name <- gensym (); + IO_return (Sexp_node name ss); + }) + (lambda _ -> gensym ()) + io-serr io-serr io-serr io-serr; in Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then - (gensym ()) else + (rename (List_nth 0 ss Sexp_error)) else (IO_return Sexp_error)) io-serr io-serr io-serr io-serr io-serr; View it on GitLab: https://gitlab.com/monnier/typer/commit/5c4ba82976eced85b5bc2dc5f645babb986… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/5c4ba82976eced85b5bc2dc5f645babb986… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][graveline] `plain-let` with grammar setup
by Jonathan Graveline 31 Jul '18

31 Jul '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: b27dd3ea by Jonathan Graveline at 2018-07-31T17:28:32Z `plain-let` with grammar setup - - - - - 2 changed files: - btl/pervasive.typer - btl/plain-let.typer Changes: ===================================== btl/pervasive.typer ===================================== @@ -541,4 +541,13 @@ do = let lib = load_ "btl/do.typer" in lib.do; case_ = let lib = load_ "btl/case.typer" in lib.case_; +%%%% plain-let + +%% Not recursive and not sequential + +define-operator "plain-let" () 3; +%% define-operator "in" 3 67; + +plain-let_in_ = let lib = load_ "btl/plain-let.typer" in lib.plain-let_in_; + %%% pervasive.typer ends here. ===================================== btl/plain-let.typer ===================================== @@ -4,24 +4,24 @@ %%%% normal `let` but not recursive nor sequential %%%% -io-serr = lambda _ -> IO_return Sexp_error; - -serr = lambda _ -> Sexp_error; - -xserr = lambda _ -> (nil : List Sexp); - -List_nth = list.nth; -List_fold2 = list.fold2; -List_map = list.map; -List_foldl = list.foldl; -List_reverse = list.reverse; -List_tail = list.tail; +%% List_nth = list.nth; +%% List_fold2 = list.fold2; +%% List_map = list.map; +%% List_foldl = list.foldl; +%% List_reverse = list.reverse; +%% List_tail = list.tail; impl : List Sexp -> IO Sexp; impl args = let + serr = lambda _ -> Sexp_error; + gen-sym : Sexp -> IO Sexp; - gen-sym arg = Sexp_dispatch arg + gen-sym arg = let + + io-serr = lambda _ -> IO_return Sexp_error; + + in Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then (gensym ()) else (IO_return Sexp_error)) @@ -88,7 +88,11 @@ impl args = let in let-in (let-decls decls0) (let-in (let-decls decls1) body); get-decls : Sexp -> List Sexp; - get-decls sexp = Sexp_dispatch sexp + get-decls sexp = let + + xserr = lambda _ -> (nil : List Sexp); + + in Sexp_dispatch sexp (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_;_")) then (ss) else (nil)) @@ -105,6 +109,5 @@ in do { plain-let_in_ = macro (lambda args -> do { r <- impl args; - r <- Sexp_debug_print r; IO_return r; }); View it on GitLab: https://gitlab.com/monnier/typer/commit/b27dd3eac7e93842bf21cb341786ac34262… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/b27dd3eac7e93842bf21cb341786ac34262… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] Introduce translation operator; reduce number of assumptions in sec.3 and prove new lemmas instead
by Nathaniel 31 Jul '18

31 Jul '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: 2eb3b210 by nbos at 2018-07-31T15:55:21Z Introduce translation operator; reduce number of assumptions in sec.3 and prove new lemmas instead - - - - - 1 changed file: - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/typer_theory.tex ===================================== @@ -163,14 +163,14 @@ There are two notable differences between explicit and erasable typing rules: \textbf{Notation:} We use a vector notation to refer to an arbitrary countable number of instances of some kind of term, i.e. $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the term vector $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to an $i$ member of the set $\{1,2,3,...,n\}$ for $n = |\vec{N}|$. \begin{definition} -We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. + We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} \begin{definition} -We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: + We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: -$$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$ + $$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$ -Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. + Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. \end{definition} We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: \begin{itemize} @@ -266,20 +266,20 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \end{mathpar} \begin{definition} -A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. + A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. \end{definition} \begin{definition} -The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. The condition $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is determined by structural induction on term $M$: -\begin{align*} - \D_\V\{M\} && = && \text{True} && \text{if } f \notin \fv{M}\\ - \D_\V\{\la (z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ - \D_\V\{(z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ - \D_\V\{\Letrec ?\} && = && \ ? \\ - \D_\V\{\Ind(X\:A)\<\vec{C}\>\} && = && \D_\V\{A\} \land \D_\V\{\vec{C}\} \\ - \D_\V\{f \vec{P}\} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V\{\vec{P}\} \\ - \D_\V\{\Case\ N\:S \text{ of } \<\vec{G}\>\} \todo\\ - \D_\V\{N \vec{P}\} \todo\\ -\end{align*} + The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. The condition $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is determined by structural induction on term $M$: + \begin{align*} + \D_\V\{M\} && = && \text{True} && \text{if } f \notin \fv{M}\\ + \D_\V\{\la (z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{(z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ + \D_\V\{\Letrec ?\} && = && \ ? \\ + \D_\V\{\Ind(X\:A)\<\vec{C}\>\} && = && \D_\V\{A\} \land \D_\V\{\vec{C}\} \\ + \D_\V\{f \vec{P}\} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V\{\vec{P}\} \\ + \D_\V\{\Case\ N\:S \text{ of } \<\vec{G}\>\} \todo\\ + \D_\V\{N \vec{P}\} \todo\\ + \end{align*} \end{definition} \subsection{Conversion Rules} @@ -376,10 +376,17 @@ In this section we will prove that the erasable terms of Typer allow for a repre Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ \CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than, for example, Miquel's definition of \CC\ \cite{miquel}. + \subsection{Translation} +We introduce a translator operator \rew{\ } which is defined on all expressions of our syntax for \CC. We will consider a translation valid if for each context and each typing judgement of \CC, we have the following: +\begin{align} + \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} \~ \\ + \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} \~ \rew{e}:\rew{\tau} +\end{align} +We will proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated type theoric premises by the induction hypothesis and and the translated set theoric premises by an injective map from \CC's to Typer's PTS; we then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. -We set up a correspondance between \CC's and Typer's PTS structures to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: +The correspondance between \CC's and Typer's PTS structures is first defined between the universe hierarchies $\rew{\ } : \S_{CC} \to \S$: \begin{align*} \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \\ \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \\ @@ -387,31 +394,31 @@ We set up a correspondance between \CC's and Typer's PTS structures to allow for \vdots~~~~~ ~~~ &= ~~~ ~~~~~~~\vdots \end{align*} -Axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s. +Then, axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s. -Finally, the translation of a rules in $\R_{CC}$ will translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule +Finally, rules in $\R_{CC}$ translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule \begin{align*} -\rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \\ - &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R + \rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \\ + &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R \end{align*} and conversly, the translation of the impredicative rule \begin{align*} -\rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \\ + \rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \\ &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. \end{align*} -In general, if a product rule of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$. In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product rule will be $s_3 = (s_1 \cup s_2)$. +In general, if a product type of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$ (see Figure 7). In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product type will be $s_3 = (s_1 \cup s_2)$. Thus, the translation of set theoric propositions is the following: \begin{align*} \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \\ \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \\ \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ - \begin{cases} - (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\\[-4pt] - & \text{and $s_2 = \Prop$}\\ - (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} - \end{cases} + \begin{cases} + (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\\[-4pt] + & \text{and $s_2 = \Prop$}\\ + (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} + \end{cases} \end{align*} We define the translation on context recursively: @@ -420,15 +427,6 @@ We define the translation on context recursively: \rew{\Ga, x:e} &\leadsto\ \rew{\Ga}, x:\rew{e} \end{align*} -The translation on terms is the one which maintains the provability of translated judgements: -\begin{align} - \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} \~ \\ - \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} \~ \rew{e}:\rew{\tau} -\end{align} - -We proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. - - \underline{\textbf{Case 1:}} \begin{mathpar} \infer @@ -456,10 +454,22 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. \tag{CC-Wf-S} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} -\end{mathpar} -which allows us to infer the translation of the conclusion by rule +$$\rew{\Ga} \~ \rew{T}:\rew{s}$$ + +and we have that +$$\rew{s \in S_{CC}} \leadsto \rew{s} \in \S.$$ + +We have yet to show that +$$x \notin \dv{\rew{\Ga}}$$ + +\begin{lemma} + The following holds: + $$x \notin \dv{\Ga} \Rightarrow x \notin \dv{\rew{\Ga}}$$ + \begin{proof} + \todo + \end{proof} +\end{lemma} +We can now infer the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} @@ -475,10 +485,12 @@ which allows us to infer the translation of the conclusion by rule \tag{CC-Sort} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} -\end{mathpar} -and reach the translation of the conclusion by rule +$$\rew{\Ga} \~$$ + +and we have that +$$\rew{(s_1:s_2) \in \A_{CC}} \leadsto (\rew{s_1}:\rew{s_2}) \in \A.$$ + +We reach the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} @@ -494,9 +506,16 @@ and reach the translation of the conclusion by rule \tag{CC-Var} \end{mathpar} By the induction hypothesis we can assume -\begin{mathpar} - {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} -\end{mathpar} +$$\rew{\Ga} \~$$ + +\begin{lemma} + The following holds: + $$(x:T) \in \Ga \Rightarrow (x:\rew{T}) \in \rew{\Ga}$$ + \begin{proof} + If $\Ga = \cdot\ $, then the implication is true by the fact that the antecedant is false. Else, if $\Ga = \Delta, (x : T)$, then + \end{proof} +\end{lemma} + and reach the translation of the conclusion by rule \begin{mathpar} \infer @@ -517,8 +536,10 @@ By the induction hypothesis, there are two subcases to consider---a predicative \textbf{Predicative subcase:}\\ We have the assumptions \begin{mathpar} - {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2}} \end{mathpar} +and we know that +$$\rew{(s_1,s_2,s_3) \in \R_{CC}} \leadsto (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ from which we can conclude \begin{mathpar} \infer @@ -530,8 +551,10 @@ from which we can conclude \textbf{Impredicative subcase:}\\ We have the assumptions \begin{mathpar} - {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop}} \end{mathpar} +and we know that +$$\rew{(\Type_i,\Prop,\Prop) \in \R_{CC}} \Rightarrow (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ from which we can conlcude \begin{mathpar} \infer @@ -540,14 +563,14 @@ from which we can conlcude \tag{E-Prod} \end{mathpar} -\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so all translations of product types will follow this rule: -\begin{align*} - \rew{(x:T)\explicit U} \leadsto - \begin{cases} - (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $(T:\Type_i)$} \\ - (x:\rew{T})\explicit \rew{U} & \text{otherwise} - \end{cases} -\end{align*} +\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so we know that all translations of product types will follow the rule: + \begin{align*} + \rew{(x:T)\explicit U} \leadsto + \begin{cases} + (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $(T:\Type_i)$} \\ + (x:\rew{T})\explicit \rew{U} & \text{otherwise} + \end{cases} + \end{align*} \end{remark} \underline{\textbf{Case 6:}\\} @@ -610,7 +633,7 @@ The impredicative product type translates to an erasable product type $(x:\rew{T but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases. \begin{lemma} - By our currently defined translation \rew{\ }, the following holds: \vspace{-5mm} + The following holds: \vspace{-5mm} \end{lemma} \begin{mathpar} \infer @@ -620,12 +643,12 @@ but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of \end{mathpar} \begin{proof} Because we have a well typed erasable product type which can only be constructed by means of rule \textsc{E-Prod}, we can assume under the induction hypothesis that $T:\Type_i$ and that $U:\Prop$. With those additional assumptions, we will show that $x \notin \fv{\rew{M}^*}$ by case analysis on $\rew{M}$. -\begin{align*} - s^* &= s & x^* &= x \\[5pt] - (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\ - (\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt] - (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* -\end{align*} + \begin{align*} + s^* &= s & x^* &= x \\[5pt] + (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\ + (\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt] + (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* + \end{align*} \end{proof} View it on GitLab: https://gitlab.com/monnier/typer/commit/2eb3b21039b42625aefadf9dece27105959… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/2eb3b21039b42625aefadf9dece27105959… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] 2 commits: Add a few theorem-style environments; clean some unused commands
by Nathaniel 31 Jul '18

31 Jul '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: da1e981a by nbos at 2018-07-31T12:36:38Z Add a few theorem-style environments; clean some unused commands - - - - - 42ee60bb by nbos at 2018-07-31T12:39:09Z Begin Lemma 3.1; clean translation format; add theorem-style environments where appropriate - - - - - 2 changed files: - doc/formal/commands.tex - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/commands.tex ===================================== @@ -1,4 +1,14 @@ \renewcommand{\rmdefault}{ptm} +%% Theorems +\newtheorem{theorem}{Theorem}[section] +\newtheorem{lemma}{Lemma}[section] + +\theoremstyle{definition} +\newtheorem{definition}{Definition}[section] + +\theoremstyle{definition} +\newtheorem{remark}{Remark}[section] + %% Defined/Free variables \newcommand{\Dom}[1]{\textsf{Dom}(#1)} @@ -52,11 +62,13 @@ \newcommand{\implicit}{\hspace{\ProdSpace}\Rightarrow\hspace{\ProdSpace}} \newcommand{\erasable}{\hspace{\ProdSpace}\Rrightarrow\hspace{\ProdSpace}} -% \infer options -\mprset {sep=6mm} - % Misc +\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center} + \bf \underline{#1} + \end{center}} + \renewcommand{\tag}[1]{\textsc{(#1)}} +\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}} \newcommand{\emptyctx}{% \mathchoice{\raisebox{1pt}{$\displaystyle\cdot$}} @@ -68,16 +80,9 @@ \newcommand{\app}{\raisebox{1.7pt}{\scalebox{0.8}{$||$}}} \newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}} -\renewcommand{\u}{$\scriptstyle\cup\ $} -\newcommand{\CC}{\text{CC$\omega$}} - -\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center} - \bf \underline{#1} - \end{center}} - \renewcommand{\:}{\hspace{-3pt}:\hspace{-3pt}} \newcommand{\nottype}{/\hspace{-7pt}:} -\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}} +\newcommand{\CC}{\text{CC$\omega$}} \newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} \newcommand{\Tdash}{\vdash_{\hspace{-2pt}_{T}}} \ No newline at end of file ===================================== doc/formal/typer_theory.tex ===================================== @@ -151,7 +151,7 @@ The typing rules for explicit and erasable terms are shown in Figure X. They are \end{figure} -There are two differences between explicit and erasable typing rules: +There are two notable differences between explicit and erasable typing rules: \begin{enumerate} \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$ \item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with incoherent terms. @@ -162,14 +162,16 @@ There are two differences between explicit and erasable typing rules: \subsection{Inductive Definitions} \textbf{Notation:} We use a vector notation to refer to an arbitrary countable number of instances of some kind of term, i.e. $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ..., $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the term vector $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to an $i$ member of the set $\{1,2,3,...,n\}$ for $n = |\vec{N}|$. -\textbf{Definition:} We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. - -\textbf{Definition:} We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: +\begin{definition} +We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. +\end{definition} +\begin{definition} +We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax: $$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~ (\vec{x}:\vec{M})C$$ Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$. - +\end{definition} We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are: \begin{itemize} \renewcommand{\labelitemi}{$-$} @@ -263,9 +265,11 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \textsc{ (Let)} \end{mathpar} -\textbf{Definition:} A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. - -\textbf{Definition:} The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. The condition $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is determined by structural induction on term $M$: +\begin{definition} +A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP\{i,C\}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$. +\end{definition} +\begin{definition} +The \emph{guarded by destructors} condition is written as the predicate $\D_\V\{f,k,x,M\}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V\{M\}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V\{f,k,x,M\}$. We also write $\D_\V\{\vec{M}\}$ instead of $\bigwedge_i \D_\V\{M_i\}$. The condition $\D_\V\{M\} = \D_\V\{f,k,x,M\}$ is determined by structural induction on term $M$: \begin{align*} \D_\V\{M\} && = && \text{True} && \text{if } f \notin \fv{M}\\ \D_\V\{\la (z:P)\to Q\} && = && \D_\V\{P\} \land \D_\V\{Q\} \\ @@ -276,6 +280,7 @@ Recursion is specified through the use of a recursive operator \Letrec \todo \D_\V\{\Case\ N\:S \text{ of } \<\vec{G}\>\} \todo\\ \D_\V\{N \vec{P}\} \todo\\ \end{align*} +\end{definition} \subsection{Conversion Rules} Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $\cong$. [Expand \todo] @@ -372,7 +377,9 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than, for example, Miquel's definition of \CC\ \cite{miquel}. \subsection{Translation} -We set up a correspondance between \CC's and Typer's PTS structures such to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: + + +We set up a correspondance between \CC's and Typer's PTS structures to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: \begin{align*} \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \\ \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \\ @@ -401,7 +408,7 @@ Thus, the translation of set theoric propositions is the following: \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \\ \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ \begin{cases} - (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\\[-4pt] + (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\\[-4pt] & \text{and $s_2 = \Prop$}\\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} \end{cases} @@ -421,11 +428,13 @@ The translation on terms is the one which maintains the provability of translate We proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. -\textbf{Case \textsc{CC-Wf-E}:} + +\underline{\textbf{Case 1:}} \begin{mathpar} \infer {\ } {\emptyctx \CCdash} + \tag{CC-Wf-E} \end{mathpar} The translation is immediately true under Typer by rule \textsc{Wf-E}. \begin{mathpar} @@ -439,17 +448,16 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. \tag{Wf-E} \end{mathpar} -\textbf{Case \textsc{CC-Wf-S}:} +\underline{\textbf{Case 2:}} \begin{mathpar} \infer {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} {\Ga , x:T \CCdash} + \tag{CC-Wf-S} \end{mathpar} By the induction hypothesis we can assume \begin{mathpar} - \infer {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} - {\ } \end{mathpar} which allows us to infer the translation of the conclusion by rule \begin{mathpar} @@ -459,17 +467,16 @@ which allows us to infer the translation of the conclusion by rule \tag{WF-S} \end{mathpar} -\textbf{Case \textsc{CC-Sort}:}\\ +\underline{\textbf{Case 3:}\\} \begin{mathpar} \infer {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} {\Ga \CCdash s_1:s_2} + \tag{CC-Sort} \end{mathpar} By the induction hypothesis we can assume \begin{mathpar} - \infer {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} - {\ } \end{mathpar} and reach the translation of the conclusion by rule \begin{mathpar} @@ -479,17 +486,16 @@ and reach the translation of the conclusion by rule \tag{Sort} \end{mathpar} -\textbf{Case \textsc{CC-Var}:}\\ +\underline{\textbf{Case 4:}\\} \begin{mathpar} \infer {\Ga \CCdash \\ (x:T) \in \Ga} {\Ga \CCdash x:T} + \tag{CC-Var} \end{mathpar} By the induction hypothesis we can assume \begin{mathpar} - \infer {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} - {\ } \end{mathpar} and reach the translation of the conclusion by rule \begin{mathpar} @@ -499,20 +505,19 @@ and reach the translation of the conclusion by rule \tag{Var} \end{mathpar} -\textbf{Case \textsc{CC-Prod}:}\\ +\underline{\textbf{Case 5:}\\} \begin{mathpar} \infer {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} {\Ga \CCdash (x:T) \explicit U : s_3} + \tag{CC-Prod} \end{mathpar} By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one: -\underline{Predicative:}\\ +\textbf{Predicative subcase:}\\ We have the assumptions \begin{mathpar} - \infer {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} - {\ } \end{mathpar} from which we can conclude \begin{mathpar} @@ -522,51 +527,50 @@ from which we can conclude \tag{X-Prod} \end{mathpar} -\underline{Impredicative:}\\ +\textbf{Impredicative subcase:}\\ We have the assumptions \begin{mathpar} - \infer - {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} - {\ } + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} \end{mathpar} from which we can conlcude \begin{mathpar} \infer - {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} \~ \rew{T}:\rew{\Type_i} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} {\rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} \tag{E-Prod} \end{mathpar} -Thus we have that -\begin{align} + +\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so all translations of product types will follow this rule: +\begin{align*} \rew{(x:T)\explicit U} \leadsto \begin{cases} - (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $\neg(T:\Prop)$} \\ + (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $(T:\Type_i)$} \\ (x:\rew{T})\explicit \rew{U} & \text{otherwise} \end{cases} -\end{align} +\end{align*} +\end{remark} -\textbf{Case \textsc{CC-App}:}\\ +\underline{\textbf{Case 6:}\\} \begin{mathpar} \infer {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} {\Ga \CCdash M|N : U\{N/x\}} + \tag{CC-App} \end{mathpar} By the induction hypothesis we can assume \begin{mathpar} - \infer {\rew{\Ga} \~ \rew{M} : \rew{(x:T) \explicit U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} - {\ } \end{mathpar} -And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$ (see (3)): +And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$ (see Remark 3.1): -\underline{Predicative:}\\ +\textbf{Predicative subcase:}\\ \begin{mathpar} \infer {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} {\rew{\Ga} \~ \rew{M}|\rew{N} : \rew{U}\{\rew{N}/x\}} \tag{X-App} \end{mathpar} -\underline{Impredicative:}\\ +\textbf{Impredicative subcase:}\\ \begin{mathpar} \infer {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} @@ -574,21 +578,20 @@ And we again have two subcases to consider for the translation $\rew{(x:T) \expl \tag{E-App} \end{mathpar} -\textbf{Case \textsc{CC-Lam}:}\\ +\underline{\textbf{Case 7:}\\} \begin{mathpar} \infer {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} + \tag{CC-Lam} \end{mathpar} By the induction hypothesis we can assume \begin{mathpar} - \infer {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ \rew{(x:T) \explicit U} : \rew{s}} - {\ } \end{mathpar} -And by (3), we have two subcases to consider for the translation \rew{(x:T) \explicit U}: +And by Remark 3.1, we have two subcases to consider for the translation \rew{(x:T) \explicit U}: -\underline{Predicative:}\\ +\textbf{Predicative subcase:}\\ The predicative product type translates to an explicit product type $(x:\rew{T}) \explicit \rew{U}$ and we apply the explicit \textsc{X-Lam} typing rule to derive the typing of the explicit lambda abstraction. \begin{mathpar} \infer @@ -596,20 +599,37 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) {\rew{\Ga} \~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} \tag{X-Lam} \end{mathpar} -\underline{Impredicative:}\\ -The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ and we apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction. However, an additional premise is required \todo +\textbf{Impredicative subcase:}\\ +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort \Prop\ by Remark 3.1. We would expect to apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction, \begin{mathpar} \infer - {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{s} \\ x \notin \fv{\rew{M}^*}} + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \\ x \notin \fv{\rew{M}^*}} {\rew{\Ga} \~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} \tag{E-Lam} \end{mathpar} +but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases. -\textbf{Lemma:} \todo +\begin{lemma} + By our currently defined translation \rew{\ }, the following holds: \vspace{-5mm} +\end{lemma} +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} + { x \notin \fv{\rew{M}^*}} + \tag{L1} +\end{mathpar} \begin{proof} - + Because we have a well typed erasable product type which can only be constructed by means of rule \textsc{E-Prod}, we can assume under the induction hypothesis that $T:\Type_i$ and that $U:\Prop$. With those additional assumptions, we will show that $x \notin \fv{\rew{M}^*}$ by case analysis on $\rew{M}$. +\begin{align*} + s^* &= s & x^* &= x \\[5pt] + (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \\ + (\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \\[5pt] + (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* +\end{align*} \end{proof} + + \subsection{Example} \newpage View it on GitLab: https://gitlab.com/monnier/typer/compare/b2fdff75dab72f50d5ddf163dbcfcd00a2… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/b2fdff75dab72f50d5ddf163dbcfcd00a2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] 8 commits: `plain-let` (not recursive nor sequential) without grammar yet
by Jonathan Graveline 30 Jul '18

30 Jul '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 572470f8 by Jonathan Graveline at 2018-07-27T05:30:17Z `plain-let` (not recursive nor sequential) without grammar yet - - - - - 84261c57 by Jonathan Graveline at 2018-07-27T06:20:33Z keep count of `insert`/`remove` for faster `length` calculation - - - - - 4d149272 by Jonathan Graveline at 2018-07-27T06:22:26Z use `if ... then ... else ...` syntax where appropriate - - - - - 0ab2e43c by Jonathan Graveline at 2018-07-27T12:39:23Z Minimal built-in functions for unit tests in Typer - - - - - 14f1aafb by Jonathan Graveline at 2018-07-30T20:57:35Z Correction of some unit test primitive (put action in `Vcommand` and set to correct type) New primitive Integer->String (useful with Sexp_dispatch) - - - - - e1917e8b by Jonathan Graveline at 2018-07-30T21:05:01Z Don't print related name with the single character symbol "_" Added boolean operation from samples/bool.typer to pervasive.typer - - - - - 35f6bc54 by Jonathan Graveline at 2018-07-30T21:09:57Z *polyfun.typer: Implicit `case` at function definition level (macro not working if at top-level, but working in `let`) - - - - - a9f1a0dd by Jonathan Graveline at 2018-07-30T21:13:49Z macro for tuple creation and access (more to come) (`_,_` not working yet, temporarily using `_:_`) - - - - - 12 changed files: - btl/builtins.typer - btl/case.typer - btl/do.typer - btl/pervasive.typer - + btl/plain-let.typer - + btl/polyfun.typer - + btl/tuple.typer - samples/bbst.typer - samples/table.typer - src/debruijn.ml - src/eval.ml - src/util.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -134,6 +134,8 @@ Integer_eq = Built-in "Integer.=" : Integer -> Integer -> Bool; Integer_<= = Built-in "Integer.<=" : Integer -> Integer -> Bool; Integer_>= = Built-in "Integer.>=" : Integer -> Integer -> Bool; +Integer->String = Built-in "Integer->String" : Integer -> String; + Float_+ = Built-in "Float.+" : Float -> Float -> Float; Float_- = Built-in "Float.-" : Float -> Float -> Float; Float_* = Built-in "Float.*" : Float -> Float -> Float; @@ -262,4 +264,24 @@ Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; Elab_isconstructor = Built-in "Elab.isconstructor" : String -> Elab_Context -> Bool; +%%%% Unit test helper IO + +%% Print message and/or fail (terminate) +%% These message are registered like any other error + +Test_fatal = Built-in "Test.fatal" : String -> String -> IO Unit; +Test_warning = Built-in "Test.warning" : String -> String -> IO Unit; +Test_info = Built-in "Test.info" : String -> String -> IO Unit; + +%% Get a string representing location of call ("file:line:column") + +Test_location = Built-in "Test.location" : Unit -> String; + +%% Do some test which print a message + +Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; +Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; +Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; +Test_neq = Built-in "Test.neq" : (a : Type) ≡> String -> a -> a -> IO Bool; + %%% builtins.typer ends here. ===================================== btl/case.typer ===================================== @@ -85,7 +85,8 @@ is-dflt : Var -> Bool; is-dflt v = Sexp_eq dflt-var v; %% -%% Get pattern to match +%% Get pattern to match as a List of pair +%% with all patterns and the user code for each branches %% get-branches : List Sexp -> List (Pair Pats Code); @@ -122,9 +123,12 @@ renamed-pat pat names = let mf : Sexp -> Int -> Sexp; mf v i = Sexp_dispatch v - (lambda sym ss -> if_then_else_ (Sexp_eq sym (Sexp_symbol "_:=_")) - (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) - (List_nth i names Sexp_error)) + (lambda sym ss -> + if (Sexp_eq sym (Sexp_symbol "_:=_")) + then + (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) + else + (List_nth i names Sexp_error)) (lambda _ -> List_nth i names Sexp_error) serr serr serr serr; @@ -133,12 +137,6 @@ in return (Sexp_dispatch pat (lambda s -> Sexp_symbol s) serr serr serr serr); -%%% -%%% -%%% -%%% -%%% - %% %% Takes an Sexp as argument and return `IO true` if it is a pattern %% (i.e. a constructor with or without argument) @@ -203,12 +201,7 @@ introduced-vars pat = let (lambda s ss -> do { o <- o; % bind if_then_else_ (Sexp_eq s (Sexp_symbol "_:=_")) - %% (if_then_else_ (Sexp_eq (List_nth 0 ss Var_error) dflt-var) - %% (return (List_concat o (cons dflt-var nil))) (return (List_concat o (cons (List_nth 1 ss Var_error) nil))) - %% there's no introduced variable here - %% `case` on sub pattern will introduce new variable - %% but not here (return (List_concat o (cons dflt-var nil))); }) (lambda s -> do { @@ -288,10 +281,8 @@ in Sexp_dispatch pat return r; }) (lambda sym -> do { - %% %% constructor has no argument %% so there can't be any sub pattern - %% return nil; }) err err err err; @@ -331,10 +322,8 @@ pattern-sub-pats-vars rvars branches = let (return (List_mapi (lambda c n -> let new-sym = List_nth n rvars Var_error; prev-sym = List_nth n psubs dflt-var; - in if_then_else_ (is-dflt c) - (prev-sym) - (new-sym) - ) subs)); + in if_then_else_ (is-dflt c) (prev-sym) (new-sym) + ) subs)); }; in List_foldl ff (return nil) pats; @@ -351,9 +340,11 @@ pattern-term : Pat -> List Var -> IO (List (Pair Var Var)); pattern-term pat rvars = let ff : List (Pair Var Var) -> Var -> Var -> List (Pair Var Var); - ff o v0 v1 = if_then_else_ (is-dflt v0) - (o) - (List_concat o (cons (pair v0 v1) nil)) + ff o v0 v1 = + if (is-dflt v0) then + (o) + else + (List_concat o (cons (pair v0 v1) nil)); in do { ivars <- introduced-vars pat; @@ -372,7 +363,7 @@ in do { part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); %% -%% return a pair of renamed and patitioned pattern +%% return a pair of renamed and partitioned pattern %% (i.e. a Pair of renamed pattern, introduced variables, old pattern and tail of branches) %% (Yeah, I need old pattern to get sub pattern at some point) %% @@ -401,7 +392,7 @@ partition-branches branches = let %% %% Type for first step partition %% - %% Pair of List sorted with similar hd (hd as in `fst`) + %% Pair of List sorted with similar head (head as in first) %% pre-part-type = Pair (List Pat) (List (Pair Pats Code)); @@ -416,18 +407,22 @@ partition-branches branches = let ff o p = case p | pair pat tail => (case o | nil => cons (pair (cons pat nil) (cons tail nil)) nil | cons part parts => (case part | pair ps _ => - if_then_else_ (is-dflt pat) - %% default is both equivalent and different from every pattern? - %% the are merged with `merge-dflt` - (case part | pair pp tt => cons - (pair (List_concat pp (cons pat nil)) - (List_concat tt (cons tail nil))) - (ff parts p)) %% This line sometimes produce too many patterns - (if_then_else_ (is-similar pat (List_nth 0 ps Pat_error)) + + %% default is both equivalent and different from every pattern? + %% they are merged with `merge-dflt` + + if (is-dflt pat) then + (case part | pair pp tt => cons + (pair (List_concat pp (cons pat nil)) + (List_concat tt (cons tail nil))) + (ff parts p)) % This line sometimes produce too many patterns + else + (if (is-similar pat (List_nth 0 ps Pat_error)) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) parts) + else (cons part (ff parts p))))); in List_foldl ff nil hd-pair; @@ -489,20 +484,24 @@ merge-dflt parts odflt = let in case parts | cons part parts => (case part | pair p pp => - (case p | triplet pat _ vars => if_then_else_ (is-dflt pat) - (case odflt - | some dflt => merge-dflt parts (some (append pat vars pp dflt)) - | none => merge-dflt parts (some part)) - (case odflt - %% merge previous default to all branches - | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) - | none => cons part (merge-dflt parts odflt)))) + (case p | triplet pat _ vars => + if (is-dflt pat) then + (case odflt + | some dflt => merge-dflt parts (some (append pat vars pp dflt)) + | none => merge-dflt parts (some part)) + else + (case odflt + %% merge previous default to all branches + | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) + | none => cons part (merge-dflt parts odflt)))) | nil => (case odflt | some dflt => (cons dflt nil) | none => nil); +%% %% takes some branches and preppend default variable to smaller branches - +%% + adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); adjust-len branches = let @@ -511,9 +510,11 @@ adjust-len branches = let ff : Int -> Pair Pats Code -> Int; ff n branch = case branch - | pair pats _ => if_then_else_ (Int_< n (List_length pats)) - (List_length pats) - (n); + | pair pats _ => + if (Int_< n (List_length pats)) then + (List_length pats) + else + (n); in List_foldl ff 0 branches; @@ -521,9 +522,11 @@ adjust-len branches = let preppend-dflt n branch = let sup : Int -> Pats; - sup n = if_then_else_ (Int_eq n 0) - (nil) - (cons dflt-var (sup (n - 1))); + sup n = + if (Int_eq n 0) then + (nil) + else + (cons dflt-var (sup (n - 1))); in case branch | pair pats code => pair (List_concat (sup (n - (List_length pats))) pats) code; @@ -683,9 +686,11 @@ rec-case args = let %% Only the Sexp after "_|_" are interesting case1 : Sexp -> List Sexp -> IO Sexp; - case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) - (case0 ss) - (IO_return Sexp_error); + case1 s ss = + if (Sexp_eq (Sexp_symbol "_|_") s) then + (case0 ss) + else + (IO_return Sexp_error); err = (lambda _ -> IO_return Sexp_error); ===================================== btl/do.typer ===================================== @@ -25,12 +25,10 @@ get-sym sexp = let dflt-sym = (lambda _ -> (Sexp_symbol " %not used% ")); in Sexp_dispatch sexp - - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (s) - (dflt-sym ()) - ) - + (lambda s ss -> if (Sexp_eq (List_nth 0 ss Sexp_error) assign) then + (s) + else + (dflt-sym ())) dflt-sym dflt-sym dflt-sym dflt-sym dflt-sym; % there must be a command @@ -41,9 +39,10 @@ get-op sexp = let helper = (lambda sexp -> Sexp_dispatch sexp - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) - (Sexp_node s ss) + ( lambda s ss -> if (Sexp_eq (List_nth 0 ss Sexp_error) assign) then + (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) + else + (Sexp_node s ss) ) as-is as-is as-is as-is as-is @@ -51,7 +50,7 @@ get-op sexp = let op = (helper sexp); -in if_then_else_ (Sexp_eq op (Sexp_symbol "")) Sexp_error op; +in if (Sexp_eq op (Sexp_symbol "")) then Sexp_error else op; get-decl : List Sexp -> List Sexp; get-decl args = let ===================================== btl/pervasive.typer ===================================== @@ -378,7 +378,7 @@ BoolMod = (##datacons %% %% typecons _ (cons (τ₁ : Type) (t : τ₁) %% (τ₂ : Type) (true : τ₂) - %% (τ₃ : Type) (false : τ₃) + %% (τ₃ : Type) (false : τ₃)) %% %% And it's actually even worse because it tries to generalize %% over the level of those `Type`s, so we end up with an invalid @@ -488,6 +488,28 @@ if_then_else_ | true => uquote e2 | false => uquote e3))); +%%%% More boolean + +%% FIXME: Type annotations should not be needed below. +not : Bool -> Bool; +%% FIXME: We use braces here to delay parsing, otherwise the if/then/else +%% part of the grammar declared above is not yet taken into account. +not x = { if x then false else true }; + +or : Bool -> Bool -> Bool; +or x y = { if x then x else y }; + +and : Bool -> Bool -> Bool; +and x y = { if x then y else x }; + +xor : Bool -> Bool -> Bool; +xor x y = { if x then (not y) else y }; + +%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic, +%% which we don't support in `load` yet. +fold : Bool -> (a : Type) ≡> a -> a -> a; +fold x t e = { if x then t else e}; + %%%% Test test1 : ?; test2 : Option Int; ===================================== btl/plain-let.typer ===================================== @@ -0,0 +1,110 @@ +%%%% +%%%% Macro `plain-let` +%%%% +%%%% normal `let` but not recursive nor sequential +%%%% + +io-serr = lambda _ -> IO_return Sexp_error; + +serr = lambda _ -> Sexp_error; + +xserr = lambda _ -> (nil : List Sexp); + +List_nth = list.nth; +List_fold2 = list.fold2; +List_map = list.map; +List_foldl = list.foldl; +List_reverse = list.reverse; +List_tail = list.tail; + +impl : List Sexp -> IO Sexp; +impl args = let + + gen-sym : Sexp -> IO Sexp; + gen-sym arg = Sexp_dispatch arg + (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then + (gensym ()) else + (IO_return Sexp_error)) + io-serr io-serr io-serr io-serr io-serr; + + get-def : Sexp -> Sexp; + get-def arg = Sexp_dispatch arg + (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then + (List_nth 1 ss Sexp_error) else + (Sexp_error)) + serr serr serr serr serr; + + get-var : Sexp -> Sexp; + get-var arg = Sexp_dispatch arg + (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then + (List_nth 0 ss Sexp_error) else + (Sexp_error)) + serr serr serr serr serr; + + get-sym-def : List Sexp -> IO (List (Pair Sexp Sexp)); + get-sym-def args = do { + r <- List_foldl (lambda o arg -> do { + o <- o; + sym <- gen-sym arg; + def <- IO_return (get-def arg); + IO_return (cons (pair sym def) o); % order doesn't matter + }) (IO_return nil) args; + IO_return r; + }; + + get-var-sym : List Sexp -> List (Pair Sexp Sexp) -> IO (List (Pair Sexp Sexp)); + get-var-sym args syms = let + + ff : IO (List (Pair Sexp Sexp)) -> Pair Sexp Sexp -> Sexp -> IO (List (Pair Sexp Sexp)); + ff o p arg = do { + o <- o; + sym <- IO_return (case p | pair s _ => s); + var <- IO_return (get-var arg); + IO_return (cons (pair var sym) o); + }; + + in do { + r <- List_fold2 ff (IO_return nil) syms args; + IO_return r; + }; + + let-in : Sexp -> Sexp -> Sexp; + let-in decls body = Sexp_node (Sexp_symbol "let_in_") (cons decls (cons body nil)); + + let-decls : List Sexp -> Sexp; + let-decls decls = Sexp_node (Sexp_symbol "_;_") decls; + + gen-code : List (Pair Sexp Sexp) -> List (Pair Sexp Sexp) -> Sexp -> Sexp; + gen-code sym-def var-sym body = let + + mf : Pair Sexp Sexp -> Sexp; + mf p = case p | pair s0 s1 => + Sexp_node (Sexp_symbol "_=_") (cons s0 (cons s1 nil)); + + decls0 = List_map mf sym-def; + + decls1 = List_map mf var-sym; + + in let-in (let-decls decls0) (let-in (let-decls decls1) body); + + get-decls : Sexp -> List Sexp; + get-decls sexp = Sexp_dispatch sexp + (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_;_")) then + (ss) else + (nil)) + xserr xserr xserr xserr xserr; + +in do { + defs <- IO_return (get-decls (List_nth 0 args Sexp_error)); + body <- IO_return (List_nth 1 args Sexp_error); + sym-def <- get-sym-def defs; + sym-def <- IO_return (List_reverse (List_tail sym-def) nil); + var-sym <- get-var-sym defs sym-def; + IO_return (gen-code sym-def var-sym body); +}; + +plain-let_in_ = macro (lambda args -> do { + r <- impl args; + r <- Sexp_debug_print r; + IO_return r; +}); ===================================== btl/polyfun.typer ===================================== @@ -0,0 +1,94 @@ +%%%% +%%%% Polymorphic function +%%%% +%%%% (Just a `case` at function definition level) +%%%% + +serr = lambda _ -> Sexp_error; + +xserr = lambda a ≡> lambda s -> (nil : List a); + +%% List_nth = list.nth; +%% List_map = list.map; +%% List_tail = list.tail; + +%% Not working because of `_=_` and `_;_` +%% I don't know what the right syntax for the declaration to be top-level + +fun-decl : Sexp -> Sexp -> Sexp; +fun-decl decl body = Sexp_node (Sexp_symbol "_;_") (cons (quote ( + (uquote decl) = (uquote body) +)) nil); + +%% Sexp_node (Sexp_symbol "_;_") (cons +%% (Sexp_node (Sexp_symbol "_=_") (cons decl (cons body nil))) +%% nil); + +fun-args : Sexp -> List Sexp; +fun-args decl = Sexp_dispatch decl + (lambda s ss -> let + + mf : Sexp -> Sexp; + mf arg = Sexp_dispatch arg + (lambda s ss -> + if (Sexp_eq s (Sexp_symbol "_:_")) then + (List_nth 0 ss Sexp_error) + else + (Sexp_node s ss)) + (lambda s -> Sexp_symbol s) + serr serr serr serr; + + in List_map mf ss) + xserr xserr xserr xserr xserr; + +fun-cases : List Sexp -> List (Pair (List Sexp) Sexp); +fun-cases args = let + + node2list : Sexp -> List Sexp; + node2list node = Sexp_dispatch node + (lambda s ss -> cons s ss) + xserr xserr xserr xserr xserr; + + mf : Sexp -> Pair (List Sexp) Sexp; + mf arg = let + + err = lambda _ -> pair nil Sexp_error; + + in Sexp_dispatch arg + (lambda s ss -> + if (Sexp_eq s (Sexp_symbol "_=>_")) then + (pair (node2list (List_nth 0 ss Sexp_error)) (List_nth 1 ss Sexp_error)) + else + (err ())) + err err err err err; + +in List_map mf args; + +cases-to-sexp : List Sexp -> List (Pair (List Sexp) Sexp) -> Sexp; +cases-to-sexp vars cases = let + + mf : Pair (List Sexp) Sexp -> Sexp; + mf p = case p | pair xs body => + Sexp_node (Sexp_symbol "_=>_") + (cons (Sexp_node (Sexp_symbol "_,_") xs) + (cons body nil)); + +in Sexp_node (Sexp_symbol "case_") (cons + (Sexp_node (Sexp_symbol "_|_") (cons + (Sexp_node (Sexp_symbol "_,_") vars) + (List_map mf cases))) nil); + +_|_ = macro (lambda args -> let + + decl : Sexp; + decl = List_nth 0 args Sexp_error; + + fargs : List Sexp; + fargs = fun-args decl; + + cases : List (Pair (List Sexp) Sexp); + cases = fun-cases (List_tail args); + +in do { + IO_return (fun-decl decl (cases-to-sexp fargs cases)); +}); ===================================== btl/tuple.typer ===================================== @@ -0,0 +1,137 @@ +%%%% +%%%% macro '_,_' for tuple +%%%% + +%% +%% Sample tuple: a module holding Bool and its constructors. +%% +%% We need the `?` metavars to be lexically outside of the +%% `typecons` expression, otherwise they end up generalized, so +%% we end up with a type constructor like +%% +%% typecons _ (cons (τ₁ : Type) (t : τ₁) +%% (τ₂ : Type) (true : τ₂) +%% (τ₃ : Type) (false : τ₃)) +%% +%% And it's actually even worse because it tries to generalize +%% over the level of those `Type`s, so we end up with an invalid +%% inductive type. +%% +%% BoolMod = (##datacons +%% ((lambda t1 t2 t3 +%% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) +%% ? ? ?) +%% cons) +%% (_ := Bool) (_ := true) (_ := false); +%% + +%% List_nth = list.nth; +%% List_map = list.map; +%% List_mapi = list.mapi; +%% List_map2 = list.map2; +%% List_concat = list.concat; + +%% Move IO outside List (from element to List) +%% (Was helpful for me when translating code that used to not be IO code) +%% (The function's type explain everything) +io-list : List (IO ?a) -> IO (List ?a); +io-list l = let + ff : IO (List ?a) -> IO ?a -> IO (List ?a); + ff o v = do { + o <- o; + v <- v; + IO_return (cons v o); + }; +in do { + l <- (List_foldl ff (IO_return nil) l); + IO_return (List_reverse l nil); +}; + +%% +%% Generate a List of pseudo-unique symbol +%% +%% Takes a List of Sexp and generate a List of new name of the same length +%% whatever are the element of the List +%% + +gen-vars : List Sexp -> IO (List Sexp); +gen-vars vars = io-list (List_map + (lambda _ -> gensym ()) + vars); + +gen-tuple-names : List Sexp -> List Sexp; +gen-tuple-names vars = List_mapi + (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i))) + vars; + +gen-deduce : List Sexp -> List Sexp; +gen-deduce vars = List_map + (lambda _ -> Sexp_symbol "?") + vars; + +make-tuple : List Sexp -> IO Sexp; +make-tuple values = let + + mf1 : Sexp -> Sexp -> Sexp; + mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); + + mf2 : Sexp -> Sexp; + mf2 value = Sexp_node (Sexp_symbol "_:=_") (cons (Sexp_symbol "_") (cons value nil)); + +in do { + args <- gen-vars values; + names <- IO_return (gen-tuple-names values); + fun <- IO_return (Sexp_node (Sexp_symbol "lambda_->_") + (cons (Sexp_node (List_nth 0 args Sexp_error) (List_tail args)) (cons + (Sexp_node (Sexp_symbol "typecons") (cons (Sexp_symbol "_") + (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args)) nil))) + nil)) + ); + call-fun <- IO_return (Sexp_node fun (gen-deduce values)); + tuple <- IO_return (Sexp_node (Sexp_symbol "##datacons") + (cons call-fun (cons (Sexp_symbol "cons") nil))); + affect <- IO_return (Sexp_node tuple (List_map mf2 values)); + IO_return affect; +}; + +_:_ = macro (lambda args -> + make-tuple args +); + +%%% +%%% Access one tuple's element +%%% + +%% tuple_nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type; + +tuple_nth = macro (lambda args -> let + + nerr = lambda _ -> (Int->Integer (-1)); + + n : Integer; + n = Sexp_dispatch (List_nth 1 args Sexp_error) + (lambda _ _ -> nerr ()) + nerr nerr + (lambda n -> n) + nerr nerr; + + elem-sym : Sexp; + elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); + + tup : Sexp; + tup = List_nth 0 args Sexp_error; + +in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) +); + +%%% +%%% Affectation, unwraping tuple +%%% + +%% _=_ = macro (lambda args -> +%% +%% ); + + + + ===================================== samples/bbst.typer ===================================== @@ -23,7 +23,7 @@ type BbsTree (a : Type) %% type Bbst (a : Type) - | bbst (c : a -> a -> Bool) (t : BbsTree a); + | bbst (s : Int) (c : a -> a -> Bool) (t : BbsTree a); %% %% Fold the tree in an unspecified order @@ -55,7 +55,7 @@ fold f o t = let | node-leaf => o; in case t - | bbst c t => helper f o t; + | bbst _ c t => helper f o t; %% %% Fold the tree leftmost element first @@ -89,12 +89,12 @@ foldl f o t = let | node-leaf => o; in case t - | bbst c t => helper f o t; + | bbst _ c t => helper f o t; %% %% Fold the tree rightmost element first %% -%% (If comparator is ">=" then it fold the biggest first) +%% (If comparator is "<=" then it fold the biggest first) %% foldr : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Bbst a -> b; @@ -123,13 +123,17 @@ foldr f o t = let | node-leaf => o; in case t - | bbst c t => helper f o t; + | bbst _ c t => helper f o t; %% %% Get the number of element in the tree %% -length = fold (lambda len _ -> len + 1) 0; +%% length = fold (lambda len _ -> len + 1) 0; + +length : (a : Type) ≡> Bbst a -> Int; +length tree = case tree + | bbst s _ _ => s; %% %% Is the tree empty? @@ -146,6 +150,63 @@ comp-equal comp x y = if_then_else_ (comp x y) (comp y x) (false); +%% +%% Find an element in the tree and return it +%% + +find : (a : Type) ≡> a -> Bbst a -> Option a; +find elem tree = let + + helper : (a -> a -> Bool) -> a -> BbsTree a -> Option a; + helper comp elem tree = case tree + | node2 d0 l0 l1 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (helper comp elem l1) + | node3 d0 d1 l0 l1 l2 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (some d1) + (helper comp elem l1)) + (helper comp elem l2)) + | node4 d0 d1 d2 l0 l1 l2 l3 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (some d1) + (helper comp elem l1)) + (if_then_else_ (comp elem d2) + (if_then_else_ (comp d2 elem) + (some d2) + (helper comp elem l2)) + (helper comp elem l3))) + | node-leaf => none; + +in case tree + | bbst _ c t => helper c elem t; + +%% +%% Is elem in the tree? +%% + +member : (a : Type) ≡> a -> Bbst a -> Bool; +member elem tree = let + + oe = find elem tree; + +in case oe + | some _ => true + | none => false; + %% %% Insert an element in the tree %% @@ -264,8 +325,11 @@ insert elem tree = let | node-leaf => node2 e node-leaf node-leaf; -in case tree - | bbst c t => bbst c (helper c elem t); +in if_then_else_ (member elem tree) + (case tree % we may want to replace an element (partial comparison function) + | bbst s c t => bbst s c (helper c elem t)) + (case tree + | bbst s c t => bbst (s + 1) c (helper c elem t)); %% %% Remove the smallest element. Used in remove. @@ -578,72 +642,17 @@ remove elem tree = let | node-leaf => node-leaf; -in case tree - | bbst c t => bbst c (helper c elem t); - -%% -%% Find an element in the tree and return it -%% - -find : (a : Type) ≡> a -> Bbst a -> Option a; -find elem tree = let - - helper : (a -> a -> Bool) -> a -> BbsTree a -> Option a; - helper comp elem tree = case tree - | node2 d0 l0 l1 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) - (some d0) - (helper comp elem l0)) - (helper comp elem l1) - | node3 d0 d1 l0 l1 l2 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) - (some d0) - (helper comp elem l0)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) - (some d1) - (helper comp elem l1)) - (helper comp elem l2)) - | node4 d0 d1 d2 l0 l1 l2 l3 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) - (some d0) - (helper comp elem l0)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) - (some d1) - (helper comp elem l1)) - (if_then_else_ (comp elem d2) - (if_then_else_ (comp d2 elem) - (some d2) - (helper comp elem l2)) - (helper comp elem l3))) - | node-leaf => none; - -in case tree - | bbst c t => helper c elem t; - -%% -%% Is elem in the tree? -%% - -member : (a : Type) ≡> a -> Bbst a -> Bool; -member elem tree = let - - oe = find elem tree; - -in case oe - | some _ => true - | none => false; +in if_then_else_ (member elem tree) + (case tree + | bbst s c t => bbst (s - 1) c (helper c elem t)) + (tree); %% %% An empty tree with a key compare function as argument %% empty : (a : Type) ≡> (a -> a -> Bool) -> Bbst a; -empty comp-fun = bbst comp-fun node-leaf; +empty comp-fun = bbst 0 comp-fun node-leaf; %%% %%% Test helper ===================================== samples/table.typer ===================================== @@ -19,7 +19,7 @@ type TableTree (a : Type) | table-nil; type Table (a : Type) - | table (c : a -> a -> Bool) (h : a -> Int) (t : TableTree a); + | table (s : Int) (c : a -> a -> Bool) (h : a -> Int) (t : TableTree a); %% %% fold left in an unspecified order @@ -38,7 +38,7 @@ foldl f o t = let | table-nil => o; in case t - | table _ _ t => helper f o t; + | table _ _ _ t => helper f o t; %% %% Get the number of element in the tree @@ -47,9 +47,13 @@ in case t %% (currently O(n)) %% -length t = let - fold-fun len _ = len + 1; -in foldl fold-fun 0 t; +%% length t = let +%% fold-fun len _ = len + 1; +%% in foldl fold-fun 0 t; + +length : (a : Type) ≡> Table a -> Int; +length t = case t + | table s _ _ _ => s; %% %% Is the tree empty? @@ -57,6 +61,40 @@ in foldl fold-fun 0 t; is-empty t = Int_eq (length t) 0; +%% +%% Find an element in the tree and return it +%% + +find : (a : Type) ≡> a -> Table a -> Option a; +find elem tree = let + + get : a -> (a -> a -> Bool) -> List a -> Option a; + get e c es = case es + | cons e1 es => if_then_else_ (c e e1) (some e1) (get e c es) + | nil => none; + + helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Option a; + helper e c h t = case t + | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) + (helper e c (Int_lsr h 1) l) + (helper e c (Int_lsr h 1) r) + | table-leaf h1 es => if_then_else_ (Int_eq h h1) + (get e c es) + (none) % element not found + | table-nil => none; % element not found + +in case tree + | table _ c h t => (helper elem c (h elem) t); + +%% +%% Is this element in the tree? +%% + +member : (a : Type) ≡> a -> Table a -> Bool; +member elem tree = case (find elem tree) + | some _ => true + | none => false; + %% %% Insert an element in the tree %% @@ -85,8 +123,11 @@ insert elem tree = let (table-node table-nil (table-leaf (Int_lsr h1 1) es)))) | table-nil => table-leaf h (cons e nil); -in case tree - | table c h t => table c h (helper elem c (h elem) t); +in if_then_else_ (member elem tree) + (case tree % we may want to replace a variable (partial comparison function) + | table s c h t => table s c h (helper elem c (h elem) t)) + (case tree + | table s c h t => table (s + 1) c h (helper elem c (h elem) t)); %% %% Remove an element from the tree. @@ -125,8 +166,10 @@ remove elem tree = let (table-leaf h1 es) % element not found | table-nil => table-nil; % element not found -in case tree - | table c h t => table c h (helper elem c (h elem) t); +in if_then_else_ (member elem tree) + (case tree + | table s c h t => table (s - 1) c h (helper elem c (h elem) t)) + (tree); %% %% Change an element @@ -140,62 +183,12 @@ in case tree update : (a : Type) ≡> a -> Table a -> Table a; update elem tree = insert elem tree; % used to be more complicated -%% -%% Is this element in the tree? -%% - -member : (a : Type) ≡> a -> Table a -> Bool; -member elem tree = let - - is-in : a -> (a -> a -> Bool) -> List a -> Bool; - is-in e c es = case es - | cons e1 es => if_then_else_ (c e e1) (true) (is-in e c es) - | nil => false; - - helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Bool; - helper e c h t = case t - | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) - (helper e c (Int_lsr h 1) l) - (helper e c (Int_lsr h 1) r) - | table-leaf h1 es => if_then_else_ (Int_eq h h1) - (is-in e c es) - (false) % element not found - | table-nil => false; % element not found - -in case tree - | table c h t => (helper elem c (h elem) t); - -%% -%% Find an element in the tree and return it -%% - -find : (a : Type) ≡> a -> Table a -> Option a; -find elem tree = let - - get : a -> (a -> a -> Bool) -> List a -> Option a; - get e c es = case es - | cons e1 es => if_then_else_ (c e e1) (some e1) (get e c es) - | nil => none; - - helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Option a; - helper e c h t = case t - | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) - (helper e c (Int_lsr h 1) l) - (helper e c (Int_lsr h 1) r) - | table-leaf h1 es => if_then_else_ (Int_eq h h1) - (get e c es) - (none) % element not found - | table-nil => none; % element not found - -in case tree - | table c h t => (helper elem c (h elem) t); - %% %% An empty tree with a key compare function and a key hash function as argument %% empty : (a : Type) ≡> (a -> a -> Bool) -> (a -> Int) -> Table a; -empty comp-fun hash-fun = table comp-fun hash-fun table-nil; +empty comp-fun hash-fun = table 0 comp-fun hash-fun table-nil; %%% %%% Test helper ===================================== src/debruijn.ml ===================================== @@ -151,7 +151,8 @@ let _get_related_name (n : db_ridx) name map = ps ) map [] in if ((String.sub name 0 1) = "_" || - (String.sub name ((String.length name) - 1) 1) = "_") then + (String.sub name ((String.length name) - 1) 1) = "_") && + ((String.length name) > 1) then search r else [] ===================================== src/eval.ml ===================================== @@ -129,6 +129,8 @@ let ttrue = Vcons ((dloc, "true"), []) let tfalse = Vcons ((dloc, "false"), []) let o2v_bool b = if b then ttrue else tfalse +let tunit = Vcons ((dloc, "()"), []) + (* * Builtins *) @@ -669,11 +671,15 @@ let io_return loc depth args_val = match args_val with let float_to_string loc depth args_val = match args_val with | [Vfloat x] -> Vstring (string_of_float x) - | _ -> error loc "Float->String expects one Float arg" + | _ -> error loc "Float->String expects one Float argument" let int_to_string loc depth args_val = match args_val with | [Vint x] -> Vstring (string_of_int x) - | _ -> error loc "Int->String expects one Int arg" + | _ -> error loc "Int->String expects one Int argument" + +let integer_to_string loc depth args_val = match args_val with + | [Vinteger x] -> Vstring (BI.string_of_big_int x) + | _ -> error loc "Integer->String expects one Integer argument" let sys_exit loc depth args_val = match args_val with | [Vint n] -> Vcommand (fun _ -> exit n) @@ -710,7 +716,7 @@ let ref_read loc depth args_val = match args_val with let ref_write loc depth args_val = match args_val with | [value; Vref (actual)] -> - Vcommand (fun () -> actual := value; Vcons ((dloc,"()"),[])) + Vcommand (fun () -> actual := value; tunit) | _ -> error loc "Ref.write takes a value and a Ref as argument" let gensym = let count = ref 0 in @@ -793,6 +799,67 @@ let array_empty loc depth args_val = match args_val with | [_] -> Varray (Array.make 0 Vundefined) | _ -> error loc "Array.empty takes a Unit as single argument" +let test_fatal loc depth args_val = match args_val with + | [Vstring section; Vstring msg] -> + Vcommand (fun () -> Util.msg_user_fatal section loc msg; + tunit) + | _ -> error loc "Test.fatal takes two String as argument" + +let test_warning loc depth args_val = match args_val with + | [Vstring section; Vstring msg] -> + Vcommand (fun () -> Util.msg_user_warning section loc msg; + tunit) + | _ -> error loc "Test.warning takes two String as argument" + +let test_info loc depth args_val = match args_val with + | [Vstring section; Vstring msg] -> + Vcommand (fun () -> Util.msg_user_info section loc msg; + tunit) + | _ -> error loc "Test.info takes two String as argument" + +let test_location loc depth args_val = match args_val with + | [_] -> Vstring (loc.file ^ ":" ^ string_of_int loc.line + ^ ":" ^ string_of_int loc.column) + | _ -> error loc "Test.location takes a Unit as argument" + +let test_true loc depth args_val = match args_val with + | [Vstring name; Vcons ((dloc, b), [])] -> + if b = "true" then + Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); + ttrue) + else + Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); + tfalse) + | _ -> error loc "Test.true takes a String and a Bool as argument" + +let test_false loc depth args_val = match args_val with + | [Vstring name; Vcons ((dloc, b), [])] -> + if b = "false" then + Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); + ttrue) + else + Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); + tfalse) + | _ -> error loc "Test.false takes a String and a Bool as argument" + +let test_eq loc depth args_val = match args_val with + | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then + Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); + ttrue) + else + Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); + tfalse) + | _ -> error loc "Test.eq takes a String and two values as argument" + +let test_neq loc depth args_val = match args_val with + | [Vstring name; v0; v1] -> if Env.value_equal v0 v1 then + Vcommand (fun () -> print_string ("[FAIL] "^name^"\n"); + tfalse) + else + Vcommand (fun () -> print_string ("[ OK] "^name^"\n"); + ttrue) + | _ -> error loc "Test.neq takes a String and two values as argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -811,6 +878,7 @@ let register_builtin_functions () = ("Sexp.debug_print", sexp_debug_print, 1); ("Float->String" , float_to_string, 1); ("Int->String" , int_to_string, 1); + ("Integer->String", integer_to_string, 1); ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); @@ -834,6 +902,14 @@ let register_builtin_functions () = ("Array.set" , array_set,3); ("Array.get" , array_get,3); ("Array.empty" , array_empty,1); + ("Test.fatal" , test_fatal,2); + ("Test.warning" , test_warning,2); + ("Test.info" , test_info,2); + ("Test.location" , test_location,1); + ("Test.true" , test_true,2); + ("Test.false" , test_false,2); + ("Test.eq" , test_eq,3); + ("Test.neq" , test_neq,3); ] let _ = register_builtin_functions () ===================================== src/util.ml ===================================== @@ -63,6 +63,9 @@ let internal_error s = raise (Internal_error s) exception Unreachable_error of string let typer_unreachable s = raise (Unreachable_error s) +exception User_error of string +let user_error s = raise (User_error s) + exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s) @@ -137,6 +140,15 @@ let msg_error = msg_message true 1 "Error:" let msg_warning = msg_message false 2 "Warning:" let msg_info = msg_message false 3 "Info:" +let msg_user_fatal s l m = + msg_message true 1 "Unit test (fatal):" s l m; + flush stdout; + reset_error_log (); + user_error "User Fatal Error" + +let msg_user_warning = msg_message false 2 "Unit test (warning):" +let msg_user_info = msg_message false 3 "Unit test (info):" + (* Compiler Internal Debug print *) let debug_msg expr = if 4 <= !typer_verbose then (print_string expr; flush stdout) else () View it on GitLab: https://gitlab.com/monnier/typer/compare/b0b911ec7fcc4cebd576ebff4815f39d2d… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/b0b911ec7fcc4cebd576ebff4815f39d2d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][bosn] 4 commits: Cleaned text; fixed translation to account for new rules of CCw
by Nathaniel 30 Jul '18

30 Jul '18

Nathaniel pushed to branch bosn at Stefan / Typer Commits: 26b5c9c8 by nbos at 2018-07-27T02:27:37Z Cleaned text; fixed translation to account for new rules of CCw - - - - - 25024193 by nbos at 2018-07-30T08:11:16Z New commands; removed unecesary math layer in sans keywords - - - - - 618d6ae9 by nbos at 2018-07-30T08:15:13Z Restructured whole proof of extention of CCω - - - - - b2fdff75 by nbos at 2018-07-30T09:59:21Z Added room for special case E-Lam - - - - - 2 changed files: - doc/formal/commands.tex - doc/formal/typer_theory.tex Changes: ===================================== doc/formal/commands.tex ===================================== @@ -6,20 +6,24 @@ \newcommand{\fv}[1]{\textsf{FV}(#1)} %% Sans -\newcommand{\Ind}{\ensuremath{\mathsf{Ind}}} -\newcommand{\Constr}{\ensuremath{\mathsf{Constr}}} -\newcommand{\Case}{\ensuremath{\mathsf{Case}}} -\newcommand{\Elim}{\ensuremath{\mathsf{Elim}}} -\newcommand{\Fix}{\ensuremath{\mathsf{Fix}}} -\newcommand{\Letrec}{\ensuremath{\mathsf{Letrec}}} -\newcommand{\Let}{\ensuremath{\mathsf{Let}}} -\newcommand{\In}{\ensuremath{\mathsf{in}}} - -\newcommand{\Prop}{\ensuremath{\mathsf{Prop}}} -\newcommand{\Type}{\ensuremath{\mathsf{Type}}} -\newcommand{\TypeLevel}{\ensuremath{\mathsf{TypeLevel}}} +\newcommand{\Ind}{\textsf{Ind}} +\newcommand{\Constr}{\textsf{Constr}} +\newcommand{\Case}{\textsf{Case}} +\newcommand{\Elim}{\textsf{Elim}} +\newcommand{\Fix}{\textsf{Fix}} +\newcommand{\Letrec}{\textsf{Letrec}} +\newcommand{\Let}{\textsf{Let}} +\newcommand{\In}{\textsf{in}} + +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\TypeLevel}{\textsf{TypeLevel}} +\newcommand{\SortL}{\textsf{SortL}} +\newcommand{\Sort}{\textsf{Sort}} +\newcommand{\z}{\textsf{z}} +\newcommand{\s}{\textsf{s}} + \newcommand{\Sortw}{\ensuremath{\mathsf{Sort}_\omega}} -\newcommand{\SortL}{\ensuremath{\mathsf{SortL}}} % Bolds \newcommand{\todo}{\textbf{ TODO }} @@ -72,5 +76,8 @@ \end{center}} \renewcommand{\:}{\hspace{-3pt}:\hspace{-3pt}} +\newcommand{\nottype}{/\hspace{-7pt}:} +\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}} -\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} \ No newline at end of file +\newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}} +\newcommand{\Tdash}{\vdash_{\hspace{-2pt}_{T}}} \ No newline at end of file ===================================== doc/formal/typer_theory.tex ===================================== @@ -1,7 +1,7 @@ \documentclass[10pt]{article} % \usepackage[a4paper,margin=1in,footskip=0.25in]{geometry} -\usepackage{amsmath,amsthm,amssymb,mathtools} +\usepackage{amsmath,amsthm,amssymb,mathtools,stmaryrd} \usepackage{mathpartir,mdframed,empheq} \usepackage{parskip,authblk} @@ -43,7 +43,7 @@ We here formalize the Typer language and prove some of its properties. The gist \end{figure} \subsection{Universes and Universe Polymorphism} -Each type universe $\mathsf{Type}\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ %% FIXME: We'll need somewhere to clarify that those `l`s have to be present %% in the Γ environment with type TypeLevel. All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs and thus contains a type level $\l \in \mathbb{L}$ for every conventional natural number $n \in \mathbb{N}$. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. @@ -53,12 +53,12 @@ We have that \Sortw\ is the unique sort of all the types of universe polymorphic \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \\ - \S = \{ & \mathsf{SortL};\ \mathsf{Sort}_\omega;\ \mathsf{Type } \l\} &\forall\l \in \mathbb{L} \\[9pt] - \A = \{ &(\mathsf{TypeLevel} : \mathsf{SortL}); \\ - &(\mathsf{Type}\ \l : \mathsf{Type}\ (\mathsf{s}\ \l))\} &\forall\l \in \mathbb{L} \\[9pt] - \R = \{ &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \\ - &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \\ - &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ (\l_1 \cup \l_2))\} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] + \S = \{ & \SortL;\ \Sortw;\ \Type\ \l\} &\forall\l \in \mathbb{L} \\[9pt] + \A = \{ &(\TypeLevel : \SortL); \\ + &(\Type\ \l : \Type\ (\mathsf{s}\ \l))\} &\forall\l \in \mathbb{L} \\[9pt] + \R = \{ &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \\ + &(\SortL,\ \Sortw,\ \Sortw); \\ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ (\l_1 \cup \l_2))\} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Pure Type System} @@ -68,9 +68,9 @@ Because of the impredicativity of the erasable part of Typer, we need to define \begin{figure}[h] \begin{empheq}[box=\fbox]{align*} \hspace{15mm} & \ & \ & \hspace{7mm} \\ - \R_e = \{ &(\mathsf{SortL},\ \mathsf{Type}\ \l,\ \mathsf{Sort}_\omega); &\forall\l \in \mathbb{L} \\ - &(\mathsf{SortL},\ \mathsf{Sort}_\omega,\ \mathsf{Sort}_\omega); \\ - &(\mathsf{Type}\ \l_1,\ \mathsf{Type}\ \l_2,\ \mathsf{Type}\ \l_2) \} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] + \R_e = \{ &(\SortL,\ \Type\ \l,\ \Sortw); &\forall\l \in \mathbb{L} \\ + &(\SortL,\ \Sortw,\ \Sortw); \\ + &(\Type\ \l_1,\ \Type\ \l_2,\ \Type\ \l_2) \} &\forall\l_1,\l_2 \in \mathbb{L}\\[-4pt] \end{empheq} \vspace{-5mm} \caption{Typer's Impredicative Rules} @@ -176,7 +176,7 @@ We extend our abstract syntax with four terms introduced in \cite{gimenez} to ex \setlength\itemsep{-3pt} \item $\Ind(X:A) \<\vec{C}\>$ which is an inductively defined type recursively bound to $X$. $\vec{C}$ is the list of constructor signatures which must be a \emph{form of constructor} w.r.t. $X$. \item $\Constr(i:I)$ stands for the $i$th constructor of an inductive type $I$. -\item $\mathsf{Case}\ M\: S \text{ of } \<\vec{G}\>$ which is the function by case analysis on the expression $M$ of type $S$ and where $\<\vec{G}\>$ is the list of cases, represented as abstractions of the respective patterns of constructions. +\item $\Case\ M\: S \text{ of } \<\vec{G}\>$ which is the function by case analysis on the expression $M$ of type $S$ and where $\<\vec{G}\>$ is the list of cases, represented as abstractions of the respective patterns of constructions. \end{itemize} The typing rules for inductive definitions and case analysis are presented in Figure X. @@ -215,9 +215,9 @@ The typing rules for inductive definitions and case analysis are presented in Fi %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq_refl : ((x : ?t) ≡> Eq x x); %% Eq_cast : (x : ?t) ≡> (y : ?t) - %% ≡> (p : Eq x y) - %% ≡> (f : ?t -> ?t') - %% ≡> f x -> f y; + %% ≡> (p : Eq x y) + %% ≡> (f : ?t -> ?t') + %% ≡> f x -> f y; %% %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce %% to `x`), but there is no corresponding normalization rule applied @@ -244,7 +244,7 @@ The typing rules for inductive definitions and case analysis are presented in Fi \Ga \stackrel{\forall i \in |\vec{G}|}{\~} G_i:Q} %% FIXME: Similarly, here, the return type is just Q with no `\vec{P}` %% nor `M` argument. - {\Ga \~ \Case\ M:(I\ \vec{P}) \text{ of } \<\vec{G}\> : (Q \vec{P} M)} + {\Ga \~ \Case\ M:(I\ \vec{P}) \text{ of } \<\vec{G}\> : Q} \textsc{ (Case)} \end{mathpar} } @@ -305,7 +305,7 @@ Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $ \caption{Typer's Conversion Rules} \end{figure} -\section{Relative Expressivity to the Calculus of Constructions} +\section{Typer as an Extention of a Calculus of Constructions} In this section we will prove that the erasable terms of Typer allow for a representation of all typing derivations from a Calculus of Constructions with an impredicative $\mathsf{Prop}$ and an infinite hierarchy of predicative universes (\CC). \subsection{Definition of \CC} @@ -368,38 +368,249 @@ In this section we will prove that the erasable terms of Typer allow for a repre \caption{\CC's Typing Rules} \end{figure} -Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above the impredicative $\mathsf{Prop}$. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4...$$ +Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$ \CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than, for example, Miquel's definition of \CC\ \cite{miquel}. \subsection{Translation} - By induction on typing derivation steps. - \textsc{CC-Wf-E} and \textsc{CC-Var} both directly translate to \textsc{Wf-E} and \textsc{Var} respectively since they introduce nothing new. Because \textsc{CC-Sort} and \textsc{CC-Wf-S} call upon $\A_{CC}$ and $\S_{CC}$, we make a mapping between the universe hierarchies $\S_{CC} \to \S$: - \begin{align*} - \mathsf{Prop} ~~~ &\mapsto ~~~ \mathsf{Type\ z} \\ - \mathsf{Type_1} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ z)} \\ - \mathsf{Type_2} ~~~ &\mapsto ~~~ \mathsf{Type\ (s\ (s\ z))} \\ - \vdots~~~~~ ~~~ &\mapsto ~~~ ~~~~~~~\vdots - \end{align*} +We set up a correspondance between \CC's and Typer's PTS structures such to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$: +\begin{align*} + \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \\ + \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \\ + \rew{\Type_2} ~~~ &= ~~~ \Type\ \mathsf{(s\ (s\ z))} \\ + \vdots~~~~~ ~~~ &= ~~~ ~~~~~~~\vdots +\end{align*} - And axioms of $\A_{CC}$ become axioms of $\A$ by the translation of respective sorts, e.g. $\mathsf{(Prop : Type_1)}$ becomes $\mathsf{(Type\ z : Type\ (s\ z))}$. +Axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s. - The typing rule \textsc{CC-Prod} calls upon the set of product rules $\R_{CC}$ which is analogous to both $\R$ and $\R_e$ at the same time. In particular, the first product rule scheme $$(\mathsf{Type}_i, \mathsf{Prop}, \mathsf{Prop}) \in R_{CC}$$ translates to - $$(\mathsf{Type}\ \l_, \mathsf{Type\ z}, \mathsf{Type\ z}) \in \R_e ~~~~~~ \forall \l \in \mathbb{L}$$ - and the second product rule scheme $$(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i) \in R_{CC}$$ is a special case of - $$(\mathsf{Type}\ \l_1, \mathsf{Type}\ \l_2, \mathsf{Type}\ (\l_1 \cup \l_2))\} \in \R ~~~~~~ \forall\l_1,\l_2 \in \mathbb{L}$$ - specifically when $\l_1 = \l_2$. Thus, use of the typing rule \textsc{CC-Prod} translate to use of \textsc{X-Prod} when a rule is of form $(\mathsf{Type}_i, \mathsf{Type}_i, \mathsf{Type}_i)$ and the resulting dependent product in Typer is explicit. \textsc{CC-Prod} translates to \textsc{E-Prod} when of form $(\Type_i, \Prop, \Prop)$.\\ +Finally, the translation of a rules in $\R_{CC}$ will translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule +\begin{align*} +\rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \\ + &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R +\end{align*} -As for \textsc{CC-Lam} and \textsc{CC-App}, depending on whether the product type in the premises has already been translated as either explicit or erasable, the corresponding typing rules will apply, i.e. \textsc{X-Lam} and \textsc{X-App} if explicit or \textsc{E-Lam} and \textsc{E-App} if erasable. +and conversly, the translation of the impredicative rule +\begin{align*} +\rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \\ + &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. +\end{align*} +In general, if a product rule of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$. In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product rule will be $s_3 = (s_1 \cup s_2)$. -\subsection{Example} -Suppose the following typing judgement on a universe polymorphic $\mathsf{pair}$ type in the \CC\ language. +Thus, the translation of set theoric propositions is the following: \begin{align*} - \~ \quad & \la (t_1 : \Type_1) \explicit \la (t_2 : \Type_1) \explicit \la (x:t_1) \explicit \la (y:t_2) \explicit \la (t:\Prop) \explicit \\ - & \la (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y \\[5pt] - & \hspace{-9pt}: (t_1 : \Type_1) \explicit (t_2 : \Type_1) \explicit (x:t_1) \explicit (y:t_2) \explicit (t:\Prop) \explicit \\ - & (f:t_1\explicit t_2\explicit t) \explicit f\ x\ y + \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \\ + \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \\ + \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ + \begin{cases} + (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\\[-4pt] + & \text{and $s_2 = \Prop$}\\ + (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} + \end{cases} \end{align*} -The derivation by which we arrive to this typing judgement \todo + +We define the translation on context recursively: +\begin{align*} + \rew{\cdot} &\leadsto\ \cdot \\ + \rew{\Ga, x:e} &\leadsto\ \rew{\Ga}, x:\rew{e} +\end{align*} + +The translation on terms is the one which maintains the provability of translated judgements: +\begin{align} + \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} \~ \\ + \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} \~ \rew{e}:\rew{\tau} +\end{align} + +We proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. + +\textbf{Case \textsc{CC-Wf-E}:} +\begin{mathpar} + \infer + {\ } + {\emptyctx \CCdash} +\end{mathpar} +The translation is immediately true under Typer by rule \textsc{Wf-E}. +\begin{mathpar} + \infer + {\ } + {\rew{\cdot} \~} + ~~~ \leadsto ~~~ + \infer + {\ } + {\cdot \~} + \tag{Wf-E} +\end{mathpar} + +\textbf{Case \textsc{CC-Wf-S}:} +\begin{mathpar} + \infer + {\Ga \CCdash T:s \\ s \in \S_{CC} \\ x \notin \dv{\Ga}} + {\Ga , x:T \CCdash} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} + {\ } +\end{mathpar} +which allows us to infer the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s} \\ \rew{s} \in \S \\ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} , x:\rew{T} \~} + \tag{WF-S} +\end{mathpar} + +\textbf{Case \textsc{CC-Sort}:}\\ +\begin{mathpar} + \infer + {\Ga \CCdash \\ (s_1:s_2) \in \A_{CC}} + {\Ga \CCdash s_1:s_2} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} + {\ } +\end{mathpar} +and reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (\rew{s_1}:\rew{s_2}) \in \A} + {\rew{\Ga} \~ \rew{s_1}:\rew{s_2}} + \tag{Sort} +\end{mathpar} + +\textbf{Case \textsc{CC-Var}:}\\ +\begin{mathpar} + \infer + {\Ga \CCdash \\ (x:T) \in \Ga} + {\Ga \CCdash x:T} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} + {\ } +\end{mathpar} +and reach the translation of the conclusion by rule +\begin{mathpar} + \infer + {\rew{\Ga} \~ \\ (x:\rew{T}) \in \rew{\Ga}} + {\rew{\Ga} \~ x:\rew{T}} + \tag{Var} +\end{mathpar} + +\textbf{Case \textsc{CC-Prod}:}\\ +\begin{mathpar} + \infer + {\Ga \CCdash T:s_1 \\ \Ga, x:T \CCdash U:s_2 \\ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} +\end{mathpar} +By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one: + +\underline{Predicative:}\\ +We have the assumptions +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\ } +\end{mathpar} +from which we can conclude +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{s_2} \\ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} + {\rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} + \tag{X-Prod} +\end{mathpar} + +\underline{Impredicative:}\\ +We have the assumptions +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\ } +\end{mathpar} +from which we can conlcude +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{T}:\rew{s_1} \\ \rew{\Ga}, x:\rew{T} \~ \rew{U}:\rew{\Prop} \\ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e} + {\rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} + \tag{E-Prod} +\end{mathpar} +Thus we have that +\begin{align} + \rew{(x:T)\explicit U} \leadsto + \begin{cases} + (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $\neg(T:\Prop)$} \\ + (x:\rew{T})\explicit \rew{U} & \text{otherwise} + \end{cases} +\end{align} + +\textbf{Case \textsc{CC-App}:}\\ +\begin{mathpar} + \infer + {\Ga \CCdash M : (x:T) \explicit U \\ \Ga \CCdash N:T} + {\Ga \CCdash M|N : U\{N/x\}} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : \rew{(x:T) \explicit U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\ } +\end{mathpar} +And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$ (see (3)): + +\underline{Predicative:}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{X-App} +\end{mathpar} +\underline{Impredicative:}\\ +\begin{mathpar} + \infer + {\rew{\Ga} \~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \\ \rew{\Ga} \~ \rew{N}:\rew{T}} + {\rew{\Ga} \~ \rew{M}|||\rew{N} : \rew{U}\{\rew{N}/x\}} + \tag{E-App} +\end{mathpar} + +\textbf{Case \textsc{CC-Lam}:}\\ +\begin{mathpar} + \infer + {\Ga, x:T \CCdash M:U \\ \Ga \CCdash (x:T) \explicit U : s} + {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} +\end{mathpar} +By the induction hypothesis we can assume +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ \rew{(x:T) \explicit U} : \rew{s}} + {\ } +\end{mathpar} +And by (3), we have two subcases to consider for the translation \rew{(x:T) \explicit U}: + +\underline{Predicative:}\\ +The predicative product type translates to an explicit product type $(x:\rew{T}) \explicit \rew{U}$ and we apply the explicit \textsc{X-Lam} typing rule to derive the typing of the explicit lambda abstraction. +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \explicit \rew{U} : \rew{s}} + {\rew{\Ga} \~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} + \tag{X-Lam} +\end{mathpar} +\underline{Impredicative:}\\ +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ and we apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction. However, an additional premise is required \todo +\begin{mathpar} + \infer + {\rew{\Ga}, x:\rew{T} \~ \rew{M}:\rew{U} \\ \rew{\Ga} \~ (x:\rew{T}) \erasable \rew{U} : \rew{s} \\ x \notin \fv{\rew{M}^*}} + {\rew{\Ga} \~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} + \tag{E-Lam} +\end{mathpar} + +\textbf{Lemma:} \todo +\begin{proof} + +\end{proof} + +\subsection{Example} \newpage \bibliographystyle{alpha} View it on GitLab: https://gitlab.com/monnier/typer/compare/7d6653236691d857e2c2c6e7e445db7440… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/7d6653236691d857e2c2c6e7e445db7440… You're receiving this email because of your account on gitlab.com.

1 0

***SPAM*** [Git][monnier/typer][graveline] 8 commits: Allow `let` vars to be erasable in some circumstances
by Jonathan Graveline 26 Jul '18

26 Jul '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: d21c5eb6 by Stefan Monnier at 2018-07-25T19:13:16Z Allow `let` vars to be erasable in some circumstances * src/opslexp.ml (nerased_let): New function. (check'): Use it. * tests/eval_test.ml ("Let-erased"): New test. - - - - - 450e86fa by Jonathan Graveline at 2018-07-25T20:28:33Z *samples/list.typer, more consistent function's type declaration - - - - - 5d4e2008 by Jonathan Graveline at 2018-07-25T20:35:26Z Stop compilation on error in `check` and elab functions Also store all errors and warnings for future use - - - - - 2b2bac1b by Jonathan Graveline at 2018-07-25T20:40:47Z Print related name only when the name has underscore - - - - - 26e9e4c2 by Jonathan Graveline at 2018-07-25T21:25:59Z Add an exception for sform_load's context when in pervasive.typer - - - - - a188451f by Jonathan Graveline at 2018-07-26T02:52:06Z Merge branch 'master' of https://gitlab.com/monnier/typer into graveline - - - - - be29169e by Jonathan Graveline at 2018-07-26T04:45:56Z Change lost somewhere in previous commit *samples/case2.typer *samples/do.typer *samples/list.typer - - - - - b0b911ec by Jonathan Graveline at 2018-07-26T04:55:06Z Many change to use `load` in pervasive.typer and move some definition Temporary workaround for tuple access in macro `.` renamed: samples/case2.typer -> btl/case.typer renamed: samples/do.typer -> btl/do.typer renamed: samples/list.typer -> btl/list.typer modified: btl/pervasive.typer deleted: samples/case.typer modified: src/opslexp.ml modified: tests/array_test.ml modified: tests/case_test.ml - - - - - 14 changed files: - samples/case2.typer → btl/case.typer - samples/do.typer → btl/do.typer - samples/list.typer → btl/list.typer - btl/pervasive.typer - − samples/case.typer - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/util.ml - tests/array_test.ml - tests/case_test.ml - tests/eval_test.ml Changes: ===================================== samples/case2.typer → btl/case.typer ===================================== @@ -8,6 +8,22 @@ %%%% argument may be sub pattern or variable) %%%% +%% Move IO outside List (from element to List) +%% (Was helpful for me when translating code that used to not be IO code) +%% (The function's type explain everything) +io-list : List (IO ?a) -> IO (List ?a); +io-list l = let + ff : IO (List ?a) -> IO ?a -> IO (List ?a); + ff o v = do { + o <- o; + v <- v; + IO_return (cons v o); + }; +in do { + l <- (List_foldl ff (IO_return nil) l); + IO_return (List_reverse l nil); +}; + %% %% Generate a List of pseudo-unique symbol %% @@ -187,6 +203,8 @@ introduced-vars pat = let (lambda s ss -> do { o <- o; % bind if_then_else_ (Sexp_eq s (Sexp_symbol "_:=_")) + %% (if_then_else_ (Sexp_eq (List_nth 0 ss Var_error) dflt-var) + %% (return (List_concat o (cons dflt-var nil))) (return (List_concat o (cons (List_nth 1 ss Var_error) nil))) %% there's no introduced variable here %% `case` on sub pattern will introduce new variable ===================================== samples/do.typer → btl/do.typer ===================================== @@ -1,9 +1,6 @@ -%%% -%%% Macro : do -%%% -%%% This file may not be up to date with version -%%% in pervasive.typer -%%% +%%%% +%%%% Macro : do +%%%% %% %% Here's an example : ===================================== samples/list.typer → btl/list.typer ===================================== @@ -2,18 +2,29 @@ %%%%% List %%%%% -%%%% List type +%% +%% I kept it simple: +%% not using macro `lambda` +%% not usgin macro `case` +%% in case we want to change order of definition in pervasive.typer +%% -%% FIXME: "t : ?" should be sufficient but triggers +%%%% List type -t : Type -> Type; -type t (a : Type) - | nil - | cons (hd : a) (tl : t a); +%% +%% FIXME: "List : ?" should be sufficient but triggers +%% macro `type` isn't actually defined where this file is included +%% in pervasive.typer +%% +%% List : Type -> Type; +%% type List (a : Type) +%% | nil +%% | cons (hd : a) (tl : List a); +%% %%%% List functions -length : (a : Type) ≡> t a -> Int; +length : (a : Type) ≡> List a -> Int; length xs = case xs | nil => 0 | cons hd tl => @@ -21,71 +32,71 @@ length xs = case xs %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: -%% - Provide a default value : `a -> t a -> a`; -%% - Disallow problem case : `(l : t a) -> (l != nil) -> a`; +%% - Provide a default value : `a -> List a -> a`; +%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error -head1 : (a : Type) ≡> t a -> Option a; +head1 : (a : Type) ≡> List a -> Option a; head1 xs = case xs | nil => none | cons hd tl => some hd; -head : (a : Type) ≡> t a -> Option a; +head : (a : Type) ≡> List a -> Option a; head xs = case xs | cons x _ => some x | nil => none; -tail : (a : Type) ≡> t a -> t a; +tail : (a : Type) ≡> List a -> List a; tail xs = case xs | nil => nil | cons hd tl => tl; -map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; +map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (map f xs); -mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> t a -> t b; -mapi f xs = let - helper : (a -> Int -> b) -> Int -> t a -> t b; - helper f i xs = case xs +mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +mapi = lambda f -> lambda xs -> let + helper : (a -> Int -> b) -> Int -> List a -> List b; + helper = lambda f -> lambda i -> lambda xs -> case xs | nil => nil | cons x xs => cons (f x i) (helper f (i + 1) xs); in helper f 0 xs; -map2 : (?a -> ?b -> ?c) -> t ?a -> t ?b -> t ?c; -map2 f xs ys = case xs +map2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c) -> List a -> List b -> List c; +map2 = lambda f -> lambda xs -> lambda ys -> case xs | nil => nil | cons x xs => case ys | nil => nil % error | cons y ys => cons (f x y) (map2 f xs ys); -foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> t b -> a; -foldli f o xs = let - helper : (a -> b -> Int -> a) -> Int -> a -> t b -> a; - helper f i o xs = case xs +foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> List b -> a; +foldli = lambda f -> lambda o -> lambda xs -> let + helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a; + helper = lambda f -> lambda i -> lambda o -> lambda xs -> case xs | nil => o | cons x xs => helper f (i + 1) (f o x i) xs; in helper f 0 o xs; %% Fold 2 List as long as both List are non-empty -fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> t ?b -> t ?c -> ?a; -fold2 f o xs ys = case xs +fold2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c -> a) -> a -> List b -> List c -> a; +fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | cons x xs => ( case ys | cons y ys => fold2 f (f o x y) xs ys | nil => o ) % may be an error | nil => o; % may or may not be an error -foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> t b -> a -> a; -foldr f = lambda xs -> lambda i -> case xs +foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +foldr = lambda f -> lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (foldr f xs i); -find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; -find f = lambda xs -> case xs +find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +find = lambda f -> lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => find f xs; -nth : (a : Type) ≡> Int -> t a -> a -> a; +nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs @@ -93,21 +104,21 @@ nth = lambda n -> lambda xs -> lambda d -> case xs | true => x | false => nth (n - 1) xs d; -reverse : (a : Type) ≡> t a -> t a -> t a; -reverse l t = case l +reverse : (a : Type) ≡> List a -> List a -> List a; +reverse = lambda l -> lambda t -> case l | nil => t | cons hd tl => reverse tl (cons hd t); -concat : (a : Type) ≡> t a -> t a -> t a; -concat l t = reverse (reverse l nil) t; +concat : (a : Type) ≡> List a -> List a -> List a; +concat = lambda l -> lambda t -> reverse (reverse l nil) t; -foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> t b -> a; -foldl f i xs = case xs +foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +foldl = lambda f -> lambda i -> lambda xs -> case xs | nil => i | cons x xs => foldl f (f i x) xs; -remove : (a : Type) ≡> (a -> Bool) -> t a -> t a; -remove f l = case l +remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; +remove = lambda f -> lambda l -> case l | nil => nil | cons x xs => ( case (f x) | true => remove f xs @@ -116,8 +127,8 @@ remove f l = case l %% Merge two List to a List of Pair %% Both List must be of same length -merge : t ?a -> t ?b -> t (Pair ?a ?b); -merge xs ys = case xs +merge : (a : Type) ≡> (b : Type) ≡> List a -> List b -> List (Pair a b); +merge = lambda xs -> lambda ys -> case xs | cons x xs => ( case ys | cons y ys => cons (pair x y) (merge xs ys) | nil => nil ) % error @@ -125,50 +136,34 @@ merge xs ys = case xs %% `Unmerge` a List of Pair %% The two functions name said it all -map-fst : t (Pair ?a ?b) -> t ?a; -map-fst xs = let - mf : Pair ?a ?b -> ?a; +map-fst : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List a; +map-fst = lambda xs -> let + mf : Pair a b -> a; mf p = case p | pair x _ => x; in map mf xs; -map-snd : t (Pair ?a ?b) -> t ?b; -map-snd xs = let - mf : Pair ?a ?b -> ?b; +map-snd : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List b; +map-snd = lambda xs -> let + mf : Pair a b -> b; mf p = case p | pair _ y => y; in map mf xs; -%% Is argument List empty? -empty : t ?a -> Bool; -empty xs = Int_eq (length xs) 0; - -%% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (The function's type explain everything) -io-list : t (IO ?a) -> IO (t ?a); -io-list l = let - ff : IO (t ?a) -> IO ?a -> IO (t ?a); - ff o v = do { - o <- o; - v <- v; - IO_return (cons v o); - }; -in do { - l <- (foldl ff (IO_return nil) l); - IO_return (reverse l nil); -}; +%% Is argument List empty +empty : (a : Type) ≡> List a -> Bool; +empty = lambda xs -> Int_eq (length xs) 0; %%%% Sorting List -sort : (a : Type) ≡> (a -> a -> Bool) -> t a -> t a; -sort o l = let +sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; +sort = lambda o -> lambda l -> let - sortp : Option a -> t a -> t a -> t a -> t a; - sortp p lt gt l = case p + sortp : Option a -> List a -> List a -> List a -> List a; + sortp = lambda p -> lambda lt -> lambda gt -> lambda l -> case p | none => nil | some (pp) => ( case l | nil => ( let - ltp : t a; ltp = sortp (head1 lt) nil nil (tail lt); - gtp : t a; gtp = sortp (head1 gt) nil nil (tail gt); + ltp : List a; ltp = sortp (head1 lt) nil nil (tail lt); + gtp : List a; gtp = sortp (head1 gt) nil nil (tail gt); in concat ltp (cons pp gtp) ) | cons x xs => ( case (o x pp) @@ -181,8 +176,8 @@ in sortp (head1 l) nil nil (tail l); %%%% Some algo on sorted list -sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Option a; -sfind o f a l = case l +sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; +sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l | nil => none | cons x xs => ( case (f x) | true => some x @@ -192,39 +187,53 @@ sfind o f a l = case l ) ); -sall : (a : Type) ≡> (a -> Bool) -> t a -> t a; -sall f l = case l +sall : (a : Type) ≡> (a -> Bool) -> List a -> List a; +sall = lambda f -> lambda l -> case l | nil => nil | cons x xs => ( case (f x) | true => cons x (sall f xs) | false => sall f xs ); -sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Bool; -sexist o f a l = case (sfind o f a l) +sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool; +sexist = lambda o -> lambda f -> lambda a -> lambda l -> case (sfind o f a l) | none => false | some _ => true; -sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -sinsert o a l = case l +sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sinsert = lambda o -> lambda a -> lambda l -> case l | nil => cons a l | cons x xs => ( case (o x a) | true => cons a l | false => cons x (sinsert o a xs) ); -ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -ssup o a l = case l +ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +ssup = lambda o -> lambda a -> lambda l -> case l | nil => nil | cons x xs => ( case (o x a) | true => l | false => ssup o a xs ); -sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -sinf o a l = case l +sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sinf = lambda o -> lambda a -> lambda l -> case l | nil => nil | cons x xs => ( case (o x a) | true => nil | false => cons x (sinf o a xs) ); + +%%%% +%%%% Array from List +%%%% + +List->Array : (a : Type) ≡> List a -> Array a; +List->Array xs = let + + helper : List a -> Array a -> Array a; + helper xs a = case xs + | cons x xs => helper xs (Array_append x a) + | nil => a; + +in (helper xs (Array_empty ())); ===================================== btl/pervasive.typer ===================================== @@ -405,10 +405,13 @@ __\.__ = nil); branch = Sexp_node (Sexp_symbol "_=>_") (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") + tmp-fix def = quote (let + (uquote (Sexp_symbol "%tuple element%")) = (uquote def) in + (uquote (Sexp_symbol "%tuple element%"))); + in tmp-fix (Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons o (cons branch nil))) - nil) + nil)) in macro (lambda args -> IO_return case args @@ -501,138 +504,19 @@ test4 = test1 : Option ?; test3 = test4; %%%% -%%%% Macro : do +%%%% Common library %%%% -%% -%% Here's an example : -%% -%% fun = do { -%% str <- return "\n\tHello world!\n\n"; -%% print str; -%% }; -%% -%% str is bind by macro, -%% -%% fun is a command, -%% -%% do may contain do because it returns a command. -%% - -assign = Sexp_symbol "<-"; - -get-sym : Sexp -> Sexp; -get-sym sexp = let - - dflt-sym = (lambda _ -> (Sexp_symbol " %not used% ")); - - in Sexp_dispatch sexp - - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (s) - (dflt-sym ()) - ) - - dflt-sym dflt-sym dflt-sym - dflt-sym dflt-sym; % there must be a command - -get-op : Sexp -> Sexp; -get-op sexp = let - - as-is = lambda _ -> sexp; - - helper = (lambda sexp -> Sexp_dispatch sexp - - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) - (Sexp_node s ss) - ) - - as-is as-is as-is as-is as-is - ); - - op = (helper sexp); +%% `List` is the type and `list` is the module (tuple) -in if_then_else_ (Sexp_eq op (Sexp_symbol "")) Sexp_error op; +list = load_ "btl/list.typer"; -get-decl : List Sexp -> List Sexp; -get-decl args = let +%% macro `do` for easier series of IO operation - err = lambda _ -> cons Sexp_error nil; - - % Expecting a Block of command separated by ";" - - node = Sexp_dispatch (List_nth 0 args Sexp_error) - - (lambda _ _ -> cons Sexp_error nil) err err err err - - (lambda l -> Parser_default l); +do = let lib = load_ "btl/do.typer" in lib.do; -in node; - -%% -%% The idea of the macro is : -%% -%% IO_bind a-op (lambda a-sym -> [next command or return a-sym]) -%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym]))) -%% -%% this way a-sym is defined within b-op and so on -%% a-sym is now just `a` and not `IO a` -%% - -set-fun : List Sexp -> Sexp; -set-fun args = let - - helper : Sexp -> List Sexp -> Sexp; - helper lsym args = case args - | cons s ss => (let - - sym = get-sym s; - - op = get-op s; - - in Sexp_node (Sexp_symbol "IO_bind") (cons (op) - (cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil)) - ) - - | nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil); - -in helper (Sexp_symbol "") args; % return Unit if no command given - -%% Serie of command - -do = macro (lambda args -> - (IO_return (set-fun (get-decl args))) -); - -%%%% -%%%% Array from List -%%%% +%% macro `case` for a little more complex pattern matching -List->Array : (a : Type) ≡> List a -> Array a; -List->Array xs = let - - helper : List a -> Array a -> Array a; - helper xs a = case xs - | cons x xs => helper xs (Array_append x a) - | nil => a; - -in (helper xs (Array_empty ())); - -%% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (The function's type explain everything) -io-list : List (IO ?a) -> IO (List ?a); -io-list l = let - ff : IO (List ?a) -> IO ?a -> IO (List ?a); - ff o v = do { - o <- o; - v <- v; - IO_return (cons v o); - }; -in do { - l <- (List_foldl ff (IO_return nil) l); - IO_return (List_reverse l nil); -}; +case_ = let lib = load_ "btl/case.typer" in lib.case_; %%% pervasive.typer ends here. ===================================== samples/case.typer deleted ===================================== @@ -1,521 +0,0 @@ -%%% -%%% Macro : case ... | ... -%%% -%%% (pattern matching) -%%% -%%% TODO : -%%% - Handle named constructor variable -%%% - Find a way to get no error when there's no default case -%%% and user pattern is exhaustive -%%% - -%% -%% Match every variable in each pattern with a list of VarTest. -%% -%% VarTest : -%% -%% var_test is (var_test [ctor to match]) -%% -%% Push current var n_times for sub test -%% push_var is (push_var n_times) -%% -%% sub_test introduce a variable for testing sub pattern -%% sub_test is (sub_test [sup. var name] [ctor to match]) -%% -%% Pattern : -%% -%% branch is (branch [list of var test] [user fun on match]) -%% -%% dflt_branch is (dflt_branch [user fun]) and always match -%% - -type VarTest - | var_test Sexp - | push_var Int - | sub_test Sexp Sexp; - -type Pattern - | branch (List VarTest) Sexp - | dflt_branch Sexp; - -%% -%% Get matched expression (e.g. case (var1,var2,...) | ...) -%% -%% Expression are separated by "," so it is useful for -%% case (expr1,expr2,...) ... -%% but also for -%% case ... | (expr3,expr4,...) => ... -%% - -get_exprs : Sexp -> List Sexp; -get_exprs sexp = let - - err = (lambda _ -> cons Sexp_error nil); - - get_exprs_helper : Sexp -> List Sexp -> List Sexp; - get_exprs_helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) - | true => (ss) % tuple - % constructor or function called (only 1 pattern) - | false => (cons (Sexp_node s ss) nil); - -in Sexp_dispatch sexp - get_exprs_helper - (lambda s -> (cons (Sexp_symbol s) nil)) - err err err - (lambda ss -> cons ss nil); % do nothing to Block - -mapi : (Sexp -> Int -> Sexp) -> Int -> List Sexp -> List Sexp; -mapi f i xs = case xs - | nil => nil - | cons x xs => cons (f x i) (mapi f (i + 1) xs); - -io_list : List (IO ?a) -> IO (List ?a); -io_list l = let - - fold_fun : IO (List ?a) -> IO ?a -> IO (List ?a); - fold_fun o v = do - { - o <- o; - v <- v; - IO_return (cons v o); - }; - -in do -{ - l <- (List_foldl fold_fun (IO_return nil) l); - IO_return (List_reverse l nil); -}; - -get_num_vars : List Sexp -> IO (List Sexp); -get_num_vars vars = io_list (List_map - (lambda _ -> gensym ()) - vars); - -%% -%% Get pattern to match -%% - -get_cases : List Sexp -> List Pattern; -get_cases sexps = let - - to_case : Sexp -> Pattern; - to_case sexp = Sexp_dispatch sexp - - (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) - % expecting a Sexp_node as second argument to _=>_ - | true => (branch - (List_map (lambda ctor -> var_test ctor) (get_exprs (List_nth 0 ss Sexp_error))) - (List_nth 1 ss Sexp_error)) - | false => (dflt_branch (Sexp_node s ss))) - - (lambda s -> dflt_branch (Sexp_symbol s)) - (lambda s -> dflt_branch (Sexp_string s)) - (lambda i -> dflt_branch (Sexp_integer i)) - (lambda f -> dflt_branch (Sexp_float f)) - - (lambda ss -> dflt_branch ss); - - helper : List Sexp -> List Pattern; - helper sexps = List_map (lambda s -> (to_case s)) sexps; - -in helper sexps; - -%% -%% return true if v is a ctor -%% -is_ctor : Sexp -> IO Bool; -is_ctor v = Sexp_dispatch v - (lambda _ _ -> IO_return true) - (lambda s -> do - { - env <- Elab_getenv (); - IO_return (Elab_isconstructor s env); - }) - (lambda _ -> IO_return false) (lambda _ -> IO_return false) - (lambda _ -> IO_return false) (lambda _ -> IO_return false); - -%% -%% Rename nth constructor inside ctor to sym -%% - -rename_nth : Int -> Sexp -> Sexp -> IO Sexp; -rename_nth n ctor sym = let - - mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) - -> Int -> IO (List Sexp) -> IO (List Sexp); - mapiif f b i xs = let - - helper : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - helper f b i xs = case xs - | nil => IO_return nil - | cons x xs => (let - - apply : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - apply f b i xs = do - { - xs <- (helper f b (i + 1) xs); - IO_return (cons (f x i) xs); - }; - - continue : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - continue f b i xs = do - { - xs <- (helper f b i xs); - IO_return (cons x xs); - }; - - in do - { - bv <- b x; - (if_then_else_ bv (apply f b i xs) (continue f b i xs)); - }); - - in do - { - xs <- xs; - helper f b i xs; - }; - - err = (lambda _ -> Sexp_symbol "<not a ctor (0)>"); - - %% - %% Check for ctor within englobing ctor and rename variable - %% - - sub_ctor : Sexp -> Int -> Sexp; - sub_ctor ctor i = Sexp_dispatch ctor - (lambda s ss -> if_then_else_ (Int_eq i n) - (sym) - (Sexp_symbol "_")) - (lambda s -> if_then_else_ (Int_eq i n) - (sym) - (Sexp_symbol "_")) - err err err err ; - - io_err = (lambda _ -> IO_return (Sexp_symbol "<not a ctor (1)>")); - -in (Sexp_dispatch ctor - (lambda s ss -> do - { - ss <- (mapiif sub_ctor is_ctor 0 (IO_return ss)); - IO_return (Sexp_node s ss); - }) - (lambda s -> IO_return (Sexp_symbol s)) - io_err io_err io_err io_err); - -%% -%% Expand sub pattern into sub_test -%% and optionaly push_var when there's -%% - -expand_cases : List Pattern -> IO (List Pattern); -expand_cases pats = let - - foldi : (Sexp -> Int -> ?a -> ?a) - -> Int -> ?a -> List Sexp -> ?a; - foldi f i o xs = case xs - | nil => o - | cons x xs => foldi f (i + 1) (f x i o) xs; - - get_sub_pattern : Sexp -> IO (List Sexp); - get_sub_pattern ctor = let - - err = (lambda _ -> Sexp_error); - - no_pattern : List Sexp -> ? -> IO (List Sexp); - no_pattern pats = (lambda _ -> IO_return pats); - - helper : List Sexp -> IO (List Sexp); - helper vars = List_foldl (lambda pats var -> do - { - pats <- pats; - Sexp_dispatch var - (lambda s ss -> IO_return (cons (Sexp_node s ss) pats)) - (lambda s -> do - { - b <- is_ctor (Sexp_symbol s); - if_then_else_ b - (IO_return (cons (Sexp_symbol s) pats)) - (no_pattern pats ()); - }) - (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) - }) (IO_return nil) vars; - - in Sexp_dispatch ctor - (lambda s ss -> helper ss) - (no_pattern nil) (no_pattern nil) - (no_pattern nil) (no_pattern nil) (no_pattern nil); - - expand_one : IO (List VarTest) -> VarTest -> IO (List VarTest); - expand_one all test = case test - | push_var n => IO_bind all (lambda all -> - IO_return (List_concat all (cons (push_var n) nil))) - | _ => (let - - expand : VarTest -> IO (List VarTest); - expand test = let - - %% I don't expect to use multiple not_unique_sym at the same time - %% so the name may be reused - - not_unique_sym : Sexp; - not_unique_sym = Sexp_symbol " %not gensym% "; - - t : Sexp; - t = case test - | (var_test t) => t - | (sub_test _ t) => t - | _ => Sexp_error; - - renamed : Int -> IO VarTest; - renamed i = case test - | (var_test t) => IO_bind (rename_nth i t not_unique_sym) - (lambda t -> IO_return (var_test t)) - | (sub_test v t) => IO_bind (rename_nth i t not_unique_sym) - (lambda t -> IO_return (sub_test v t)) - | _ => IO_return (var_test Sexp_error); - - sub_pattern : IO (List Sexp); - sub_pattern = do - { - l <- get_sub_pattern t; - IO_return (List_reverse l nil); - }; - - sub_case : IO (List VarTest); - sub_case = let - - helper : Sexp -> VarTest -> List VarTest -> IO (List VarTest); - helper c r o = IO_return (List_concat o - (cons r (cons (sub_test not_unique_sym c) nil))); - - l : IO (List VarTest); - l = do - { - sub_pattern <- sub_pattern; - (foldi - (lambda c i o -> do - { - o <- o; - r <- (renamed i); - helper c r o; - }) 0 (IO_return nil) sub_pattern) - }; - - in do - { - l <- l; - sub_pattern <- sub_pattern; - IO_return (cons (push_var (List_length sub_pattern)) l); - }; - - in do - { - sub_pattern <- sub_pattern; - if_then_else_ (Int_eq (List_length sub_pattern) 0) - (do - { - all <- all; - IO_return (List_concat all (cons test nil)); - }) - (do - { - sub_case <- sub_case; - all <- all; - IO_return (List_concat all sub_case); - }) - }; - - in expand test); - - expand_all : Pattern -> IO Pattern; - expand_all p = case p - | (dflt_branch _) => IO_return p - | (branch cs f) => (let - - ctors : IO (List VarTest); - ctors = (List_foldl expand_one (IO_return nil) cs); - - stop_on_id : List VarTest -> IO Pattern; - stop_on_id ctors = if_then_else_ - (Int_eq (List_length cs) (List_length ctors)) - (IO_return (branch ctors f)) - (expand_all (branch ctors f)); - - in do - { - ctors <- ctors; - stop_on_id ctors; - }); - -in io_list (List_map expand_all pats); - -pattern_to_sexp : List Sexp -> List Pattern -> IO Sexp; -pattern_to_sexp vars pats = let - - vars_wrap : List Sexp -> Sexp -> List Sexp -> Sexp; - vars_wrap numvs succ vs = Sexp_node (List_foldl - (lambda o v -> (quote (lambda_->_ (uquote v) (uquote o)))) - succ vs) ( numvs ); - - to_case : Sexp -> Sexp -> Sexp -> Option Sexp -> Sexp; - to_case var ctor succ fail = case fail - | some fail => (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ)) - (_=>_ _ (uquote fail))))) - | none => (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ))))); - - push : Int -> List Sexp -> List Sexp; - push n vars = if_then_else_ (Int_<= n 1) - (vars) - (case vars - | (cons v _) => push (n - 1) (cons v vars) - | nil => nil); - - chain_ctors : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp; - chain_ctors vars tests succ fail = case vars - | (cons v vv) => (case tests - | (cons t tt) => (case t - | (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vv tt succ fail) none) - (to_case v t (chain_ctors vv tt succ fail) (some fail)) - | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vars tt succ fail) none) - (to_case v t (chain_ctors vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors (push n vars) tt succ fail)) - | nil => Sexp_error) - | nil => (case tests - | (cons t tt) => (case t - | (var_test _) => Sexp_error - | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vars tt succ fail) none) - (to_case v t (chain_ctors vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors (push n vars) tt succ fail)) - | nil => succ); - - chain_ctors_nofail : List Sexp -> List VarTest -> Sexp -> Sexp; - chain_ctors_nofail vars tests succ = case vars - | (cons v vv) => (case tests - | (cons t tt) => (case t - | (var_test t) => - (to_case v t (chain_ctors_nofail vv tt succ) none) - | (sub_test v t) => - (to_case v t (chain_ctors_nofail vars tt succ) none) - | (push_var n) => (chain_ctors_nofail (push n vars) tt succ)) - | nil => Sexp_error) - | nil => (case tests - | (cons t tt) => (case t - | (var_test _) => Sexp_error - | (sub_test v t) => - (to_case v t (chain_ctors_nofail vars tt succ) none) - | (push_var n) => (chain_ctors_nofail (push n vars) tt succ)) - | nil => succ); - - one_to_sexp : List Sexp -> Pattern -> Sexp -> Sexp; - one_to_sexp vars pat fail = case pat - | (dflt_branch f) => f - | (branch tests f) => (chain_ctors vars tests f fail); - - last_to_sexp : List Sexp -> Pattern -> Sexp; - last_to_sexp vars pat = case pat - | (dflt_branch f) => f - | (branch tests f) => (chain_ctors_nofail vars tests f); - - test_fun : List Sexp -> Pattern -> Sexp -> Sexp; - test_fun vars pat fail = (quote (lambda (_ : Unit) -> - (uquote (one_to_sexp vars pat (quote ((uquote fail) ())))))); - - last_test_fun : List Sexp -> Pattern -> Sexp; - last_test_fun vars pat = (quote (lambda (_ : Unit) -> - (uquote (last_to_sexp vars pat)))); - - %% Same thing as not_unique_sym, I can reuse the name because - %% only the last defined is important - - fail_sym : Sexp; - fail_sym = Sexp_symbol " %fail sym% "; - - helper : List Sexp -> List Pattern -> Sexp; - helper vars pats = case pats - | (cons p pats) => (case pats - | (cons _ _) => Sexp_node (Sexp_symbol "let_in_") - (cons (Sexp_node (Sexp_symbol "_;_") - (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym - (cons (helper vars pats) nil))) nil)) - (cons (test_fun vars p fail_sym) nil)) - | nil => (last_test_fun vars p)) - | nil => Sexp_error; - -in IO_return (quote ((uquote (helper vars pats)) ())); - -%% -%% The macro we want. -%% - -case_ = macro (lambda args -> let - - foldi : (?a -> Int -> ?b -> ?b) -> Int -> ?b -> List ?a -> ?b; - foldi f i o xs = case xs - | nil => o - | cons x xs => foldi f (i + 1) (f x i o) xs; - - case0 : List Sexp -> IO Sexp; - case0 args = let - - vars : List Sexp; - vars = case args - | (cons s ss) => get_exprs s - | nil => nil; - - pats : List Pattern; - pats = case args - | (cons s ss) => get_cases ss - | nil => nil; - - num_vars : IO (List Sexp); - num_vars = get_num_vars vars; - - free_vars : IO (List Sexp); - free_vars = get_num_vars vars; - - vars_wrap : List Sexp -> List Sexp -> Sexp -> IO Sexp; - vars_wrap fvars nvars fun = let - - rvars : List Sexp; - rvars = List_reverse vars nil; - - nfun : Sexp; - nfun = fun; - - in IO_return ( (foldi - (lambda v i fun -> (quote ( - let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun)))) - 0 nfun vars)); - - in do - { - pats <- expand_cases pats; - num_vars <- num_vars; - free_vars <- free_vars; - f <- pattern_to_sexp num_vars pats; - vars_wrap free_vars num_vars f; - }; - - %% Only the Sexp after "_|_" are interesting - - case1 : Sexp -> List Sexp -> IO Sexp; - case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) - (case0 ss) - (IO_return Sexp_error); - - err = (lambda _ -> IO_return Sexp_error); - -%% Expecting only one Sexp_node containing a case with arguments - -in (Sexp_dispatch (List_nth 0 args Sexp_error) - case1 err err err err err) -); ===================================== src/REPL.ml ===================================== @@ -235,7 +235,7 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Util.Stop_Compilation s -> + with Stop_Compilation s -> (print_string s; (i,clxp,rctx)) in repl clxp rctx; @@ -261,8 +261,8 @@ let rec repl i clxp rctx = List.iter (print_eval_result i) ret; repl clxp rctx with e -> match e with - | Util.Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> repl clxp rctx) + | Stop_Compilation msg -> (print_string msg; repl clxp rctx) + | _ -> catch_error (); repl clxp rctx) let arg_files = ref [] ===================================== src/debruijn.ml ===================================== @@ -143,13 +143,17 @@ let _make_senv_type = (0, _make_scope) let _make_myers = M.nil let _get_related_name (n : db_ridx) name map = - let r = Str.regexp (name^".*") in - SMap.fold (fun name idx ps -> + let r = Str.regexp (".*"^name^".*") in + let search r = SMap.fold (fun name idx ps -> if (Str.string_match r name 0) then (n - idx - 1)::ps else ps - ) map [] + ) map [] in + if ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") then + search r + else [] (* Public methods: DO USE * ---------------------------------- *) ===================================== src/elab.ml ===================================== @@ -140,14 +140,16 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp - with e -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + with e -> match e with + | Stop_Compilation _ -> raise e + | _ -> print_string "Exception while checking type `"; + lexp_print ltp; + (match var with + | (_, None) -> () + | (_, Some name) + -> print_string ("` of var `" ^ name ^"`\n")); + print_lexp_ctx (ectx_to_lctx ctx); + raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -155,10 +157,12 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp - with e -> - lexp_error loc lxp "Error while type-checking"; - print_lexp_ctx (ectx_to_lctx ctx); - raise e in + with e -> match e with + (* lexp_error is fatal but Stop_Compilation isn't *) + | Stop_Compilation _ -> raise e + | _ -> lexp_error loc lxp "Error while type-checking"; + print_lexp_ctx (ectx_to_lctx ctx); + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' with e -> print_string ("Exception while conversion-checking types:\n"); @@ -1108,21 +1112,24 @@ and lexp_decls_1 _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (EV.set_getenv nctx; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + let res = _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + (stop_on_error (); res)) and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = - match sdecls with - | [] -> [], ectx_new_scope ctx - | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls sdecls nctx in - decls :: declss, nnctx + let impl sdecls ctx = match sdecls with + | [] -> [], ectx_new_scope ctx + | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in + let declss, nnctx = lexp_p_decls sdecls nctx in + decls :: declss, nnctx in + let res = impl sdecls ctx in (stop_on_error (); res) and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = - List.map (fun pe -> let e, _ = infer pe ctx in e) p + let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in + (stop_on_error (); res) and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer e ctx in e + let e, _ = infer e ctx in (stop_on_error (); e) (* -------------------------------------------------------------------------- * Special forms implementation @@ -1545,6 +1552,8 @@ let lexp_print_var_info ctx = print_string "\n") done +let _in_pervasive = ref true + (* arguments : elab_context from where load is called, loc is location of load call, @@ -1563,7 +1572,10 @@ let sform_load usr_elctx loc sargs ot = (* read file as elab_context *) let ld_elctx = match sargs with - | [String (_,file_name)] -> read_file file_name !_sform_default_ectx + | [String (_,file_name)] -> if !_in_pervasive then + read_file file_name usr_elctx + else + read_file file_name !_sform_default_ectx | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in (* get lexp_context *) @@ -1575,9 +1587,18 @@ let sform_load usr_elctx loc sargs ot = let usr_len = M.length usr_lctx in let dflt_len = M.length dflt_lctx in - (* create a tuple from context and shift it to user context *) - let tuple = OL.ctx2tup dflt_lctx ld_lctx in - let tuple' = (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in + (* create a tuple from context and shift it to user context * + * also check if we are in pervasive in which case * + * we want to load in the current context rather than the default *) + let tuple = if !_in_pervasive then + OL.ctx2tup usr_lctx ld_lctx + else + OL.ctx2tup dflt_lctx ld_lctx in + + let tuple' = if !_in_pervasive then + tuple + else + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in (tuple',Lazy) @@ -1665,7 +1686,9 @@ let default_ectx builtin_size := get_size lctx; + let _ = _in_pervasive := true in let lctx = read_file (btl_folder ^ "/pervasive.typer") lctx in + let _ = _in_pervasive := false in let _ = _set_default_ectx lctx in lctx @@ -1688,7 +1711,8 @@ let _lexp_expr_str (str: string) (tenv: token_env) (* specialized version *) let lexp_expr_str str ctx = - _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + with Stop_Compilation s -> (print_string s; []) let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = let sdecls = _sexp_parse_str str tenv grm limit in @@ -1696,7 +1720,8 @@ let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = (* specialized version *) let lexp_decl_str str ctx = - _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + with Stop_Compilation s -> (print_string s; ([],ctx)) (* Eval String @@ -1709,7 +1734,7 @@ let _eval_expr_str str lctx rctx silent = (EV.eval_all elxps rctx silent) let eval_expr_str str lctx rctx = try _eval_expr_str str lctx rctx false - with Util.Stop_Compilation s -> (print_string s; []) + with Stop_Compilation s -> (print_string s; []) let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1717,5 +1742,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Util.Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) ===================================== src/lexp.ml ===================================== @@ -215,7 +215,7 @@ let mkCall (f, es) * that is transient and hence immediately GC'd. *) let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 -(* When building the type of a tuple (x1=e1, x2=e2, ..., xn=en) +(* When computing the type of "load"ed modules * we end up building substitutions of the form * * ((Susp e3 (((Susp e2 (e1 · id)) · e1 · id) @@ -223,11 +223,18 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * · ((Susp e2 (e1 · id)) · e1 · id) * · e1 · id) * - * with exponential size (but lots of sharing). So it's indispensible + * with 2^n size (but lots of sharing). So it's indispensible * to memoize the computation to avoid the exponential waste of time. * - * FIXME: I still don't understand why we build substitutions - * of such a shape! *) + * This shows up because of the dependent type of `let`: + * + * let z = e₃ in e : τ[e₃/z] + * let y = e₂ in let z = e₃ in e : (τ[e₃/z])[e₂/y] = τ[(e₃[e₂/y])/z,e₂/y] + * let x = e₁ in let y = e₂ in let z = e₃ in e + * : (τ[(e₃[e₂/y])/z,e₂/y])[e₁/x] + * = τ[(e₃[(e₂[e₁/x])/y,e₁/x])/z,(e₂[e₁/x])/y,e₁/x] + * ... + *) let rec mkSusp e s = if S.identity_p s then e else ===================================== src/opslexp.ml ===================================== @@ -366,9 +366,34 @@ let dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased +let nerased_let defs erased = + (* Let bindings are not erasable, with the important exception of + * let-bindings of the form `x = y` where `y` is an erasable var. + * This exception is designed so that macros like `case` which need to + * rebind variables to user-specified names can do so without having + * to pay attention to whether the var is erasable or not. + *) + (* FIXME: Maybe allow more cases of erasable let-bindings. *) + let nerased = DB.set_sink (List.length defs) erased in + let es = List.map + (fun (_v, e, _t) -> + (* Look for `x = y` where `y` is an erasable var. + * FIXME: `nerased` assumes all the vars in `defs` + * will be non-erasable, so in `let x = z; y = x ...` + * where `z` is erasable, `x` will be found + * to be erasable, but not `y`. *) + match e with Var (_, idx) -> DB.set_mem idx nerased + | _ -> false) + defs in + if not (List.mem true es) then nerased else + List.fold_left + (fun erased e + -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + erased es + (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check' erased ctx e = - let check = check' in +let rec check'' erased ctx e = + let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () else (U.msg_error "TC" (lexp_location e) @@ -433,14 +458,17 @@ let rec check' erased ctx e = -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx v ForwardRef t)) ctx defs in - (* FIXME: Allow erasable let-bindings! *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = nerased_let defs erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (v, e, t) - -> assert_type nctx e - (push_susp t (S.shift n)) - (check nerased nctx e); + -> assert_type + nctx e + (push_susp t (S.shift n)) + (check (if DB.set_mem (n - 1) nerased + then DB.set_empty + else nerased) + nctx e); n - 1) (List.length defs) defs in mkSusp (check nerased nctx e) @@ -624,7 +652,11 @@ let rec check' erased ctx e = check erased ctx e | MVar (_, t, _) -> push_susp t s) -let check = check' DB.set_empty +let check' ctx e = + let res = check'' DB.set_empty ctx e in + (U.stop_on_error (); res) + +let check = check' (** Compute the set of free (meta)variables. **) @@ -919,7 +951,7 @@ and clean_map cases = (** Turning a set of declarations into an object. **) let ctx2tup ctx nctx = - U.debug_msg ("Entering ctx2tup\n"); + (*U.debug_msg ("Entering ctx2tup\n");*) assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); let rec get_blocs nctx blocs = @@ -937,7 +969,7 @@ let ctx2tup ctx nctx = let type_label = (loc, "record") in let offset = List.length types in let types = List.rev types in - U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n"); + (*U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) Call (Cons (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) ===================================== src/util.ml ===================================== @@ -66,30 +66,71 @@ let typer_unreachable s = raise (Unreachable_error s) exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s) +(* `error list * warning list` both of type `level * kind * section * loc * msg` *) +type error_log_type = ((int * string * string * location * string) list * + (int * string * string * location * string) list) + +let empty_error_log : error_log_type = ([],[]) + +let error_log = ref empty_error_log + +let error_count () : int = let errors, _ = !error_log in + List.length errors + +let warning_count () : int = let _, warnings = !error_log in + List.length warnings + +let new_error lvl kind section loc msg = let errors, warnings = !error_log in + error_log := ((lvl,kind,section,loc,msg)::errors,warnings) + +let new_warning lvl kind section loc msg = let errors, warnings = !error_log in + error_log := (errors,(lvl,kind,section,loc,msg)::warnings) + +let reset_error_log () = error_log := empty_error_log + (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) -let msg_message stop lvl kind section (loc: location) msg = - let preppend_loc msg = (loc.file +let msg_message (error : bool) lvl kind section (loc: location) msg = + let message = (loc.file ^ ":" ^ string_of_int loc.line ^ ":" ^ string_of_int loc.column ^ ":" ^ kind ^ (if section = "" then " " else "(" ^ section ^ ") ") ^ msg ^ "\n") in + + if error then + new_error lvl kind section loc msg + else + new_warning lvl kind section loc msg; + if lvl <= !typer_verbose then - (print_string (preppend_loc msg); - if stop then - stop_compilation (preppend_loc "Compiler stopped on first error") - else ()) - else if stop then - stop_compilation (preppend_loc "Compiler stopped on first error") + print_string message else () -(* I would like to add optional stop on warning but I think *) -(* warning may be thrown at runtime *) +let stop_on_error () = if (0 < (error_count ())) then + (let count = error_count () in + reset_error_log (); + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" error\n")) + else () + +let stop_on_warning () = (stop_on_error (); + if (0 < (warning_count ())) then + let count = warning_count () in + reset_error_log (); + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warning\n") + else ()) + +let catch_error () = try stop_on_error () + with e -> match e with + | Stop_Compilation msg -> print_string msg + | _ -> () let msg_fatal s l m = msg_message false 0 "[X] Fatal " s l m; flush stdout; + reset_error_log (); internal_error "Compiler Fatal Error" let msg_error = msg_message true 1 "Error:" ===================================== tests/array_test.ml ===================================== @@ -149,6 +149,8 @@ let _ = (add_test "ARRAY" "Array.get" (fun () -> let _ = (add_test "ARRAY" "Array.empty, List->Array" (fun () -> let dcode = " + List->Array = list.List->Array; + empty1 = Array_empty (); empty2 = List->Array nil; ===================================== tests/case_test.ml ===================================== @@ -14,12 +14,8 @@ open Env let ectx = Elab.default_ectx let rctx = Elab.default_rctx +let case_decl = "" (* - Macro case break some test so I read definition here. - It's temporary. I will need to modify other test to use ##case_ (which is what - they need to test) or modify the macro to work with everything (there's strange - case in eval_test.ml which I did not expect). -*) let case_decl = let read_file filename = let lines = ref [] in let chan = open_in filename in @@ -32,6 +28,7 @@ let case_decl = let read_file filename = List.rev !lines in String.concat "\n" (read_file "samples/case2.typer") +*) (* eval case.typer only once! *) let rctx, ectx = Elab.eval_decl_str case_decl ectx rctx ===================================== tests/eval_test.ml ===================================== @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" let _ = test_eval_eqv_named "Let3" @@ -104,7 +104,15 @@ let _ = test_eval_eqv_named TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" + +let _ = test_eval_eqv_named + "Let-erasable" + + "c = 3; e = 1; f = 2; d = 4;" + + "let id = lambda t ≡> lambda (x : t) -> x; + in (lambda t ≡> let t1 = t in id (t := t1)) 3" (* == *) "3" (* Lambda * ------------------------ *) View it on GitLab: https://gitlab.com/monnier/typer/compare/c8fad5182993207af7e5c5b77de524008f… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/c8fad5182993207af7e5c5b77de524008f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Allow `let` vars to be erasable in some circumstances
by Stefan 25 Jul '18

25 Jul '18

Stefan pushed to branch master at Stefan / Typer Commits: d21c5eb6 by Stefan Monnier at 2018-07-25T19:13:16Z Allow `let` vars to be erasable in some circumstances * src/opslexp.ml (nerased_let): New function. (check'): Use it. * tests/eval_test.ml ("Let-erased"): New test. - - - - - 3 changed files: - src/lexp.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== src/lexp.ml ===================================== @@ -215,7 +215,7 @@ let mkCall (f, es) * that is transient and hence immediately GC'd. *) let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 -(* When building the type of a tuple (x1=e1, x2=e2, ..., xn=en) +(* When computing the type of "load"ed modules * we end up building substitutions of the form * * ((Susp e3 (((Susp e2 (e1 · id)) · e1 · id) @@ -223,11 +223,18 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * · ((Susp e2 (e1 · id)) · e1 · id) * · e1 · id) * - * with exponential size (but lots of sharing). So it's indispensible + * with 2^n size (but lots of sharing). So it's indispensible * to memoize the computation to avoid the exponential waste of time. * - * FIXME: I still don't understand why we build substitutions - * of such a shape! *) + * This shows up because of the dependent type of `let`: + * + * let z = e₃ in e : τ[e₃/z] + * let y = e₂ in let z = e₃ in e : (τ[e₃/z])[e₂/y] = τ[(e₃[e₂/y])/z,e₂/y] + * let x = e₁ in let y = e₂ in let z = e₃ in e + * : (τ[(e₃[e₂/y])/z,e₂/y])[e₁/x] + * = τ[(e₃[(e₂[e₁/x])/y,e₁/x])/z,(e₂[e₁/x])/y,e₁/x] + * ... + *) let rec mkSusp e s = if S.identity_p s then e else ===================================== src/opslexp.ml ===================================== @@ -366,6 +366,31 @@ let dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased +let nerased_let defs erased = + (* Let bindings are not erasable, with the important exception of + * let-bindings of the form `x = y` where `y` is an erasable var. + * This exception is designed so that macros like `case` which need to + * rebind variables to user-specified names can do so without having + * to pay attention to whether the var is erasable or not. + *) + (* FIXME: Maybe allow more cases of erasable let-bindings. *) + let nerased = DB.set_sink (List.length defs) erased in + let es = List.map + (fun (_v, e, _t) -> + (* Look for `x = y` where `y` is an erasable var. + * FIXME: `nerased` assumes all the vars in `defs` + * will be non-erasable, so in `let x = z; y = x ...` + * where `z` is erasable, `x` will be found + * to be erasable, but not `y`. *) + match e with Var (_, idx) -> DB.set_mem idx nerased + | _ -> false) + defs in + if not (List.mem true es) then nerased else + List.fold_left + (fun erased e + -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + erased es + (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) let rec check' erased ctx e = let check = check' in @@ -433,14 +458,17 @@ let rec check' erased ctx e = -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx v ForwardRef t)) ctx defs in - (* FIXME: Allow erasable let-bindings! *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = nerased_let defs erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (v, e, t) - -> assert_type nctx e - (push_susp t (S.shift n)) - (check nerased nctx e); + -> assert_type + nctx e + (push_susp t (S.shift n)) + (check (if DB.set_mem (n - 1) nerased + then DB.set_empty + else nerased) + nctx e); n - 1) (List.length defs) defs in mkSusp (check nerased nctx e) ===================================== tests/eval_test.ml ===================================== @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" let _ = test_eval_eqv_named "Let3" @@ -104,7 +104,15 @@ let _ = test_eval_eqv_named TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" + +let _ = test_eval_eqv_named + "Let-erasable" + + "c = 3; e = 1; f = 2; d = 4;" + + "let id = lambda t ≡> lambda (x : t) -> x; + in (lambda t ≡> let t1 = t in id (t := t1)) 3" (* == *) "3" (* Lambda * ------------------------ *) View it on GitLab: https://gitlab.com/monnier/typer/commit/d21c5eb6bdc2bcc6eb39e601e216fd561be… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/d21c5eb6bdc2bcc6eb39e601e216fd561be… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][graveline] update on macro `case`
by Jonathan Graveline 25 Jul '18

25 Jul '18

Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: c8fad518 by Jonathan Graveline at 2018-07-25T00:08:43Z update on macro `case` - - - - - 2 changed files: - samples/case2.typer - tests/case_test.ml Changes: ===================================== samples/case2.typer ===================================== @@ -106,7 +106,9 @@ renamed-pat pat names = let mf : Sexp -> Int -> Sexp; mf v i = Sexp_dispatch v - (lambda _ _ -> List_nth i names Sexp_error) + (lambda sym ss -> if_then_else_ (Sexp_eq sym (Sexp_symbol "_:=_")) + (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) + (List_nth i names Sexp_error)) (lambda _ -> List_nth i names Sexp_error) serr serr serr serr; @@ -130,9 +132,20 @@ is-pat : Pat -> IO Bool; is-pat pat = let err = lambda _ -> return false; + + serr = lambda _ -> "< error >"; + + sym-str : Sexp -> String; + sym-str sexp = Sexp_dispatch sexp + (lambda _ _ -> serr ()) + (lambda str -> str) + serr serr serr serr; in Sexp_dispatch pat - (lambda _ _ -> return true) + (lambda sym _ -> do { + env <- Elab_getenv (); + return (Elab_isconstructor (sym-str sym) env); + }) (lambda sym -> do { env <- Elab_getenv (); return (Elab_isconstructor sym env); @@ -171,12 +184,14 @@ introduced-vars pat = let ff : IO (List Sexp) -> Sexp -> IO (List Sexp); ff o v = Sexp_dispatch v - (lambda _ _ -> do { + (lambda s ss -> do { o <- o; % bind - %% there's no introduced variable here - %% `case` on sub pattern will introduce new variable - %% but not here - return (List_concat o (cons dflt-var nil)); + if_then_else_ (Sexp_eq s (Sexp_symbol "_:=_")) + (return (List_concat o (cons (List_nth 1 ss Var_error) nil))) + %% there's no introduced variable here + %% `case` on sub pattern will introduce new variable + %% but not here + (return (List_concat o (cons dflt-var nil))); }) (lambda s -> do { o <- o; % bind @@ -201,8 +216,11 @@ in Sexp_dispatch pat wrap-vars : List Var -> List Var -> Code -> Code; wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> + %% + %% I prefer `let` definition because a lambda function would need a type + %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) + %% (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) - %%(quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) fun ivars rvars; %% @@ -308,6 +326,7 @@ in List_foldl ff (return nil) pats; %% %% new variable should be identical for each branches %% but old variable (from user code) are arbitrary +%% (except for explicit field pattern...) %% pattern-term : Pat -> List Var -> IO (List (Pair Var Var)); ===================================== tests/case_test.ml ===================================== @@ -241,8 +241,6 @@ let _ = (add_test "CASE MACROS" "sub pattern 1" (fun () -> let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in - - let print x = print_string ("\n"^(string_of_int x)) in let ret = Elab.eval_expr_str ecode ectx rctx in @@ -251,14 +249,52 @@ let _ = (add_test "CASE MACROS" "sub pattern 1" (fun () -> Vint e; Vint f; Vint g; Vint h] -> ( match (a,b,c,d,e,f,g,h) with | (1,1,1,2,0,0,0,2) -> success () - | (_,_,_,_,_,_,_,_) -> - (print a; print b; print c; print d; - print e; print f; print g; print h; - failure ()) ) + | (_,_,_,_,_,_,_,_) -> failure () ) | _ -> failure ()) ) let _ = (add_test "CASE MACROS" "sub pattern 2" (fun () -> + let dcode = (" + f : List (Option Bool) -> List (Option Bool) -> Int; + f xs ys = case (xs,ys) + | (cons (some true) xs, cons (some true) ys) => f xs ys + | (cons none nil, cons none nil) => 2 + | (cons none xs, cons none ys) => f xs ys + | (nil,nil) => 1 + | (cons (some false) (cons (some false) nil), + cons (some false) (cons (some false) nil)) => 7 + | (_,_) => 0; + + va = f (cons (some true) nil) (cons (some true) nil); + vb = f (cons (some true) (cons (some true) nil)) + (cons (some true) (cons (some true) nil)); + vc = f nil nil; + vd = f (cons (some true) (cons none nil)) (cons (some true) (cons none nil)); + ve = f (cons (some false) nil) (cons (some false) nil); + vf = f (cons none nil) (cons (some true) nil); + vg = f (cons (some true) nil) (cons none nil); + vh = f (cons (none : Option Bool) nil) (cons (none : Option Bool) nil); + vi = f (cons none (cons (some true) nil)) (cons none (cons (some true) nil)); + vj = f (cons (some false) (cons (some false) nil)) + (cons (some false) (cons (some false) nil)); + ") in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "va; vb; vc; vd; ve; vf; vg; vh; vi; vj;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint a; Vint b; Vint c; Vint d; Vint e; + Vint f; Vint g; Vint h; Vint i; Vint j] -> ( + match (a,b,c,d,e,f,g,h,i,j) with + | (1,1,1,2,0,0,0,2,1,7) -> success () + | (_,_,_,_,_,_,_,_,_,_) -> failure () ) + | _ -> failure ()) +) + +let _ = (add_test "CASE MACROS" "sub pattern 3" (fun () -> let dcode = (" f : Option Bool -> Option Bool -> Int; f ob0 ob1 = case (ob0,ob1) @@ -298,7 +334,7 @@ let _ = (add_test "CASE MACROS" "sub pattern 2" (fun () -> | _ -> failure ()) ) -let _ = (add_test "CASE MACROS" "sub pattern 3" (fun () -> +let _ = (add_test "CASE MACROS" "sub pattern 4" (fun () -> let dcode = (" g : Bool -> Bool -> Int; g b0 b1 = case (b0,b1) @@ -362,6 +398,46 @@ let _ = (add_test "CASE MACROS" "no default" (fun () -> | _ -> failure ()) ) +let _ = (add_test "CASE MACROS" "introduced variable name" (fun () -> + let dcode = (" + and : Bool -> Bool -> Int; + and b0 b1 = case (b0, b1) + | (true, true) => 2 + | (true, false) => 1 + | (false, true) => 1 + | (false, false) => 0; + + %% `cons x xs` vs `cons a as` and `cons y ys` vs `cons b bs` + + f : List Bool -> List Bool -> Int; + f xs ys = case (xs, ys) + | (cons x xs, nil) => (and x false) + (f xs nil) + | (nil, cons y ys) => (and false y) + (f nil ys) + | (cons a as, cons b bs) => (and a b) + (f as bs) + | (nil, nil) => 0; + + va = f (cons true nil) nil; + vb = f nil (cons false nil); + vc = f (cons true nil) (cons true nil); + vd = f (cons false nil) (cons false nil); + ve = f (cons true nil) (cons false nil); + vf = f nil nil; + ") in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "va; vb; vc; vd; ve; vf;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint a; Vint b; Vint c; Vint d; Vint e; Vint f] -> ( + match (a,b,c,d,e,f) with + | (1,0,2,0,1,0) -> success () + | (_,_,_,_,_,_) -> failure () ) + | _ -> failure ()) +) + (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/commit/c8fad5182993207af7e5c5b77de524008f2… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/c8fad5182993207af7e5c5b77de524008f2… You're receiving this email because of your account on gitlab.com.

1 0