[ lab ] folder organization

lab/Syntax/Core.agda

@@ -0,0 +1,359 @@
+{-
+This module exposes the Internal syntax. A term is either checkable or
+inferable. As the name indicates, a term of type CheckableTerm is a
+term we must check. Similarly, a term of type InferableTerm, it is a
+term we can infer.
+-}
+
+module MiniJuvix.Syntax.Core 
+  where
+
+--------------------------------------------------------------------------------
+
+open import Haskell.Prelude
+open import Agda.Builtin.Equality
+
+--------------------------------------------------------------------------------
+-- Haskell stuff 
+--------------------------------------------------------------------------------
+
+{-# FOREIGN AGDA2HS
+{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+#-}
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+
+import MiniJuvix.Prelude
+
+--------------------------------------------------------------------------------
+-- Quantity (a.k.a. Usage)
+--------------------------------------------------------------------------------
+#-}
+
+data Quantity : Set where
+  Zero One Many : Quantity
+{-# COMPILE AGDA2HS Quantity #-}
+
+instance
+  QuantityEq : Eq Quantity
+  QuantityEq ._==_ Zero Zero = true
+  QuantityEq ._==_ One  One  = true
+  QuantityEq ._==_ Many Many = true
+  QuantityEq ._==_ _    _    = false
+{-# COMPILE AGDA2HS QuantityEq #-}
+ 
+compareQuantity : Quantity -> Quantity -> Ordering
+compareQuantity Zero  Zero = EQ
+compareQuantity Zero  _    = LT
+compareQuantity _    Zero  = GT
+compareQuantity One  One   = EQ
+compareQuantity One  _     = LT
+compareQuantity _    One   = GT
+compareQuantity Many Many  = EQ
+{-# COMPILE AGDA2HS compareQuantity #-}
+
+instance
+  QuantityOrd : Ord Quantity
+  QuantityOrd .compare  = compareQuantity 
+  QuantityOrd ._<_  x y = compareQuantity x y == LT
+  QuantityOrd ._>_  x y = compareQuantity x y == GT
+  QuantityOrd ._<=_ x y = compareQuantity x y /= GT
+  QuantityOrd ._>=_ x y = compareQuantity x y /= LT
+  QuantityOrd .max  x y = if compareQuantity x y == LT then y else x
+  QuantityOrd .min  x y = if compareQuantity x y == GT then y else x
+  -- Using ordFromCompare didnn' work, I might need to open an issue
+  -- for this in agda2hs, Idk.
+
+-- The type of usages forms an ordered semiring.
+
+instance
+  QuantitySemigroup : Semigroup Quantity
+  QuantitySemigroup ._<>_ Zero _ = Zero
+  QuantitySemigroup ._<>_ One m = m
+  QuantitySemigroup ._<>_ Many Zero = Zero
+  QuantitySemigroup ._<>_ Many One = Many
+  QuantitySemigroup ._<>_ Many Many = Many
+
+  QuantityMon : Monoid Quantity
+  QuantityMon .mempty = Zero
+
+  QuantitySemiring : Semiring Quantity
+  QuantitySemiring .one = One
+  QuantitySemiring .times Zero _ = Zero
+  QuantitySemiring .times One m = m
+  QuantitySemiring .times Many Zero = Zero
+  QuantitySemiring .times Many One = Many
+  QuantitySemiring .times Many Many = Many
+
+{-# COMPILE AGDA2HS QuantityOrd #-}
+{-# COMPILE AGDA2HS QuantitySemigroup #-}
+{-# COMPILE AGDA2HS QuantityMon #-}
+{-# COMPILE AGDA2HS QuantitySemiring #-}
+
+--------------------------------------------------------------------------------
+-- Being relevant for a term is to have non zero quantity.
+
+data Relevance : Set where
+  Relevant   : Relevance  -- terms to compute.
+  Irrelevant : Relevance  -- terms to contemplate (for type formation).
+{-# COMPILE AGDA2HS Relevance #-}
+{-# FOREIGN AGDA2HS
+deriving stock instance Eq Relevance
+deriving stock instance Ord Relevance
+#-}
+
+relevancy : Quantity → Relevance
+relevancy Zero = Irrelevant
+relevancy _    = Relevant
+{-# COMPILE AGDA2HS relevancy #-}
+
+--------------------------------------------------------------------------------
+-- 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". 
+--------------------------------------------------------------------------------
+
+-- DeBruijn index.
+Index : Set
+Index = Nat
+{-# COMPILE AGDA2HS Index #-}
+
+-- A variable can be "bound", "binding bound", or simply free. For
+-- example, consider  the term "x(λy.y)". The variable x is free, the
+-- first y is a binding bound variable, and the latter y is bound.
+
+BindingName : Set
+BindingName = String
+{-# COMPILE AGDA2HS BindingName #-}
+
+-- A named variable can be in a local or global enviroment. In the
+-- lambda term above, for example, the second occurrence of y is
+-- globally bound. However, inside the the body of the lambda, the
+-- variable is local free.
+
+data Name : Set where
+  -- the variable has zero binding 
+  Global : String → Name
+  -- the variable has a binding in its scope.
+  Local : BindingName → Index → Name
+{-# COMPILE AGDA2HS Name #-}
+
+instance
+  nameEq : Eq Name
+  nameEq ._==_ (Global x) (Global y) = x == y
+  nameEq ._==_ (Local x1 y1) (Local x2 y2) = x1 == x2 && y1 == y2
+  nameEq ._==_ _ _ = false
+{-# COMPILE AGDA2HS nameEq #-}
+
+-- A variable is then a number indicating its DeBruijn index.
+-- Otherwise, it is free, with an identifier as a name, or
+-- inside 
+data Variable : Set where
+  Bound : Index → Variable
+  Free  : Name → Variable
+{-# COMPILE AGDA2HS Variable #-}
+
+instance
+  variableEq : Eq Variable 
+  variableEq ._==_ (Bound x) (Bound y) = x == y
+  variableEq ._==_ (Free x) (Free y) = x == y
+  variableEq ._==_ _ _ = false
+{-# COMPILE AGDA2HS variableEq #-}
+
+-- TODO: May I want to have Instances of Ord, Functor, Applicative, Monad?
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+#-}
+
+{- 
+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 
+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
+    introduced.
+  - for a elimination rule is the connective that is eliminated.
+- Principal Judgement of a rule is the judgment that contains the
+  principal connective.
+-}
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+-- Type-checkable terms.
+--------------------------------------------------------------------------------
+#-}
+
+data CheckableTerm : Set
+data InferableTerm : Set
+
+data CheckableTerm where
+  {- Universe types. 
+  See the typing rule Univ⇐.
+  -}
+  UniverseType : CheckableTerm
+  {- 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. 
+  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. 
+  See the typing rule 1-F-⇐ and 1-I-⇐.
+    1. 𝟙 : U
+    2. ⋆ : 𝟙
+  -}
+  UnitType : CheckableTerm
+  Unit : CheckableTerm
+  {- Disjoint sum types.
+  See the typing rules
+    1. S + T : U
+    2. inl x : S + T
+    3. inr x : S + T
+  -}
+  SumType : CheckableTerm → CheckableTerm → CheckableTerm
+  Inl : CheckableTerm → CheckableTerm
+  Inr : CheckableTerm → CheckableTerm
+  -- Inferrable terms are clearly checkable, see typing rule Inf⇐.
+  Inferred : InferableTerm → CheckableTerm
+
+{-# COMPILE AGDA2HS CheckableTerm #-}
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+-- Type-inferable terms (a.k.a terms that synthesise)
+--------------------------------------------------------------------------------
+#-}
+
+data InferableTerm where
+  -- | 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
+  -}
+  Ann : CheckableTerm → CheckableTerm → InferableTerm
+  -- |  Application (eliminator).
+  App : InferableTerm → CheckableTerm → InferableTerm
+  -- | Dependent Tensor product eliminator. See section 2.1.3 in Atkey 2018.
+  -- let z@(u, v) = M in N :^q (a ⊗ b))
+  TensorTypeElim
+    : Quantity       -- q is the multiplicity of the eliminated pair.
+    → BindingName          -- z is the name of the variable binding the pair in the
+                     -- type annotation of the result of elimination.
+    → BindingName          -- u is the name of the variable binding the first element.
+    → BindingName          -- v is the name of the variable binding the second element.
+    → InferableTerm  -- (u,v) is the eliminated pair.
+    → CheckableTerm  -- Result of the elimination.
+    → 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) 
+  SumTypeElim        -- Case
+    :  Quantity      -- Multiplicity of the sum contents.
+    →  BindingName         -- Name of the variable binding the sum in the type
+                     -- annotation of the result of elimination.
+    → InferableTerm  -- The eliminated sum.
+    → BindingName          -- u is the name of the variable binding the left element.
+    → CheckableTerm  -- r1 is the result of the elimination in case the sum contains
+                     -- the left element.
+    → BindingName          -- v is the name of the variable binding the right element.
+    → CheckableTerm  -- r2 is the result of the elimination in case the sum contains
+                     -- the right element.
+    → CheckableTerm  -- Type annotation of the result of the elimination.
+    → InferableTerm
+{-# COMPILE AGDA2HS InferableTerm #-}
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+-- Term Equality
+--------------------------------------------------------------------------------
+#-}
+
+checkEq : CheckableTerm → CheckableTerm → Bool
+inferEq : InferableTerm → InferableTerm → Bool
+
+-- We below explicitly use `checkEq` and `inferEq` to have a more
+-- reliable Haskell output using Agda2HS. The traditional way gives an
+-- extraneous instance definitions.
+
+checkEq UniverseType UniverseType = true
+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₂
+checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq UnitType UnitType = true
+checkEq Unit Unit = true
+checkEq (SumType x₁ y₁) (SumType x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq (Inl x) (Inl y) = checkEq  x y
+checkEq (Inr x) (Inr y) = checkEq  x y
+checkEq (Inferred x) (Inferred y) = inferEq x y
+checkEq _ _ = false
+{-# COMPILE AGDA2HS checkEq #-}
+
+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₂) 
+  = q₁ == q₂ &&  inferEq a₁ a₂ &&  checkEq b₁ b₂ &&  checkEq c₁ 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
+{-# COMPILE AGDA2HS inferEq #-}
+
+instance
+  CheckableTermEq : Eq CheckableTerm
+  CheckableTermEq ._==_ = checkEq
+{-# COMPILE AGDA2HS CheckableTermEq #-}
+
+instance
+  InferableTermEq : Eq InferableTerm
+  InferableTermEq ._==_ = inferEq
+{-# COMPILE AGDA2HS InferableTermEq #-}
+
+data Term : Set where
+  Checkable : CheckableTerm → Term  -- terms with a type checkable.
+  Inferable : InferableTerm → Term  -- terms that which types can be inferred.
+{-# COMPILE AGDA2HS Term #-}
+
+termEq : Term → Term → Bool
+termEq (Checkable (Inferred x))  (Inferable y) = x == y
+termEq (Checkable x) (Checkable y) = x == y
+termEq (Inferable x) (Checkable (Inferred y)) = x == y
+termEq (Inferable x) (Inferable y) = x == y
+termEq _ _ = false
+{-# COMPILE AGDA2HS termEq #-}
+
+instance 
+  TermEq : Eq Term 
+  TermEq ._==_ = termEq
+
+{-# COMPILE AGDA2HS TermEq #-}   
+
+--------------------------------------------------------------------------------
+-- Other Instances
+--------------------------------------------------------------------------------

lab/Syntax/Core.hs

@@ -0,0 +1,200 @@
+{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
+
+module MiniJuvix.Syntax.Core where
+
+--------------------------------------------------------------------------------
+
+-- import Algebra.Graph.Label (Semiring (..))
+import MiniJuvix.Prelude hiding (Local)
+import Numeric.Natural (Natural)
+
+--------------------------------------------------------------------------------
+-- Quantity (a.k.a. Usage)
+--------------------------------------------------------------------------------
+
+data Quantity
+  = Zero
+  | One
+  | Many
+
+instance Eq Quantity where
+  Zero == Zero = True
+  One == One = True
+  Many == Many = True
+  _ == _ = False
+
+compareQuantity :: Quantity -> Quantity -> Ordering
+compareQuantity Zero Zero = EQ
+compareQuantity Zero _ = LT
+compareQuantity _ Zero = GT
+compareQuantity One One = EQ
+compareQuantity One _ = LT
+compareQuantity _ One = GT
+compareQuantity Many Many = EQ
+
+instance Ord Quantity where
+  compare = compareQuantity
+  x < y = compareQuantity x y == LT
+  x > y = compareQuantity x y == GT
+  x <= y = compareQuantity x y /= GT
+  x >= y = compareQuantity x y /= LT
+  max x y = if compareQuantity x y == LT then y else x
+  min x y = if compareQuantity x y == GT then y else x
+
+instance Semigroup Quantity where
+  Zero <> _ = Zero
+  One <> m = m
+  Many <> Zero = Zero
+  Many <> One = Many
+  Many <> Many = Many
+
+instance Monoid Quantity where
+  mempty = Zero
+
+instance Semiring Quantity where
+  one = One
+  (<.>) Zero _ = Zero
+  (<.>) One m = m
+  (<.>) Many Zero = Zero
+  (<.>) Many One = Many
+  (<.>) Many Many = Many
+
+data Relevance
+  = Relevant
+  | Irrelevant
+
+deriving stock instance Eq Relevance
+
+deriving stock instance Ord Relevance
+
+relevancy :: Quantity -> Relevance
+relevancy Zero = Irrelevant
+relevancy _ = Relevant
+
+type Index = Natural
+
+type BindingName = String
+
+data Name
+  = Global String
+  | Local BindingName Index
+
+instance Eq Name where
+  Global x == Global y = x == y
+  Local x1 y1 == Local x2 y2 = x1 == x2 && y1 == y2
+  _ == _ = False
+
+data Variable
+  = Bound Index
+  | Free Name
+
+instance Eq Variable where
+  Bound x == Bound y = x == y
+  Free x == Free y = x == y
+  _ == _ = False
+
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+-- Type-checkable terms.
+--------------------------------------------------------------------------------
+
+data CheckableTerm
+  = UniverseType
+  | PiType Quantity BindingName CheckableTerm CheckableTerm
+  | Lam BindingName CheckableTerm
+  | TensorType Quantity BindingName CheckableTerm CheckableTerm
+  | TensorIntro CheckableTerm CheckableTerm
+  | UnitType
+  | Unit
+  | SumType CheckableTerm CheckableTerm
+  | Inl CheckableTerm
+  | Inr CheckableTerm
+  | Inferred InferableTerm
+
+data InferableTerm
+  = Var Variable
+  | Ann CheckableTerm CheckableTerm
+  | App InferableTerm CheckableTerm
+  | TensorTypeElim
+      Quantity
+      BindingName
+      BindingName
+      BindingName
+      InferableTerm
+      CheckableTerm
+      CheckableTerm
+  | SumTypeElim
+      Quantity
+      BindingName
+      InferableTerm
+      BindingName
+      CheckableTerm
+      BindingName
+      CheckableTerm
+      CheckableTerm
+
+--------------------------------------------------------------------------------
+-- Type-inferable terms (a.k.a terms that synthesise)
+--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
+-- Term Equality
+--------------------------------------------------------------------------------
+
+checkEq :: CheckableTerm -> CheckableTerm -> Bool
+checkEq UniverseType UniverseType = True
+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₂
+checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂) =
+  checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq UnitType UnitType = True
+checkEq Unit Unit = True
+checkEq (SumType x₁ y₁) (SumType x₂ y₂) =
+  checkEq x₁ x₂ && checkEq y₁ y₂
+checkEq (Inl x) (Inl y) = checkEq x y
+checkEq (Inr x) (Inr y) = checkEq x y
+checkEq (Inferred x) (Inferred y) = inferEq x y
+checkEq _ _ = False
+
+inferEq :: InferableTerm -> InferableTerm -> Bool
+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₂) =
+    q₁ == q₂ && inferEq a₁ a₂ && checkEq b₁ b₂ && checkEq c₁ 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
+
+instance Eq CheckableTerm where
+  (==) = checkEq
+
+instance Eq InferableTerm where
+  (==) = inferEq
+
+data Term
+  = Checkable CheckableTerm
+  | Inferable InferableTerm
+
+termEq :: Term -> Term -> Bool
+termEq (Checkable (Inferred x)) (Inferable y) = x == y
+termEq (Checkable x) (Checkable y) = x == y
+termEq (Inferable x) (Checkable (Inferred y)) = x == y
+termEq (Inferable x) (Inferable y) = x == y
+termEq _ _ = False
+
+instance Eq Term where
+  (==) = termEq

lab/Syntax/Eval.agda

@@ -0,0 +1,187 @@
+module MiniJuvix.Syntax.Eval where
+
+--------------------------------------------------------------------------------
+
+open import Haskell.Prelude
+open import Agda.Builtin.Equality
+
+open import MiniJuvix.Syntax.Core
+
+--------------------------------------------------------------------------------
+-- Haskell stuff
+--------------------------------------------------------------------------------
+
+{-# FOREIGN AGDA2HS
+{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
+#-}
+
+{-# FOREIGN AGDA2HS
+import MiniJuvix.Syntax.Core
+import MiniJuvix.Prelude
+#-}
+
+{-# FOREIGN AGDA2HS
+--------------------------------------------------------------------------------
+-- Values and neutral terms
+--------------------------------------------------------------------------------
+#-}
+
+{-
+  We are interested in a normal form for posibbly open terms. This
+  means that a term may have free variables. Therefore, we must
+  consider two kind of reduced terms: values and neutral terms. A term
+  that do not longer beta-reduce (i.e. that it contains an evaluation
+  answer) is called a value. A term is neutral whenever its futher
+  beta-reduction depends on a free variable. Terms in normal form are
+  then defined by mutual recursion with neutral terms.
+-}
+
+{- Since Agda2HS does not support indexed data types, we have to
+  repeat ourselves with syntax for values and neutral terms based on
+  Core syntax. The following is ideally for formal verification, but
+  not doable.
+-}
+
+{-
+data Value : Term → Set
+data Neutral : Term → Set
+
+data Value where
+  IsUniverse : Value (Checkable UniverseType)
+  IsNeutral : (t : Term) → Neutral t → Value t
+  IsUnit : Value (Checkable Unit)
+  IsUnitType : Value (Checkable UnitType)
+  ...
+
+data Neutral where
+  IsFree : (b : Name) → Neutral (Inferable (Free b))
+  ...
+-}
+
+{-# NO_POSITIVITY_CHECK #-}
+data Value : Set
+data Neutral : Set
+
+data Value where
+  IsUniverse : Value
+  IsPiType : Quantity → BindingName → Value → (Value -> Value) -> Value
+  IsLam : BindingName → (Value -> Value) -> Value
+  IsTensorType : Quantity → BindingName → Value → (Value -> Value) -> Value
+  IsTensorIntro : Value → Value -> Value
+  IsUnitType : Value
+  IsUnit : Value
+  IsSumType : Value → Value -> Value
+  IsInl : Value -> Value
+  IsInr : Value -> Value
+  IsNeutral : Neutral -> Value
+
+{-# COMPILE AGDA2HS Value #-}
+
+data Neutral where
+  IsFree : Name → Neutral
+  IsApp : Neutral → Value → Neutral
+  IsTensorTypeElim :
+    Quantity → BindingName → BindingName → BindingName
+    → Neutral
+    → (Value -> Value -> Value)
+    → (Value -> Value)
+    → Neutral
+  NSumElim :
+    Quantity
+    → BindingName
+    → Neutral
+    → BindingName
+    → (Value -> Value)
+    → BindingName
+    → (Value -> Value)
+    → (Value -> Value)
+    → Neutral
+
+{-# COMPILE AGDA2HS Neutral #-}
+
+-- We can have an embedding from values to terms as a sort of quoting.
+-- Usages: we can check for value equality by defining term equality.
+
+valueToTerm : Value → Term
+valueToTerm v = Checkable Unit -- TODO
+{-# COMPILE AGDA2HS valueToTerm #-}
+
+--------------------------------------------------------------------------------
+-- Substitution of bound variables. Recall a bound variable is
+-- constructed using Bound and a natural number. The following is one
+-- special case of substitution. See a relevant discussion on
+-- ekmett/bound-making-de-bruijn-succ-less. For QTT, see Def. 12 in
+-- Conor's paper.
+--------------------------------------------------------------------------------
+
+substCheckableTerm
+  : CheckableTerm    -- Term N
+  → Index            -- Bound variable x
+  -> InferableTerm   -- M
+  -> CheckableTerm   -- N[x := M]
+
+substInferableTerm
+  : InferableTerm    -- Term N
+  →  Index           -- bound variable x
+  -> InferableTerm   -- inferable term M
+  -> InferableTerm   -- N[x := M]
+
+substCheckableTerm UniverseType x m = UniverseType
+substCheckableTerm (PiType q y a b) x m
+  = PiType q y
+      (substCheckableTerm a x m)
+      (substCheckableTerm b (x + 1) m)
+substCheckableTerm (Lam y n) x m
+  = Lam y (substCheckableTerm n (x + 1) m)
+substCheckableTerm (TensorType q y s t) x m
+  = TensorType q y
+      (substCheckableTerm s x m)
+      (substCheckableTerm t (x + 1) m)
+substCheckableTerm (TensorIntro p1 p2) x m
+  = TensorIntro
+      (substCheckableTerm p1 x m)
+      (substCheckableTerm p2 x m)
+substCheckableTerm UnitType x m = UnitType
+substCheckableTerm Unit x m = Unit
+substCheckableTerm (SumType a b) x m
+  = SumType
+      (substCheckableTerm a x m)
+      (substCheckableTerm b x m)
+substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
+substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
+substCheckableTerm (Inferred n) x m
+  = Inferred (substInferableTerm n x m)
+{-# COMPILE AGDA2HS substCheckableTerm #-}
+
+-- Variable substitution.
+substInferableTerm (Var (Bound y)) x m = if x == y then m else Var (Bound y)
+substInferableTerm (Var (Free y)) x m  = Var (Free y)
+-- we subst. checkable parts.
+substInferableTerm (Ann y a) x m
+  = Ann (substCheckableTerm y x m)
+        (substCheckableTerm a x m)
+substInferableTerm (App f t) x m
+  = App (substInferableTerm f x m)
+        (substCheckableTerm t x m)
+substInferableTerm (TensorTypeElim q z u v n a b) x m
+  = TensorTypeElim q z u v
+      (substInferableTerm n x m)
+      (substCheckableTerm a (x + 2) m)
+      (substCheckableTerm b (x + 1) m)
+substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m
+  = SumTypeElim q z
+    (substInferableTerm esum x m)
+    u (substCheckableTerm r1 (x + 1) m)
+    v (substCheckableTerm r2 (x + 1) m)
+    (substCheckableTerm ann (x + 1) m)
+{-# COMPILE AGDA2HS substInferableTerm #-}
+
+{-- Substitution, denoted by (N[x := M]) is defined by mutual
+  recursion and by induction on N, and replace all the ocurrences of
+  'x' by M in the term N. Recall that N is a term of type either
+  CheckableTerm or InferableTerm.
+-}
+
+substTerm : Term → Nat → InferableTerm → Term
+substTerm (Checkable n) x m = Checkable (substCheckableTerm n x m)
+substTerm (Inferable n) x m = Inferable (substInferableTerm n x m)

lab/Syntax/Eval.hs

@@ -0,0 +1,106 @@
+{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
+
+module MiniJuvix.Syntax.Eval where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Core
+
+--------------------------------------------------------------------------------
+-- Values and neutral terms
+--------------------------------------------------------------------------------
+
+data Value
+  = IsUniverse
+  | IsPiType Quantity BindingName Value (Value -> Value)
+  | IsLam BindingName (Value -> Value)
+  | IsTensorType Quantity BindingName Value (Value -> Value)
+  | IsTensorIntro Value Value
+  | IsUnitType
+  | IsUnit
+  | IsSumType Value Value
+  | IsInl Value
+  | IsInr Value
+  | IsNeutral Neutral
+
+data Neutral
+  = IsFree Name
+  | IsApp Neutral Value
+  | IsTensorTypeElim
+      Quantity
+      BindingName
+      BindingName
+      BindingName
+      Neutral
+      (Value -> Value -> Value)
+      (Value -> Value)
+  | NSumElim
+      Quantity
+      BindingName
+      Neutral
+      BindingName
+      (Value -> Value)
+      BindingName
+      (Value -> Value)
+      (Value -> Value)
+
+valueToTerm :: Value -> Term
+valueToTerm v = Checkable Unit
+
+substCheckableTerm ::
+  CheckableTerm -> Index -> InferableTerm -> CheckableTerm
+substCheckableTerm UniverseType x m = UniverseType
+substCheckableTerm (PiType q y a b) x m =
+  PiType
+    q
+    y
+    (substCheckableTerm a x m)
+    (substCheckableTerm b (x + 1) m)
+substCheckableTerm (Lam y n) x m =
+  Lam y (substCheckableTerm n (x + 1) m)
+substCheckableTerm (TensorType q y s t) x m =
+  TensorType
+    q
+    y
+    (substCheckableTerm s x m)
+    (substCheckableTerm t (x + 1) m)
+substCheckableTerm (TensorIntro p1 p2) x m =
+  TensorIntro
+    (substCheckableTerm p1 x m)
+    (substCheckableTerm p2 x m)
+substCheckableTerm UnitType x m = UnitType
+substCheckableTerm Unit x m = Unit
+substCheckableTerm (SumType a b) x m =
+  SumType (substCheckableTerm a x m) (substCheckableTerm b x m)
+substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
+substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
+substCheckableTerm (Inferred n) x m =
+  Inferred (substInferableTerm n x m)
+
+substInferableTerm ::
+  InferableTerm -> Index -> InferableTerm -> InferableTerm
+substInferableTerm (Var (Bound y)) x m =
+  if x == y then m else Var (Bound y)
+substInferableTerm (Var (Free y)) x m = Var (Free y)
+substInferableTerm (Ann y a) x m =
+  Ann (substCheckableTerm y x m) (substCheckableTerm a x m)
+substInferableTerm (App f t) x m =
+  App (substInferableTerm f x m) (substCheckableTerm t x m)
+substInferableTerm (TensorTypeElim q z u v n a b) x m =
+  TensorTypeElim
+    q
+    z
+    u
+    v
+    (substInferableTerm n x m)
+    (substCheckableTerm a (x + 2) m)
+    (substCheckableTerm b (x + 1) m)
+substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m =
+  SumTypeElim
+    q
+    z
+    (substInferableTerm esum x m)
+    u
+    (substCheckableTerm r1 (x + 1) m)
+    v
+    (substCheckableTerm r2 (x + 1) m)
+    (substCheckableTerm ann (x + 1) m)

lab/Syntax/Makefile

@@ -0,0 +1,86 @@
+PWD=$(CURDIR)
+PREFIX="$(PWD)/.stack-work/prefix"
+UNAME := $(shell uname)
+
+AGDA_FILES := $(wildcard ./*.agda)
+GEN_HS := $(patsubst %.agda, %.hs, $(AGDA_FILES))
+
+ifeq ($(UNAME), Darwin)
+	THREADS := $(shell sysctl -n hw.logicalcpu)
+else ifeq ($(UNAME), Linux)
+	THREADS := $(shell nproc)
+else
+	THREADS := $(shell echo %NUMBER_OF_PROCESSORS%)
+endif
+
+all:
+	make prepare-push
+
+.PHONY : checklines
+checklines :
+	@grep '.\{81,\}' \
+		--exclude=*.agda \
+		-l --recursive src; \
+		status=$$?; \
+		if [ $$status = 0 ] ; \
+		then echo "Lines were found with more than 80 characters!" >&2 ; \
+		else echo "Succeed!"; \
+		fi
+
+.PHONY : hlint
+hlint :
+	hlint src
+
+.PHONY : haddock
+haddock :
+	cabal --docdir=docs/ --htmldir=docs/ haddock --enable-documentation
+
+.PHONY : docs
+docs :
+	cd docs ; \
+	sh conv.sh
+
+.PHONY : cabal
+cabal :
+	cabal build all
+
+.PHONY : stan
+stan :
+	stan check --include --filter-all --directory=src
+
+setup:
+	stack build --only-dependencies --jobs $(THREADS)
+
+.PHONY : build
+build:
+	stack build --fast --jobs $(THREADS)
+
+clean:
+	cabal clean
+	stack clean
+
+clean-full:
+	stack clean --full
+
+.PHONY: install-agda
+install-agda:
+	git clone https://github.com/agda/agda.git
+	cd agda
+	cabal update
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.6
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
+	pwd
+	cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' -foptimise-heavily
+
+.PHONY : install-agda2hs
+install-agda2hs:
+	git clone https://github.com/agda/agda2hs.git
+	cd agda2hs &&	cabal new-install --overwrite-policy=always
+	mkdir -p .agda/
+	touch .agda/libraries
+	echo "agda2hs/agda2hs.agda-lib" > ~/.agda/libraries
+
+.PHONY : agda
+agda :
+	agda2hs ./Core.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
+	agda2hs ./Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses

lab/Syntax/minijuvix.agda-lib

@@ -0,0 +1,3 @@
+name: MiniJuvix
+include: src
+depend: agda2hs

lab/Termination/CallGraphOld.hs

@@ -0,0 +1,210 @@
+module MiniJuvix.Termination.CallGraphOld
+  ( module MiniJuvix.Termination.Types,
+    module MiniJuvix.Termination.CallGraphOld,
+  )
+where
+
+import qualified Data.HashMap.Strict as HashMap
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+import MiniJuvix.Syntax.Abstract.Pretty.Base
+import MiniJuvix.Termination.Types
+import Prettyprinter as PP
+
+type Edges = HashMap (FunctionName, FunctionName) Edge
+
+data Edge = Edge
+  { _edgeFrom :: FunctionName,
+    _edgeTo :: FunctionName,
+    _edgeMatrices :: [CallMatrix]
+  }
+
+newtype CompleteCallGraph = CompleteCallGraph Edges
+
+data ReflexiveEdge = ReflexiveEdge
+  { _redgeFun :: FunctionName,
+    _redgeMatrices :: [CallMatrix]
+  }
+
+data RecursiveBehaviour = RecursiveBehaviour
+  { _recBehaviourFunction :: FunctionName,
+    _recBehaviourMatrix :: [[Rel]]
+  }
+
+makeLenses ''RecursiveBehaviour
+makeLenses ''Edge
+makeLenses ''ReflexiveEdge
+
+multiply :: CallMatrix -> CallMatrix -> CallMatrix
+multiply a b = map sumProdRow a
+  where
+    rowB :: Int -> CallRow
+    rowB i = CallRow $ case b !? i of
+      Just (CallRow (Just c)) -> Just c
+      _ -> Nothing
+    sumProdRow :: CallRow -> CallRow
+    sumProdRow (CallRow mr) = CallRow $ do
+      (ki, ra) <- mr
+      (j, rb) <- _callRow (rowB ki)
+      return (j, mul' ra rb)
+
+multiplyMany :: [CallMatrix] -> [CallMatrix] -> [CallMatrix]
+multiplyMany r s = [multiply a b | a <- r, b <- s]
+
+composeEdge :: Edge -> Edge -> Maybe Edge
+composeEdge a b = do
+  guard (a ^. edgeTo == b ^. edgeFrom)
+  return
+    Edge
+      { _edgeFrom = a ^. edgeFrom,
+        _edgeTo = b ^. edgeTo,
+        _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
+      }
+
+fromFunCall :: FunctionName -> FunCall -> Call
+fromFunCall caller fc =
+  Call
+    { _callFrom = caller,
+      _callTo = fc ^. callName,
+      _callMatrix = map fst (fc ^. callArgs)
+    }
+
+completeCallGraph :: CallMap -> CompleteCallGraph
+completeCallGraph cm = CompleteCallGraph (go startingEdges)
+  where
+    startingEdges :: Edges
+    startingEdges = foldr insertCall mempty allCalls
+      where
+        insertCall :: Call -> Edges -> Edges
+        insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
+          where
+            aux :: Maybe Edge -> Edge
+            aux me = case me of
+              Nothing -> Edge _callFrom _callTo [_callMatrix]
+              Just e -> over edgeMatrices (_callMatrix :) e
+    allCalls :: [Call]
+    allCalls =
+      [ fromFunCall caller funCall
+        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
+          (_, funCalls) <- HashMap.toList callerMap,
+          funCall <- funCalls
+      ]
+
+    go :: Edges -> Edges
+    go m
+      | edgesCount m == edgesCount m' = m
+      | otherwise = go m'
+      where
+        m' = step m
+
+    step :: Edges -> Edges
+    step s = edgesUnion (edgesCompose s startingEdges) s
+
+    fromEdgeList :: [Edge] -> Edges
+    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
+
+    edgesCompose :: Edges -> Edges -> Edges
+    edgesCompose a b =
+      fromEdgeList $
+        catMaybes
+          [composeEdge ea eb | ea <- toList a, eb <- toList b]
+    edgesUnion :: Edges -> Edges -> Edges
+    edgesUnion = HashMap.union
+    edgesCount :: Edges -> Int
+    edgesCount = HashMap.size
+
+reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
+reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
+  where
+    reflexive :: Edge -> Maybe ReflexiveEdge
+    reflexive e
+      | e ^. edgeFrom == e ^. edgeTo =
+        Just $ ReflexiveEdge (e ^. edgeFrom) (e ^. edgeMatrices)
+      | otherwise = Nothing
+
+callMatrixDiag :: CallMatrix -> [Rel]
+callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
+  where
+    col :: Int -> CallRow -> Rel
+    col i (CallRow row) = case row of
+      Nothing -> RNothing
+      Just (j, r')
+        | i == j -> RJust r'
+        | otherwise -> RNothing
+
+recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
+recursiveBehaviour re =
+  RecursiveBehaviour
+    (re ^. redgeFun)
+    (map callMatrixDiag (re ^. redgeMatrices))
+
+findOrder :: RecursiveBehaviour -> Maybe LexOrder
+findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
+  where
+    b0 :: [[Rel]]
+    b0 = rb ^. recBehaviourMatrix
+    indexed = map (zip [0 :: Int ..] . take minLength) b0
+      where
+        minLength = minimum (map length b0)
+
+    startB = removeUselessColumns indexed
+
+    -- removes columns that don't have at least one ≺ in them
+    removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
+    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
+
+    isLexOrder :: [Int] -> Maybe [Int]
+    isLexOrder = go startB
+      where
+        go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
+        go [] _ = Just []
+        go b perm = case perm of
+          [] -> error "The permutation should have one element at least!"
+          (p0 : ptail)
+            | Just r <- find (isLess . snd . (!! p0)) b,
+              all (notNothing . snd . (!! p0)) b,
+              Just perm' <- go (b' p0) (map pred ptail) ->
+              Just (fst (r !! p0) : perm')
+            | otherwise -> Nothing
+          where
+            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
+              where
+                r' r = case splitAt i r of
+                  (x, y) -> x ++ drop 1 y
+
+    notNothing = (RNothing /=)
+    isLess = (RJust RLe ==)
+
+    allPerms :: [[Int]]
+    allPerms = case nonEmpty startB of
+      Nothing -> []
+      Just s -> permutations [0 .. length (head s) - 1]
+
+instance PrettyCode Edge where
+  ppCode Edge {..} = do
+    fromFun <- ppSCode _edgeFrom
+    toFun <- ppSCode _edgeTo
+    matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode _edgeMatrices
+    return $
+      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
+        <> matrices
+    where
+      ppMatrices = vsep2 . map ppMatrix
+      ppMatrix (i, t) =
+        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
+          <> t
+
+instance PrettyCode CompleteCallGraph where
+  ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
+  ppCode (CompleteCallGraph edges) = do
+    es <- vsep2 <$> mapM ppCode (toList edges)
+    return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
+
+instance PrettyCode RecursiveBehaviour where
+  ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
+  ppCode (RecursiveBehaviour f m) = do
+    f' <- ppSCode f
+    let m' = vsep (map (PP.list . map pretty) m)
+    return $
+      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
+        <> indent 2 (align m')

lab/docs/examples/Example1.mjuvix

@@ -0,0 +1,223 @@
+-- Comments as in Haskell.
+--This is another comment
+------ This is another comment
+-- This is another comment --possible text-- 
+  -- This is a comment, as it is not indent
+  -- sensitive. It should be fine.
+
+-- reserved symbols (with their Unicode counterpart):
+-- , ; : { } -> |-> := === @ _ \
+-- reserved words:
+-- module close open axiom inductive record options
+-- where let in
+
+-- Options to check/run this file.
+options { 
+debug   := INFO;
+phase   := { parsing , check };
+backend := none; -- llvm.
+};
+
+module Example1;
+
+module M;
+-- This creates a module called M,
+-- which it must be closed with:
+end M;
+
+open M;  -- comments can follow after ;
+close M;
+
+-- import moduleName {names} hiding {names};
+import Primitives;       -- imports all the public names.
+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. 
+-- `x : M;`
+
+-- Nonindexed inductive type declaration:
+inductive Nat
+{ zero : Nat ;
+	suc : Nat -> Nat ;
+};
+
+-- Term definition uses := instead of =.
+-- = is not a reserved name.
+-- == is not a reserved name.
+-- === is a reserved symbol for def. equality.
+zero' : Nat;
+zero'                 
+:= zero; 
+
+-- Axioms/definitions.
+axiom A : Type;
+axiom a a' : A; 
+
+f : Nat -> A;
+f := \x -> match x
+{
+	zero |-> a  ;
+	suc  |-> a' ;
+}; 
+
+g : Nat -> A;
+g Nat.zero    := a;
+g (Nat.suc t) := a';
+
+-- Qualified names for pattern-matching seems convenient.
+-- For example, if we define a function without a type sig.
+-- that also matches on inductive type with constructor names
+-- appearing in another type, e.g. Nat and Fin.
+
+inductive Fin (n : Nat) {
+	zero : Fin Nat.zero;
+	suc  : (n : Nat) -> Fin (Nat.suc n);
+};
+
+infixl 10 _+_ ; -- fixity notation as in Agda or Haskell.
+_+_ : Nat → Nat → Nat ;
+_+_ Nat.zero m    := m;
+_+_ (Nat.suc n) m := Nat.suc (n + m) ;
+
+-- Unicode is possible.
+ℕ : Type;
+ℕ := Nat;
+-- Maybe consider alises for types and data constructors:
+-- `alias ℕ := Nat` ;
+
+-- The function `g` should be transformed to
+-- a function of the form f. (aka. case-tree compilation)
+
+-- Examples we must have to make things interesting:
+-- Recall ; goes after any declarations.
+
+inductive Unit { tt : Unit;};
+
+-- Indexed inductive type declarations:
+inductive Vec (n : Nat) (A : Type)
+{
+	zero : Vec Nat.zero A;
+	succ : A -> Vec n A -> Vec (Nat.succ n) A;
+};
+
+Vec' : Nat -> Type -> Type;
+Vec' Nat.zero A      := Unit;
+Vec' (Vec'.suc n) A := A -> Vec' n A;
+
+inductive Empty{};
+
+exfalso : (A : Type) -> Empty -> A;
+exfalso A e := match e {};
+
+neg : Type -> Type;
+neg := A -> Empty;
+
+-- Record
+record Person {
+	name : String;
+	age: Nat;
+};
+
+h : Person -> Nat;
+h := \x -> match x {
+	{name = s , age = n} |-> n;
+};
+
+h' : Person -> Nat;
+h' {name = s , age = n} := n;
+
+-- projecting fields values.
+h'' : Person -> String;
+h'' p := Person.name p;
+
+-- maybe, harder to support but very convenient.
+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`. 
+-- If the quantity n is not explicit, then the judgement
+-- is `x :Any M`.
+
+-- The following says that the term z of type A has quantity 0.
+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;  
+
+-- Tensor product type.
+f' : [ x :1 A ] -> B;
+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;
+g'' = \p -> match p {
+	(k , a) |-> k a;
+};
+
+axiom C : Type;
+axiom D : Type;
+
+-- A quantity can annotate a field name in a record type.
+record P (A : Type) (B : A -> Type) {
+	proj1 : C;
+	proj2 :0 D;
+} 
+eta-equality, constructor prop;  -- extra options.
+
+-- More inductive types.
+inductive Id (A : Type) (x : A)
+{
+	refl : Id A x;
+};
+
+
+a-is-a : a = a;
+a-is-a := refl;
+
+-- Where
+
+a-is-a' : a = a;
+a-is-a' := helper
+where helper := a-is-a;
+
+a-is-a'' : a = a;
+a-is-a'' := helper
+where {
+helper : a = a;
+helper := a-is-a';
+}
+
+-- `Let` can appear in type level definition
+-- but also in term definitions.
+
+a-is-a-3 : a = a;
+a-is-a-3 := let { helper : a = a; helper := a-is-a;} in helper;
+
+a-is-a-4 : let {
+typeId : (M : Type) -> (x : M) -> Type;
+typeId M x := x = x;
+} in typeId A a;
+a-is-a-4 := a-is-a;
+
+end Example1;
+
+-- future:
+-- module M' (X : Type);
+-- x-is-x : (x : X) -> x = x;
+-- x-is-x x := refl;
+-- end M';
+-- open M' A;
+-- a-is-a-5 := a = a;
+-- a-is-a-5 = x-is-x a;
+-- Also, for debugging:
+
+-- print e; print out the internal representation for e, without normalising it.
+-- eval e;  compute e and print it out;

lab/docs/examples/Example2.mjuvix

@@ -0,0 +1,44 @@
+-- Based on example2.ju in anoma/juvix
+
+module Example2;
+
+import Prelude hiding {Bool, True, False};
+
+record Account {
+   balance : Nat;
+   name    : String;
+};
+
+record Transaction {
+  sender   : Account;
+  receiver : Account;
+};
+
+record Storage { trans : Transaction; };
+
+inductive TrustLevel {
+  Trusted    : Nat -> TrustLevel;
+  NotTrusted : TrustLevel
+};
+
+determine-trust-level : String -> TrustLevel;
+determine-trust-level s :=
+  if s === "bob"  then (Trusted 30)
+  else if s === "maria" then (Trusted 50)
+  else NotTrusted;
+
+inductive Bool {
+True : Bool;
+False : Bool;
+};
+
+accept-withdraws-from : Storage -> Storage -> Bool;
+accept-withdraws-from initial final := 
+  let { trusted? := determine-trust-level initial.trans.receiver.name; }
+  in match trusted? {
+     Trusted funds |-> 
+          funds.maximum-withdraw >=final.trans.sender.balance - initial.trans.sender.balance;
+     NotTrusted |-> False;
+  };
+
+end Example2;

lab/docs/examples/Example3.mjuvix

@@ -0,0 +1,32 @@
+-- Based on example3.ju in anoma/juvix
+
+module Example3;
+
+import Prelude;
+
+record Account {
+   balance : Nat;
+   name    : String;
+};
+
+record Transaction {
+  sender   : Account;
+  receiver : Account;
+};
+
+record Storage { trans : Transaction; };
+
+determine-maximum-withdraw : String -> Nat;
+determine-maximum-withdraw s := 
+  if s === "bob" then 30
+  else if s === "maria" then 50
+  else 0;
+
+accept-withdraws-from : Storage -> Storage -> Bool;
+accept-withdraws-from initial final :=
+  let { withdrawl-amount :=
+    determine-maximum-withdraw initial.trans.receiver.name;
+  } in 
+  withdrawl-amount >= final.trans.sender.balance - initial.trans.sender.balance;
+
+end Example3;

lab/docs/examples/FirstMilestone.mjuvix

@@ -0,0 +1,243 @@
+module FirstMilestone;
+
+--------------------------------------------------------------------------------
+-- Module declaration
+--------------------------------------------------------------------------------
+
+module M;  -- This creates a module called M.
+end;       -- This closes the current module in scope.
+
+--------------------------------------------------------------------------------
+-- Import definitions from existing modules
+--------------------------------------------------------------------------------
+
+import Primitives;
+
+{- The line above will import to the local scope all the
+   public names qualified in the module called
+   Primitives.
+-}
+
+open Primitives;
+
+{- The line above will import to the local scope all the
+   public names unqualified in the module called
+   Prelude.
+-}
+
+import Backend;
+
+-- Additionally, one can only import unqualified names by means of
+-- the keyword "using".
+open Backend using { LLVM };  -- this imports to the local scope only the
+                              -- variable called LLVM.
+-- One can use ---in combination with `using`--- the keyword `hiding`
+-- to avoid importing undesirable names.
+
+import Prelude;
+open Prelude hiding { Nat ; Unit ; Empty } ;
+
+--------------------------------------------------------------------------------
+-- Inductive type declarations
+--------------------------------------------------------------------------------
+
+-- An inductive type named Empty without data constructors.
+inductive Empty {};
+
+-- An inductive type named Unit with only one constructor.
+inductive Unit { tt : Unit; };
+
+inductive Nat' : Type
+{ zero : Nat' ;
+  suc : Nat' -> Nat' ;
+};
+
+-- The use of the type `Type` below is optional.
+-- The following declaration is equivalent to Nat'.
+
+inductive Nat {
+  zero : Nat ;
+  suc : Nat -> Nat ;
+};
+
+-- A term definition uses the symbol (:=) instead of the traditional
+-- symbol (=). The symbol (===) is reserved for def. equality. The
+-- symbols (=) and (==) are not reserved.
+
+zero' : Nat;
+zero' := zero;
+
+
+-- * Inductive type declarations with paramenters.
+
+-- The n-point type.
+inductive Fin (n : Nat) {
+  zero : Fin zero;
+  suc  : (n : Nat) -> Fin (suc n);
+};
+
+-- The type of sized vectors.
+inductive Vec (n : Nat) (A : Type)
+{
+  zero : Vec Nat.zero A;
+  succ : A -> Vec n A -> Vec (Nat.succ n) A;
+};
+
+-- * Indexed inductive type declarations.
+
+-- A very interesting data type.
+inductive Id (A : Type) (x : A) : A -> Type
+{
+  refl : Id A x x;
+};
+
+--------------------------------------------------------------------------------
+-- Unicode, whitespaces, newlines
+--------------------------------------------------------------------------------
+
+-- Unicode symbols are permitted.
+ℕ : Type;
+ℕ := Nat;
+
+-- Whitespaces and newlines are optional. The following term
+-- declaration is equivalent to the previous one.
+ℕ'
+  : Type;
+ℕ'
+:=
+  Nat;
+
+-- Again, whitespaces are optional in declarations. For example,
+-- `keyword nameID { content ; x := something; };` is equivalent to
+-- `keyword nameID{content;x:=something;};`. However, we must strive
+-- for readability and therefore, the former expression is better.
+
+--------------------------------------------------------------------------------
+-- Axioms/definitions
+--------------------------------------------------------------------------------
+
+axiom A : Type;
+axiom a : A;
+axiom a' : A;
+
+--------------------------------------------------------------------------------
+-- Pattern-matching
+--------------------------------------------------------------------------------
+
+f : Nat -> A;
+f := \x -> match x  -- \x  or λ x to denote a lambda abstraction.
+  {
+    zero ↦ a   ; -- case declaration uses the mapsto symbol or the normal arrow.
+    suc  -> a' ;
+  };
+
+-- We can use qualified names to disambiguate names for
+-- pattern-matching. For example, imagine the case where there are
+-- distinct matches of the same constructor name for different
+-- inductive types (e.g. zero in Nat and Fin), AND the function type
+-- signature is missing.
+
+g : Nat -> A;
+g Nat.zero    := a;
+g (Nat.suc t) := a';
+
+-- For pattern-matching, the symbol `_` is the wildcard pattern as in
+-- Haskell or Agda. The following function definition is equivalent to
+-- the former.
+
+g' : Nat -> A;
+g' zero := a;
+g' _    := a';
+
+-- Note that the function `g` will be transformed to a function equal
+-- to the function f above in the case-tree compilation phase.
+
+-- The absurd case for patterns.
+
+exfalso : (A : Type) -> Empty -> A;
+exfalso A e := match e {};
+
+neg : Type -> Type;
+neg := A -> Empty;
+
+-- An equivalent type for sized vectors.
+
+Vec' : Nat -> Type -> Type;
+Vec' Nat.zero A    := Unit;
+Vec' (Nat.suc n) A := A -> Vec' n A;
+
+--------------------------------------------------------------------------------
+-- Fixity notation similarly as in Agda or Haskell.
+--------------------------------------------------------------------------------
+
+infixl 10 + ;
++ : Nat → Nat → Nat ;
++ Nat.zero m    := m;
++ (Nat.suc n) m := Nat.suc (n + m) ;
+
+--------------------------------------------------------------------------------
+-- Quantities for variables.
+--------------------------------------------------------------------------------
+
+-- A quantity for a variable in MiniJuvix can be either 0,1, or Any.
+-- If the quantity n is not explicit, then it is Any.
+
+-- The type of functions that uses once its input of type A to produce a number.
+axiom funs : (x :1 A) -> Nat;
+
+axiom B : (x :1 A) -> Type;   -- B is a type family.
+axiom em : (x :1 A) -> B;
+
+--------------------------------------------------------------------------------
+-- Where
+--------------------------------------------------------------------------------
+
+a-is-a : Id A a a;
+a-is-a := refl;
+
+a-is-a' : Id A a a;
+a-is-a' := helper
+  where {
+    open somemodule;
+    helper : Id A a a;
+    helper := a-is-a;
+    };
+
+--------------------------------------------------------------------------------
+-- Let
+--------------------------------------------------------------------------------
+
+-- `let` can appear in term and type level definitions.
+
+a-is-a'' : Id A a a;
+a-is-a'' := let { helper : Id A a a;
+                  helper := a-is-a; }
+            in helper;
+
+a-is-a''' : let { typeId : (M : Type) -> (x : M) -> Type;
+                  typeId M x := Id M x x;
+                } in typeId A a;
+a-is-a''' := a-is-a;
+
+--------------------------------------------------------------------------------
+-- Debugging
+--------------------------------------------------------------------------------
+
+e : Nat;
+e : suc zero + suc zero;
+
+two : Nat;
+two := suc (suc zero);
+
+e-is-two : Id Nat e two;
+e-is-two := refl;
+
+-- print out the internal representation for e without normalising it.
+print e;
+
+-- compute e and print e.
+eval e;
+
+--------------------------------------------------------------------------------
+
+end;

lab/docs/examples/declarations/module/Makefile

@@ -0,0 +1,6 @@
+
+all:
+	- make test
+
+test :
+	shelltest fail succeed -c --execdir -h --all

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

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

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

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

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

@@ -0,0 +1 @@
+module Top;

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

@@ -0,0 +1,8 @@
+module Top;
+  module A;
+    module O; end;
+  end;
+  module B;
+    module O; end;
+  end;
+end;

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

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

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

@@ -0,0 +1,6 @@
+module Top;
+  module A;
+    module P; end;
+  end;
+  import A;
+end;

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

@@ -0,0 +1,11 @@
+# An empty file is not valid
+$ stack -- exec minijuvix parse ./../examples/E0.mjuvix
+>2
+minijuvix: user error (./../examples/E0.mjuvix:1:1:
+  |
+1 | <empty line>
+  | ^
+unexpected end of input
+expecting "module"
+)
+>= 1

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

@@ -0,0 +1,23 @@
+# Every module declaration ends with 'end;'
+$ stack -- exec minijuvix parse ./../examples/E1.mjuvix
+>2
+minijuvix: user error (./../examples/E1.mjuvix:3:1:
+  |
+3 | <empty line>
+  | ^
+unexpected end of input
+expecting "axiom", "end", "eval", "import", "inductive", "infix", "infixl", "infixr", "module", "open", "postfix", "prefix", or "print"
+)
+>= 1
+
+
+$ stack -- exec minijuvix scope ./../examples/E1.mjuvix
+>2
+minijuvix: user error (./../examples/E1.mjuvix:3:1:
+  |
+3 | <empty line>
+  | ^
+unexpected end of input
+expecting "axiom", "end", "eval", "import", "inductive", "infix", "infixl", "infixr", "module", "open", "postfix", "prefix", or "print"
+)
+>= 1

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

@@ -0,0 +1,34 @@
+<
+$ stack -- exec minijuvix parse ./../examples/E2.mjuvix
+>
+Module
+  { modulePath =
+      TopModulePath
+        { modulePathDir = Path { pathParts = [] }
+        , modulePathName = Sym "Top"
+        }
+  , moduleBody =
+      [ StatementModule
+          Module
+            { modulePath = Sym "A"
+            , moduleBody =
+                [ StatementModule Module { modulePath = Sym "O" , moduleBody = [] }
+                ]
+            }
+      , StatementModule
+          Module
+            { modulePath = Sym "B"
+            , moduleBody =
+                [ StatementModule Module { modulePath = Sym "O" , moduleBody = [] }
+                ]
+            }
+      ]
+  }
+>= 0
+
+
+<
+$ stack -- exec minijuvix scope ./../examples/E2.mjuvix
+>2
+minijuvix: user error (ErrAlreadyDefined (Sym "O"))
+>= 1

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

@@ -0,0 +1,22 @@
+<
+$ stack -- exec minijuvix parse ./../examples/E3.mjuvix
+>
+Module
+  { modulePath =
+      TopModulePath
+        { modulePathDir = Path { pathParts = [] }
+        , modulePathName = Sym "Top"
+        }
+  , moduleBody =
+      [ StatementModule Module { modulePath = Sym "A" , moduleBody = [] }
+      , StatementModule Module { modulePath = Sym "A" , moduleBody = [] }
+      ]
+  }
+>= 0
+
+
+<
+$ stack -- exec minijuvix scope ./../examples/E3.mjuvix
+>2
+minijuvix: user error (ErrAlreadyDefined (Sym "A"))
+>= 1

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

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

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

@@ -0,0 +1,30 @@
+$ cat ./../examples/A.mjuvix
+>
+module A;
+  module B;
+  end;
+end;
+>= 0
+
+$ stack -- exec minijuvix parse ./../examples/A.mjuvix
+>
+Module
+  { modulePath =
+      TopModulePath
+        { modulePathDir = Path { pathParts = [] }
+        , modulePathName = Sym "A"
+        }
+  , moduleBody =
+      [ StatementModule Module { modulePath = Sym "B" , moduleBody = [] }
+      ]
+  }
+>= 0
+
+
+$ stack -- exec minijuvix scope ./../examples/A.mjuvix -- --show-name-ids
+>
+module A;
+  module B@0;
+  end;
+end;
+>= 0

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

@@ -0,0 +1,27 @@
+$ stack -- exec minijuvix parse ./../examples/T.mjuvix
+>
+Module
+  { modulePath =
+      TopModulePath
+        { modulePathDir = Path { pathParts = [] }
+        , modulePathName = Sym "Top"
+        }
+  , moduleBody =
+      [ StatementModule
+          Module
+            { modulePath = Sym "A"
+            , moduleBody =
+                [ StatementModule Module { modulePath = Sym "P" , moduleBody = [] }
+                ]
+            }
+      , StatementImport
+          Import
+            { importModule =
+                TopModulePath
+                  { modulePathDir = Path { pathParts = [] }
+                  , modulePathName = Sym "A"
+                  }
+            }
+      ]
+  }
+>= 0

lab/docs/examples/syntax.miniju

@@ -0,0 +1,51 @@
+-- The syntax is very similar to that of Agda. However, we need some extra ';'
+module Example where
+
+   -- The natural numbers can be inductively defined thus:
+   data ℕ : Type 0 ;
+      | zero : ℕ
+      | suc : ℕ → ℕ ;
+
+   -- A list of elements with typed size:
+   data Vec (A : Type) : ℕ → Type 0 ;
+     | nil : A → Vec A zero
+     | cons : (n : ℕ) → A → Vec A n → Vec A (suc n) ;
+
+   module ℕ-Ops where
+     infixl 6 + ;
+     + : ℕ → ℕ → ℕ ;
+     + zero b = b ;
+     + (suc a) b = suc (a + b) ;
+
+     infixl 7 * ;
+     * : ℕ → ℕ → ℕ ;
+     * zero b = zero ;
+     * (suc a) b = b + a * b ;
+   end
+
+   module M1 (A : Type 0) where
+      aVec : ℕ → Type 0 ;
+      aVec = Vec A ;
+   end
+
+   module Bot where
+      data ⊥ : Type 0 ;
+   end
+
+   open module M1 ℕ ;
+
+   two : ℕ ;
+   two = suc (suc zero) ;
+
+   id : (A : Type) → A → A ;
+   id _ = λ x → x ;
+
+   natVec : aVec (cons zero) ;
+   natVec = cons (two * two + one) nil ;
+     -- The 'where' part belongs to the clause
+     where
+     open module ℕ-Ops ;
+     one : ℕ ;
+     one = suc zero ;
+
+end

lab/docs/examples/token.mjuvix

@@ -0,0 +1,417 @@
+module Token;
+
+import Data.Nat;
+open Data.Nat using {<=};
+
+import Data.String;
+open Data.String using {compare};
+
+--------------------------------------------------------------------------------
+-- Boiler plate taken from previous code
+--------------------------------------------------------------------------------
+
+{-
+total_order : (a:eqtype) (f: (a -> a -> Tot Bool)) =
+   (forall a1 a2. (f a1 a2 /\ f a2 a1)  ==> a1 = a2)  (* anti-symmetry *)
+ /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)  (* transitivity  *)
+ /\ (forall a1 a2. f a1 a2 \/ f a2 a1)                (* totality      *)
+
+string_cmp' s1 s2 =  String.compare s1 s2 <= 0
+
+(* The F* defn just calls down to OCaml, since we know comparison in OCaml is total
+ * just admit it
+ *)
+
+string_cmpTotal : unit -> Lemma (total_order string string_cmp')
+string_cmpTotal () = admit ()
+
+// hack function so, the data structure doesn't forget the proof!
+string_cmp : Map.cmp string
+string_cmp = string_cmpTotal (); string_cmp'
+
+-}
+
+--------------------------------------------------------------------------------
+-- Type definitions
+--------------------------------------------------------------------------------
+
+Address : Type;
+Address := String;
+
+-- Accounts : Map.ordmap Address Nat string_cmp
+
+inductive Account {
+  mkAccount : Nat -> SortedMap Address Nat -> Account;
+}
+
+balance : Account -> Nat;
+balance (mkAccount n _) := n;
+
+allowances : Account -> SortedMap Address Nat ;
+allowances (mkAccount _ s) := s;
+
+
+add_account_values_acc : Accounts → Nat -> Nat
+add_account_values_acc Accounts n  =
+ MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts n
+
+// we have to specify they are Nats :(
+add_account_values : Accounts -> Nat
+add_account_values Accounts =
+ MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts 0
+
+inductive Storage {
+  mkStorage : Nat -> Accounts
+  total-supply : Nat;
+  Accounts : a : Accounts { total-supply = add_account_values a };
+}
+
+empty-storage : storage
+empty-storage = {
+  total-supply = 0;
+  Accounts = Map.empty;
+}
+
+inductive Token {
+  mkToken :
+    Storage ->   -- storage
+    Nat ->       -- version
+    String ->    -- name
+    Char ->      -- symbol
+    Address ->   -- owner
+    Token
+}
+
+storage : Token -> Storage;
+storage (mkToken s _ _ _ _ _) := s;
+
+version : Token -> Nat;
+version (mkToken _ n _ _ _ _) := n;
+
+name    : Token -> String;
+name    (mkToken _ _ n _ _ _) := n;
+
+symbol  : Token -> Char;
+symbol  (mkToken _ _ _ s _ _) := s;
+
+owner   : Token -> Address;
+owner   (mkToken _ _ _ _ _ a) := a;
+
+
+type txTransfer = {
+  from_account    : Address;
+  to_account      : Address;
+  transfer_amount : Nat
+}
+
+type tx_mint = {
+  mint_amount     : Nat;
+  mintTo_account : Address
+}
+
+type tx_burn = {
+  burn_amount       : Nat;
+  burn_from_account : Address
+}
+
+inductive txData {
+  transfer : txTransfer -> txData;
+  mint     : txMint -> txData;
+  burn     : txBurn -> txData;
+  }
+
+type tx = {
+  tx_data               : tx_data;
+  tx_authroized_account : Address;
+}
+
+--------------------------------------------------------------------------------
+-- Begin Functions On Accounts
+--------------------------------------------------------------------------------
+
+has_n : Accounts -> Address -> Nat -> Bool
+has_n accounts add toTransfer :=
+  match Map.select add Accounts {
+   (Some n) -> toTransfer <= n;
+   None     -> false;
+  }
+
+account-sub :
+  (acc : Accounts) ->
+  (add : Address) ->
+  (num : Nat {has_n acc add num}) ->
+  Accounts
+account-sub Accounts add number =
+  match Map.select add Accounts with
+   { Some balance -> Map.update add (balance - number) Accounts };
+
+
+// No feedback given, so don't know next move :(
+transfer-sub : 
+  (acc : Accounts) ->
+  (add : Address) ->
+  (num : Nat) ->
+  Lemma ->
+  (requires (has_n acc add num)) ->
+  (ensures (  add_account_values acc - num
+           == add_account_values (account-sub acc add num)))
+transfer-sub acc add num :=
+  match Map.select add acc {
+   Some balance ->;
+    remaining : Nat = balance - num in
+    admit ()
+  };
+
+account_add : acc : Accounts
+                -> add : Address
+                -> num : Nat
+                -> Accounts
+account_add acc add num =
+  match Map.select add acc with
+   Some b' -> Map.update add (b' + num) acc;
+   None    -> Map.update add num        acc;
+
+--------------------------------------------------------------------------------
+(**** Experimental Proofs on Transfer *)
+--------------------------------------------------------------------------------
+
+transfer_add_lemma : acc : Accounts
+                       -> add : Address
+                       -> num : Nat
+                       -> Lemma
+                       (ensures
+                         (i =
+                           match Map.select add acc with
+                            None   -> 0;
+                            Some v -> v;
+                          in i + num = Some?.v (Map.select add (account_add acc add num))))
+transfer_add_lemma acc add num = ()
+
+transfer_add_unaffect : acc : Accounts
+                          -> add : Address
+                          -> num : Nat
+                          -> Lemma
+                          (ensures
+                            (forall x. Map.contains x acc /\ x <> add
+                              ==> Map.select x acc = Map.select x (account_add acc add num)))
+transfer_add_unaffect acc add num = ()
+
+
+transfer-same_when_remove : acc : Accounts
+                              -> add : Address
+                              -> num : Nat
+                              -> Lemma
+                              (ensures
+                                (new_account = account_add acc add num in
+                                    add_account_values (Map.remove add acc)
+                                 == add_account_values (Map.remove add new_account)))
+transfer-same_when_remove acc add num =
+  new_account = account_add acc add num in
+  assert (Map.equal (Map.remove add acc) (Map.remove add new_account))
+
+// Useful stepping stone to the real answer!
+// sadly admitted for now
+transfer_acc_behavior : acc : Accounts
+                          -> add : Address
+                          -> Lemma
+                            (ensures
+                              (i =
+                                match Map.select add acc with
+                                 None   -> 0;
+                                 Some v -> v;
+                                in add_account_values_acc (Map.remove add acc) i
+                                  == add_account_values acc))
+transfer_acc_behavior acc add =
+  admit ()
+
+// No feedback given, so don't know next move :(
+transfer_add : acc : Accounts
+                 -> add : Address
+                 -> num : Nat
+                 -> Lemma
+                  (ensures ( add_account_values acc + num
+                           == add_account_values (account_add acc add num)))
+transfer_add acc add num =
+  admit ();
+  transfer-same_when_remove acc add num;
+  transfer_add_unaffect acc add num;
+  transfer_add_lemma acc add num
+
+--------------------------------------------------------------------------------
+(**** Failed Experimental Proofs Over *)
+--------------------------------------------------------------------------------
+
+
+transfer_acc : acc     : Accounts
+                -> add_from : Address
+                -> addTo   : Address
+                -> num      : Nat {has_n acc add_from num}
+                -> Accounts
+transfer_acc Accounts add_from addTo number =
+  new_Accounts = account-sub Accounts add_from number in
+  account_add new_Accounts addTo number
+
+transfer_maintains-supply
+  : acc      : Accounts
+  -> add_from : Address
+  -> addTo   : Address
+  -> num      : Nat
+  -> Lemma
+    (requires (has_n acc add_from num))
+    (ensures (add_account_values acc
+              == add_account_values (transfer_acc acc add_from addTo num)))
+transfer_maintains-supply acc add_from addTo num =
+  transfer-sub acc add_from num;
+  transfer_add (account-sub acc add_from num) addTo num
+
+transfer-stor
+  : stor     : storage
+  -> add_from : Address
+  -> addTo   : Address
+  -> num      : Nat {has_n stor.Accounts add_from num}
+  -> storage
+transfer-stor stor add_from addTo num =
+  new_acc = account_add (account-sub stor.Accounts add_from num) addTo num in
+  transfer_maintains-supply stor.Accounts add_from addTo num;
+  { total-supply = stor.total-supply;
+    Accounts     = new_acc
+  }
+
+
+--------------------------------------------------------------------------------
+(* End Type Definitions *)
+(**** Begin Validations On Tokens *)
+--------------------------------------------------------------------------------
+
+
+validTransfer : token -> tx -> Bool
+validTransfer token tx =
+  match tx.tx_data with
+   Transfer {from_account; transfer_amount} ->;
+    has_n token.storage.Accounts from_account transfer_amount
+    && tx.tx_authroized_account = from_account
+   Mint _  Burn _ ->;
+    false
+
+valid_mint : token -> tx -> Bool
+valid_mint token tx =
+  match tx.tx_data with
+   Mint mint           -> token.owner = tx.tx_authroized_account;
+   Transfer _  Burn _ -> false;
+
+valid_burn : token -> tx -> Bool
+valid_burn token tx =
+  match tx.tx_data with
+   Burn {burn_from_account; burn_amount} ->;
+    has_n token.storage.Accounts burn_from_account burn_amount
+    && tx.tx_authroized_account = burn_from_account
+   Transfer _  Mint _ ->;
+    false
+
+
+--------------------------------------------------------------------------------
+(* End validations on tokens *)
+(**** Begin Functions On Tokens *)
+--------------------------------------------------------------------------------
+
+tokenTransaction : (token -> tx -> Bool) -> Type0
+tokenTransaction f =
+  tok : token -> tx : tx { f tok tx } -> token
+
+transfer : tokenTransaction validTransfer
+transfer token transaction =
+  match transaction.tx_data with
+   Transfer {from_account; to_account; transfer_amount} ->;
+    { token
+      with storage = transfer-stor token.storage
+                                   from_account
+                                   to_account
+                                   transfer_amount
+    }
+
+mint : tokenTransaction valid_mint
+mint token transaction =
+  match transaction.tx_data with
+   Mint {mint_amount; mintTo_account} ->;
+    transfer_add token.storage.Accounts mintTo_account mint_amount;
+    { token
+      with storage = {
+        total-supply = token.storage.total-supply + mint_amount;
+        Accounts     = account_add token.storage.Accounts mintTo_account mint_amount
+      }}
+
+burn : tokenTransaction valid_burn
+burn token transaction =
+  match transaction.tx_data with
+   Burn {burn_from_account; burn_amount} ->;
+    transfer-sub token.storage.Accounts burn_from_account burn_amount;
+    { token
+      with storage = {
+        total-supply = token.storage.total-supply - burn_amount;
+        Accounts     = account-sub token.storage.Accounts burn_from_account burn_amount
+      }}
+
+type transaction_error =
+   Not_enough_funds;
+   Not-same_account;
+   Not_ownerToken;
+   Not_enoughTokens;
+
+executeTransaction : token -> tx -> c_or transaction_error token
+executeTransaction token tx =
+  match tx.tx_data with
+   Transfer _ ->;
+    if validTransfer token tx
+    then Right (transfer token tx)
+    else Left Not_enough_funds // todo determine what the error is
+   Mint _ ->;
+    if valid_mint token tx
+    then Right (mint token tx)
+    else Left Not_ownerToken
+   Burn _ ->;
+    if valid_burn token tx
+    then Right (burn token tx)
+    else Left Not_enoughTokens
+
+validTransferTransaction
+  : tok : token
+  -> tx  : tx
+  -> Lemma (requires (validTransfer tok tx))
+          (ensures (
+            Right newTok = executeTransaction tok tx in
+            tok.storage.total-supply == newTok.storage.total-supply))
+validTransferTransaction tok tx = ()
+
+
+valid_mintTransaction
+  : tok : token
+  -> tx  : tx
+  -> Lemma (requires (valid_mint tok tx))
+          (ensures (
+            Right newTok = executeTransaction tok tx in
+            Mint {mint_amount} = tx.tx_data in
+            tok.storage.total-supply + mint_amount == newTok.storage.total-supply))
+valid_mintTransaction tok tx = ()
+
+valid_burnTransaction
+  : tok : token
+  -> tx  : tx
+  -> Lemma (requires (valid_burn tok tx))
+          (ensures (
+            Right newTok = executeTransaction tok tx in
+            Burn {burn_amount} = tx.tx_data in
+            tok.storage.total-supply - burn_amount == newTok.storage.total-supply))
+valid_burnTransaction tok tx = ()
+
+isLeft = function
+   Left _  -> true;
+   Right _ -> false;
+
+non_validTransaction
+  : tok : token
+  -> tx  : tx
+  -> Lemma (requires (not (valid_burn tok tx)
+                   /\ not (valid_mint tok tx)
+                   /\ not (validTransfer tok tx)))
+          (ensures (isLeft (executeTransaction tok tx)))
+non_validTransaction tok tx = ()

lab/docs/notes/Example.agda

@@ -0,0 +1,100 @@
+-- testing
+module MiniJuvix.Syntax.Core where
+
+open import Haskell.Prelude
+open import Agda.Builtin.Equality
+
+-- language extensions
+{-# FOREIGN AGDA2HS
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+#-}
+
+{-# FOREIGN AGDA2HS
+{-
+M , N := x
+    | λ x . M
+    | M N
+    | ⊤
+    | ⊥
+    | if_then_else
+    | x : M
+where
+    variables x.
+    M := Bool | M -> M
+-}
+#-}
+
+VarType : Set
+VarType = String
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+data Type : Set where
+  BoolType : Type
+  ArrowType : Type → Type → Type
+
+{-# COMPILE AGDA2HS Type deriving (Show, Eq) #-}
+
+-------------------------------------------------------------------------------
+-- Terms
+-------------------------------------------------------------------------------
+
+data Term : Set where
+  Var : VarType → Term
+  TT : Term
+  FF : Term
+  Abs : VarType → Term → Term
+  App : Term → Term → Term
+  If : Term → Term → Term → Term
+  Jud : Term → Type → Term
+
+
+{-# COMPILE AGDA2HS Term deriving (Show, Eq) #-}
+
+-------------------------------------------------------------------------------
+-- Context
+-------------------------------------------------------------------------------
+
+Context : Set
+Context = List (VarType × Type)
+
+{-# COMPILE AGDA2HS Context #-}
+
+-------------------------------------------------------------------------------
+
+-- | Bidirectional type-checking algorithm:
+-- defined by mutual recursion:
+
+-- type inference (a.k.a. type synthesis).
+infer : Context → Term → Maybe Type
+-- type checking.
+check : Context → Term → Type → Maybe Type
+
+
+codomain : Type → Maybe Type
+codomain BoolType = Nothing
+codomain (ArrowType a b) = Just b
+
+helper : Context → Term →  Maybe Type → Maybe Type
+helper γ x (Just (ArrowType _ tB)) = check γ x tB
+helper _ _ _ = Nothing
+
+{-# COMPILE AGDA2HS helper #-}
+
+-- http://cdwifi.cz/#/
+
+infer γ (Var x) = lookup x γ
+infer γ TT = pure BoolType
+infer γ FF = pure BoolType
+infer γ (Abs x t) = pure BoolType -- TODO
+infer γ (App f x) = case (infer γ f) of helper γ x
+infer γ (If a t f) = pure BoolType
+infer γ (Jud x m) = check γ x m
+
+check γ x T = {!!}
+
+{-# COMPILE AGDA2HS infer #-}
+{-# COMPILE AGDA2HS check #-}

lab/docs/notes/forTesting.md

@@ -0,0 +1,2 @@
+
+Examples to test the typechecker:

lab/docs/notes/module-scoping.org

@@ -0,0 +1,35 @@
+* Module scoping
+  This document contains some notes on how the implementation of module scoping
+  is supposed to work.
+
+** Import statements
+   What happens when we see:
+   #+begin_example
+   import Data.Nat
+   #+end_example
+   All symbols *defined* in =Data.Nat= become available in the current module
+   through qualified names. I.e. =Data.Nat.zero=.
+
+** Open statements
+   What happens when we see:
+   #+begin_example
+   open Data.Nat
+   #+end_example
+   All symbols *defined* in =Data.Nat= become available in the current module
+   through unqualified names. I.e. =zero=.
+
+ =using= and =hiding= modifiers are handled in the expected way.
+
+** Nested modules
+   What happens when we see:
+   #+begin_example
+   module Local;
+   ...
+   end;
+   #+end_example
+   We need to answer two questions.
+   1. What happens after =module Local;=. Inside =Local= *all* symbols that were
+      in scope, continue to be in scope.
+   2. What happens after =end;=. All symbols *defined in* =Local= are in scope
+      through qualified names. One can think of this as the same as importing
+ =Local= if it was a top module.

lab/docs/notes/tooling.md

@@ -0,0 +1,72 @@
+Tools used so far:
+
+- cabal-edit
+- hlint and checkout
+  https://github.com/kowainik/relude/blob/main/.hlint.yaml for a
+  complex configuration and better hints.
+- stan
+- summoner
+- ghcup
+- `implicit-hie` generates `hie.yaml`.
+
+- For a good prelude, I tried with Protolude, but it seems a bit
+  abandoned, and it doesn't have support the new Haskell versions.
+  Relude just offered the same, and it is better documented. Let us
+  give it a shot. NoImplicitPrelude plus base-noprelude.
+  https://kowainik.github.io/projects/relude
+
+- For Pretty printer, we will use the package
+  https://hackage.haskell.org/package/prettyprinter, which supports
+  nice annotations and colors using Ansi-terminal subpackage:
+    `cabal-edit add prettyprinter-ansi-terminal`.
+
+- Two options for the kind of container we can use for Context. Using
+  the package container and for performance, unordered-containers. The
+  latter seems to have the same API naming than the former. So, in
+  principle, it doesn't matter which we use.
+
+
+- See
+  [gluedeval](https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784).
+  During elaboration different kind of evaluation strategies may be
+  needed.
+    - 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
+  https://kowainik.github.io/posts/haddock-tips
+
+Initial task order for Minijuvix indicated between parenthesis:
+1. Parser (3.)
+2. Typechecker   (1.)
+3. Compiler (2.)
+4. Interpreter (4.)
+
+- On deriving stuff using Standalone Der.
+See https://kowainik.github.io/posts/deriving.
+- To avoid boilerplate in the cabal file, one could use [common
+  stanzas](https://vrom911.github.io/blog/common-stanzas). At the
+  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. 
+
+- TODO: make a `ref.bib` listing all the repositories and the
+  source-code from where I took code, inspiration, whatever thing.
+
+- The haskell library https://hackage.haskell.org/package/capability
+  seems to be a right choice. Still, I need to check the details. I
+  will use Juvix Prelude.
+
+- Let us use qualified imports to prevent namespace pollution,
+  as much as possible. Checkout:
+  - https://www.haskell.org/onlinereport/haskell2010/haskellch5.html
+  - https://ro-che.info/articles/2019-01-26-haskell-module-system-p2
+  - https://mmhaskell.com/blog/2017/5/8/4-steps-to-a-better-imports-list.
+
+- TODO: https://kowainik.github.io/posts/2018-09-09-dhall-to-hlint So
+  far, I have proposed a hlint file, it's clean, but for refactoring,
+  seems to me, the link above shows a better approach.
+
+- Let us use the Safe pragma.
+  https://stackoverflow.com/questions/61655158/haskell-safe-and-trustworthy-extensions