base.egi

--
--
-- Base
--
--

-- | Type class for equality
class Eq a where
  (==) (x: a) (y: a) : Bool
  (/=) (x: a) (y: a) : Bool

-- | Eq instances for basic types
instance Eq Integer where
  (==) x y := x = y
  (/=) x y := not (x == y)

instance Eq Float where
  (==) x y := x = y
  (/=) x y := not (x == y)

instance Eq String where
  (==) x y := x = y
  (/=) x y := not (x == y)

instance Eq Bool where
  (==) x y := x = y
  (/=) x y := not (x == y)

instance Eq Char where
  (==) x y := x = y
  (/=) x y := not (x == y)

instance {Eq a} Eq (Tensor a) where
  (==) t1 t2 := t1 = t2
  (/=) t1 t2 := not (t1 == t2)

def eq {Eq a} : Matcher a :=
  matcher
    | #$val as () with
      | $tgt -> if val == tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

-- The primitive matchers are eq's body inlined at each concrete type.
-- Matcher types are rigid (two different Matcher types never unify), so a
-- polymorphic matcher value cannot be specialized by annotation: `def
-- integer : Matcher Integer := eq` does not type-check, and an unannotated
-- alias `def integer := eq` would keep eq's polymorphic scheme, which a
-- concrete hole (e.g. `as (integer, ...)` at an Integer hole) rejects just
-- as it rejects `something`.  A concrete matcher literal instead derives
-- its capability at the annotated type (T-MATCHER in checking mode).
-- The #$val arm uses the built-in equality `=` (same convention as
-- sortedList's #$val arm); for the base types it coincides with ==.

def bool : Matcher Bool :=
  matcher
    | #$val as () with
      | $tgt -> if val = tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

def char : Matcher Char :=
  matcher
    | #$val as () with
      | $tgt -> if val = tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

def integer : Matcher Integer :=
  matcher
    | #$val as () with
      | $tgt -> if val = tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

def float : Matcher Float :=
  matcher
    | #$val as () with
      | $tgt -> if val = tgt then [()] else []
    | $ as something with
      | $tgt -> [tgt]

-- Additive hierarchy
class AddSemigroup a where
  (+) (x: a) (y: a) : a

class AddMonoid a extends AddSemigroup a where
  zero : a

class AddGroup a extends AddMonoid a where
  neg (x: a) : a

-- Multiplicative hierarchy
class MulSemigroup a where
  (*) (x: a) (y: a) : a

class MulMonoid a extends MulSemigroup a where
  one : a

class MulGroup a extends MulMonoid a where
  inv (x: a) : a

-- Composite structures
class Ring a extends AddGroup a, MulMonoid a
class Field a extends Ring a, MulGroup a

class GCDDomain a extends Ring a where
  gcd (x: a) (y: a) : a

class EuclideanDomain a extends GCDDomain a where
  divMod (x: a) (y: a) : (a, a)

-- Derived operators
def (-) {AddGroup a} (x: a) (y: a) : a := x + neg y
def (/) {Field a} (x: a) (y: a) : a := x * inv y
def modulo {EuclideanDomain a} (x: a) (y: a) : a := snd (divMod x y)
def quotient {EuclideanDomain a} (x: a) (y: a) : a := fst (divMod x y)

-- MathValue instances
instance AddSemigroup MathValue where
  (+) x y := plusForMathValue x y

instance AddMonoid MathValue where
  zero := 0

instance AddGroup MathValue where
  neg x := minusForMathValue 0 x

instance MulSemigroup MathValue where
  (*) x y := multForMathValue x y

instance MulMonoid MathValue where
  one := 1

instance MulGroup MathValue where
  inv x := divForMathValue 1 x

instance Ring MathValue
instance Field MathValue

instance GCDDomain MathValue where
  gcd x y := gcdForMathValue x y

instance EuclideanDomain MathValue where
  divMod x y := (i.quotient x y, i.modulo x y)

-- Float instances
instance AddSemigroup Float where
  (+) x y := f.+ x y

instance AddMonoid Float where
  zero := 0.0

instance AddGroup Float where
  neg x := f.- 0.0 x

instance MulSemigroup Float where
  (*) x y := f.* x y

instance MulMonoid Float where
  one := 1.0

instance MulGroup Float where
  inv x := f./ 1.0 x

instance Ring Float
instance Field Float

--
-- CAS type widening / narrowing
--
-- After Phase C, both `Embed` and the `coerceTo*` helper functions have been
-- removed in favor of the unified `reshape` mechanism: the type checker
-- inserts a `TIReshape T` node whenever a `def x : T := e` annotation is
-- encountered (where T is a concrete CAS scalar — Integer, Factor, Frac _,
-- Poly _ _, Term _ _). At runtime, `casReshapeAs T v` structurally rewrites
-- the CAS value to fit T (collapsing Frac with denom=1 to Integer, lifting
-- Integer into Poly form, etc.).
--
-- Subtype unification handles the static side (Integer ⊂ Frac Integer ⊂
-- Poly Integer [..] ⊂ Poly (Frac Integer) [..] ⊂ Frac (Poly Integer [..])).
-- Together this gives "trust the annotation" semantics:
--
--   def n : Integer            := someExpr   -- reshapes runtime to Integer
--   def p : Poly Integer [x,y] := someExpr   -- reshapes to specific atom set
--   def t : Term MathValue [..]:= someExpr   -- reshapes to single-term form
--

--
-- Rule application combinators (Phase 7.5 helper)
--
-- `applyRules` runs each rule once, left-to-right. `iterateRules` runs
-- the chain repeatedly until the value stops changing (fixed point).
-- Users hand-build the rule list from `rule.<name>` references.
--

def applyRules {a} (rules : [a -> a]) (v : a) : a :=
  foldl (\acc r -> r acc) v rules

def iterateRules {Eq a} (rules : [a -> a]) (v : a) : a :=
  let v' := applyRules rules v
   in if v == v' then v else iterateRules rules v'

--
-- Utility
--

def id {a} (x: a) : a := x

def fst {a, b} (x: a, _: b) : a := x
def snd {a, b} (_: a, y: b) : b := y

def ($) {a, b} (f: a -> b) (x: a) : b := f x

def compose {a, b, c} (f: a -> b) (g: b -> c) : a -> c := \x -> g (f x)

def flip {a, b, c} (fn: a -> b -> c) : b -> a -> c := \x y -> fn y x

def eqAs {a} (m: MatcherSlot a a) (x: a) (y: a) : Bool :=
  match x as m with
    | #y -> True
    | _ -> False

def curry {a, b, c} (f: (a, b) -> c) (x: a) (y: b) : c := f (x, y)
def uncurry {a, b, c} (f: a -> b -> c) (x: a, y: b) : c := f x y

--
-- Boolean
--

def (&&) (b1: Bool) (b2: Bool) : Bool := if b1 then b2 else False
def (||) (b1: Bool) (b2: Bool) : Bool := if b1 then True else b2

def not (b: Bool) : Bool := if b then False else True

--
-- Unordered Pair
--

def unorderedPair {a} (m: MatcherSlot a a) : Matcher (a, a) :=
  matcher
    | ($, $) as (m, m) with
      | ($x, $y) -> [(x, y), (y, x)]
    | $ as something with
      | $tgt -> [tgt]