lovely-error

homogenise the repr of generics / dyn Trait / (*mut/*const/&/&mut) dyn Trait
 
abstract value = (generic / dyn Trait / (*mut/*const/&/&mut) dyn Trait) value;
abstracted function = (takes at least one arg that is abstract or returns abstract value) and the fun is nonspecialisible;
at the 'lower level' abstract args are represented by wide pointers;
devise some opt passes to 'degeneralise' uses of abstracted funs at some sites;
specifically: 
1. uses within an 'inner world' (libs with visible impl)
2. cross bondry code must be generated to adhere to the wide pointer repr tho

lovely-error

inductive NatNum : Type | zero | succ (n:NatNum)


def add (a b:NatNum): NatNum := 
  match a with | .zero => b | .succ n => .succ (add n b)


#eval (add (.succ (.succ .zero)) (.succ (.succ .zero)))

#check add.induct

lovely-error

#![feature(decl_macro)]

trait MemLayout where Self:Sized {
    // size, excluding trailing padding
    fn size() -> usize {
        core::mem::size_of::<Self>()
    }
    /// highest alignment among the members 
    /// of the product
    fn alignment() -> usize;

lovely-error

import Mathlib
set_option pp.proofs true in
example
  {V:Real}{n1:Int}{r1 : (2:Real) = V}
  {eq1:@HEq { i:Int // n1 = i } ⟨n1, rfl⟩ { i:Int // V = ↑i } ⟨(2:Int), Eq.symm r1⟩ }
: n1 = 2 ∧ (HEq (rfl (a:=n1)) (Eq.symm r1))
:= by
  -- cases eq1
  admit

lovely-error

macro "rwi" pat:term "=>" new:term ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ])

macro "rwi" pat:term "=>" new:term "at" loc:Lean.Parser.Tactic.locationHyp ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ] at $loc)

lovely-error

import Mathlib
import Lean.Meta

macro "rwi" pat:term "=>" new:term ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ])

macro "rwi" pat:term "=>" new:term "at" loc:Lean.Parser.Tactic.locationHyp ":=" prf:term : tactic =>
  `(tactic| rewrite [let _eq : $pat = $new := $prf ; _eq ] at $loc)

def wmap : Type _ -> Type _ -> Type _ | A, B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i

lovely-error

module REG (CLK, WE, D, O);

  parameter BITWIDTH = 1;
  parameter [BITWIDTH-1:0] INIT = '0;

  input CLK;
  input WE;
  input [BITWIDTH-1:0] D;
  output [BITWIDTH-1:0] O;

lovely-error

use core::marker::PhantomData;
use core::mem::ManuallyDrop;

#[repr(C)] #[derive(Copy, Clone)]
union TaggedPtr64Repr<T> {
    num: u64,
    tag: ManuallyDrop<T>,
}

lovely-error

import Mathlib

example (p1: (V:Rat) = I * R)(vnz: Not (V = 0))(rnz: Not (R = 0)) : R = (I *  R ^ 2) / V := by
  let target := p1
  let s1 : V = I * R <-> V / V = I * R / V := by 
    exact (iff_true_right (congrFun (congrArg HDiv.hDiv p1) V)).mpr p1
  rw [s1] at target
  let v_on_v_one: V / V = 1 := by
    exact (div_eq_one_iff_eq vnz).mpr rfl
  rw [v_on_v_one] at target

lovely-error

#![feature(decl_macro)]
macro d($ptr:expr) { unsafe { *$ptr } }
macro p($val:expr) { &raw mut $val }
macro pc($val:expr) { &raw const $val }