Teoria do tipo dependente de Frozenset do Python com orientação familiar

e1 = 42
e2 = lambda: 42
e3 = {() : 42}

def myrule(foo : Judge1, bar : Judge2) -> Judge3: ...

type Env = tuple(object,...)
type Ctx = frozenset(Env) # a set of environments
type InCtx(T) = dict(Env, T)  # a family of stuff indexed by environments

def is_ctx(ctx : Ctx) -> bool:
    assert isinstance(ctx, frozenset)
    assert len(ctx) >= 1
    return isinstance(ctx, frozenset) and all(isinstance(env, tuple) for env in ctx) # same length also

# empty context
emp : Ctx = {()} # () |-

def lweak(T)(ctx : Ctx, x : InCtx(T)) -> InCtx(T):
    """
    G |- yada     ctx |-
    --------------------- leftweak
    ctx, G |- yada 
    """
    return {env + env0  : v for env0,v in x.items() for env in ctx}

def rweak(T)(ctx : Ctx, x : InCtx(T)) -> InCtx(T):
    """
    G |- yada     ctx |-
    --------------------- rightweak
    G, ctx |- yada 
    """
    return {env0 + env  : v for env0,v in x.items() for env in ctx}

def proj_ctx(T)(x : InCtx(T)) -> Ctx:
    """
       G |- yada
    ------------ proj
       G |-

    Not usually a rule. But ought to be admissible.
    That the context is a proectable piece out of the judgement is a central point in fiber bundle stuff
    Jacobs book
    """
    return frozenset(x.keys())

# more general thinning


type Thin = list(bool) # Thinnings describe how to extract a subsequence from another. True means takse, False means don't take
def thin(t : list(bool), env : Env) -> Env:
    assert len(t) == len(env)
    return tuple(e for e, b in zip(env, t) if not b)

"""
  G |- yada      G 

def weak(T)(newctx : Ctx, t : list(bool), x : InCtx(T)) -> InCtx(T):
    return { x(thin(t, env)) for env in newctx}

type PreType = frozenset(object) # I will often be too lazy to wrap set in frozenset. frozenset looks like shit too.
# There is no "Type" really. only Family. Family is Type
type Family = dict(Env, PreType)

"""
------------------- BoolType
   () |- Bool Type
"""
Bool : Family = {() : {True, False}}
Unit : Family = {() : {()}}
Void : Family = {() : {}}
RGB : Family = {() : {"R", "G", "B"}}
def Fin(n : int) -> Family:
    # This is meta parametrized (python function), since I can't make a dictionary of all integers
    return {() : frozenset(range(n))}

"""
A family with a nontrivial context
x : Bool |- (if x then Bool else Unit) Type
"""
ifUnitBool : Family = {(False,) : {()}, (True,) : {True, False}}

"""
   G |-
---------
  G |- Bool Type

Is an admissible rule
"""
def Bool1(ctx : Ctx) -> Family:
    return rweak(ctx, Bool)

"""
    G |- A Type
------------------- extend_ctx
   G, x : A |- 
"""
def extend_ctx(A : Family) -> Ctx:
    return frozenset({env + (x,)  for env, As in A.items() for x in As})

ctxBool : Ctx = extend_ctx(Bool)  # x : Bool |-

assert is_ctx(ctxBool)
ctxBool

Bool_Unit : Family = rweak(ctxBool, Unit)   # x : Bool |- Unit Type
ctxBoolUnit : Ctx = extend_ctx(Bool_Unit)   # x : Bool, y : Unit |-
ctxBoolUnit

type Section = InCtx(object) # Section is "term". Basically sections are functions.

# empty context / 0-arity "functions" are constants / values
tt : Section = {() : ()}
true : Section = {() : True}
false : Section = {() : False}

"""

G |- t : A       G |- e : A    G |- c : Bool
--------------------------------------------
   G |- if c then t else e : A

"""

def ite(c : Section, t : Section, e : Section) -> Section:
    assert proj_ctx(t) == proj_ctx(e) == proj_ctx(c)
    return {env : t(env) if c(env) else e(env) for env in proj_ctx(t)}

"""
     G |- A type
-------------------
  G, x : A |- x : A
"""

def id(A : Family) -> Section:
   # schema for identity function. Not a Pi internalized one.
   return {env + (x,) : x for env, As in A.items() for x in As}

def Pair(A : Family, B : Family) -> Family:
    assert proj_ctx(A) == proj_ctx(B)
    return { ctx : { (a,b)  for a in A for b in B(ctx)} for ctx,A in A.items()}

Pair(Bool, Bool)

"""
        G |- Pair A B 
  ---------------------
     G, x : Pair A B |- fst(a) 

"""

def pair(a : Section, b : Section) -> Section:
    assert proj_ctx(a) == proj_ctx(b)
    return {env : (a(env), b(env)) for env in proj_ctx(a)}
def fst(AB : Family) -> Section:
    return {env + ((a,b),) : a for env, ABs in AB.items() for (a,b) in ABs}
def snd(AB : Family) -> Section:
    return {env + ((a,b),) : b for env, ABs in AB.items() for (a,b) in ABs}

snd(Pair(Unit, Bool))

def Sigma(A : Family, B : Family) -> Family:
    return {ctx : { (a, b) for a in As for b in B(ctx + (a,))}  for ctx, As in A.items()}
Sigma(Bool, ifUnitBool)

import itertools
from frozendict import frozendict
def Pi(A : Family, B : Family) -> Family:
    assert proj_ctx(A) == {ctx(1:) for ctx in proj_ctx(B)}
    A = {k : list(v) for k,v in A.items()}
    return { ctx : {frozendict({a : b for a,b in zip(As, bvs)}) for bvs in itertools.product(*(B(ctx + (a,)) for a in As))}  for ctx, As in A.items() }
Pi(Bool, ifUnitBool)

"""
 G, x : A |- t : B
 ----------------------
   G |- lam x, t : Pi A B

"""

def lam(body : Family) -> Section:
    return {subenv :  { env(-1) : body(env) for env in envs} for subenv, envs in itertools.groupby(sorted(body.keys()), key=lambda e: e(:-1))}

lam(id(Bool)) # |- lam x : Bool, x 
lam(ite(id(Bool), lweak(ctxBool, false), lweak(ctxBool, true))) # |- lam x : Bool, if x then false else true

"""
G |- f      G |- arg 
-------------------------------
    G |- apply f arg
"""

def apply(f : Section, arg : Section) -> Section:
    assert proj_ctx(f) == proj_ctx(arg)
    return {env : f(env)(arg(env)) for env in proj_ctx(f)}

assert apply(lam(id(Bool)), true) == true
assert apply(lam(ite(id(Bool), lweak(ctxBool, false), lweak(ctxBool, true))), false) == true 

def Id(A : Family) -> Family:
    return { ctx + (x,y) : {"refl"} if x == y else {} for ctx, As in A.items() for x in As for y in As}
Id(Bool)
# Pi(leftweak(_, Bool), Id(Bool))

"""
  G, x : A |- 
 --------------
  G |- A type
"""
def proj_family(F : Ctx) -> Family:
    return {subctx : {ctx(-1) for ctx in ctxs}  for subctx, ctxs in itertools.groupby(sorted(F), lambda ctx: ctx(:-1))}
proj_family()


```python
42
{() : 42}

def dictthunk(v):
    return {() : v}
dictthunk(42)

def Arr(A : Family, B : Family) -> Family:
    assert proj_ctx(A) == proj_ctx(B)
    return {ctx : {    }  for ctx,A in A.items()}

type CtxMap = dict(Env, Env)

def comp(f : CtxMap, g : CtxMap) -> CtxMap:
    return {env1 : f(env2) for env1, env2 in g.items()}
def idmap(ctx : Ctx) -> CtxMap:
    return {env : env for env in ctx}
def inctx_map(x : InCtx(object), t : CtxMap) -> InCtx(object):
    return {env1 : x(env2) for env1, env2 in t.items()}

import itertools
def Pi(T : Family) -> Family:
    return {subenv : {itertools.product(* )e for e,v in f} for subenv, f in itertools.groupby(
        sorted(T.items()),
        key=lambda kv: kv(0)(:-1),
    )}
Pi(UnitBool)

    # assert A == { {c(-1) for c in fullctx}  for ctx, fullctx itertools.groupby(proj_ctx(B), key=lambda ctx: ctx(:-1))}

"""
 Gamma  |-
 ------------------
 Gamma |- Bool Type
"""



def Bool(ctx : Ctx):
    assert is_ctx(ctx)
    return {env : frozenset((True, False)) for env in ctx}
def Unit(ctx : Ctx):
    assert is_ctx(ctx)
    return {env : frozenset((())) for env in ctx}
Bool = {() : frozenset((True, False))}
Unit = {() : frozenset((()))}
def wrap0(T0 : PreType) -> Family:
    return {() : T0}




type Section = dict(Env, object)

def true(ctx : Ctx) -> Section:
    assert is_ctx(ctx)
    return {env : True for env in ctx}

true1 = {() : True}
false1 = {() : False}

def false(ctx : Ctx) -> Section:
    assert is_ctx(ctx)
    return {env : False for env in ctx}

def tt(ctx : Ctx) -> Section:
    assert is_ctx(ctx)
    return {env : () for env in ctx}


# Do we keep t and T coupled or no?
# Perhaps this is a church vs curry kind of thing.
# G |- t : T
true1 = {() : (True, {True, False})}


import itertools
# non dependent product
def Tuple(T1 : Family, T2 : Family) -> Family:
    assert proj_ctx(T1) == proj_ctx(T2)
    return {env : {frozenset(itertools.product(s1, T2(env)))} for env, s1 in T1.items()}
"""
It is however somewhat annoying to manually reconcile the contexts


"""
#def Arr()
"""
G, x : A |- B
------------
G |- Pi x : A. B
"""

def Pi(T : Family) -> Family:
    # no, it should be a frozenset of dicts
    return {subenv : {e(-1) : v for e,v in f} for subenv, f in itertools.groupby(
        T.items(),
        key=lambda kv: kv(0)(:-1),
    )}
def Sigma(T : Family) -> Family:
    # Can you infer family 1 or no?
    return {subenv : frozenset(( (e(-1), v) for e,v in f )) for subenv, f in itertools.groupby(
        T.items(),
        key=lambda kv: kv(0)(:-1),
    )}

def Sigma2(T : Family, T2 :Family) -> Family:
    # not inferred version instead checks that is compatible
    # common context -> (set i, {i -> set j}) -> const -> (i, j)
    assert proj_ctx(T) == { env(:-1) for env in proj_ctx(T2)}
    # todo

def thunk(v):
    return lambda: v
def dethunk(t):
    return t()
e3 = thunk(e1) # another way of writing e2

type Type = frozenset(tuple(object, frozenset(int)))
# basically all taints are possible? as long as there is a pathway from the input type to final type
type Type = frozenset(tuple(int, object)) # type in context?
type CtxType = frozenset(tuple(int, frozenset(int), object)) # type in context with taint
# ((Gamma |- T)) = CtxType
type IsType = ...
type HasType = ...
type Family = HasType # (G |- A type) means A is a family of sets indexed by iterated domain G
type Family = dict(object, Family) | frozenset(object)  # trie of families. But should be equal length across all branches
type Ctx = tuple(object, ...)
type Family = dict(Ctx, frozenset(object))
type Family = frozenset(tuple(Ctx, frozenset(object))) # dicts are just functional sets of tuples

# you kind of want to know where the int cutoff is. Either as a Type() wrapper. Or perhaps as a just carried int

type Ctx = dict(object, Ctx) | None
type Family = tuple(Ctx, int) # how deep to put the turnsilte. Where to consider G vs A. G |- A. yes, Ctx and Family are very similar.

type Type = tuple(Ctx, typing.Literal(0)) # Type in empty context.
# kind of Type is what you might get from indexing Family.
type Type = Ctx # The remainder.

type Thinning = dict(object, Thinning) | None | tuple(None, Thinning) # How to interpolate into a new context.

def is_thin(bigctx : Ctx, littlectx : Ctx, thin : list(bool)) -> bool: ...
def subctx(bigctx : Ctx, littlectx : Ctx) -> list(bool) | None:
    # recurse through bihctx and littlectx.
    # see if returned thinnings match
    # see if current key space also matches?
    ...

type ctxobject0 = dict(object, ctxobject0) | object # since dict is object, not strictly speaking useful, but gets at something
type ctxobject = tuple(int, ctxobject0)
#type Ctx = tuple(int, ctxobject) # a projection off of an object in context. Kind of done lazily. No make it None at end

# a functor over contexts?
def ctxobjectmap(ctx : ctxobject, f):
    def worker(m, data):
        if m == 0:
            return f(data)
        else:
            return {k : worker(m-1, v) for k, v in data.items()}
    return worker(ctx(0), ctx(1))




def Thin(): ...
def Weak(): ...
    # weakening just in the front is easier

Bool0 = (0, {True: None, False: None})
Unit0 = 

def Bool(ctx : Ctx) -> Family:
    ctx.map(lambda x : {})


def Pi(B : Family) -> Family:
    nctx, data = B
    assert nctx > 0
    return (nctx-1, data)
    # group by context.
    #return {(ctx(1:),   for ctx, B in f}
#{True : }


from itertools import chain, combinations

def powerset(iterable):
    s = list(iterable)
    return chain.from_iterable(combinations(s, r) for r in range(len(s)+1))

def Void(ctx : int) -> Type:
    return frozenset()

def Unit(ctx : int) -> Type:
    return frozenset({((), ) for taint in powerset(range(ctx))})
# in empty context, Unit(0) ~ {()}

type Ctx = int

# the taint and the set are basically uncoupled.
# Except once you start talking about about functions
# twisted product? 
def proj(T : Type) -> Ctx:
    ...


def Arr(ctx : Ctx, T1 : Type, T2 : Type) -> Type: ...

type Term = str
Bool0 : frozenset(Term) = {"True", "False"}
Unit0 : frozenset(Term) = {"()"}
Type0 = {"Bool", "Unit"}

type Code = str
def El(c : Code):
    assert c in Type
    return eval(c)

@dataclass(frozen=True)
class Code():
    code : str
    def __add__(self, other):
        if not isinstance(other, Code):
            other = quote(other)
        return Code(self.code + " + " + other.code)
    def __radd__(self, other):
        if not isinstance(other, Code):
            other = quote(other)
        return Code(other.code + " + " + self.code)
    def __mul__(self, other):
        if not isinstance(other, Code):
            other = quote(other)
        return Code(self.code + " * " + other.code)
    def __call__(self, *args):
        args = (arg if isinstance(arg, Code) else quote(arg) for arg in args)
        return Code(self.code + "(" + ", ".join(arg.code for arg in args) + ")")

def quote(x): # is quote really the right word? Reify?
    return Code(repr(x))


def quote_lam(f, n):
    names = (f"x{i}" for i in range(n))
    body = f(*(Code(name) for name in names))
    return Code("lambda " + ", ".join(names) + ": " + body.code)
# I could discover n in an error loop. Cheeky. Or maybe inspect can determine?

def quote_lam(f):
    names = inspect.signature(f).parameters.keys()
    body = f(*(Code(name) for name in names))
    return Code("lambda " + ", ".join(names) + ": " + body.code)
# I could discover n in an error loop. Cheeky. Or maybe inspect can determine?

def quote(x):
    if isinstance(x, Code):
        return Code(repr(x))
    elif callable(x):
        return quote_lam(x)
    else:
        return Code(repr(x))


#quote_lam(lambda x,y: x, 2)
quote_lam(lambda x,y: x)

quote("hello")
quote(lambda x,y: x + 3 + 4)

assert quote(lambda x,y: 3 + 4 + x) == Code("lambda x, y: 7 + x") # a little normalization
assert quote(lambda x : (1,3,4) + (4,5,6) + x) == Code("lambda x: (1, 3, 4, 4, 5, 6) + x")

def pow(x, n):
    if n == 0:
        return 1
    elif n == 1:
        return x
    else:
        return x * pow(x, n - 1)

assert quote(Code("3")) == Code("Code(code="3")")
quote(lambda x: pow(x, 3))