clean up of old files

SciLean/Core/FloatAsReal.lean

@@ -25,7 +25,7 @@ instance : CommRing Float where
   nsmul_zero := sorry_proof
   nsmul_succ n x := sorry_proof
   sub_eq_add_neg a b := sorry_proof
-  natCast n := n.toUSize.toFloat
+  natCast n := n.toUInt64.toFloat
   natCast_zero := sorry_proof
   natCast_succ := sorry_proof
   intCast n := if n ≥ 0 then n.toNat.toUInt64.toFloat else -((-n).toNat.toUInt64).toFloat

SciLean/Core/Meta/ExtendContext.lean

@@ -1,6 +1,6 @@
 import SciLean.Core.Objects.FinVec
 import SciLean.Lean.Meta.Basic
-import SciLean.Data.Index
+import SciLean.Data.IndexType
 
 open Lean Meta Qq
 

SciLean/Core/Objects/SemiInnerProductSpace.lean

@@ -3,8 +3,6 @@ import SciLean.Core.Objects.Vec
 import SciLean.Core.Objects.Scalar
 import SciLean.Core.NotationOverField
 
-import SciLean.Data.EnumType
-
 namespace SciLean
 open LeanColls
 

SciLean/Core/Rand/Distributions/WalkOnSpheres.lean

@@ -69,8 +69,7 @@ def harmonicRec_fwdDeriv (n : ℕ)
     induction n n' du h
       . simp[harmonicRec]; autodiff
       . simp[harmonicRec];
-        simp only [smul_push]
-        autodiff; autodiff
+        simp only [smul_push]; autodiff
 
 
 def harmonicRec.arg_x.fwdDeriv_randApprox (n : ℕ)

SciLean/Data/ArrayType/Basic.lean

@@ -1,5 +1,4 @@
 import SciLean.Util.SorryProof
-import SciLean.Data.Index
 import SciLean.Data.ListN
 import SciLean.Data.StructType.Basic
 import SciLean.Data.Function

SciLean/Data/ArrayType/Notation.lean

@@ -27,8 +27,11 @@ abbrev introElemNotation {Cont Idx Elem} [DecidableEq Idx] [ArrayType Cont Idx E
 open Lean.TSyntax.Compat in
 -- macro "⊞ " x:term " => " b:term:51 : term => `(introElemNotation fun $x => $b)
 -- macro "⊞ " x:term " : " X:term " => " b:term:51 : term => `(introElemNotation fun ($x : $X) => $b)
+
+-- The `by exact` is a hack to make certain case work
+--    see: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/uncurry.20fails.20with.20.60Icc.60
 open Term Function in
-macro "⊞ " xs:funBinder* " => " b:term:51 : term => `(introElemNotation (HasUncurry.uncurry fun $xs* => $b))
+macro "⊞ " xs:funBinder* " => " b:term:51 : term => `(introElemNotation (HasUncurry.uncurry (by exact (fun $xs* => $b))))
 
 
 @[app_unexpander introElemNotation]
@@ -153,11 +156,11 @@ partial def expand' (l : List (TSyntax `dimSpec)) : TermElabM Expr :=
     match t with
     | `(dimSpec| $n:term) => do
       try
-        let n ← elabTerm n q(USize)
+        let n ← elabTerm n q(Nat)
         return ← mkAppM ``Fin #[n]
       catch _ =>
         return ← elabTerm n none
-    | `(dimSpec| [$n:term : $m:term]) => do elabTerm (← `(Idx' $n $m)) none
+    | `(dimSpec| [$n:term : $m:term]) => do elabTerm (← `(↑(Set.Icc ($n : Int) ($m : Int)))) q(Type)
     | `(dimSpec| [$ds:dimSpec,*]) => expand' ds.getElems.toList
     | _ => throwError "unexpected type power syntax"
   | t :: l' =>  do
@@ -184,7 +187,7 @@ elab_rules (kind:=typeIntPower) : term
 
   let Y ← expand' ns.getElems.toList
   let C ← mkFreshTypeMVar
-  let inst ← synthInstance <| mkAppN (← mkConst ``ArrayTypeNotation) #[C,Y,X]
+  let inst ← synthInstance <| mkAppN (← mkConstWithFreshMVarLevels ``ArrayTypeNotation) #[C,Y,X]
   let C ← whnfR (← instantiateMVars C)
   return ← instantiateMVars <| ← mkAppOptM ``arrayTypeCont #[Y,X,C,inst]
 

SciLean/Data/DataArray/DataArray.lean

@@ -65,7 +65,7 @@ def DataArray.reserve  (arr : DataArray α) (capacity : Nat) : DataArray α :=
     let newBytes := pd.bytes capacity
     let mut arr' : DataArray α := ⟨ByteArray.mkArray newBytes 0, arr.size, sorry_proof⟩
     -- copy over the old data
-    for i in fullRange (Fin arr.size) do
+    for i in IndexType.univ (Fin arr.size) do
       arr' := arr'.set ⟨i.1,sorry_proof⟩ (arr.get i)
     arr'
 

SciLean/Data/DataArray/PlainDataType.lean

@@ -1,5 +1,6 @@
 import SciLean.Util.SorryProof
-import SciLean.Data.Index
+-- import SciLean.Data.Index
+import LeanColls.Classes.IndexType
 
 namespace SciLean
 open LeanColls
@@ -302,101 +303,102 @@ instance : PlainDataType Bool where
   btype := .inl Bool.bitType
 
 
---------------- Idx n ------------------------------------------------
+--------------- Fin n ------------------------------------------------
 ----------------------------------------------------------------------
 
-/-- Number of bits necessary to store `Idx n` -/
-def Idx.bitSize  (n : USize) : USize := (USize.log2 n + (n - (1 <<< (USize.log2 n)) != 0).toUInt64.toUSize)
-def Idx.byteSize (n : USize) : USize := (Idx.bitSize n + 7) / 8
+/-- Number of bits necessary to store `Fin n` -/
+def Fin.bitSize  (n : Nat) : Nat := (Nat.log2 n + (n - (1 <<< (Nat.log2 n)) != 0).toUInt64.toNat)
+def Fin.byteSize (n : Nat) : Nat := (Fin.bitSize n + 7) / 8
 
 
--- INCONSISTENT: This breaks consistency with (n=0) as we could make `Idx 0` from a byte
+-- INCONSISTENT: This breaks consistency with (n=0) as we could make `Fin 0` from a byte
 -- Adding assumption (n≠0) is really annoying, what to do about this?
-def Idx.bitType (n : USize) (_ : n ≤ 256) : BitType (Idx n) where
+def Fin.bitType (n : Nat) (_ : n ≤ 256) : BitType (Fin n) where
   bits := (bitSize n).toUInt8
   h_size := sorry_proof
-  fromByte b := ⟨b.toUSize % n, sorry_proof⟩ --- The modulo here is just in case to remove junk bit values, also we need `n≠0` for consistency
+  fromByte b := ⟨b.toNat % n, sorry_proof⟩ --- The modulo here is just in case to remove junk bit values, also we need `n≠0` for consistency
   toByte   b := b.1.toUInt8
   fromByte_toByte := sorry_proof
 
-def Idx.byteType (n : USize) (_ : 256 < n) : ByteType (Idx n) where
-  bytes := byteSize n
+def Fin.byteType (n : Nat) (_ : 256 < n) : ByteType (Fin n) where
+  bytes := (byteSize n).toUSize
   h_size := sorry_proof
 
   fromByteArray b i _ := Id.run do
     let bytes  := byteSize n
-    let ofByte := i * bytes
+    let ofByte := i * bytes.toUSize
 
     let mut val : USize := 0
-    for j in fullRange (Idx bytes) do
-      val := val + ((b[ofByte+j.1]'sorry_proof).toUSize <<< (j.1*(8:USize)))
-    ⟨val, sorry_proof⟩
+    for j in IndexType.univ (Fin bytes) do
+      val := val + ((b[ofByte+j.1.toUSize]'sorry_proof).toUSize <<< (j.1.toUSize*(8:USize)))
+    ⟨val.toNat, sorry_proof⟩
 
   toByteArray b i _ val := Id.run do
     let bytes  := byteSize n
-    let ofByte := i * bytes
+    let ofByte := i * bytes.toUSize
 
     let mut b := b
-    for j in fullRange (Idx bytes) do
-      b := b.uset (ofByte+j.1) (val.1 >>> (j.1*(8:USize))).toUInt8 sorry_proof
+    for j in IndexType.univ (Fin bytes) do
+      b := b.uset (ofByte+j.1.toUSize) (val.1.toUSize >>> (j.1.toUSize*(8:USize))).toUInt8 sorry_proof
     b
 
   toByteArray_size := sorry_proof
   fromByteArray_toByteArray := sorry_proof
   fromByteArray_toByteArray_other := sorry_proof
 
--- INCONSISTENT: This breaks consistency see Idx.bitType
-instance (n) : PlainDataType (Idx n) where
+-- INCONSISTENT: This breaks consistency see Fin.bitType
+instance (n) : PlainDataType (Fin n) where
   btype :=
     if h : n ≤ 256
-    then .inl (Idx.bitType n h)
-    else .inr (Idx.byteType n (by simp at h; apply h))
+    then .inl (Fin.bitType n h)
+    else .inr (Fin.byteType n (by simp at h; apply h))
 
--------------- Index ----------------------------------------------
-----------------------------------------------------------------------
+-- TODO: change to IndexType
+-- -------------- Index ----------------------------------------------
+-- ----------------------------------------------------------------------
 
-def Index.bitType (α : Type) [Index α] (h : Index.size α ≤ 256) : BitType α where
-  bits := Idx.bitSize (Index.size α) |>.toUInt8
-  h_size := sorry_proof
-  fromByte b := fromIdx <| (Idx.bitType (Index.size α) h).fromByte b
-  toByte a   := (Idx.bitType (Index.size α) h).toByte (toIdx a)
-  fromByte_toByte := sorry_proof
+-- def Index.bitType (α : Type) [Index α] (h : Index.size α ≤ 256) : BitType α where
+--   bits := Idx.bitSize (Index.size α) |>.toUInt8
+--   h_size := sorry_proof
+--   fromByte b := fromIdx <| (Idx.bitType (Index.size α) h).fromByte b
+--   toByte a   := (Idx.bitType (Index.size α) h).toByte (toIdx a)
+--   fromByte_toByte := sorry_proof
 
-def Index.byteType (α : Type) [Index α] (hn : 256 < Index.size α ) : ByteType α where
-  bytes := Idx.byteSize (Index.size α)
-  h_size := sorry_proof
+-- def Index.byteType (α : Type) [Index α] (hn : 256 < Index.size α ) : ByteType α where
+--   bytes := Idx.byteSize (Index.size α)
+--   h_size := sorry_proof
 
-  fromByteArray b i h := fromIdx <| (Idx.byteType (Index.size α) hn).fromByteArray b i h
-  toByteArray b i h a := (Idx.byteType (Index.size α) hn).toByteArray b i h (toIdx a)
+--   fromByteArray b i h := fromIdx <| (Idx.byteType (Index.size α) hn).fromByteArray b i h
+--   toByteArray b i h a := (Idx.byteType (Index.size α) hn).toByteArray b i h (toIdx a)
 
-  toByteArray_size := sorry_proof
-  fromByteArray_toByteArray := sorry_proof
-  fromByteArray_toByteArray_other := sorry_proof
+--   toByteArray_size := sorry_proof
+--   fromByteArray_toByteArray := sorry_proof
+--   fromByteArray_toByteArray_other := sorry_proof
 
 
-/-- Index is `PlainDataType` via conversion from/to `Idx n`
+-- /-- Index is `PlainDataType` via conversion from/to `Idx n`
 
-**Instance diamond** This instance `instPlainDataTypeProd` is prefered over this one.
+-- **Instance diamond** This instance `instPlainDataTypeProd` is prefered over this one.
 
-This instance makes a diamond together with `instPlainDataTypeProd`. Using this instance is more computationally intensive when writting and reading from `DataArra` but it consumes less memory. The `instPlainDataTypeProd` is doing the exact opposite.
+-- This instance makes a diamond together with `instPlainDataTypeProd`. Using this instance is more computationally intensive when writting and reading from `DataArra` but it consumes less memory. The `instPlainDataTypeProd` is doing the exact opposite.
 
-Example: `Idx (2^4+1) × Idx (2^4-1)`
+-- Example: `Idx (2^4+1) × Idx (2^4-1)`
 
-As Product:
-  The type `Idx (2^4+1)` needs 5 bits.
-  The type `Idx (2^4-1)` needs 4 bits.
-  Thus `Idx (2^4+1) × Idx (2^4-1)` needs 9 bits, thus 2 bytes, as `instPlainDataTypeProd`
+-- As Product:
+--   The type `Idx (2^4+1)` needs 5 bits.
+--   The type `Idx (2^4-1)` needs 4 bits.
+--   Thus `Idx (2^4+1) × Idx (2^4-1)` needs 9 bits, thus 2 bytes, as `instPlainDataTypeProd`
 
-As Index:
-  `Idx (2^4+1) × Idx (2^4-1) ≈ Idx (2^8-1)`
-  The type `Idx (2^8-1)` needs 8 bits thus only a single byte as `instPlainDataTypeIndex`
+-- As Index:
+--   `Idx (2^4+1) × Idx (2^4-1) ≈ Idx (2^8-1)`
+--   The type `Idx (2^8-1)` needs 8 bits thus only a single byte as `instPlainDataTypeIndex`
 
--/
-instance (priority := low) instPlainDataTypeIndex  {α : Type} [Index α] : PlainDataType α where
-  btype :=
-    if h : (Index.size α) ≤ 256
-    then .inl (Index.bitType α h)
-    else .inr (Index.byteType α (by simp at h; apply h))
+-- -/
+-- instance (priority := low) instPlainDataTypeIndex  {α : Type} [Index α] : PlainDataType α where
+--   btype :=
+--     if h : (Index.size α) ≤ 256
+--     then .inl (Index.bitType α h)
+--     else .inr (Index.byteType α (by simp at h; apply h))
 
 -------------- Float -------------------------------------------------
 ----------------------------------------------------------------------