[ pre-commit ] Add support and hooks

.hlint.yaml

@@ -12,7 +12,7 @@
   - name: [MultiWayIf, PatternGuards, RecordWildCards]
   - name: [ScopedTypeVariables]
   - name: [ConstraintKinds, RankNTypes, TypeFamilies]
-  # - {name: nameEXT, within: [moduleName]} 
+  # - {name: nameEXT, within: [moduleName]}
 
 - flags:
   - default: false
@@ -20,7 +20,7 @@
 
 - modules:
   # if you import Data.Set qualified, it must be as 'Set'
-  - {name: [Data.Set, Data.HashSet], as: Set} 
+  - {name: [Data.Set, Data.HashSet], as: Set}
   - {name: [Data.Map, Data.HashMap.Strict, Data.HashMap.Lazy], as: Map}
   # - {name: Control.Arrow, within: []} # Certain modules are banned entirely
 
@@ -57,4 +57,4 @@
 - ignore: {name: Use let, within: [Test.All]}
 - ignore: {name: Use String}
 - ignore: {name: Avoid restricted flags}
-- ignore: {name: Avoid restricted extensions, within: [MiniJuvix.Parsing.Language]}
+- ignore: {name: Avoid restricted extensions, within: [MiniJuvix.Parsing.Language]}

.pre-commit-config.yaml

@@ -0,0 +1,21 @@
+# $ pip install pre-commit
+# $ pre-commit install
+# $ pre-commit run --all-files
+# See https://pre-commit.com for more information
+# See https://pre-commit.com/hooks.html for more hooks
+repos:
+-   repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v4.1.0
+    hooks:
+    -   id: trailing-whitespace
+    -   id: end-of-file-fixer
+    -   id: check-yaml
+    -   id: check-added-large-files
+    -   id: check-case-conflict
+    -   id: mixed-line-ending
+
+-   repo:  https://github.com/heliaxdev/minijuvix
+    rev: a54abcd6a50518476ee75b329e245c3341d02341
+    hooks:
+    -   id: ormolu
+    -   id: hlint

.pre-commit-hooks.yaml

@@ -0,0 +1,11 @@
+-   id: hlint
+    name: hlint
+    description: Run Hlint linter
+    entry: make hlint
+    language: system
+
+-   id: ormolu
+    name: ormolu
+    description: Run Ormolu linter
+    entry: make format
+    language: system

Makefile

@@ -1,6 +1,8 @@
 PWD=$(CURDIR)
 PREFIX="$(PWD)/.stack-work/prefix"
 UNAME := $(shell uname)
+HLINTQUIET :=
+
 
 ifeq ($(UNAME), Darwin)
 	THREADS := $(shell sysctl -n hw.logicalcpu)
@@ -26,7 +28,8 @@ checklines :
 
 .PHONY : hlint
 hlint :
-	hlint src
+	hlint src ${HLINTQUIET}
+	hlint app ${HLINTQUIET}
 
 .PHONY : haddock
 haddock :
@@ -91,4 +94,4 @@ update-submodules :
 
 .PHONY : minijuvix-stdlib
 minijuvix-stdlib:
-	git submodule update --init minijuvix-stdlib
+	git submodule update --init minijuvix-stdlib

lab/Syntax/Core.agda

@@ -5,7 +5,7 @@ term we must check. Similarly, a term of type InferableTerm, it is a
 term we can infer.
 -}
 
-module MiniJuvix.Syntax.Core 
+module MiniJuvix.Syntax.Core
   where
 
 --------------------------------------------------------------------------------
@@ -14,7 +14,7 @@ open import Haskell.Prelude
 open import Agda.Builtin.Equality
 
 --------------------------------------------------------------------------------
--- Haskell stuff 
+-- Haskell stuff
 --------------------------------------------------------------------------------
 
 {-# FOREIGN AGDA2HS
@@ -44,7 +44,7 @@ instance
   QuantityEq ._==_ Many Many = true
   QuantityEq ._==_ _    _    = false
 {-# COMPILE AGDA2HS QuantityEq #-}
- 
+
 compareQuantity : Quantity -> Quantity -> Ordering
 compareQuantity Zero  Zero = EQ
 compareQuantity Zero  _    = LT
@@ -57,7 +57,7 @@ compareQuantity Many Many  = EQ
 
 instance
   QuantityOrd : Ord Quantity
-  QuantityOrd .compare  = compareQuantity 
+  QuantityOrd .compare  = compareQuantity
   QuantityOrd ._<_  x y = compareQuantity x y == LT
   QuantityOrd ._>_  x y = compareQuantity x y == GT
   QuantityOrd ._<=_ x y = compareQuantity x y /= GT
@@ -114,7 +114,7 @@ relevancy _    = Relevant
 -- Variables. Relevant on the following design is the separation for a
 -- variable between Bound and Free as a data constructr, due to
 -- McBride and McKinna in "Functional Pearl: I am not a Number—I am a
--- Free Variable". 
+-- Free Variable".
 --------------------------------------------------------------------------------
 
 -- DeBruijn index.
@@ -136,7 +136,7 @@ BindingName = String
 -- variable is local free.
 
 data Name : Set where
-  -- the variable has zero binding 
+  -- the variable has zero binding
   Global : String → Name
   -- the variable has a binding in its scope.
   Local : BindingName → Index → Name
@@ -151,14 +151,14 @@ instance
 
 -- A variable is then a number indicating its DeBruijn index.
 -- Otherwise, it is free, with an identifier as a name, or
--- inside 
+-- inside
 data Variable : Set where
   Bound : Index → Variable
   Free  : Name → Variable
 {-# COMPILE AGDA2HS Variable #-}
 
 instance
-  variableEq : Eq Variable 
+  variableEq : Eq Variable
   variableEq ._==_ (Bound x) (Bound y) = x == y
   variableEq ._==_ (Free x) (Free y) = x == y
   variableEq ._==_ _ _ = false
@@ -170,16 +170,16 @@ instance
 --------------------------------------------------------------------------------
 #-}
 
-{- 
+{-
 Core syntax follows the pattern design for bidirectional typing
 algorithmgs in [Dunfield and Krishnaswami, 2019]. Pfenning's principle
 is one of such criterion and stated as follows.
 
 1. If the rule is an introduction rule, make the principal judgement
-   "checking", and 
+   "checking", and
 2. if the rule is an elimination rule, make the principal judgement
    "synthesising".
-   
+
 Jargon:
 - Principal connective of a rule:
   - for an introduction rule is the connective that is being
@@ -199,25 +199,25 @@ data CheckableTerm : Set
 data InferableTerm : Set
 
 data CheckableTerm where
-  {- Universe types. 
+  {- Universe types.
   See the typing rule Univ⇐.
   -}
   UniverseType : CheckableTerm
-  {- Dependent function types. 
+  {- Dependent function types.
   See the typing rules →F⇐ and →I⇐.
     1. (Π[ x :ρ S ] P x) : U
     2. (λ x. t) : Π[ x :ρ S ] P x
   -}
   PiType : Quantity → BindingName → CheckableTerm → CheckableTerm → CheckableTerm
   Lam : BindingName → CheckableTerm → CheckableTerm
-  {- Dependent tensor product types. 
+  {- Dependent tensor product types.
   See the typing rules ⊗-F-⇐,  ⊗-I₀⇐, and ⊗-I₁⇐.
     1. * S ⊗ T : U
     2. (M , N) : S ⊗ T
   -}
   TensorType : Quantity → BindingName → CheckableTerm → CheckableTerm → CheckableTerm
   TensorIntro : CheckableTerm → CheckableTerm → CheckableTerm
-  {- Unit types. 
+  {- Unit types.
   See the typing rule 1-F-⇐ and 1-I-⇐.
     1. 𝟙 : U
     2. ⋆ : 𝟙
@@ -245,11 +245,11 @@ data CheckableTerm where
 #-}
 
 data InferableTerm where
-  -- | Variables, typing rule Var⇒. 
+  -- | Variables, typing rule Var⇒.
   Var : Variable → InferableTerm
   -- | Annotations, typing rule Ann⇒.
   {- Maybe, I want to have the rules here like this:
-  
+
     OΓ ⊢ S ⇐0 𝕌     Γ ⊢ M ⇐0 𝕌
     ­────────────────────────────── Ann⇒
            Γ ⊢ (M : S) ⇒ S
@@ -270,7 +270,7 @@ data InferableTerm where
     → CheckableTerm  -- Type annotation of the result of elimination.
     → InferableTerm
   -- | Sum type eliminator (a.k.a. case)
-  -- let (z : S + T) in (case z of {(inl u) ↦ r1; (inr v) ↦ r2}  :^q  T) 
+  -- let (z : S + T) in (case z of {(inl u) ↦ r1; (inr v) ↦ r2}  :^q  T)
   SumTypeElim        -- Case
     :  Quantity      -- Multiplicity of the sum contents.
     →  BindingName         -- Name of the variable binding the sum in the type
@@ -300,7 +300,7 @@ inferEq : InferableTerm → InferableTerm → Bool
 -- extraneous instance definitions.
 
 checkEq UniverseType UniverseType = true
-checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂) 
+checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂)
   = q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
 checkEq (TensorType q₁ _ a₁ b₁) (TensorType q₂ _ a₂ b₂)
    = q₁ == q₂ && checkEq a₁ a₂ &&  checkEq b₁ b₂
@@ -317,9 +317,9 @@ checkEq _ _ = false
 inferEq (Var x) (Var y) = x == y
 inferEq (Ann x₁ y₁) (Ann x₂ y₂) = checkEq x₁ x₂ &&  checkEq y₁ y₂
 inferEq (App x₁ y₁) (App x₂ y₂) =  inferEq x₁ x₂ &&  checkEq y₁ y₂
-inferEq (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁) (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂) 
+inferEq (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁) (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂)
   = q₁ == q₂ &&  inferEq a₁ a₂ &&  checkEq b₁ b₂ &&  checkEq c₁ c₂
-inferEq (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁) 
+inferEq (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁)
       (SumTypeElim q₂ _ x₂ _ a₂ _ b₂ c₂)
   = q₁ == q₂ &&  inferEq x₁ x₂ && checkEq a₁ a₂ &&  checkEq b₁ b₂ &&  checkEq c₁ c₂
 inferEq _ _ = false
@@ -348,12 +348,12 @@ termEq (Inferable x) (Inferable y) = x == y
 termEq _ _ = false
 {-# COMPILE AGDA2HS termEq #-}
 
-instance 
-  TermEq : Eq Term 
+instance
+  TermEq : Eq Term
   TermEq ._==_ = termEq
 
-{-# COMPILE AGDA2HS TermEq #-}   
+{-# COMPILE AGDA2HS TermEq #-}
 
 --------------------------------------------------------------------------------
 -- Other Instances
---------------------------------------------------------------------------------
+--------------------------------------------------------------------------------

lab/docs/Agda.css

@@ -59,4 +59,4 @@ pre.Agda {
 
 pre.Agda a:hover {
   text-decoration: none;
-}
+}

lab/docs/README.md

@@ -2,7 +2,7 @@
 
 [![hackmd-github-sync-badge](https://hackmd.io/R8f7FXyOTAKdQ5_cZ-L-og/badge)](https://hackmd.io/R8f7FXyOTAKdQ5_cZ-L-og)
 
-<!-- Latex stuff adapted from Andy's record proposal: 
+<!-- Latex stuff adapted from Andy's record proposal:
 https://hackmd.io/Xlvu82eFQ_m-cebUWAtGsw?edit -->
 
 $$
@@ -31,7 +31,7 @@ $$
 
 ###### tags: `Juvix`
 
-## Abstract 
+## Abstract
 
 MiniJuvix implements a programming language that takes variable resources very
 seriously in the programs. As mathematical foundation, we are inspired by
@@ -87,7 +87,7 @@ u, v &\EQ \mathsf{Var}(x)    &\text{variable}\\
 &\OR \color{gray}{D} &\color{gray}{\text{data type decl.}}\\
 &\OR \color{gray}{c} &\color{gray}{\text{data constr.}}\\
 &\OR \color{gray}{R}  &\color{gray}{\text{...check andy's record constr decl..}} \\
-&\OR \color{gray}{r}  &\color{gray}{\text{record. intro}} \\ 
+&\OR \color{gray}{r}  &\color{gray}{\text{record. intro}} \\
 &\OR \color{gray}{\cdots}  &\color{gray}{\text{record. proj.}} \\[.7em]
 \Gamma &\EQ \emptyset \Or \Gamma, x :^{\sigma} A & \text{ contexts}
 \\[1em]
@@ -101,7 +101,7 @@ respectively, using a red and blue arrow.
 
 $$
 \begin{gathered}
-\check{\Gamma}{t}{\sigma}{M}  
+\check{\Gamma}{t}{\sigma}{M}
 \qquad
 \infer{\Gamma}{t}{\sigma}{M}
 \end{gathered}
@@ -117,7 +117,7 @@ computation is required in the $\sigma$ zero theory. Otherwise, we say that the
 **Contexts** The context in which a term is judged is fundamental to determine
 well-formed terms. Another name for context is *environment*. A context can be
 either empty or it can be extended by binding name annotations of the form $x
-\overset{\sigma}{:} M$ for a given type $A$. 
+\overset{\sigma}{:} M$ for a given type $A$.
 
 $$
 \begin{aligned}
@@ -141,7 +141,7 @@ The addition operation for contexts is a binary operation only defined between
 contexts with the same variable set. The latter condition is the proposition
 stating $0 \cdot \Gamma_1 = 0 \cdot \Gamma_2$ between contexts $\Gamma_1$ and
 $\Gamma_2$. Consequently, adding contexts create another context with the same
-variables from the input but with their resource summed up. 
+variables from the input but with their resource summed up.
 
 $$
 \begin{aligned}
@@ -160,7 +160,7 @@ example, in forming new inductive types.
 
 The $\color{gray}{gray}$ cases below are expected to be incorporated in the future.
 
-**Types** A *type* in the theory is one of the following synthactical cases.  
+**Types** A *type* in the theory is one of the following synthactical cases.
 
 $$
 \begin{aligned}
@@ -182,7 +182,7 @@ $\mathsf{False} : \mathsf{Bool}$.
 
 **Terms** We refer to terms as those elements that can inhabit a type. So far,
 we have used as a term the metavariable $x$. A term can take one of the
-following shapes. 
+following shapes.
 
 $$
 \begin{aligned}
@@ -192,7 +192,7 @@ u, v , t , f &\EQ \mathsf{Var}(x)    &\text{(variable)}\\
 &\OR\mathsf{App}(u,v)            &\text{(application)}\\
 &\OR *                           &\text{(unit)}\\
 &\OR \color{gray}{\mathsf{Fun}} &\color{gray}{\text{(named function)}}\\
-&\OR \color{gray}{\mathsf{Con}} &\color{gray}{\text{(data constr.)}} 
+&\OR \color{gray}{\mathsf{Con}} &\color{gray}{\text{(data constr.)}}
 \end{aligned}
 $$
 
@@ -205,9 +205,9 @@ i.e., $x : A$ and $x \overset{\sigma}{:} A$.
 # Typing rules
 
 We present the types rules almost in the same way as one would expect to see them in the
-implementation, i.e., using the bidirectional notation. 
+implementation, i.e., using the bidirectional notation.
 
-It must be assumed that contexts appearing in the rules are *well-formed*, i.e. terms build up using the following derivation rules. 
+It must be assumed that contexts appearing in the rules are *well-formed*, i.e. terms build up using the following derivation rules.
 
 $$
 \rule{\mathsf{empty}\mbox{-}\mathsf{ctx}}{
@@ -262,7 +262,7 @@ $$
 The variables $p_i$ in the rule above are inner steps of the algorithm and the order
 in which they are presented matters. For example, an inner step can be infering
 a type, checking if a property holds for a term, reducing a term, or simply
-checking a term against another type. 
+checking a term against another type.
 
 A *reduction* step is denoted by $\Gamma \vdash
 t \rightsquigarrow t'$ or simply by $t \rightsquigarrow t'$ whenever the context
@@ -299,7 +299,7 @@ conclusion.
 - [x] TensorType
 - [x] TensorIntro
 - [x] UnitType
-- [x] Unit 
+- [x] Unit
 - [ ] SumType
 
 
@@ -313,7 +313,7 @@ $$
 \qquad
 \begin{gathered}
 \rule{Univ{\Leftarrow}}{
-(0\cdot \Gamma) \ \mathsf{ctx} 
+(0\cdot \Gamma) \ \mathsf{ctx}
 }{
 0\cdot \Gamma \vdash \mathcal{U}\, \overset{0}{\color{red}\Leftarrow}\,\, \mathcal{U}
 }
@@ -392,7 +392,7 @@ part of the theory, after studying the usage variable in the conclusion. Recall
 that forming pairs is the way one introduces values of the tensor product.
 One then must check the rule conclusion. After doing this, the types $A$ and $B$ become
 known facts and it makes sense to check the types in the premises. The usage
-bussiness follows a similar reasoning as infering applications. 
+bussiness follows a similar reasoning as infering applications.
 
 
 $$\begin{gathered}
@@ -425,7 +425,7 @@ Finally, we obtain the following two rules that make up the original one.
 0\cdot \Gamma \vdash u \,\overset{0}{\color{red}\Leftarrow}\,A
 \qquad
 \Gamma \vdash v \,\overset{\sigma}{\color{red}\Leftarrow}\,B[u/x]
-\qquad 
+\qquad
 }{
 \Gamma \vdash (u,v)\overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A) \otimes B
 }
@@ -442,7 +442,7 @@ $$
 \qquad
 \color{gray}{0 \cdot \Gamma_1 = 0\cdot \Gamma_2}\quad
 }{
-\color{green}{\sigma\pi}\cdot \Gamma_{1}+\Gamma_{2} \vdash (u,v)\overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A) \otimes B 
+\color{green}{\sigma\pi}\cdot \Gamma_{1}+\Gamma_{2} \vdash (u,v)\overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A) \otimes B
 }
 \end{gathered}
 %
@@ -462,7 +462,7 @@ $$
 }{
 \check{0\cdot\Gamma}{1}{0}{\mathcal{U}}
 }
-\qquad 
+\qquad
 \rule{*\mbox{-}I}{
 0 \cdot \Gamma \ \mathsf{ctx}
 }{
@@ -483,9 +483,9 @@ TODO
 
 
 Include the rules for definitional equality:
-- [ ] β-equality, 
-- [ ] reflexivity, 
-- [ ] symmetry, 
+- [ ] β-equality,
+- [ ] reflexivity,
+- [ ] symmetry,
 - [ ] transitivity, and
 - [ ] congruence.
 
@@ -494,7 +494,7 @@ $$\begin{gathered}
 \rule{conv{\Leftarrow}}{
 \Gamma \vdash M \,\overset{\sigma}{\color{blue}\Rightarrow}\,S \qquad
 \Gamma \vdash S\, \overset{0}{\color{red}\Leftarrow}\, \mathcal{U}\qquad
-\Gamma \vdash T \,\overset{0}{\color{red}\Leftarrow}\,\mathcal{U} \qquad 
+\Gamma \vdash T \,\overset{0}{\color{red}\Leftarrow}\,\mathcal{U} \qquad
 \color{green}{S =_{\beta} T}\ \,\,\,
 }{
 \Gamma \vdash M \overset{\sigma}{\color{red}\Leftarrow} T
@@ -507,7 +507,7 @@ $$
 ## Type inference
 
 The algorithm that implements type inference is called `infer`. Inspired by Agda and its inference strategy, MiniJuvix only infer values that are *uniquely* determined by the context.
-There are no guesses. Either we fail or get a unique answer, giving us a predicatable behaviour. 
+There are no guesses. Either we fail or get a unique answer, giving us a predicatable behaviour.
 
 
 By design, a term is inferable if it is one of the following cases.
@@ -518,7 +518,7 @@ By design, a term is inferable if it is one of the following cases.
 - [x] Tensor type elim
 - [ ] Sum type elim
 
-Each case above has as a rule in what follows. 
+Each case above has as a rule in what follows.
 
 The Haskell type of `infer` would be similar as the following.
 
@@ -529,7 +529,7 @@ infer :: Quantity -> InferableTerm -> Output (Type , Resources)
 where
 
 ```haskell
-Output = Either ErrorType 
+Output = Either ErrorType
 Resources = Map Name Quantity
 ```
 
@@ -558,19 +558,19 @@ $$
 3. Therefore, we ask if the variable is in the context.
 4. If it's not the case, throw an error.
 5. Otherwise, one gets a hypothesis $x :^\sigma S$ from the context that matches $x$.
-6. At the end, we return two things: 
+6. At the end, we return two things:
   6.1. first, the inferred type and
   6.2. a table with the new usage information for  each variable.
-  
+
 Haskell prototype:
 
 ```haskell
 infer σ (Free x) = do
   Γ <- asks contextMonad
   case find ((== x) . getVarName) Γ of
-    Just (BindingName _ _σ typeM) 
+    Just (BindingName _ _σ typeM)
       -> return (typeM, updateResources (x, _σ) )
-    Nothing               
+    Nothing
       -> throwError "Variable not present in the context"
 ```
 
@@ -606,7 +606,7 @@ one issue here. This type checking expects $A$ to be in normal form. When it is
 not, typechecking the judgement $\Gamma \vdash x \Leftarrow^\sigma A$ may give us
 a false negative.
 
-  - *Example*: Why do we need $A'$? Imagine that we want to infer the type of $v$ given $\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2))$. Clearly, the answer should be `Vec(Nat,4)`. 
+  - *Example*: Why do we need $A'$? Imagine that we want to infer the type of $v$ given $\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2))$. Clearly, the answer should be `Vec(Nat,4)`.
   However, this reasoning step requires computation. $$\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2)) \Rightarrow \mathsf{Vec}(\mathsf{Nat},4))\,.$$
 
 - Using $M'$ as the normal form of $A$, it remains to check if $x$ is of type
@@ -674,7 +674,7 @@ $$
 
 The first judgement about $f$ is *principal*. Then, it must be an inference step.
 After having inferred the type of $f$, the types $A$ and $B$ become known facts.
-It is then correct to check the type of $x$ against $A$. 
+It is then correct to check the type of $x$ against $A$.
 
 $$\begin{gathered}
 \rule{}{
@@ -738,7 +738,7 @@ infer σ (App f x) = do
     IsPiType π _ typeA typeB -> do
       σπ <- case (σ .*. π) of
        -- Rule No. 1
-       Zero -> do 
+       Zero -> do
          (_ , nqs) <- check x typeA (mult Zero context)
           return nqs
        -- Rule No. 2
@@ -774,7 +774,7 @@ $$\begin{gathered}
 \check{(\Gamma_{2}, u \overset{\sigma\pi}{:} A, v\overset{\sigma}{:}B)}{%
 N}{\sigma}{C[(x,y)/z]}
 }{
-\Gamma_{1}+\Gamma_{2} \vdash \mathsf{let}\,z@(u,v)=M\,\,\mathsf{in}\,\,N :C \overset{\sigma}{\color{blue}\Rightarrow}\, C[M/x] 
+\Gamma_{1}+\Gamma_{2} \vdash \mathsf{let}\,z@(u,v)=M\,\,\mathsf{in}\,\,N :C \overset{\sigma}{\color{blue}\Rightarrow}\, C[M/x]
 }
 \end{gathered}
 %

lab/docs/examples/Example1.mjuvix

@@ -1,7 +1,7 @@
 -- Comments as in Haskell.
 --This is another comment
 ------ This is another comment
--- This is another comment --possible text-- 
+-- This is another comment --possible text--
   -- This is a comment, as it is not indent
   -- sensitive. It should be fine.
 
@@ -12,7 +12,7 @@
 -- where let in
 
 -- Options to check/run this file.
-options { 
+options {
 debug   := INFO;
 phase   := { parsing , check };
 backend := none; -- llvm.
@@ -34,7 +34,7 @@ import Backend {LLVM};   -- imports to local scope a var. called LLVM.
 import Prelude hiding {Nat, Vec, Empty, Unit};
 	-- same as before, but without the names inside `hiding`
 
--- Judgement decl. 
+-- Judgement decl.
 -- `x : M;`
 
 -- Nonindexed inductive type declaration:
@@ -48,19 +48,19 @@ inductive Nat
 -- == is not a reserved name.
 -- === is a reserved symbol for def. equality.
 zero' : Nat;
-zero'                 
-:= zero; 
+zero'
+:= zero;
 
 -- Axioms/definitions.
 axiom A : Type;
-axiom a a' : A; 
+axiom a a' : A;
 
 f : Nat -> A;
 f := \x -> match x
 {
 	zero |-> a  ;
 	suc  |-> a' ;
-}; 
+};
 
 g : Nat -> A;
 g Nat.zero    := a;
@@ -137,7 +137,7 @@ h''' : Person -> String;
 h''' p := p.name;
 
 -- So far, we haven't used quantites, here is some examples.
--- We mark a type judgment `x : M` of quantity n as `x :n M`. 
+-- We mark a type judgment `x : M` of quantity n as `x :n M`.
 -- If the quantity n is not explicit, then the judgement
 -- is `x :Any M`.
 
@@ -146,7 +146,7 @@ axiom z :0 A;
 axiom B : (x :1 A) -> Type;   -- type family
 axiom T : [ A ] B;            -- Tensor product type. usages Any
 axiom T' : [ x :1 A ] B;      -- Tensor product type.
-axiom em : (x :1 A) -> B;  
+axiom em : (x :1 A) -> B;
 
 -- Tensor product type.
 f' : [ x :1 A ] -> B;
@@ -154,8 +154,8 @@ f' x := em x;
 
 -- Pattern-matching on tensor pairs;
 
-g' : ([ A -> B ] A) -> B;  -- it should be the same as `[ A -> B ] A -> B` 
-g' (k , a) = k a; 			   
+g' : ([ A -> B ] A) -> B;  -- it should be the same as `[ A -> B ] A -> B`
+g' (k , a) = k a;
 
 g'' : ([ A -> B ] A) -> B;
 g'' = \p -> match p {
@@ -169,7 +169,7 @@ axiom D : Type;
 record P (A : Type) (B : A -> Type) {
 	proj1 : C;
 	proj2 :0 D;
-} 
+}
 eta-equality, constructor prop;  -- extra options.
 
 -- More inductive types.

lab/docs/examples/Example2.mjuvix

@@ -33,10 +33,10 @@ False : Bool;
 };
 
 accept-withdraws-from : Storage -> Storage -> Bool;
-accept-withdraws-from initial final := 
+accept-withdraws-from initial final :=
   let { trusted? := determine-trust-level initial.trans.receiver.name; }
   in match trusted? {
-     Trusted funds |-> 
+     Trusted funds |->
           funds.maximum-withdraw >=final.trans.sender.balance - initial.trans.sender.balance;
      NotTrusted |-> False;
   };

lab/docs/examples/Example3.mjuvix

@@ -17,7 +17,7 @@ record Transaction {
 record Storage { trans : Transaction; };
 
 determine-maximum-withdraw : String -> Nat;
-determine-maximum-withdraw s := 
+determine-maximum-withdraw s :=
   if s === "bob" then 30
   else if s === "maria" then 50
   else 0;
@@ -26,7 +26,7 @@ accept-withdraws-from : Storage -> Storage -> Bool;
 accept-withdraws-from initial final :=
   let { withdrawl-amount :=
     determine-maximum-withdraw initial.trans.receiver.name;
-  } in 
+  } in
   withdrawl-amount >= final.trans.sender.balance - initial.trans.sender.balance;
 
 end Example3;

lab/docs/examples/declarations/module/examples/E2.mjuvix

@@ -5,4 +5,4 @@ module Top;
   module B;
     module O; end;
   end;
-end;
+end;

lab/docs/examples/declarations/module/examples/E3.mjuvix

@@ -1,4 +1,4 @@
 module Top;
   module A; end;
   module A; end;
-end;
+end;

lab/docs/examples/declarations/module/examples/T.mjuvix

@@ -3,4 +3,4 @@ module Top;
     module P; end;
   end;
   import A;
-end;
+end;

lab/docs/examples/declarations/module/fail/E2.test

@@ -31,4 +31,4 @@ Module
 $ stack -- exec minijuvix scope ./../examples/E2.mjuvix
 >2
 minijuvix: user error (ErrAlreadyDefined (Sym "O"))
->= 1
+>= 1

lab/docs/examples/declarations/module/fail/E3.test

@@ -19,4 +19,4 @@ Module
 $ stack -- exec minijuvix scope ./../examples/E3.mjuvix
 >2
 minijuvix: user error (ErrAlreadyDefined (Sym "A"))
->= 1
+>= 1

lab/docs/examples/declarations/module/fail/T.test

@@ -1,4 +1,4 @@
 $ stack -- exec minijuvix scope ./../examples/T.mjuvix
 >2
 minijuvix: examples/T.mjuvix/A.mjuvix: openFile: inappropriate type (Not a directory)
->= 1
+>= 1

lab/docs/examples/declarations/module/succeed/T.test

@@ -24,4 +24,4 @@ Module
             }
       ]
   }
->= 0
+>= 0

lab/docs/examples/syntax.miniju

@@ -48,4 +48,4 @@ module Example where
      one : ℕ ;
      one = suc zero ;
 
-end
+end

lab/docs/examples/token.mjuvix

@@ -147,7 +147,7 @@ account-sub Accounts add number =
 
 
 // No feedback given, so don't know next move :(
-transfer-sub : 
+transfer-sub :
   (acc : Accounts) ->
   (add : Address) ->
   (num : Nat) ->

lab/docs/main.css

@@ -87,4 +87,4 @@ pre {
     font-size: smaller;
     color: gray;
     margin-left: 20px;
-}
+}

lab/docs/notes/tooling.md

@@ -30,7 +30,7 @@ Tools used so far:
   [gluedeval](https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784).
   During elaboration different kind of evaluation strategies may be
   needed.
-    - top vs. local scope. 
+    - top vs. local scope.
 - On equality type-checking, see
   [abstract](https://github.com/anjapetkovic/anjapetkovic.github.io/blob/master/talks/2021-06-17-TYPES2021/abstract.pdf)
 - To document the code, see
@@ -49,7 +49,7 @@ See https://kowainik.github.io/posts/deriving.
   moment, I'm using cabal-edit to keep the bounds and this tool does
   not support stanzas. So be it.
 
-- Using MultiParamTypeClasses to allow me deriving multi instances in one line. 
+- Using MultiParamTypeClasses to allow me deriving multi instances in one line.
 
 - TODO: make a `ref.bib` listing all the repositories and the
   source-code from where I took code, inspiration, whatever thing.

lab/docs/template.html5

@@ -72,4 +72,4 @@ $lastCommit$
 </pre>
 $endif$
 </body>
-</html>
+</html>

stack.yaml

@@ -2,4 +2,4 @@ ghc-options:
   "$locals": -optP-Wno-nonportable-include-path
 resolver: nightly-2022-03-23
 allow-newer: true
-extra-deps: []
+extra-deps: []

tests/negative/BindGroupConflict/Clause.mjuvix

@@ -7,4 +7,4 @@ module Clause;
   fst : (a : Type) → (b : Type) → Pair a b → a ;
   fst _ _ (mkPair _ _ x x) ≔ x;
 
-end;
+end;

tests/negative/BindGroupConflict/Lambda.mjuvix

@@ -7,4 +7,4 @@ module Lambda;
   fst : (a : Type) → (b : Type) → Pair a b → a ;
   fst ≔ λ { _ _ (mkPair _ _ x x) ↦ x };
 
-end;
+end;

tests/negative/DuplicateFixity.mjuvix

@@ -5,4 +5,4 @@ module DuplicateFixity;
 
   infixl 3 +;
   axiom + : Type → Type → Type;
-end;
+end;

tests/negative/ImportCycle/A.mjuvix

@@ -1,4 +1,4 @@
 module A;
 
 import B;
-end;
+end;

tests/negative/ImportCycle/B.mjuvix

@@ -2,4 +2,4 @@ module B;
 
 import C;
 
-end;
+end;

tests/negative/ImportCycle/C.mjuvix

@@ -1,3 +1,3 @@
 module C;
 import D;
-end;
+end;

tests/negative/ImportCycle/D.mjuvix

@@ -2,4 +2,4 @@ module D;
 
 import B;
 
-end;
+end;

tests/negative/InfixError.mjuvix

@@ -4,4 +4,4 @@ module InfixError;
   axiom + : Type → Type → Type;
 
   axiom T : Type + Type + ;
-end;
+end;

tests/negative/InfixErrorP.mjuvix

@@ -9,4 +9,4 @@ module InfixErrorP;
   fst : Pair → Type;
   fst (x , ) ≔ x;
 
-end;
+end;

tests/negative/LacksFunctionClause.mjuvix

@@ -1,4 +1,4 @@
 module LacksFunctionClause;
 
   id : Type → Type → Type;
-end;
+end;

tests/negative/LacksTypeSig.mjuvix

@@ -2,4 +2,4 @@ module LacksTypeSig;
 
 
    some ≔ Type;
-end;
+end;

tests/negative/ModuleNotInScope.mjuvix

@@ -8,4 +8,4 @@ module ModuleNotInScope;
     open M;
 
 
-end;
+end;

tests/negative/MultipleDeclarations.mjuvix

@@ -4,4 +4,4 @@ module MultipleDeclarations;
 
 
   axiom a : Type;
-end;
+end;

tests/negative/MultipleExportConflict.mjuvix

@@ -5,4 +5,4 @@ module MultipleExportConflict;
   end;
   open A public;
   axiom e : Type;
-end;
+end;

tests/negative/NotInScope.mjuvix

@@ -6,4 +6,4 @@ module NotInScope;
 
   axiom test : bla;
 
-end;
+end;

tests/negative/UnusedOperatorDef.mjuvix

@@ -1,3 +1,3 @@
 module UnusedOperatorDef;
   infixl 12 + ;
-end ;
+end ;

tests/negative/WrongModuleName.mjuvix

@@ -1,3 +1,3 @@
 module Haha;
 
-end;
+end;

tests/positive/Imports/A.mjuvix

@@ -11,5 +11,5 @@ module A;
   end ;
   import M;
   f : M.N.T;
-  f (_ M.N.t _) ≔ Type M.+ Type; 
-end;
+  f (_ M.N.t _) ≔ Type M.+ Type;
+end;

tests/positive/Imports/M.mjuvix

@@ -1,3 +1,3 @@
 module M;
   axiom T : Type;
-end;
+end;

tests/positive/Inductive.mjuvix

@@ -3,4 +3,4 @@ module Inductive;
   inductive T {
     t : T;
   };
-end ;
+end ;

tests/positive/Literals.mjuvix

@@ -17,4 +17,4 @@ module Literals;
 
   c : String;
   c := "hellooooo";
-end;
+end;

tests/positive/MicroJuvix/Simple.mjuvix

@@ -41,4 +41,4 @@ module Simple;
   sum : List → Nat;
   sum ≔ foldr (+) zero;
 
-end;
+end;

tests/positive/Operators.mjuvix

@@ -12,4 +12,4 @@ module Operators;
   plus3 : Type → Type → Type → Type → Type;
   plus3 a b c d ≔ (+) (a + b) ((+) c d);
 
-end;
+end;

tests/positive/StdlibList/Data/List.mjuvix

@@ -94,4 +94,4 @@ quickSort a cmp (∷ _ x ys) ≔
     gex y ≔ not (ltx y)
   };
 
-end;
+end;

tests/positive/StdlibList/Data/Maybe.mjuvix

@@ -5,4 +5,4 @@ module Data.Maybe;
      just : a → Maybe a;
   }
 
-end;
+end;

tests/positive/StdlibList/Data/Nat.mjuvix

@@ -14,4 +14,4 @@ module Data.Nat;
   * zero b ≔ zero;
   * (suc a) b ≔ b + a * b;
 
-end;
+end;

tests/positive/StdlibList/Data/Ord.mjuvix

@@ -4,4 +4,4 @@ module Data.Ord;
       EQ : Ordering;
       GT : Ordering;
     };
-end;
+end;

tests/positive/StdlibList/Data/Product.mjuvix

@@ -6,4 +6,4 @@ inductive × (a : Type) (b : Type) {
   , : a → b → a × b;
 };
 
-end;
+end;

tests/positive/Termination/Ack.mjuvix

@@ -7,4 +7,4 @@ module Ack;
   ack (suc m) zero ≔ ack m (suc zero);
   ack (suc m) (suc n) ≔ ack m (ack (suc m) n);
 
-end;
+end;

tests/positive/Termination/Data/Bool.mjuvix

@@ -22,4 +22,4 @@ module Data.Bool;
   ite _ true a _ ≔ a;
   ite _ false _ b ≔ b;
 
-end;
+end;

tests/positive/Termination/Data/List.mjuvix

@@ -103,4 +103,4 @@ addord (Lim f)  y := Lim (aux-addord f y);
 -- where
 aux-addord f y z := addord (f z) y;
 
-end;
+end;

tests/positive/Termination/Data/Maybe.mjuvix

@@ -5,4 +5,4 @@ module Data.Maybe;
      just : a → Maybe a;
   }
 
-end;
+end;

tests/positive/Termination/Data/Nat.mjuvix

@@ -25,4 +25,4 @@ module Data.Nat;
 
   odd zero ≔ false;
   odd (suc n) ≔ even n;
-end;
+end;

tests/positive/Termination/Data/Ord.mjuvix

@@ -4,4 +4,4 @@ module Data.Ord;
       EQ : Ordering;
       GT : Ordering;
     };
-end;
+end;

tests/positive/Termination/Data/Product.mjuvix

@@ -6,4 +6,4 @@ inductive × (a : Type) (b : Type) {
   , : a → b → a × b;
 };
 
-end;
+end;

tests/positive/Termination/Data/Tree.mjuvix

@@ -12,4 +12,4 @@ g : (A : Type) → Tree A → Tree A → Tree A;
 g A x leaf         := x;
 g A x (branch y z) := g A z (g A x y);
 
-end;
+end;

tests/positive/VP/SimpleFungibleToken.mjuvix

@@ -147,4 +147,3 @@ vp token keys-changed verifiers :=
   auxVP (foldl (check-keys verifiers) (MakePair 0 false) keys-changed);
 
 end;
-