New target syntax and modular VP examples (#92)

* New target syntax and modular VP examples

* [ .gitignore ] updated

* Fix spaces new lines

* Remove outdated lab folder

.gitignore

@@ -66,3 +66,6 @@ docs/*.html
 /src/MiniJuvix/Utils/OldParser.hs
 CHANGELOG.md
 UPDATES-FOR-CHANGELOG.org
+
+# C Code generation
+*.wasm

examples/milestone/ValidityPredicates/Anoma/Base.hs

@@ -0,0 +1,16 @@
+module Anoma.Base where
+
+import Prelude
+
+readPre :: String -> Int
+readPre "change1-key" = 100
+readPre "change2-key" = 90
+readPre _ = -1
+
+readPost :: String -> Int
+readPost "change1-key" = 90
+readPost "change2-key" = 100
+readPost _ = -1
+
+isBalanceKey :: String -> String -> String
+isBalanceKey _ _ = "owner-address"

examples/milestone/ValidityPredicates/Anoma/Base.mjuvix

@@ -0,0 +1,41 @@
+module Anoma.Base;
+
+foreign ghc {
+  import Anoma.Base
+};
+
+import Prelude;
+open Prelude;
+
+--------------------------------------------------------------------------------
+-- Anoma
+--------------------------------------------------------------------------------
+
+axiom readPre : String → Int;
+compile readPre {
+  ghc ↦ "readPre";
+};
+
+axiom readPost : String → Int;
+compile readPost {
+  ghc ↦ "readPost";
+};
+
+axiom isBalanceKey : String → String → String;
+compile isBalanceKey {
+  ghc ↦ "isBalanceKey";
+};
+
+read-pre : String → Maybe Int;
+read-pre s ≔ from-int (readPre s);
+
+read-post : String → Maybe Int;
+read-post s ≔ from-int (readPost s);
+
+is-balance-key : String → String → Maybe String;
+is-balance-key token key ≔ from-string (isBalanceKey token key);
+
+unwrap-default : Maybe Int → Int;
+unwrap-default o ≔ maybe-int 0 o;
+
+end;

examples/milestone/ValidityPredicates/Data/Bool.mjuvix

@@ -0,0 +1,60 @@
+module Data.Bool;
+
+--------------------------------------------------------------------------------
+-- Booleans
+--------------------------------------------------------------------------------
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+infixr 2 ||;
+|| : Bool → Bool → Bool;
+|| false a ≔ a;
+|| true _ ≔ true;
+
+infixr 3 &&;
+&& : Bool → Bool → Bool;
+&& false _ ≔ false;
+&& true a ≔ a;
+
+if : (A : Type) → Bool → A → A → A;
+if _ true a _ ≔ a;
+if _ false _ b ≔ b;
+
+--------------------------------------------------------------------------------
+-- Backend Booleans
+--------------------------------------------------------------------------------
+
+axiom BackendBool : Type;
+compile BackendBool {
+  ghc ↦ "Bool";
+};
+
+axiom backend-true : BackendBool;
+compile backend-true {
+  ghc ↦ "True";
+};
+
+axiom backend-false : BackendBool;
+compile backend-false {
+  ghc ↦ "False";
+};
+
+
+foreign ghc {
+  bool :: Bool -> a -> a -> a
+  bool True x _ = x
+  bool False _ y = y
+};
+
+axiom bool : BackendBool → Bool → Bool → Bool;
+compile bool {
+  ghc ↦ "bool";
+};
+
+from-backend-bool : BackendBool → Bool;
+from-backend-bool bb ≔ bool bb true false;
+
+end;

examples/milestone/ValidityPredicates/Data/Int.mjuvix

@@ -0,0 +1,46 @@
+module Data.Int;
+
+import Data.Bool;
+open Data.Bool;
+
+--------------------------------------------------------------------------------
+-- Integers
+--------------------------------------------------------------------------------
+
+axiom Int : Type;
+compile Int {
+  ghc ↦ "Int";
+};
+
+infix 4 <';
+axiom <' : Int → Int → BackendBool;
+compile <' {
+  ghc ↦ "(<)";
+};
+
+infix 4 <;
+< : Int → Int → Bool;
+< i1 i2 ≔ from-backend-bool (i1 <' i2);
+
+axiom eqInt : Int → Int → BackendBool;
+compile eqInt {
+  ghc ↦ "(==)";
+};
+
+infix 4 ==Int;
+==Int : Int → Int → Bool;
+==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
+
+infixl 6 -;
+axiom - : Int -> Int -> Int;
+compile - {
+  ghc ↦ "(-)";
+};
+
+infixl 6 +;
+axiom + : Int -> Int -> Int;
+compile + {
+  ghc ↦ "(+)";
+};
+
+end;

examples/milestone/ValidityPredicates/Data/List.mjuvix

@@ -0,0 +1,26 @@
+module Data.List;
+
+import Data.Bool;
+open Data.Bool;
+
+import Data.String;
+open Data.String;
+
+--------------------------------------------------------------------------------
+-- Lists
+--------------------------------------------------------------------------------
+
+inductive List (A : Type) {
+  nil : List A;
+  cons : A → List A → List A;
+};
+
+elem : (A : Type) → (A → A → Bool) → A → List A → Bool;
+elem _ _ _ nil ≔ false;
+elem A eq s (cons x xs) ≔ eq s x || elem _ eq s xs;
+
+foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
+foldl _ _ f z nil ≔ z;
+foldl A B f z (cons h hs) ≔ foldl _ _ f (f z h) hs;
+
+end;

examples/milestone/ValidityPredicates/Data/Maybe.mjuvix

@@ -0,0 +1,16 @@
+module Data.Maybe;
+
+--------------------------------------------------------------------------------
+-- Maybe
+--------------------------------------------------------------------------------
+
+inductive Maybe (A : Type) {
+ nothing : Maybe A;
+ just : A → Maybe A;
+};
+
+maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
+maybe _ _ b _ nothing ≔ b;
+maybe _ _ _ f (just x) ≔ f x;
+
+end;

examples/milestone/ValidityPredicates/Data/Pair.mjuvix

@@ -0,0 +1,12 @@
+module Data.Pair;
+
+
+--------------------------------------------------------------------------------
+-- Pair
+--------------------------------------------------------------------------------
+
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+end;

examples/milestone/ValidityPredicates/Data/String.mjuvix

@@ -0,0 +1,24 @@
+module Data.String;
+
+import Data.Bool;
+open Data.Bool;
+
+--------------------------------------------------------------------------------
+-- Strings
+--------------------------------------------------------------------------------
+
+axiom String : Type;
+compile String {
+  ghc ↦ "[Char]";
+};
+
+axiom eqString : String → String → BackendBool;
+compile eqString  {
+  ghc ↦ "(==)";
+};
+
+infix 4 ==String;
+==String : String → String → Bool;
+==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
+
+end;

examples/milestone/ValidityPredicates/FungibleToken.mjuvix

@@ -0,0 +1,51 @@
+module FungibleToken;
+
+import Anoma.Base;
+open Anoma.Base;
+
+import Prelude;
+open Prelude;
+
+--------------------------------------------------------------------------------
+-- Misc
+--------------------------------------------------------------------------------
+
+pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
+pair-from-optionString ≔ maybe String (Pair Int Bool) (mkPair Int Bool 0 false);
+
+check-result : Pair Int Bool → Bool;
+check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
+
+--------------------------------------------------------------------------------
+-- Validity Predicate
+--------------------------------------------------------------------------------
+
+change-from-key : String → Int;
+change-from-key key ≔ unwrap-default (read-post key)
+                    - unwrap-default (read-pre key);
+
+check-vp : List String → String → Int → String → Pair Int Bool;
+check-vp verifiers key change owner ≔
+    if _
+      -- make sure the spender approved the transaction
+      (change-from-key key < 0)
+        (mkPair _ _ (change + (change-from-key key))
+                (elem _ (==String) owner verifiers))
+        (mkPair _ _ (change + (change-from-key key)) true);
+
+check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
+check-keys token verifiers (mkPair change is-success) key ≔
+    if _
+        is-success
+        (pair-from-optionString (check-vp verifiers key change)
+           (is-balance-key token key))
+        (mkPair _ _ 0 false);
+
+vp : String → List String → List String → Bool;
+vp token keys-changed verifiers ≔
+    check-result
+        (foldl _ _
+            (check-keys token verifiers)
+            (mkPair _ _ 0 true)
+            keys-changed);
+end;

examples/milestone/ValidityPredicates/Prelude.mjuvix

@@ -0,0 +1,29 @@
+module Prelude;
+
+import Data.Bool;
+import Data.Int;
+import Data.List;
+import Data.Maybe;
+import Data.Pair;
+import Data.String;
+import System.IO;
+
+open Data.Bool;
+open Data.Int;
+open Data.List;
+open Data.Maybe;
+open Data.Pair;
+open Data.String;
+open System.IO;
+
+--------------------------------------------------------------------------------
+-- Functions
+--------------------------------------------------------------------------------
+
+const : (A : Type) → (B : Type) → A → B → A;
+const _ _ a _ ≔ a;
+
+id : (A : Type) → A → A;
+id _ a ≔ a;
+
+end;

examples/milestone/ValidityPredicates/System/IO.mjuvix

@@ -0,0 +1,32 @@
+module System.IO;
+
+--------------------------------------------------------------------------------
+-- Actions
+--------------------------------------------------------------------------------
+
+axiom Action : Type;
+compile Action {
+ ghc ↦ "IO ()";
+};
+
+axiom putStr : String → Action;
+compile putStr {
+  ghc ↦ "putStr";
+};
+
+axiom putStrLn : String → Action;
+compile putStrLn {
+  ghc ↦ "putStrLn";
+};
+
+infixl 1 >>;
+axiom >> : Action → Action → Action;
+compile >> {
+  ghc ↦ "(>>)";
+};
+
+show-result : Bool → String;
+show-result true ≔ "OK";
+show-result false ≔ "FAIL";
+
+end;

examples/milestone/ValidityPredicates/Tests.mjuvix

@@ -0,0 +1,37 @@
+module Tests;
+
+import Prelude;
+open Prelude;
+
+import SimpleFungibleToken;
+open SimpleFungibleToken;
+
+--------------------------------------------------------------------------------
+-- Testing VP
+--------------------------------------------------------------------------------
+
+token : String;
+token ≔ "owner-token";
+
+owner-address : String;
+owner-address ≔ "owner-address";
+
+change1-key : String;
+change1-key ≔ "change1-key";
+
+change2-key : String;
+change2-key ≔ "change2-key";
+
+verifiers : List String;
+verifiers ≔ cons String owner-address (nil String);
+
+keys-changed : List String;
+keys-changed ≔ cons String change1-key (cons String change2-key (nil String));
+
+main : Action;
+main ≔
+    (putStr "VP Status: ")
+    >> (putStrLn (show-result (vp token keys-changed verifiers)));
+end;
+
+end;

lab/Syntax/Core.agda

@@ -1,359 +0,0 @@
-{-
-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

@@ -1,197 +0,0 @@
-{-# 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 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

@@ -1,187 +0,0 @@
-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

@@ -1,106 +0,0 @@
-{-# 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

@@ -1,86 +0,0 @@
-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

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

lab/Termination/CallGraphOld.hs

@@ -1,210 +0,0 @@
-module MiniJuvix.Termination.CallGraphOld
-  ( module MiniJuvix.Termination.Types,
-    module MiniJuvix.Termination.CallGraphOld,
-  )
-where
-
-import Data.HashMap.Strict qualified 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/Agda.css

@@ -1,62 +0,0 @@
-/* Aspects. */
-
-/* Code. */
-pre.highlight { padding: .4em .4em; border-style: dashed !important; }
-
-code { font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif; font-size: .85em; white-space: pre; }
-
-/* Agda. */
-pre.Agda { font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif; font-size: .85em; padding: .4em .4em; }
-
-pre.Spec { font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif; font-size: .85em; padding: .4em .4em; border-style: dashed !important; color: #B22222; }
-
-.Agda .Comment       { color: #9d9d9d }
-.Agda .Background    {}
-.Agda .Markup        { color: #000000 }
-.Agda .Keyword       { color: #CD6600 }
-.Agda .String        { color: #B22222 }
-.Agda .Number        { color: #A020F0 }
-.Agda .Symbol        { color: #404040 }
-.Agda .PrimitiveType { color: #0000CD }
-.Agda .Pragma        { color: black   }
-.Agda .Operator      {}
-
-/* NameKinds. */
-.Agda .Bound                  { color: black   }
-.Agda .Generalizable          { color: black   }
-.Agda .InductiveConstructor   { color: #008B00 }
-.Agda .CoinductiveConstructor { color: #8B7500 }
-.Agda .Datatype               { color: #0000CD }
-.Agda .Field                  { color: #EE1289 }
-.Agda .Function               { color: #0000CD }
-.Agda .Module                 { color: #A020F0 }
-.Agda .Postulate              { color: #0000CD }
-.Agda .Primitive              { color: #0000CD }
-.Agda .Record                 { color: #0000CD }
-
-/* OtherAspects. */
-.Agda .DottedPattern        {}
-.Agda .UnsolvedMeta         { color: black; background: yellow         }
-.Agda .UnsolvedConstraint   { color: black; background: yellow         }
-.Agda .TerminationProblem   { color: black; background: #FFA07A        }
-.Agda .IncompletePattern    { color: black; background: #F5DEB3        }
-.Agda .Error                { color: red;   text-decoration: underline }
-.Agda .TypeChecks           { color: black; background: #ADD8E6        }
-.Agda .Deadcode             { color: black; background: #808080        }
-.Agda .ShadowingInTelescope { color: black; background: #808080        }
-
-/* Standard attributes. */
-.Agda a { text-decoration: none }
-.Agda a[href]:hover { background-color: #B4EEB4 }
-
-pre.Agda {
-  padding: 12px;
-  background-color: white;
-  border-left: 1px solid rgb(210, 218, 224);
-  border-radius: 5px;
-  white-space:pre;
-}
-
-pre.Agda a:hover {
-  text-decoration: none;
-}

lab/docs/README.md

@@ -1,800 +0,0 @@
-# Proposal : MiniJuvix [draft]
-
-[![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:
-https://hackmd.io/Xlvu82eFQ_m-cebUWAtGsw?edit -->
-
-$$
-% ---------- To typeset grammars -----------------------------
-\renewcommand\.{\mathord.}
-\newcommand{\EQ}{\mkern5mu\mathrel{::=}}
-\newcommand{\OR}[1][]{\mkern17mu | \mkern12mu}
-\newcommand{\Or}{\mathrel|}
-\newcommand{\RT}[1]{\{#1\}}
-\newcommand{\RV}[1]{\langle#1\rangle}
-\newcommand{\Let}{\mathbf{let}\:}
-\newcommand{\Q}{\mathrel|}
-\newcommand{\I}{\color{blue}}
-\newcommand{\O}{\color{green}}
-% ---------- To typese rules ---------------------------------
-\newcommand{\rule}[3]{%
-\frac{%
-\begin{gathered}\,{#2}%
-\end{gathered}%
-}{#3}\:{\mathsf{#1}}}
-% Bidirectional judgements
-\newcommand{\check}[4]{{{#1}\,\vdash\,{#2}\,\overset{{#3}}{\color{red}{\Leftarrow}}\, {#4}}}
-\newcommand{\infer}[4]{{{#1}\,\vdash\,{#2}\,\overset{{#3}}{\color{blue}{\Rightarrow}}\, {#4}}}
-% ------------------------------------------------------------
-$$
-
-###### tags: `Juvix`
-
-## Abstract
-
-MiniJuvix implements a programming language that takes variable resources very
-seriously in the programs. As mathematical foundation, we are inspired by
-Quantitative type theory (QTT), a dependent type theory that marriages ideas
-from linear logic and traditional dependently typed programs to writing memory-efficient programs using resource accounting. Among the language features, there is a type for a universe,
-dependent function types, tensor products, sum types, and more type formers.
-
-The main
-purpose of MiniJuvix is to serve as a guide to supporting/extending the
-[Juvix](/Q5LbuHI5RXaJ8mD08yW7-g) programming language, in particular, the design
-of a correct and efficient typechecker.
-
-In this document we provide a work in progress report containing a description
-of the MiniJuvix bidirectional type checking algorithm. We have provide some
-Haskell sketches for the algorithm implementation.
-
-The code will be available on the Github repository:
-[heliaxdev/MiniJuvix](https://github.com/heliaxdev/MiniJuvix). In this document,
-we only refer to the implementation provided in the `qtt` branch.
-
-## Language
-
-### Syntax
-
-**Quantities** In the traditional QTT, each term has a usage/quantity annotation
-in the semiring $\{0,1,\omega\}$. Besides the semiring structure, we also
-consider different ordering of these terms. One choice for such an order states
-that $0,1 < \omega$ and $0$ and $1$ are not comparable, i.e., $0 \not < 1$. This
-order is good, at least in the sense that terms of zero usage and $1$ usage live
-in completely different worlds, from the evaluation point-of-view. Terms or zero
-usage are *irrelevant* at runtime, and we therefore erase them in the *erasure*
-phase. While, non-zero terms are *present* during compilation and execution of
-the program. We embrace this distinction in the implementation with the data type
-`Relevant` with constructors *irrelevant* and *relevant*.
-
-
-$$
-\begin{aligned}
-%x,y,z &\EQ \dotsb & \text{term variable} \\[.5em]
-\pi,\rho,\sigma &\EQ 0 \Or 1 \Or \omega
-  & \text{(quantity variables)} \\[.5em]
-\end{aligned}
-$$
-<!-- A, B &\EQ \mathcal{U}                  & \text{universe} \\
-     &\OR (x :^{\sigma} A) \to B       &\text{depend. fun. type} \\
-     &\OR (x :^{\sigma} A) \otimes B   &\text{tensor prod. type} \\[.5em]
-u, v &\EQ \mathsf{Var}(x)    &\text{variable}\\
-&\OR \mathsf{Ann}(x, A) &\text{annotation}\\
-
-&\OR u\,v  &\text{application} \\
-&\OR \lambda x.v  &\text{lambda abs.} \\[.5em]
-&\OR \color{gray}{f}  &\color{gray}{\text{named function(review)}} \\
-&\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}{\cdots}  &\color{gray}{\text{record. proj.}} \\[.7em]
-\Gamma &\EQ \emptyset \Or \Gamma, x :^{\sigma} A & \text{ contexts}
-\\[1em]
-\Delta &\EQ () \Or (x : A)\,\Delta& \text{ telescopes} -->
-
-**Judgements** The core language in MiniJuvix is bidirectional syntax-directed,
-meaning that a *judgement* in the theory contains a term that is either
-*checkable* or *inferable*. A type judgement consists of a *context*, a *term* --the term quantity required--, a *judgement mode*, and a *type*. Precisely, the judgement
-mode is either *checking* or *inferring*, as illustrated in the rules below,
-respectively, using a red and blue arrow.
-
-$$
-\begin{gathered}
-\check{\Gamma}{t}{\sigma}{M}
-\qquad
-\infer{\Gamma}{t}{\sigma}{M}
-\end{gathered}
-%
-$$
-
-We will refer to the *erased* part of the theory when the variable resource
-$\sigma$ is zero in the type judgement ; otherwise, we are in the *present*
-segment of the theory. Another way to refer to this distinction is that no
-computation is required in the $\sigma$ zero theory. Otherwise, we say that the judgement possess *computation content*.
-
-
-**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$.
-
-$$
-\begin{aligned}
-\Gamma &\EQ \emptyset \Or (\Gamma, x\overset{\pi}{:} A) & \text{(contexts)}
-\end{aligned}
-$$
-
-A needed context operation is *scaling*. The *scalar product* with a context
-$\Gamma$ is defined by induction on the context structure. Given a scalar number
-$\sigma$, the product $\sigma \cdot \Gamma$ denotes the context $\Gamma$ after
-multiplying *all* its resources variables by $\sigma$.
-
-$$
-\begin{aligned}
-\color{green}{\sigma} \cdot \emptyset &:= \emptyset,\\
-\color{green}{\sigma} \cdot (\Gamma, x \overset{\color{green}{\pi}}{:} A) &:= \color{green}{\sigma} \cdot \Gamma , x \overset{\color{green}{\sigma\cdot \pi}}{:} A.
-\end{aligned}
-$$
-
-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.
-
-$$
-\begin{aligned}
-\emptyset+\emptyset &:=\emptyset \\
-(\Gamma_{1}, x \overset{\color{green}{\sigma}}{:} A)+(\Gamma_{2}, x \overset{\color{green}{\pi}}{:} A) &:=(\Gamma_{1}+\Gamma_{2}), x^{\color{green}{\sigma+\pi}} S
-\end{aligned}
-$$
-
-**Telescopes** A *resource* telescope is the name for grouping types with
-resource information. We use telescopes in forming new types, for
-example, in forming new inductive types.
-
-\begin{aligned}
-\Delta &\EQ () \Or \Delta(x \overset{\sigma}{:} A) & \text{(telescopes)}
-\end{aligned}
-
-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.
-
-$$
-\begin{aligned}
-A , B%
-&\EQ \mathcal{U} & \text{(universe type)} \\
-&\OR (x \overset{\sigma}{:} A) \to B       &\text{(depend. fun. type)} \\
-&\OR (x \overset{\sigma}{:} A) \otimes B   &\text{(tensor prod. type)} \\
-&\OR A + B   &\text{(sum type)} \\
-&\OR 1   &\text{(unit type)} \\
-&\OR \color{gray}{P} &\color{gray}{\text{(primitive type)}}\\
-&\OR \color{gray}{D} &\color{gray}{\text{(inductive type decl.)}}\\
-&\OR \color{gray}{R} &\color{gray}{\text{(record type decl.)}}
-\end{aligned}
-$$
-
-On the other hand, we want to consider a set of *primitive types*, each of these with a set of *primitive* terms. An example of a primitive types is that of the type
-of *boolens*, denoted by $\mathsf{Bool}$.  $\mathsf{true} : \mathsf{Bool}$ and
-$\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.
-
-$$
-\begin{aligned}
-u, v , t , f &\EQ \mathsf{Var}(x)    &\text{(variable)}\\
-&\OR \mathsf{Ann}(x,A)           &\text{(type annotation)}\\
-&\OR \mathsf{Lam}(x,t)           &\text{(lambda abstraction)}\\
-&\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.)}}
-\end{aligned}
-$$
-
-The explicit naming below like $\mathsf{Ann}$ is on purpose. We want to avoid
-any confussion, for example, between type annotations and usage type annotation,
-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.
-
-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}}{
-%
-}
-{\emptyset \ \mathsf{ctx}}
-\qquad
-\rule{,\mbox{-}\mathsf{ctx}}{
-\Gamma \ \mathsf{ctx}
-\qquad
-\color{green}{\Gamma \vdash A \ \mathsf{type}}
-\qquad
-\sigma \ \mathsf{Quantity}
-}
-{
-(\Gamma , x \overset{\sigma}{:} A) \ \mathsf{ctx}
-}
-$$
-$$
-\rule{\cdot\mbox{-}\mathsf{ctx}}{%
-\Gamma \ \mathsf{ctx} \qquad \sigma \ \mathsf{Quantity}
-}{
-\sigma \cdot \Gamma \ \mathsf{ctx}
-}\qquad
-\rule{\mbox{+}\mbox{-}\mathsf{ctx}}{%
-\Gamma_1 \ \mathsf{ctx} \qquad \Gamma_2 \ \mathsf{ctx} \qquad  0\cdot \Gamma_1 = 0 \cdot \Gamma_2
-}{
-\Gamma_1 + \Gamma_2 \ \mathsf{ctx}
-}
-$$
-
-Below, we describe the algorithms for checking and infering types in a mutually
-defined way. The corresponding algorithms are the functions `check` and `infer`
-in the implementation. The definition of each is the collection and
-interpretation of the typing rules (reading them bottom to top).
-
-For example, the `infer` method is defined to work with three
-arguments: one implicit argument for the context $\Gamma$ and two explicit
-arguments, respectively, the term $t$ and its quantity $\sigma$. The output of the algorithm is precisely the type $M$ for $t$ in the rule below.
-
-$$
-\begin{gathered}
-\rule{}{
-p_1 \cdots\ p_n
-}{
-\infer{\Gamma}{t}{\sigma}{M}
-}
-\end{gathered}
-%
-$$
-
-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.
-
-A *reduction* step is denoted by $\Gamma \vdash
-t \rightsquigarrow t'$ or simply by $t \rightsquigarrow t'$ whenever the context
-$\Gamma$ is known. Such a reduction is obtained by calling `eval` in the
-implementation.
-
-**Remark.**  A term in the [Core](https://github.com/heliaxdev/MiniJuvix/blob/qtt/src/MiniJuvix/Syntax/Core.agda) implementation is either a Checkable or Inferable term. We refer to these
-options as the *mode* of the term. In a typing rule the strategy/mode in a type
-judgement determines the mode of the term in the conclusion. In the example above, $t$ is Inferable.
-
-```haskell
-data Term : Set where
-  Checkable : CheckableTerm → Term  -- terms with a type checkable.
-  Inferable : InferableTerm → Term  -- terms that which types can be inferred.
-```
-
-
-**TODO**: we need to reflect on how we introduce the judgement $\Gamma \vdash A\  \mathsf{type}$ of the well-formed types. This may change the way of presenting formation rules, as the first ones below.
-
-## Checking rules
-
-This section mainly refers to the construction of checkable terms in the
-implementation.
-
-*Remark.* We omit comments in the formation rules below. The general idea is
-that no resources are needed to form a type. Therefore, we only check when
-forming a type in the erase part of the theory, for both, premises and
-conclusion.
-
-
-- [x] UniverseType
-- [x] PiType
-- [x] Lam
-- [x] TensorType
-- [x] TensorIntro
-- [x] UnitType
-- [x] Unit
-- [ ] SumType
-
-
-
-### Universe
-
-**Formation rule**
-
-$$
-\rule{}{\Gamma \ \mathsf{ctx} }{\Gamma \vdash \mathcal{U} \ \mathsf{type}}
-\qquad
-\begin{gathered}
-\rule{Univ{\Leftarrow}}{
-(0\cdot \Gamma) \ \mathsf{ctx}
-}{
-0\cdot \Gamma \vdash \mathcal{U}\, \overset{0}{\color{red}\Leftarrow}\,\, \mathcal{U}
-}
-\end{gathered}
-%
-$$
-
-### Dependent function types
-
-**Formation rule**
-
-$$
-\rule{}{\Gamma \ \mathsf{ctx}
-\qquad \Gamma \vdash A \ \mathsf{type}
-\qquad (\Gamma , x \overset{\sigma}{:} A) \vdash B(x) \ \mathsf{type}
-}{\Gamma \vdash (x \overset{\sigma}{:} A) \to B \ \ \mathsf{type}}
-\\
-\begin{gathered}
-\rule{Pi{\Leftarrow}}{
-0\cdot \Gamma \vdash A \, \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
-\qquad
-(0\cdot \Gamma,\,x\overset{0}{:}A)\vdash B \, \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}\quad
-}{
-0\cdot \Gamma \vdash (x\overset{\pi}{:}A)\rightarrow B \overset{0}{\color{red}\Leftarrow}\mathcal{U}
-}
-\end{gathered}
-%
-$$
-
-**Introduction rule**
-
-The lambda abstraction rule is the introduction rule of a dependent function
-type. The principal judgement in this case is the conclusion, and we therefore
-check against the corresponing type $(x \overset{\sigma}{:} A) \to B$. With
-the types $A$ and $B$, all the information about the premise
-becomes known, and it just remains to check its judgement.
-
-
-
-$$\begin{gathered}
-\rule{Lam{\Leftarrow}}{
-(\Gamma, x\overset{\sigma\pi}{:}A) \vdash b \,\overset{\sigma}{\color{red}\Leftarrow}\,B
-}{
-\Gamma \vdash \lambda x.b \overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A)\rightarrow B
-}
-\end{gathered}
-%
-$$
-
-Another choice here is $\lambda x.b$ instead of $\lambda\,\mathsf{Ann}(x,A). b$.
-The former option will change the strategy, to infer the conclusion, since one would have enough information for typing.
-
-### Tensor product types
-
-**Formation rule**
-
-$$\begin{gathered}
-\rule{\otimes\mbox{-}{\Leftarrow}}{
-0\cdot \Gamma \vdash A \,\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
-\qquad
-(0\cdot \Gamma, x\overset{0}{:}A) \vdash B\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}\quad
-}{
-0\cdot \Gamma \vdash (x\overset{\pi}{:}A) \otimes B \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
-}
-\end{gathered}
-%
-$$
-
-**Introduction rule**
-
-A rule to introduce pairs in QTT appears in [Section 2.1.3 in Atkey's
-paper](https://bentnib.org/quantitative-type-theory.pdf). We here present this rule
-in a more didactical way but also following the bidirectional
-recipe. Briefly, the known rule is splitted in two cases, the erased and present
-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.
-
-
-$$\begin{gathered}
-\rule{\otimes I{\Leftarrow}}{
-\check{\sigma\pi \cdot \Gamma_1}{u}{\sigma\pi}{A}
-\qquad
-\check{\Gamma_2}{v}{\sigma}{B[u/x]}\quad
-\color{gray}{0 \cdot \Gamma_1 = 0\cdot \Gamma_2}\quad
-}{
-\check{\sigma\pi\cdot \Gamma_1 + \Gamma_2}{(u,v)}{\sigma}{(x\overset{\pi}{:}A) \otimes B}
-}
-\end{gathered}
-%
-$$
-
-Essentially, we are
-forming $\sigma$ *dependent* pairs where the first cordinate, $u$, is used $\pi$
-times in the second component. This is the reason for having $\sigma\pi\cdot
-\Gamma_1$ in the conclusion since,  $u$ is taken from $\Gamma_1$. The gray
-premises below are necessary, since one must ensure that the addition between
-context is possible.
-
-Finally, we obtain the following two rules that make up the original one.
-
-
-1. $$\begin{gathered}
-\rule{\otimes I_1{\Leftarrow}}{
-\color{green}{\sigma\pi = 0}
-\qquad
-0\cdot \Gamma \vdash u \,\overset{0}{\color{red}\Leftarrow}\,A
-\qquad
-\Gamma \vdash v \,\overset{\sigma}{\color{red}\Leftarrow}\,B[u/x]
-\qquad
-}{
-\Gamma \vdash (u,v)\overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A) \otimes B
-}
-\end{gathered}
-%
-$$
-
-2. $$\begin{gathered}
-\rule{\otimes I_2{\Leftarrow}}{
-\color{green}{\sigma\pi \neq 0}\qquad
-\Gamma_{1} \vdash u \,\overset{1}{\color{red}\Leftarrow}\,A
-\qquad
-\Gamma_{2} \vdash v \,\overset{\sigma}{\color{red}\Leftarrow}\,B[u/x]
-\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
-}
-\end{gathered}
-%
-$$
-
-### Unit type
-
-$$
-\rule{}{
-0 \cdot \Gamma \ \mathsf{ctx}
-}{
-\Gamma \vdash 1 \ \mathsf{type}
-}
-\qquad
-\rule{1\mbox{-}I}{
-0 \cdot \Gamma \ \mathsf{ctx}
-}{
-\check{0\cdot\Gamma}{1}{0}{\mathcal{U}}
-}
-\qquad
-\rule{*\mbox{-}I}{
-0 \cdot \Gamma \ \mathsf{ctx}
-}{
-\check{0\cdot\Gamma}{*}{0}{1}
-}
-$$
-
-### Sum type
-
-TODO
-
-### Inductive types
-
-TODO
-
-
-## Conversion rules
-
-
-Include the rules for definitional equality:
-- [ ] β-equality,
-- [ ] reflexivity,
-- [ ] symmetry,
-- [ ] transitivity, and
-- [ ] congruence.
-
-
-$$\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
-\color{green}{S =_{\beta} T}\ \,\,\,
-}{
-\Gamma \vdash M \overset{\sigma}{\color{red}\Leftarrow} T
-}
-\end{gathered}
-%
-$$
-
-
-## 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.
-
-
-By design, a term is inferable if it is one of the following cases.
-
-- [x] Variable
-- [x] Annotation
-- [x] Application
-- [x] Tensor type elim
-- [ ] Sum type elim
-
-Each case above has as a rule in what follows.
-
-The Haskell type of `infer` would be similar as the following.
-
-```haskell
-infer :: Quantity -> InferableTerm -> Output (Type , Resources)
-```
-
-where
-
-```haskell
-Output = Either ErrorType
-Resources = Map Name Quantity
-```
-
-### Variable
-
-A variable can be *free* or *bound*. If the variable is free, the rule is as
-follows.
-
-**Free variable**
-
-$$
-\begin{gathered}
-\rule{Var⇒}{
-(x :^{\sigma} M) \in \Gamma
-}{
-  \Gamma \vdash \mathsf{Free}(x) {\color{blue}\Rightarrow}^{\sigma} M
-}
-\end{gathered}
-%
-$$
-
-*Explanation*:
-
-1. The input to `infer` is a variable term of the form `Free x`.
-2. The only case for introducing a variable is to have it in the context.
-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.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)
-      -> return (typeM, updateResources (x, _σ) )
-    Nothing
-      -> throwError "Variable not present in the context"
-```
-
-The method `updateResources` rewrites the map tracking names with their quantities.
-
-**Bound variables**
-
-The case of the`Bound` variable throws an error.
-
-### Annotations
-
-$$
-\begin{gathered}
-\rule{Ann{⇒}}{
-0\cdot \Gamma \vdash A\,{\color{red}\Leftarrow}^0\,\mathcal{U}
-\qquad
-\Gamma \vdash x\,{\color{red}\Leftarrow}^\sigma\, A
-}{
-  \Gamma \vdash \mathsf{Ann}(x,A)\,{\color{blue}\Rightarrow}^{\sigma}\,A
-}
-\end{gathered}
-%
-$$
-
-Any annotation possess type information that counts as known facts, and we therefore infer. However, this is a choice.
-
-- First, we must check that $A$ is a type, i.e., a term in *some* universe.
-Because there is only one universe we denote it by $\mathcal{U}$. The formation
-rule for types has no computation content, then the usage is zero in this case.
-- Second, the term $x$ needs to be checked against $A$ using the same usage
-$\sigma$ we need in the conclusion. The context for this is $\Gamma$. There is
-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)`.
-  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
-$A'$. If so, the returning type is $A'$ and the table resources has to be updated
-(the $\color{gray}{gray}$ $\Theta$ in the rule below).
-
-$$
-\begin{gathered}
-\rule{Ann{⇒}}{
-\check{0\cdot \Gamma}{A}{0}{\mathcal{U}}
-\qquad
-A \color{green}{\rightsquigarrow} A'
-\qquad
-\check{\Gamma}{x}{\sigma}{A'} \color{darkgrey}{\dashv \Theta}
-}{
-\infer{\Gamma}{\mathsf{Ann}(x,A)}{\sigma}{A'}
-\color{darkgrey}{\dashv \Theta}
-}
-\end{gathered}
-%
-$$
-
-Haskell prototype:
-
-```haskell
-infer _ (Ann termX typeM) = do
-  _         <- check (0 .*. context) typeM zero Universe
-  typeM'    <- evalWithContext typeM
-  (_ , newUsages) <- check context termX typeM'
-  return (typeM' , newUsages)
-```
-
-### Application
-
-**Elimination rule**
-
-Recall the task is to find $A$ in $\Gamma \vdash \mathsf{App}(f,x) :^{\sigma}
-A$. If we follow the bidirectional type-checking recipe, then it makes sense to
-infer the type for an application, i.e., $\Gamma \vdash \mathsf{App}(f,x)
-\Rightarrow^{\sigma} A$. An application essentially removes a lambda abstraction
-introduced earlier in the derivation tree. The rule for this inference case is a
-bit more settle, especially because of the usage variables.
-
-To introduce the term of an application, $\mathsf{App}(f,x)$, it requires to
-give/have a judgement saying that $f$ is a (dependent) function, i.e., $\Gamma
-\vdash f \overset{\sigma}{:} (x \overset{\pi}{:} A) \to  B$, for usages variables $\sigma$ and
-$\pi$. Then, given $\Gamma$, the function $f$ uses $\pi$ times its input,
-mandatory. We therefore need $\sigma\pi$ resources of an input for $f$ if we
-want to apply $f$ $\sigma$ times, as in the conclusion $\Gamma \vdash
-\mathsf{App}(f,x) \Rightarrow^{\sigma} A$.
-
-In summary, the elimination rule is often presented as follows.
-
-$$\begin{gathered}
-\rule{}{
-\Gamma \vdash f :^{\sigma} (x : ^\pi A) \to  B
-\qquad
-\sigma\pi\cdot\Gamma' \vdash x : ^{\sigma\pi} A
-}{
-\Gamma + \sigma\pi\cdot\Gamma'  \vdash \mathsf{App}(f,x)  :^{\sigma} B
-}
-\end{gathered}
-%
-$$
-
-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$.
-
-$$\begin{gathered}
-\rule{}{
-\Gamma \vdash f {\color{blue}\Rightarrow}^{\sigma}(x : ^\pi A) \to  B
-\qquad
-\sigma\pi\cdot\Gamma' \vdash x {\color{red}\Leftarrow}^{\sigma\pi} A
-\qquad
-\color{gray}{0 \cdot \Gamma = 0 \cdot \Gamma'}
-}{
-\Gamma + \sigma\pi\cdot\Gamma'  \vdash \mathsf{App}(f,x) \,{\color{blue}\Rightarrow^{\sigma}}\, B
-}
-\end{gathered}
-%
-$$
-
-To make our life much easier, the rule above can be splitted in two cases,
-emphasising the usage bussiness.
-
-1. $$\begin{gathered}
-\rule{App{\Rightarrow_1}}{
-\color{green}{\sigma \cdot \pi = 0}
-\qquad
-\Gamma \vdash f {\color{blue}\Rightarrow^{\sigma}} (x :^{\pi} A) \to B
-\qquad
-0\cdot \Gamma \vdash x {\color{red}\Leftarrow^{0}} A
-\qquad
-}{
-\infer{\Gamma}{\mathsf{App}(f,x)}{\sigma}{B}
-}
-\end{gathered}
-%
-$$
-
-2. $$\begin{gathered}
-\rule{App{\Rightarrow_2}}{
-\color{green}{\sigma \cdot \pi \neq 0}
-\qquad
-\infer{\Gamma_1}{f}{\sigma}{(x :^{\pi} A) \to B}
-\qquad
-\check{\Gamma_2}{x}{1}{A}
-\qquad
-\color{gray}{0 \cdot \Gamma_1 = 0 \cdot \Gamma_2}
-\quad
-}{
-\infer{\Gamma_1 + \sigma \pi\cdot \Gamma_2}{\mathsf{App}(f,x)}{\sigma}{B}
-}
-\end{gathered}
-$$
-
-
-In summary, we infer the type of $f$. If it is a $\Pi$-type, then one checks
-whether $\sigma\pi$ is zero or not. If so, we use Rule No.1, otherwise, Rule No.
-2. Otherwise, something goes wrong, an error arise.
-
-Sketch:
-
-```haskell=
-infer σ (App f x) = do
-  (arrowAtoB, usages) <- infer σ f
-  case arrowAtoB of
-    IsPiType π _ typeA typeB -> do
-      σπ <- case (σ .*. π) of
-       -- Rule No. 1
-       Zero -> do
-         (_ , nqs) <- check x typeA (mult Zero context)
-          return nqs
-       -- Rule No. 2
-       _ -> undefined -- TODO (mult σπ context)
-    -- f is not a function:
-    ty -> throwError $ Error ExpectedPiType ty (App f x)
-```
-
-In the rules above, we have the lemma:
-
-- $1 \cdot \Gamma \vdash x :^1 A$ entails that $\sigma \cdot \Gamma \vdash x
-:^\sigma A$ for any usage $\sigma$.
-
-
-## Tensor products
-
-**Elimination rule**
-
-In Atkey's QTT, there is no $\Sigma$-types but instead tensor product types. As
-with any other elimination rule, in the principal judgement, we synthetise a
-type. In our case, the principal judgement shows up in the first premise, which
-is the fact that $M$ is a tensor product type. If we infer that, the types $A$
-and $B$ become known facts. Then, the type $C$, depending on $A$ and $B$ become checkable, also making the next judgement checking.
-
-
-
-$$\begin{gathered}
-\rule{TensorElim{\Rightarrow}}{
-\infer{\Gamma_{1}}{M}{\sigma}{(x\overset{\pi}{:}A)\otimes B}
-\\
-\check{(0\cdot \Gamma_{1},z\overset{0}{:}(x\overset{\pi}{:}A)\otimes B)}{C}{0}{\mathcal{U}}
-\\
-\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]
-}
-\end{gathered}
-%
-$$
-
-*Remark* Inspired by the tensor product rules in linear logic, there is a need to
-decompose a pair in its components. We have to be sure that all the resources in
-each component are effectively used. This mechanism needs to be introduced somewhere somehow, Idk yet. It is the keyword $\mathsf{let}\mbox{-}\mathsf{in}$.
-
-## Sum type elim
-
-TODO
-
-
-## References
-
-- Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). Association for Computing Machinery, New York, NY, USA, 56–65. DOI:https://doi.org/10.1145/3209108.3209189
-- Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (June 2022), 38 pages. DOI:https://doi.org/10.1145/3450952
-- James Wood, Robert Atkey. A Linear Algebra Approach to Linear Metatheory. Arxiv: https://arxiv.org/abs/2005.02247
-- Andy Morris. Juvix: Core language documentation. https://juvix.readthedocs.io/en/latest/compiler/core/core-language.html#id6
-- Andy Morris. Proposal: Records in Core. https://hackmd.io/UT269VN1R6-qchHaWzg7KQ
-- SVOBODA, Tomáš. Additive Pairs in Quantitative Type Theory. Praha, 2021. Diplomová práce Univerzita Karlova, Matematicko-fyzikální fakulta, Katedra algebry. Vedoucí práce Šefl, Vít. http://hdl.handle.net/20.500.11956/127263
-- Conor McBride. 2016. I Got Plenty o' Nuttin'. In A List of Successes That Can Change the World-Essays Dedicated to Philip Wadler on the Occasion of His $60 t h$ Birthday. 207-233. DOI:https://doi.org/10.1007/978-3-319-30936-1

lab/docs/_config.yml

@@ -1,9 +0,0 @@
-theme: minima
-# title: "Proposal: MiniJuvix"
-keywords:
-  - minijuvix
-
-lang: en_US
-css:
-  - main.css
-  - Agda.css

lab/docs/conv.sh

@@ -1,34 +0,0 @@
-#!/bin/zsh
-# Adapted from https://jonaprieto.github.io/synthetic-graph-theory/conv.sh
-#
-# 1. Install pandoc from http://johnmacfarlane.net/pandoc/
-# 2. Copy this script into the directory containing the .md files
-# 3. Ensure that the script has all the permissions to be executed
-# $ chmod +x conv.sh
-# 4. Run the script
-# $ ./conv.sh
-
-PANDOCVERSION=$(pandoc --version | head -n 1)
-
-FILES="*.md"
-
-for f in $FILES
-do
-  filename="${f%.*}"
-  html=$filename.html
-  logdata=$(git log --pretty="format:(%as)(%h) %Creset%s by %cl" --no-merges -20)
-  echo "--------------------------------------------------------------------------------"
-  pandoc --standalone \
-         --metadata-file="_config.yml" \
-         --template=template.html5 \
-         "$f" \
-         --from markdown+tex_math_dollars+tex_math_double_backslash+latex_macros+lists_without_preceding_blankline \
-         --to=html  \
-         --mathjax \
-         -o "$html" \
-         --variable=updated:"$(date +'%A, %B %e, %Y, %I:%M %p')" \
-         --variable=lastCommit:"$logdata" \
-         --variable=pandocVersion:"${PANDOCVERSION:u}" \
-         --variable=file:"src/$filename"
-done
-cp README.html index.html

lab/docs/examples/Example1.mjuvix

@@ -1,223 +0,0 @@
--- 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

@@ -1,44 +0,0 @@
--- 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

@@ -1,32 +0,0 @@
--- 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

@@ -1,243 +0,0 @@
-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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1,11 +0,0 @@
-# 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

@@ -1,23 +0,0 @@
-# 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

@@ -1,34 +0,0 @@
-<
-$ 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

@@ -1,22 +0,0 @@
-<
-$ 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

@@ -1,4 +0,0 @@
-$ 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

@@ -1,30 +0,0 @@
-$ 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

@@ -1,27 +0,0 @@
-$ 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

@@ -1,51 +0,0 @@
--- 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

@@ -1,417 +0,0 @@
-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/main.css

@@ -1,90 +0,0 @@
-body {
-    margin: 70px;
-    width: 50%;
-    font-size: 1.2em;
-}
-nav ul, footer ul {
-    font-family:'Helvetica', 'Arial', 'Sans-Serif';
-    padding: 0px;
-    list-style: none;
-    font-weight: bold;
-}
-nav ul li, footer ul li {
-    display: inline;
-    margin-right: 20px;
-}
-a {
-    text-decoration: none;
-    color: #999;
-}
-a:hover {
-    text-decoration: underline;
-}
-h1 {
-    font-size: 2em;
-    font-family:'Helvetica', 'Arial', 'Sans-Serif';
-    margin-bottom: .1em;
-}
-p {
-    line-height: 1.4em;
-    color: #333;
-    text-align: justify;
-
-}
-p.subtitle {
-    margin-top: initial;
-    color: black;
-}
-
-footer {
-    border-top: 1px solid #d5d5d5;
-    font-size: .8em;
-}
-
-ul.posts {
-    margin: 20px auto 40px;
-}
-
-ul.posts li {
-    list-style: none;
-}
-
-pre {
-    font-size: .95rem;
-    text-overflow: clip;
-    line-height: 1rem;
-    width: 50%;
-    font-family: "Menlo","Inconsolata","Consolas","Roboto Mono","Ubuntu Mono","Liberation Mono","Courier New",monospace;
-}
-
-.changelog {
-    color: darkgray;
-    min-width: 700px;
-}
-
-.powerby {
-    font-size: .8em;
-    line-height: .9em;
-    color:#999;
-    min-width: 700px;
-}
-
-.powerby p {
- line-height: .1em;
-}
-
-.authorship{
-    font-style: italic;
-}
-
-.authorship p {
-    line-height: .2em;
-    color: rgb(44, 44, 44);
-    font-size: .9em;
-}
-
-.abstract {
-    font-size: smaller;
-    color: gray;
-    margin-left: 20px;
-}

lab/docs/notes/Example.agda

@@ -1,100 +0,0 @@
--- 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

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

lab/docs/notes/module-scoping.org

@@ -1,35 +0,0 @@
-* 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

@@ -1,72 +0,0 @@
-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

lab/docs/template.html5

@@ -1,75 +0,0 @@
-<!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml" lang="$lang$" xml:lang="$lang$"$if(dir)$ dir="$dir$"$endif$>
-<head>
-  <meta charset="utf-8" />
-  <meta name="generator" content="pandoc" />
-  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
-$for(author-meta)$
-  <meta name="author" content="$author-meta$" />
-$endfor$
-$if(date-meta)$
-  <meta name="dcterms.date" content="$date-meta$" />
-$endif$
-$if(keywords)$
-  <meta name="keywords" content="$for(keywords)$$keywords$$sep$, $endfor$" />
-$endif$
-$if(description-meta)$
-  <meta name="description" content="$description-meta$" />
-$endif$
-  <title>$if(title-prefix)$$title-prefix$ – $endif$$pagetitle$</title>
-  <style>
-    $styles.html()$
-  </style>
-$for(css)$
-  <link rel="stylesheet" href="$css$" />
-$endfor$
-$if(math)$
-  $math$
-$endif$
-  <!--[if lt IE 9]>
-    <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
-  <![endif]-->
-$for(header-includes)$
-  $header-includes$
-$endfor$
-</head>
-<body>
-<div class="powerby">
-$if(file)$
-<p>$file$.</p>
-$endif$
-<p>Version of $updated$</p>
-<p>Powered by $pandocVersion/lowercase$</p>
-</div>
-<hr>
-$for(include-before)$
-$include-before$
-$endfor$
-$if(title)$
-<header id="title-block-header">
-<h1 class="title">$title$</h1>
-$if(subtitle)$
-<p class="subtitle">$subtitle$</p>
-$endif$
-</header>
-$endif$
-$if(toc)$
-<nav id="$idprefix$TOC" role="doc-toc">
-$if(toc-title)$
-<h2 id="$idprefix$toc-title">$toc-title$</h2>
-$endif$
-$table-of-contents$
-</nav>
-$endif$
-$body$
-$for(include-after)$
-$include-after$
-$endfor$
-$if(lastCommit)$
-<h2>Recent changes</h2>
-<pre class="changelog">
-$lastCommit$
-</pre>
-$endif$
-</body>
-</html>

test/MonoJuvix/Positive.hs

@@ -37,6 +37,6 @@ tests =
       "Polymorphism.mjuvix",
     PosTest
       "Polymorphic Simple Fungible Token"
-      "VP"
+      "FullExamples"
       "PolySimpleFungibleToken.mjuvix"
   ]

test/TypeCheck/Positive.hs

@@ -48,9 +48,9 @@ tests =
       "MiniHaskell"
       "HelloWorld.mjuvix",
     PosTest
-      "GHC backend SimpleFungibleToken"
-      "VP"
-      "SimpleFungibleToken.mjuvix",
+      "GHC backend MonoSimpleFungibleToken"
+      "FullExamples"
+      "MonoSimpleFungibleToken.mjuvix",
     PosTest
       "Axiom"
       "."

tests/positive/FullExamples/MonoSimpleFungibleToken.mjuvix

@@ -1,4 +1,4 @@
-module SimpleFungibleToken;
+module MonoSimpleFungibleToken;
 
 foreign ghc {
   import Anoma