#!/usr/bin/env python3
"""Typed finite algebraic patterns, usefulness witnesses, decision trees and
acyclic backtracking bytecode. Standard library, offline, stdout JSON only.
Call validate_rows once before compilation. Inputs are already evaluated finite
Bool/List trees of the declared types. Guards are pure total nonempty_xs only.
Explicit checks remain active under python -O. No full programming-language
exception, divergence, lazy-value or dependent-type semantics are claimed.
"""
from itertools import product
from collections import Counter
import json,random

def require(x,s):
 if not x:raise ValueError(s)
def check(x,s):
 if not x:raise AssertionError(s)
W=('_',)
def V(x):return ('var',x)
def C(t,*ps):return ('con',t,tuple(ps))
def O(p,q):return ('or',p,q)
def value(t,*xs):return (t,tuple(xs))
SIG={'Bool':(('F',()),('T',())), 'List':(('Nil',()),('Cons',('Bool','List')))}
CTOR={c:(ty,fields) for ty,cs in SIG.items() for c,fields in cs}
DEFAULT={'Bool':value('F'),'List':value('Nil')}

def valid_value(v,ty):
 require(type(v) is tuple and len(v)==2 and v[0] in CTOR and type(v[1]) is tuple,'value node')
 result,fields=CTOR[v[0]];require(result==ty and len(fields)==len(v[1]),'value type/arity')
 for child,t in zip(v[1],fields):valid_value(child,t)

def pattern_vars(p,ty):
 if p==W:return {}
 if p[0]=='var':require(isinstance(p[1],str) and bool(p[1]),'variable name');return {p[1]:ty}
 if p[0]=='or':
  a=pattern_vars(p[1],ty);b=pattern_vars(p[2],ty);require(a==b,'or arms have identical typed binders');return a
 require(p[0]=='con' and p[1] in CTOR,'constructor pattern')
 result,fields=CTOR[p[1]];require(result==ty and len(fields)==len(p[2]),'pattern type/arity');names={}
 for child,t in zip(p[2],fields):
  ns=pattern_vars(child,t);require(not names.keys()&ns.keys(),'linear pattern');names.update(ns)
 return names

def validate_rows(rows,types):
 for row in rows:
  require(len(row['patterns'])==len(types),'row width');names={}
  for p,t in zip(row['patterns'],types):
   ns=pattern_vars(p,t);require(not names.keys()&ns.keys(),'linear row');names.update(ns)
  require(row.get('guard') in (None,'nonempty_xs'),'known total guard')
  if row.get('guard'):require(names.get('xs')=='List','guard interface')
  row['_binders']=tuple(sorted(names))
 for ty in SIG:valid_value(DEFAULT[ty],ty)

def match_pattern(p,v):
 if p==W:return {}
 if p[0]=='var':return {p[1]:v}
 if p[0]=='or':
  left=match_pattern(p[1],v)
  return left if left is not None else match_pattern(p[2],v)
 if p[1]!=v[0]:return None
 env={}
 for q,w in zip(p[2],v[1]):
  got=match_pattern(q,w)
  if got is None:return None
  env.update(got)
 return env

def guard_ok(name,env):return name is None or env['xs'][0]=='Cons'
def source(rows,vs):
 for row in rows:
  env={}
  for p,v in zip(row['patterns'],vs):
   got=match_pattern(p,v)
   if got is None:break
   env.update(got)
  else:
   if guard_ok(row.get('guard'),env):return row['action'],env
 return None

def expand(p):
 # One accumulator for each contiguous or tree: no repeated prefix copies.
 out=[];todo=[p]
 while todo:
  q=todo.pop()
  if q[0]=='or':todo.extend((q[2],q[1]))
  elif q[0]=='con':
   for xs in product(*(expand(child) for child in q[2])):out.append(C(q[1],*xs))
  else:out.append(q)
 return out
def expanded_vectors(ps):return [tuple(x) for x in product(*(expand(p) for p in ps))]
def erase(p):
 if p[0]=='var':return W
 if p[0]=='con':return C(p[1],*(erase(q) for q in p[2]))
 require(p[0]!='or','erase after expansion');return p

def specialize(P,c):
 arity=len(CTOR[c][1]);out=[]
 for ps in P:
  if ps[0]==W:out.append((W,)*arity+ps[1:])
  elif ps[0][1]==c:out.append(ps[0][2]+ps[1:])
 return out
def default_matrix(P):return [ps[1:] for ps in P if ps[0]==W]
def instantiate(p,ty):
 return DEFAULT[ty] if p==W else value(p[1],*(instantiate(q,t) for q,t in zip(p[2],CTOR[p[1]][1])))
def witness_core(P,q,types,stats):
 stats['calls']+=1;stats['matrix_cells']+=sum(map(len,P));stats['query_cells']+=len(q)
 if not P:return tuple(instantiate(p,t) for p,t in zip(q,types))
 if not q:return None
 if q[0]!=W:
  c=q[0][1];fields=CTOR[c][1];v=witness_core(specialize(P,c),q[0][2]+q[1:],fields+types[1:],stats)
  return None if v is None else (value(c,*v[:len(fields)]),)+v[len(fields):]
 heads={ps[0][1] for ps in P if ps[0]!=W};signature=SIG[types[0]]
 if heads=={c for c,_ in signature}:
  for c,fields in signature:
   v=witness_core(specialize(P,c),(W,)*len(fields)+q[1:],fields+types[1:],stats)
   if v is not None:return (value(c,*v[:len(fields)]),)+v[len(fields):]
  return None
 v=witness_core(default_matrix(P),q[1:],types[1:],stats)
 if v is None:return None
 c,fields=next((c,fs) for c,fs in signature if c not in heads)
 return (value(c,*(DEFAULT[t] for t in fields)),)+v

def useful(P,q,types):
 matrix=[tuple(erase(p) for p in ps) for row in P for ps in expanded_vectors(row)];stats=Counter()
 for alt in expanded_vectors(q):
  got=witness_core(matrix,tuple(erase(p) for p in alt),types,stats)
  if got is not None:return got,dict(stats)
 return None,dict(stats)

class Occurrences:
 """Constant-width slot identifiers. Pretty paths are a separate report cost."""
 def __init__(self,width):self.parents=[(-1,i) for i in range(width)];self.index={p:i for i,p in enumerate(self.parents)}
 def child(self,parent,i):
  key=parent,i
  if key not in self.index:self.index[key]=len(self.parents);self.parents.append(key)
  return self.index[key]
 def path(self,slot):
  out=[]
  while slot>=0:
   parent,i=self.parents[slot];out.append(i);slot=parent
  return tuple(reversed(out))

def annotated(ps,pool):
 binds={}
 def go(p,o):
  if p[0]=='var':binds[p[1]]=o;return W
  if p[0]=='con':return C(p[1],*(go(q,pool.child(o,j)) for j,q in enumerate(p[2])))
  require(p==W,'annotation after expansion');return W
 return tuple(go(p,i) for i,p in enumerate(ps)),binds

def compile_tree(rows,types,choose='left'):
 require(choose in ('left','right'),'known column selection')
 require(all(row.get('guard') is None for row in rows),'tree core is guard-free')
 pool=Occurrences(len(types));initial=[];stats=Counter()
 for row in rows:
  for alt in expanded_vectors(row['patterns']):
   ps,binds=annotated(alt,pool);initial.append((ps,row['action'],binds))
 def rec(matrix,occs,tys):
  stats['matrix_cells']+=sum(len(row[0]) for row in matrix);stats['calls']+=1
  if not matrix:return ('fail',)
  if all(p==W for p in matrix[0][0]):return ('leaf',matrix[0][1],matrix[0][2])
  candidates=[i for i in range(len(occs)) if any(row[0][i]!=W for row in matrix)]
  i=candidates[0] if choose=='left' else candidates[-1]
  order=(i,)+tuple(j for j in range(len(occs)) if j!=i);matrix=[(tuple(ps[j] for j in order),a,b) for ps,a,b in matrix];occs=tuple(occs[j] for j in order);tys=tuple(tys[j] for j in order)
  heads={ps[0][1] for ps,_,_ in matrix if ps[0]!=W};cases={}
  for c,fields in SIG[tys[0]]:
   if c not in heads:continue
   sub=[]
   for ps,act,bs in matrix:
    if ps[0]==W:sub.append(((W,)*len(fields)+ps[1:],act,bs))
    elif ps[0][1]==c:sub.append((ps[0][2]+ps[1:],act,bs))
   children=tuple(pool.child(occs[0],j) for j in range(len(fields)))
   cases[c]=(children,rec(sub,children+occs[1:],fields+tys[1:]))
  rest=None
  if len(heads)!=len(SIG[tys[0]]):rest=rec([(ps[1:],act,bs) for ps,act,bs in matrix if ps[0]==W],occs[1:],tys[1:])
  return ('switch',occs[0],cases,rest)
 tree=rec(initial,tuple(range(len(types))),types)
 return {'tree':tree,'slots':pool,'stats':dict(stats)}

def run_tree(compiled,vs):
 slots={i:v for i,v in enumerate(vs)};node=compiled['tree'];tests=[];projections=0
 while node[0]=='switch':
  _,o,cases,default=node;v=slots[o];tests.append((o,v[0]))
  if v[0] in cases:
   children,node=cases[v[0]]
   for child,w in zip(children,v[1]):slots[child]=w;projections+=1
  else:check(default is not None,'typed tree switch complete');node=default
 check(len({o for o,_ in tests})==len(tests),'tree never retests a slot')
 result=None if node[0]=='fail' else (node[1],{x:slots[o] for x,o in node[2].items()})
 return {'result':result,'tests':tests,'projections':projections}

def compile_backtrack(rows,types):
 pool=Occurrences(len(types));code=[]
 def emit(*ins):code.append(ins);return len(code)-1
 def gen(p,o,yes,no):
  if p==W:return yes
  if p[0]=='var':return emit('bind',p[1],o,yes)
  if p[0]=='or':return gen(p[1],o,yes,gen(p[2],o,yes,no))
  children=tuple(pool.child(o,i) for i in range(len(p[2])));entry=yes
  for q,child in reversed(tuple(zip(p[2],children))):entry=gen(q,child,entry,no)
  return emit('test',o,p[1],children,entry,no)
 next_row=emit('fail')
 for row in reversed(rows):
  require('_binders' in row,'validate rows once before compilation')
  accept=emit('accept',row['action'],row['_binders'],row.get('guard'),next_row);entry=accept
  for i in reversed(range(len(types))):entry=gen(row['patterns'][i],i,entry,next_row)
  next_row=emit('clear',entry)
 for label,ins in enumerate(code):
  targets=() if ins[0]=='fail' else ((ins[1],) if ins[0]=='clear' else ((ins[3],) if ins[0]=='bind' else ((ins[4],ins[5]) if ins[0]=='test' else (ins[4],))))
  check(all(0<=target<label for target in targets),'every bytecode transfer points to an earlier label')
 return {'code':code,'entry':next_row,'slots':pool}

def run_backtrack(compiled,vs):
 slots={i:v for i,v in enumerate(vs)};env={};pc=compiled['entry'];tests=[];projections=steps=guards=0
 while True:
  ins=compiled['code'][pc];op=ins[0];steps+=1
  check(steps<=len(compiled['code']),'acyclic failure/continuation labels')
  if op=='fail':result=None;break
  if op=='clear':env={};pc=ins[1]
  elif op=='bind':env[ins[1]]=slots[ins[2]];pc=ins[3]
  elif op=='test':
   _,o,tag,children,yes,no=ins;v=slots[o];tests.append((o,v[0]))
   if v[0]!=tag:pc=no;continue
   for child,w in zip(children,v[1]):slots[child]=w;projections+=1
   pc=yes
  else:
   _,act,names,guard,no=ins;bound={x:env[x] for x in names}
   if guard is not None:guards+=1
   if guard_ok(guard,bound):result=(act,bound);break
   pc=no
 return {'result':result,'tests':tests,'projections':projections,'steps':steps,'guards':guards}

def finite_values(ty,depth):
 out=[]
 for c,fields in SIG[ty]:
  if fields and depth==0:continue
  for args in product(*(finite_values(t,depth-1) for t in fields)):out.append(value(c,*args))
 return out

def pretty(v):return v[0] if not v[1] else v[0]+'('+','.join(map(pretty,v[1]))+')'
def count_tree(t):return 1 if t[0]!='switch' else 1+sum(count_tree(v[1]) for v in t[2].values())+(count_tree(t[3]) if t[3] is not None else 0)
def row(ps,action,guard=None):return {'patterns':tuple(ps),'action':action,'guard':guard}

def display_run(compiled,run):
 result=run['result']
 return {**{k:v for k,v in run.items() if k not in ('result','tests')},'result':None if result is None else {'action':result[0],'bindings':{x:pretty(v) for x,v in result[1].items()}},'tests':[{'occurrence':compiled['slots'].path(o),'tag':t} for o,t in run['tests']]}

def main():
 types=('List','Bool')
 rows=[row((C('Nil'),W),'empty'),row((C('Cons',C('T'),V('xs')),C('F')),'take-tail'),row((C('Cons',W,W),C('T')),'flagged'),row((C('Cons',C('F'),W),C('F')),'false-head'),row((C('Nil'),C('T')),'shadowed')]
 validate_rows(rows,types)
 partial=rows[:3]+rows[4:];missing,missing_stats=useful([x['patterns'] for x in partial],(W,W),types)
 check(missing==(value('Cons',value('F'),value('Nil')),value('F')),'concrete missing value')
 diag=[]
 for i,r in enumerate(rows):
  w,stats=useful([x['patterns'] for x in rows[:i]],r['patterns'],types);diag.append({'row':i+1,'witness':None if w is None else [pretty(v) for v in w],'work':stats})
 complete,complete_stats=useful([x['patterns'] for x in rows],(W,W),types)
 check(complete is None and diag[-1]['witness'] is None,'exhaustive table and shadowed final Nil')
 left=compile_tree(rows,types,'left');right=compile_tree(rows,types,'right');back=compile_backtrack(rows,types)
 cases=[]
 for vs in product(finite_values('List',4),finite_values('Bool',0)):
  expected=source(rows,vs);l=run_tree(left,vs);r=run_tree(right,vs);b=run_backtrack(back,vs)
  check(l['result']==r['result']==b['result']==expected,'both targets preserve full action/bindings');cases.append((len(l['tests']),len(r['tests']),len(b['tests'])))
 examples=[]
 for vs in [(value('Nil'),value('T')),(value('Cons',value('T'),value('Nil')),value('F')),(value('Cons',value('F'),value('Nil')),value('F'))]:
  examples.append({'input':list(map(pretty,vs)),'left_tree':display_run(left,run_tree(left,vs)),'right_tree':display_run(right,run_tree(right,vs)),'bytecode':display_run(back,run_backtrack(back,vs))})
 # An independently useful column-order example without a dead source row.
 bool_rows=[row((C('T'),W,C('T')),'a'),row((W,W,C('F')),'b'),row((C('F'),C('T'),C('T')),'c'),row((W,W,W),'d')]
 validate_rows(bool_rows,('Bool',)*3);tl=compile_tree(bool_rows,('Bool',)*3,'left');tr=compile_tree(bool_rows,('Bool',)*3,'right');col=[]
 for vs in product(finite_values('Bool',0),repeat=3):
  l=run_tree(tl,vs);r=run_tree(tr,vs);check(l['result']==r['result']==source(bool_rows,vs),'column choice preserves action')
  col.append({'input':list(map(pretty,vs)),'action':l['result'][0],'left_tests':len(l['tests']),'right_tests':len(r['tests'])})
 check((count_tree(tl['tree']),count_tree(tr['tree']))==(11,9),'column static tree sizes')
 check((sum(x['left_tests'] for x in col),sum(x['right_tests'] for x in col))==(20,16),'column total tag tests')
 # Shared success labels avoid expanding a Cartesian product of or alternatives.
 family=[];family_inputs=0
 for n in range(9):
  rs=[row(tuple(O(C('F'),C('T')) for _ in range(n)),'yes')];tys=('Bool',)*n;validate_rows(rs,tys)
  t=compile_tree(rs,tys);b=compile_backtrack(rs,tys)
  check(count_tree(t['tree'])==2**(n+1)-1 and len(b['code'])==2*n+3,'unshared tree versus shared continuation size')
  for vs in product(finite_values('Bool',0),repeat=n):
   check(run_tree(t,vs)['result']==run_backtrack(b,vs)['result']==source(rs,vs),'or-product target equality');family_inputs+=1
  family.append({'columns':n,'expanded_rows':2**n,'tree_nodes':count_tree(t['tree']),'bytecode_instructions':len(b['code'])})
 guarded=[row((O(C('Cons',W,V('xs')),V('xs')),),'first','nonempty_xs'),row((W,),'fallback')]
 validate_rows(guarded,('List',));bc=compile_backtrack(guarded,('List',));one=value('Cons',value('T'),value('Nil'));two=value('Cons',value('T'),one)
 check(source(guarded,(one,))==run_backtrack(bc,(one,))['result']==('fallback',{}),'or commit before guard failure')
 naive=[row((C('Cons',W,V('xs')),),'first','nonempty_xs'),row((V('xs'),),'first','nonempty_xs'),row((W,),'fallback')]
 check(source(naive,(one,))[0]=='first','wrong guarded expansion counterexample')
 guard_count=0
 for v in finite_values('List',6):check(source(guarded,(v,))==run_backtrack(bc,(v,))['result'],'all bounded guard cases');guard_count+=1
 # Empty matrices/zero columns, declared finite defaults, and invalid typed rows.
 validate_rows([],());check(useful([],(),())[0]==() and source([],()) is None,'empty matrix empty vector')
 empty=[row((),'zero')];validate_rows(empty,());check(run_tree(compile_tree(empty,()),())['result']==run_backtrack(compile_backtrack(empty,()),())['result']==('zero',{}),'zero-column first row')
 invalid=0
 for bad,tys in [([row((O(V('x'),W),),'bad')],('Bool',)),([row((V('x'),V('x')),'bad')],('Bool','Bool')),([row((C('Cons',C('Nil'),W),),'bad')],('List',)),([row((W,),'bad','nonempty_xs')],('List',))]:
  try:validate_rows(bad,tys)
  except ValueError:invalid+=1
  else:raise AssertionError('invalid typed row accepted')
 try:compile_tree(guarded,('List',))
 except ValueError:invalid+=1
 else:raise AssertionError('guard silently accepted by tree core')
 record={'status':'PASS','missing_before_repair':list(map(pretty,missing)),'missing_work':missing_stats,'row_diagnostics_after_repair':diag,'exhaustive_after_repair':complete is None,'complete_work':complete_stats,'checks':{'main_inputs':len(cases),'or_product_inputs':family_inputs,'guarded_inputs':guard_count,'invalid_inputs':invalid},'main_target_counts':{'tree_nodes':[count_tree(left['tree']),count_tree(right['tree'])],'bytecode_instructions':len(back['code']),'total_tag_tests_left_right_back':list(map(sum,zip(*cases)))},'main_examples':examples,'main_left_tree':left['tree'],'main_right_tree':right['tree'],'main_tree_slots':left['slots'].parents,'main_bytecode':back['code'],'main_bytecode_entry':back['entry'],'main_bytecode_slots':back['slots'].parents,'column_example':{'rows':bool_rows,'tree_nodes':[11,9],'total_tag_tests':[20,16],'inputs':col},'or_family':family,'guarded_example':{'bytecode':bc['code'],'entry':bc['entry'],'slots':bc['slots'].parents,'singleton':display_run(bc,run_backtrack(bc,(one,))),'two_elements':display_run(bc,run_backtrack(bc,(two,))),'wrong_expansion_action':source(naive,(one,))[0]},'scope':'Finite immutable typed Bool/List values; guard-free common core, explicit left-biased or and total pure guard extension. Test bounds do not replace structural proofs. Diagnostic annotations and pretty serialization are charged separately.'}
 print(json.dumps(record,ensure_ascii=False,indent=2))
if __name__=='__main__':main()