[ examples ] Added examples based on juvix examples

examples/Example1.mjuvix

@@ -18,23 +18,29 @@ phase   := { parsing , check };
 backend := none; -- llvm.
 };
 
-module toParse;
+module Example1;
 
 module M;
 -- This creates a module called M,
 -- which it must be closed with:
-close M;
+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 ;
+	suc : Nat -> Nat ;
 };
 
 -- Term definition uses := instead of =.
@@ -92,15 +98,15 @@ inductive Empty{};
 inductive Unit { tt : Unit;};
 
 -- Indexed inductive type declarations:
-inductive Vect (n : Nat) (A : Type)
+inductive Vec (n : Nat) (A : Type)
 {
-	zero : Vect Nat.zero A;
-	succ : A -> Vect n A -> Vect (Nat.succ n) A;
+	zero : Vec Nat.zero A;
+	succ : A -> Vec n A -> Vec (Nat.succ n) A;
 };
 
-Vect' : Nat -> Type -> Type;
-Vect' Nat.zero A      := Unit;
-Vect' (Vect'.suc n) A := A -> Vect' n A;
+Vec' : Nat -> Type -> Type;
+Vec' Nat.zero A      := Unit;
+Vec' (Vec'.suc n) A := A -> Vec' n A;
 
 -- Record
 record Person {
@@ -116,28 +122,49 @@ h := \x -> match x {
 h' : Person -> Nat;
 h' {name = s , age = n} := n;
 
--- So far, we haven't used quantites, here is some examples.
--- One candidate is @ to mark the variable quantity.
--- If the quantity is not explicit, we assume it is `Any`.
+-- projecting fields values.
+h'' : Person -> String;
+h'' p := Person.name p;
 
--- The term `a` has quantity 3.
-axiom B : (1@x : A) -> Type;  -- type family
-axiom T : [1@x : A] -> B;     -- Tensor product type.
-axiom em : (1@x : A) -> B;  
+-- 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 : [ 1@x : A ] -> B;
-f x := em x;
+f' : [ 1@x : A ] -> B;
+f' x := em x;
 
--- The construction of a record must be in principle
--- based on the tensor prod. type constr. First guess.
--- A quantity can annotate a field name.
+-- 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) {
-	1@proj1 : A;
-	0@proj2 : 
-} -- maybe after, we can parse a list of identifiers/options.
-eta-equality, constructor prop;
-
+	proj1 : C;
+	proj2 :0 D;
+} 
+eta-equality, constructor prop;  -- extra options.
 
 -- More inductive types.
 inductive Id (A : Type) (x : A)
@@ -174,7 +201,7 @@ typeId M x := x = x;
 } in typeId A a;
 a-is-a-4 := a-is-a;
 
-close toParse;
+end Example1;
 
 -- future:
 -- module M' (X : Type);

examples/Example2.mjuvix

@@ -0,0 +1,45 @@
+-- Based on example3.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;

examples/Example3.mjuvix

@@ -0,0 +1,33 @@
+-- Based on example3.ju in anoma/juvix
+-- Below would be the equivalent file
+
+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;

notes/forTesting.md

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