remove old files

Makefile

@@ -47,3 +47,6 @@ profile: .PHONY
 clean:
 	rm newt*.js iife.js min.js min.js.gz
 
+audit: .PHONY
+	(cd playground && npm audit)
+	(cd newt-vscode && npm audit)

newt/Debug.newt

@@ -1,30 +0,0 @@
-module Debug
-
-data Unit : U where
-  MkUnit : Unit
-
-infixr 7 _::_
-data List : U -> U where
-  Nil : {A : U} -> List A
-  _::_ : {A : U} -> A -> List A -> List A
-
--- prj/menagerie/papers/combinatory
-
-infixr 6 _~>_
-data Type : U where
-  ι : Type
-  _~>_ : Type -> Type -> Type
-
-A : U
-A = Unit
-
-Val : Type -> U
-Val ι = A
-Val (x ~> y) = Val x -> Val y
-
--- can't get Val to expand here.
-#check (\ x => \ y => \ z => (Val (x ~> y ~> z))) : Type -> Type -> Type -> U
-
-foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> σ))
-foo {σ} {τ} {σ} = \ x => \ y => x
-

newt/DepEq.newt

@@ -1,73 +0,0 @@
-module DepEq
-
--- https://mathstodon.xyz/@MartinEscardo/114751459092567654
--- see also https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html
-
-infixr 5 _≡_
-infixl 6 _+_
-infixl 6 _++_
-infixr 7 _::_
-infixr 5 _≡⟨_⟩_
-
-data _≡_ : ∀ a. a → a → U where
-  Refl : ∀ a. {x : a} → x ≡ x
-
-cong : ∀ X Y. (f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
-cong f Refl = Refl
-
-data ℕ : U where
-  S : ℕ → ℕ
-  Z : ℕ
-
-_+_ : ℕ → ℕ → ℕ
-Z + m = m
-S k + m = S (k + m)
-
-+-assoc : (l m n : ℕ ) → l + (m + n) ≡ (l + m) + n
-+-assoc Z m n = Refl
-+-assoc (S k) m n = cong S (+-assoc k m n)
-
-
-
-_≡⟨_⟩_ : {0 A : U} → {0 B : A → U } →  {0 x₀ x₁ : A} → B x₀ → x₀ ≡ x₁ → B x₁ → U
-b₀ ≡⟨ Refl ⟩ b₁ = b₀ ≡ b₁
-
-congd : {0 A : U} → {0 B : A → U} → (f : (a : A) → B a) → {0 a₀ a₁ : A} →
-        (p : a₀ ≡ a₁) →
-        _≡⟨_⟩_ {_} {B} (f a₀) p (f a₁)
-congd f Refl = Refl
-
-data Vect : U → ℕ → U where
-  Nil : ∀ a. Vect a Z
-  _::_ : ∀ a n . a → Vect a n → Vect a (S n)
-
-_++_ : ∀ a n m. Vect a n → Vect a m → Vect a (n + m)
-Nil ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
-
--- REVIEW - make sure we're freezing metas at the end of a typesig / def
-cong-cons : ∀ a n m.  (x : a) → {xs : Vect a n} → {ys : Vect a m} → (p : n ≡ m) →
-            _≡⟨_⟩_ {_} {Vect a} xs p ys → _≡⟨_⟩_ {_} {Vect a} (x :: xs) (cong S p) (x :: ys)
--- This is failing because the type doesn't reduce.  We need to process arg2 first, after determining that
--- TODO the type of the second argument is not useful to split until the first one is split
--- need to check the type when we decide to split on an argument
--- cong-cons _ Refl Refl = ?
-
--- and this one was having some trouble on the RHS, which turned out to `cong`
--- being undefined.
-cong-cons _ Refl x = case x of Refl => Refl
-
--- Idris' complaint about B is more readable:
-
--- Error: While processing type of appAssoc. Can't solve constraint
--- between: Vec ?a ((?l + ?n) + ?m) and ?b ((?l + ?n) + ?m).
-
-++-assoc : ∀ a l n m. (xs : Vect a l) → (ys : Vect a n) → (zs : Vect a m) →
-           -- TODO newt + idris have trouble sorting out B
-           _≡⟨_⟩_ {_} {Vect a} (xs ++ (ys ++ zs)) (+-assoc l n m) ((xs ++ ys) ++ zs)
-++-assoc Nil ys zs = Refl
--- TODO need rhs hole to look more like this in newt:
--- hole : DepEq (x :: (xs ++ (ys ++ zs))) (cong S (plusAssoc k n m)) (x :: ((xs ++ ys) ++ zs))
-++-assoc {a} {S k} {n} {m} (x :: xs) ys zs = cong-cons x (+-assoc k n m) (++-assoc xs ys zs)
-
-

newt/Equality1.newt

@@ -1,42 +0,0 @@
-module Equality1
-
--- Leibniz equality
-Eq : {A : U} -> A -> A -> U
-Eq = \ x y => (P : A -> U) -> P x -> P y
-
-refl : {A : U} {x : A} -> Eq x x
-refl = \ P Px => Px
-
-trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
-trans = \ Exy Eyz => Eyz (\ w => Eq x w) Exy
-
-sym : {A : U} {x y : A} -> Eq x y -> Eq y x
-sym = \ Exy => Exy (\ z => Eq z x) refl
-
-id : {A} -> A -> A
-id = \ x => x
-
-coerce : {A B : U} -> Eq A B -> A -> B
-coerce = \ EqAB a => EqAB id a
-
--- pi-forall's formulation
--- J : {A : U} ->
---     (x y : A) ->
---     (p : Eq x y) ->
---     {C : (z : A) -> Eq z y -> U} ->
---     (b : C y refl) ->
---     C x p
--- -- doesn't really work because we have refl and some Eq y y
--- J = \ x y eq {C} b => eq (\z => (q : Eq z y) -> C z q) (\ _ => b)
-
--- I don't think this is going to happen, maybe with funext?
--- anyway, could be useful case to improve error messages.
--- (add names)
-
-J : {A : U} ->
-    {C : (x y : A) -> Eq x y -> U} ->
-    (c : (x : _) -> C x x refl) ->
-    (x y : A) ->
-    (p : Eq x y) ->
-    C x y p
-J = \ c x y eq => eq (\ z => (q : Eq x z) -> C x z q) (\ _ => c x) eq

newt/Fix.newt

@@ -1,51 +0,0 @@
-module Fix
-
--- from piforall Fix.pi
-Type: U
-Type = U
-
--- TODO piforall makes the A in scope for the constructors
--- and has it on the let of the :
--- I think we want that for parameters?
-data D : (A : Type) -> Type where
-  F : {A : Type} -> (D A -> D A) -> D A
-  V : {A : Type} -> A -> D A
-
-
--- Here we have two A in play, so y is type of the
--- A in V and the expected return value is the other.
--- We do need to sort this out
-
-unV : { A : U} -> D A -> A
-unV (V y) = y
-unV (F f) = ?  -- was TRUSTME
-
-
-
--- And here we have D A:4 and D A:1
-unF : {A : Type} -> D A -> D A -> D A
-unF = \ {A} v x =>
-  case v of
-    F f => f x
-    V y => ? -- was TRUSTME
-
--- fix : {A : U} -> (A -> A) -> A
--- fix = \ {A} g =>
---   -- RLet is not yet implemented...
---   let omega = -- : D A -> D A =
---         (\ x => V (g (unv {A} (unF {A} x x))))
---   in unV {A} (omega (F omega))
-
--- data Nat : Type where
---    Zero : Nat
---    Succ : Nat -> Nat
-
--- fix_add : Nat -> Nat -> Nat
--- fix_add = fix [Nat -> Nat -> Nat]
---         \radd. \x. \y.
---             case x of
---               Zero   -> y
---               Succ n -> Succ (radd n y)
-
--- test : fix_add 5 2 = 7
--- test = Refl

newt/Foo.newt

@@ -1,18 +0,0 @@
--- foo
-module Foo
-
-id : (a : U) -> a -> a
-id = \ a => \ x => x
-
--- if I put foo here, it fails with 'extra toks' at "module"
--- errors aren't cutting to the top
--- I think we need the errors to be fatal if anything is consumed (since the nearest alt)
-
-List : U -> U
-List = \ A => (L : U) -> L -> (A -> L -> L) -> L
-
-nil : (A : U) -> List A
-nil = \ A L n f => n
-
-Bool : U
-

newt/JSLib.newt

@@ -1,17 +0,0 @@
-module JSLib
-
-
-
-
-infixl 4 _+_
-infixl 5 _*_
-
-pfunc _+_ : Int -> Int -> Int := `(x,y) => x + y`
-pfunc _*_ : Int -> Int -> Int := `(x,y) => x * y`
-
-ptype JVoid
-
--- REVIEW - maybe we only have body, use names from the pi-type and generate
--- the arrow (or inline?) ourselves
-pfunc log : String -> JVoid := `x => console.log(x)`
-pfunc debug : {a : U} -> String -> a -> JVoid := `(_,x,a) => console.log(x,a)`

newt/Order.newt

@@ -1,36 +0,0 @@
-module Order
-
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
-
-plus : Nat -> Nat -> Nat
-plus Z y = y
-plus (S x) y = S (plus x y)
-
-data Pair : U -> U -> U where
-  _,_ : {A B : U} -> A -> B -> Pair A B
-
-infix 1 _,_
-
-foo : Pair Nat Nat
--- vscode plugin issue: Without the space the info is rendered on Z...
-foo = (Z , S Z)
-
--- So I was going to force a (a + b, a) =?= (3,0) unification problem
--- as an example of needing _dynamic_ pattern unification
-data Eq : {A : U} -> A -> A -> U where
-  Refl : {A : U} -> {x : A} -> Eq x x
-
--- but hold up here.  This doesn't solve either.
--- Oh, because I can't reduce case.
--- And the FC is useless.
--- these go into caseeval.newt test
-two : Eq (plus Z (S (S Z))) (S (S Z))
-two = Refl
-
-two' : Eq (plus (S Z) (S Z)) (S (S Z))
-two' = Refl {Nat} {S (S Z)}
-
-three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z))
-three = Refl {Nat} {S (S (S Z))}

newt/Prelude.newt

@@ -1 +0,0 @@
-../src/Prelude.newt

newt/tutorial.newt

@@ -1,15 +0,0 @@
--- Files begin with a module declaration, modules not implemented yet
-module Tutorial
-
-
--- import Prelude  not implemented yet
-
--- declare a primitive type
-
-
--- declare a more complex primitive type
-ptype Array : U -> U
-
--- declare a primitive function
-pfunc alength : {a : U} -> Array a -> Int := `(x) => x.length`
-