"""Closed contractive mu types -> finite constructor graphs -> certificates.
Input AST uses tuples: ('mu',name,body), ('var',name), ('arr',domain,result),
('rec',((label,type),...)), or ('base','Int'/'Bool'/'Top'). Record fields immutable.
No type inference, mutable cells, unguarded recursive type, or general isomorphism.
"""
from dataclasses import dataclass
from collections import deque
import json

def need(ok,msg):
 if not ok:raise ValueError(msg)
@dataclass(frozen=True)
class Node:
 tag:str
 children:tuple=()
@dataclass(frozen=True)
class Graph:
 nodes:tuple
 root:int

def compile_type(ast):
 """Iterative finite AST traversal. Linked scope lookup costs O(depth) per var.
 Alias-only cycles are rejected, including those in reachable field subtypes.
 """
 raw=[];todo=[];visits=0
 def allocate(t,env):
  i=len(raw);raw.append(None);todo.append((i,t,env));return i
 root=allocate(ast,None)
 while todo:
  i,t,env=todo.pop();visits+=1
  need(type(t) is tuple and t and type(t[0]) is str,'finite tuple type AST')
  if t[0]=='base':
   need(len(t)==2 and t[1] in ('Int','Bool','Top'),'known base type');raw[i]=Node(t[1])
  elif t[0]=='var':
   need(len(t)==2 and type(t[1]) is str and t[1],'variable name');cur=env
   while cur is not None and cur[0]!=t[1]:cur=cur[2]
   need(cur is not None,'unbound type variable');raw[i]=Node('alias',(cur[1],))
  elif t[0]=='mu':
   need(len(t)==3 and type(t[1]) is str and t[1],'mu binder');child=allocate(t[2],(t[1],i,env));raw[i]=Node('alias',(child,))
  elif t[0]=='arr':
   need(len(t)==3,'binary function type');a=allocate(t[1],env);b=allocate(t[2],env);raw[i]=Node('arr',(('domain',a),('result',b)))
  elif t[0]=='rec':
   need(len(t)==2 and type(t[1]) is tuple,'finite record field list');fields=t[1];labels=[]
   for f in fields:need(type(f) is tuple and len(f)==2 and type(f[0]) is str and f[0],'record field');labels.append(f[0])
   need(len(set(labels))==len(labels),'duplicate record label');children=[]
   for label,child in sorted(fields):children.append((label,allocate(child,env)))
   raw[i]=Node('rec',tuple(children))
  else:raise ValueError('unknown type syntax')
 heads={}
 for i in range(len(raw)):
  if i in heads:continue
  path=[];active=set();j=i
  while j not in heads and raw[j].tag=='alias':
   need(j not in active,'unguarded alias cycle');active.add(j);path.append(j);j=raw[j].children[0]
  h=heads.get(j,j);heads[j]=h
  for j in path:heads[j]=h
 constructors=[i for i,n in enumerate(raw) if n.tag!='alias'];renumber={i:j for j,i in enumerate(constructors)}
 nodes=tuple(Node(raw[i].tag,tuple((label,renumber[heads[child]])for label,child in raw[i].children))for i in constructors)
 return Graph(nodes,renumber[heads[root]]),dict(ast_occurrences=visits,raw_nodes=len(raw),constructor_nodes=len(nodes))

def validated(g):
 need(isinstance(g,Graph) and type(g.nodes) is tuple and type(g.root) is int and 0<=g.root<len(g.nodes),'rooted finite type graph')
 for n in g.nodes:
  need(isinstance(n,Node) and n.tag in ('Int','Bool','Top','arr','rec') and type(n.children) is tuple,'constructor node')
  for item in n.children:
   need(type(item) is tuple and len(item)==2 and type(item[0]) is str and item[0] and type(item[1]) is int and 0<=item[1]<len(g.nodes),'child edge')
  labels=[a for a,_ in n.children]
  need(len(set(labels))==len(labels),'unique graph fields')
  if n.tag in ('Int','Bool','Top'):need(not labels,'nullary base')
  if n.tag=='arr':need(labels==['domain','result'],'ordered arrow ports')
 return g

class Compare:
 def __init__(self,left,right):
  validated(left);validated(right);self.cut=len(left.nodes)
  self.nodes=left.nodes+tuple(Node(n.tag,tuple((label,j+self.cut)for label,j in n.children))for n in right.nodes)
  self.root=(left.root,right.root+self.cut)
  self.fields=tuple(dict(n.children) for n in self.nodes)
 def obligations(self,pair,mode):
  need(mode in ('equal','subtype'),'comparison mode');i,j=pair;n,m=self.nodes[i],self.nodes[j]
  if mode=='subtype' and m.tag=='Top':return [],None
  if n.tag!=m.tag:return [],dict(kind='constructor',left=n.tag,right=m.tag)
  if n.tag in ('Int','Bool','Top'):return [],None
  if n.tag=='arr':
   a,b=self.fields[i],self.fields[j]
   domain=(a['domain'],b['domain']) if mode=='equal' else (b['domain'],a['domain'])
   return [('domain',domain),('result',(a['result'],b['result']))],None
  a,b=self.fields[i],self.fields[j]
  if mode=='equal' and a.keys()!=b.keys():return [],dict(kind='field-set',left=list(a),right=list(b))
  missing=[label for label in b if label not in a]
  if missing:return [],dict(kind='missing-target-field',labels=missing)
  return [(label,(a[label],b[label]))for label in b],None
 def solve(self,mode):
  queue=deque([self.root]);parent={self.root:None};done=[];edge_count=0
  while queue:
   pair=queue.popleft();deps,error=self.obligations(pair,mode);done.append(pair)
   if error is not None:
    path=[];cur=pair
    while parent[cur] is not None:
     before,label=parent[cur];path.append(label);cur=before
    return dict(passed=False,mode=mode,path=path[::-1],conflict_pair=pair,conflict=error,visited=done,edges=edge_count)
   for label,child in deps:
    edge_count+=1
    if child not in parent:parent[child]=(pair,label);queue.append(child)
  return dict(passed=True,mode=mode,pairs=done,edges=edge_count)
 def verify(self,result):
  mode=result['mode'];need(mode in ('equal','subtype') and type(result['passed']) is bool,'mode/verdict')
  if result['passed']:
   pairs=result['pairs'];allowed=set()
   for pair in pairs:
    need(type(pair) in (tuple,list) and len(pair)==2 and all(type(x)is int and 0<=x<len(self.nodes)for x in pair),'certificate node pair');allowed.add(tuple(pair))
   need(self.root in allowed,'root obligation missing')
   for pair in allowed:
    deps,error=self.obligations(pair,mode);need(error is None and all(child in allowed for _,child in deps),'certificate not closed')
  else:
   cur=self.root
   for label in result['path']:
    deps,error=self.obligations(cur,mode);need(error is None,'path continues after conflict');choices=dict(deps);need(label in choices,'invalid obligation selector');cur=choices[label]
   _,error=self.obligations(cur,mode)
   need(error is not None and tuple(result['conflict_pair'])==cur and result['conflict']==error,'path has no claimed conflict')
  return True

I=('base','Int');B=('base','Bool');TOP=('base','Top')
def var(n):return ('var',n)
def rec(**fields):return ('rec',tuple(fields.items()))
def arr(a,b):return ('arr',a,b)
def mu(x,body):return ('mu',x,body)
def examples():
 s=mu('X',rec(next=var('X'),get=arr(TOP,I),tag=B))
 s2=mu('Y',rec(next=rec(next=var('Y'),get=arr(TOP,I),tag=B),get=arr(TOP,I),tag=B))
 t=mu('Y',rec(next=var('Y'),get=arr(I,TOP)))
 bad=mu('X',rec(next=var('X'),get=arr(B,I),tag=B))
 deep=mu('Y',rec(next=rec(next=var('Y'),get=arr(TOP,I),tag=I),get=arr(TOP,I),tag=B))
 asts=dict(S=s,S2=s2,T=t,Bad=bad,Deep=deep);graphs={};stats={}
 for name,ast in asts.items():graphs[name],stats[name]=compile_type(ast)
 output={}
 for a,b,mode,wanted in [('S','S2','equal',True),('S','T','equal',False),('S','T','subtype',True),('T','S','subtype',False),('Bad','T','subtype',False),('S','Deep','equal',False)]:
  compare=Compare(graphs[a],graphs[b]);answer=compare.solve(mode);compare.verify(answer);need(answer['passed']==wanted,'example judgment');output[a+' '+mode+' '+b]=answer
 # Reusing a variable spelling at a nested binder respects lexical scope.
 shadow=mu('X',arr(mu('X',rec(next=var('X'))),var('X')))
 renamed=mu('outer',arr(mu('inner',rec(next=var('inner'))),var('outer')))
 g,_=compile_type(shadow);h,_=compile_type(renamed);c=Compare(g,h);a=c.solve('equal');need(a['passed'],'alpha shadowing');c.verify(a)
 rejected=[]
 for label,ast in [('unguarded',mu('X',var('X'))),('nested aliases',mu('X',mu('Y',var('X')))),('bad child',rec(next=mu('Y',var('Y')))),('free variable',var('X')),('duplicate fields',('rec',(('x',I),('x',B))))]:
  try:compile_type(ast)
  except ValueError:rejected.append(label)
  else:raise RuntimeError('malformed type accepted')
 return dict(status='PASS',stats=stats,graphs={name:dict(root=g.root,nodes=[dict(tag=n.tag,children=n.children)for n in g.nodes])for name,g in graphs.items()},judgments=output,alpha_shadowing=True,rejected=rejected)
def regressions():
 rejected=[]
 def reject(label,fn):
  try:fn()
  except ValueError:rejected.append(label);return
  raise RuntimeError('expected rejection '+label)
 for label,g in [('empty graph',Graph((),0)),('bad root',Graph((Node('Int'),),1)),('dangling edge',Graph((Node('rec',(('x',8),)),),0)),('duplicate field',Graph((Node('rec',(('x',0),('x',0))),),0)),('bad arrow port',Graph((Node('arr',(('x',0),('result',0))),),0)),('base with child',Graph((Node('Int',(('x',0),)),),0))]:reject(label,lambda g=g:validated(g))
 a,_=compile_type(mu('X',rec(next=var('X'),tag=B)));b,_=compile_type(mu('Y',rec(next=var('Y'),tag=I)));c=Compare(a,b)
 for mode in ('equal','subtype'):
  first=c.solve(mode);second=c.solve(mode);need(not first['passed'] and first==second,'failed cycle assumptions must not become cached success');c.verify(first)
  bad=first.copy();bad['conflict_pair']=(-1,-1);reject('false conflict '+mode,lambda bad=bad:c.verify(bad))
 good=Compare(a,a);proof=good.solve('equal');good.verify(proof)
 bad=proof.copy();bad['pairs']=proof['pairs'][:1];reject('incomplete positive certificate',lambda:good.verify(bad))
 # One unknown recursion spelling cannot alter another binder's identity.
 vacuous,_=compile_type(mu('X',mu('Y',I)));need(vacuous==Graph((Node('Int'),),0),'vacuous binder compression')
 changed=mu('X',rec(next=var('X'),get=arr(TOP,B),tag=B));target=mu('Y',rec(next=var('Y'),get=arr(I,TOP)));narrow=mu('Y',rec(next=var('Y'),get=arr(I,I)))
 gx,_=compile_type(changed);gt,_=compile_type(target);gn,_=compile_type(narrow)
 wide=Compare(gx,gt);aw=wide.solve('subtype');wide.verify(aw);need(aw['passed'],'Bool result allowed by Top target')
 strict=Compare(gx,gn);an=strict.solve('subtype');strict.verify(an);need(not an['passed'] and an['path']==['get','result'],'Bool result rejected by Int target')
 return dict(rejections=rejected,query_local_cache=True,vacuous_binders=True,result_migration=dict(wide_target=aw,narrow_target=an))
if __name__=='__main__':
 result=examples();result['checks']=regressions();print(json.dumps(result,ensure_ascii=False,indent=2))