CAEL-0.3.9.1 / native_interpretation.patch
vynly's picture
Release CAEL 0.3.9.1 native symbolic interpretation
b33a97d verified
Raw History Blame Contribute Delete
48.6 kB
--- a/cael_unified/assistant.py
+++ b/cael_unified/assistant.py
@@ -94,6 +94,8 @@
def picture_follow_up(messages):
"""'make it blue' right after a picture: an edit of that picture, not a chat message."""
+ if len(messages) < 3 or not picture_reply(messages[-2]):
+ return False
from cael_image.scene import is_edit
text = messages[-1]['content']
return len(messages) >= 3 and picture_reply(messages[-2]) and is_edit(text) and not new_picture_request(text)
@@ -179,6 +181,18 @@
# spelling repair, fact route or web lookup can read "CAEL" as someone else (self_identity.py, 0.3.8 fix).
from . import self_identity
answer = self_identity.reply(messages) if mode in ('auto', 'chat') else None
+ # A complete, single-request symbolic document owns its literal
+ # symbols before dialogue acts, spelling and memory heuristics.
+ if (answer is None and mode in ('auto','chat') and isinstance(messages,list)
+ and messages and messages[-1].get('role')=='user'
+ and all(isinstance(m,dict) and m.get('role') in ('system','user')
+ and isinstance(m.get('content'),str) for m in messages)
+ and sum(m['role']=='user' for m in messages)==1
+ and type(n) is int and 1<=n<=8
+ and (seed is None or type(seed) is int and 0<=seed<2**31)):
+ from .interpretation import reply as native_task_reply
+ task=messages[-1]['content'];framed=choice_problem(task)
+ answer=native_task_reply(framed[0],framed[1],self._reasoning) if framed else native_task_reply(task,reasoner=self._reasoning)
if answer is None and mode in ('auto','chat') and type(n) is int and 1<=n<=8 and (seed is None or type(seed) is int and 0<=seed<2**31):
from .dialogue import reply as dialogue_reply
answer=dialogue_reply(messages,lambda history:self._respond_request(history,n=n,seed=seed,mode=mode))
@@ -401,6 +415,10 @@
def _context_choice(self, context, endings):
"""The same existing solvers/counts, before an unrelated topic route."""
+ from .interpretation import reply as native_task_reply
+ native = native_task_reply(context, endings, self._reasoning)
+ if native is not None:
+ return dict(native, context_owned=True)
from .quantity_graph import choice_reply as quantity_choice
quantified=quantity_choice(context,endings)
if quantified is not None:
@@ -451,6 +469,13 @@
if not text:
raise ValueError('Request is empty')
if mode in ('auto', 'chat'):
+ # Native whole-task interpretation is shared by direct chat and MC;
+ # it never receives benchmark metadata, answer keys or model replies.
+ from .interpretation import reply as native_task_reply
+ framed = choice_problem(text)
+ native = native_task_reply(framed[0], framed[1], self._reasoning) if framed else native_task_reply(text, reasoner=self._reasoning)
+ if native is not None:
+ return native
def settled(found):
# A solver that cannot parse a clause asks for clarification; the everyday word-problem reasoner and
# the price/percent solver get a chance first (0.3.8 Q&A fix: "She gives 5 to Tom. Then she buys 8").
--- /dev/null
+++ b/cael_unified/interpretation.py
@@ -0,0 +1,54 @@
+"""Native typed interpretation -> bounded symbolic operations -> checked answer.
+
+This is part of Assistant inference, not an evaluator adapter. No benchmark IDs,
+gold answers, external models, network calls, weight changes or code execution.
+"""
+from fractions import Fraction
+from .interpretation_common import Result,TaskError,clean,display
+
+TRUTH={'true':'true','yes':'true','false':'false','no':'false','unknown':'unknown','undetermined':'unknown',
+ 'not enough information':'unknown','inconsistent':'conflicting','conflicting':'conflicting','both true and false':'conflicting'}
+
+def answer(result,options):
+ value=display(result.value)
+ proof={'family':result.family,'program':result.program,'value':value,'complete_source':True,
+ 'architecture':'bounded symbolic interpreter / relation and state automata','internet_used':False}
+ if options is not None:
+ matches=[]
+ for i,opt in enumerate(options):
+ if result.numeric:
+ try:equal=Fraction(opt.strip())==result.value
+ except (ValueError,ZeroDivisionError):equal=False
+ elif result.family=='logic':equal=TRUTH.get(clean(opt))==value
+ elif result.exact_text:equal=opt==value
+ else:equal=clean(opt)==clean(value)
+ if equal:matches.append(i)
+ if len(matches)!=1:raise TaskError('The checked result does not identify exactly one option; please clarify the answer choices.')
+ i=matches[0];response=f'{"ABCDEFGH"[i]}. {options[i]}'
+ else:
+ i=None;response=value if value else '""'
+ out={'route':'chat/native-'+result.family,'response':response,'sources':[],'reasoning':proof,
+ 'verification':{'status':'verified','check':'Complete typed source compiled to bounded '+result.family+' operations; all declared dependencies retained.'},
+ 'details':'Native non-neural interpretation of the full supplied task. '+str(result.program)}
+ if i is not None:out['choice']=i
+ return out
+
+def reply(text,options=None,reasoner=None):
+ if not isinstance(text,str) or not 0<len(text)<=40000:return None
+ if options is not None and (not 2<=len(options)<=8 or any(not isinstance(x,str) for x in options)):return None
+ from . import interpretation_data as data,interpretation_relations as relations,interpretation_arithmetic as arithmetic
+ cached=[reasoner]
+ def get_reasoner():
+ if cached[0] is None:
+ from .reasoning import Reasoner
+ cached[0]=Reasoner()
+ return cached[0]
+ for compile in (data.tables,data.strings,relations.order,lambda t:relations.state(t,get_reasoner),lambda t:relations.logic(t,get_reasoner),arithmetic.compile):
+ try:
+ result=compile(text)
+ if result is not None:return answer(result,options)
+ except TaskError as exc:
+ return {'route':'chat/native-task-clarify','response':'Please clarify: '+str(exc),'sources':[],
+ 'reasoning':{'complete_source':False,'unsupported_reason':str(exc),'internet_used':False},
+ 'details':'The complete task remains owned by its symbolic interpretation path; no unsupported clause is discarded for a statistical guess.'}
+ return None
--- /dev/null
+++ b/cael_unified/interpretation_arithmetic.py
@@ -0,0 +1,50 @@
+"""General arithmetic request boundary -> existing exact helper and checker."""
+from fractions import Fraction
+import re
+from .interpretation_common import Result,TaskError,boundary,strip_request,NUMBER
+from .helper import calculate
+from .verify import check_arithmetic,Unchecked
+
+# Function words describe the value/operation request, never extra operands or
+# conditions. Unknown content is not deleted to expose a convenient expression.
+WRAPPER=set('''what which number value result answer expression equation does do is are the a an this that it its of for from to in using with use obey follow usual standard ordinary integer exact arithmetic mathematical mathematics order operations parentheses have their meaning produce produces yield yields obtain obtained get evaluate evaluated calculate calculated compute computed work out find determine give select choose return tell me please resolve simplify amounts evaluates'''.split())
+
+def checked(expression):
+ answer=calculate('Calculate '+expression)
+ if not answer or answer.get('route')!='helper/arithmetic':raise TaskError('The complete expression is outside the bounded arithmetic interpreter.')
+ try:proof=check_arithmetic(expression,answer)
+ except (Unchecked,ValueError,ZeroDivisionError):raise TaskError('The arithmetic result could not be checked independently.')
+ if proof.get('status')!='verified':raise TaskError('The independent arithmetic check disagrees.')
+ return Fraction(answer['response'].split(' = ',1)[1].split(' (about',1)[0]),proof
+
+def compile(text):
+ t=strip_request(text)
+ # The established whole-expression reader retains percentages and supported
+ # word operators; no changes to its solver or protected kernels.
+ old=calculate(t)
+ if old and old.get('route')=='helper/arithmetic':
+ try:
+ p=check_arithmetic(t,old)
+ if p['status']=='verified':return Result(Fraction(old['response'].split(' = ',1)[1].split(' (about',1)[0]),'arithmetic',{'source_span':[0,len(text)],'operation':old['response'],'check':p},True)
+ except (Unchecked,ValueError,ZeroDivisionError):pass
+ intent=bool(re.search(r'(?i)\b(?:arithmetic|expression|calculate|compute|evaluate|work out|simplify|numeric value|number does|value of)\b',t) or re.match(r'(?i)(?:what|which|find|give|return|determine)\b.{0,35}\b(?:number|value|result)\b',t))
+ if not intent:return None
+ boundary(t)
+ # Convert lexical operators before finding a full numeric expression.
+ normalized=t
+ for phrase,op in [('multiplied by','*'),('divided by','/'),('times','*'),('plus','+'),('minus','-')]:
+ normalized=re.sub(r'(?i)\b'+phrase+r'\b',op,normalized)
+ normalized=normalized.replace('×','*').replace('÷','/').replace('−','-')
+ matches=list(re.finditer(r'(?<![\w])[+\-(.\s]*\d[\d\s()+*/%^.\-]*',normalized))
+ matches=[m for m in matches if re.search(r'\d',m[0])]
+ if not matches:
+ if re.search(r'__|\b(?:import|exec|eval|open)\s*\(',t):raise TaskError('Only bounded literal arithmetic is accepted; code and imports are not arithmetic values.')
+ return None
+ if len(matches)!=1:raise TaskError('Several numeric fragments need an explicit supported operation connecting them.')
+ m=matches[0];expression=m[0].strip().rstrip(' .?=')
+ wrapper=normalized[:m.start()]+' '+normalized[m.end():]
+ words=re.findall(r'[A-Za-z]+',wrapper.casefold())
+ if any(w not in WRAPPER for w in words) or re.search(r'[^A-Za-z\s,.:?!=\'"-]',wrapper):
+ raise TaskError('The expression has an additional clause or qualifier outside the checked arithmetic request grammar.')
+ value,proof=checked(expression)
+ return Result(value,'arithmetic',{'source_span':[0,len(text)],'expression':expression,'checked_wrapper_words':words,'check':proof},True)
--- /dev/null
+++ b/cael_unified/interpretation_common.py
@@ -0,0 +1,77 @@
+"""Shared bounded symbols/clauses for native symbolic task compilation."""
+from dataclasses import dataclass
+from fractions import Fraction
+import re
+
+class TaskError(ValueError):
+ pass
+
+ATOM=r'[A-Za-z][A-Za-z0-9_-]*(?: [A-Za-z][A-Za-z0-9_-]*){0,7}'
+NUMBER=r'[+-]?(?:\d+(?:\.\d*)?|\.\d+)(?:/[+-]?\d+)?'
+
+def clean(s):
+ s=s.strip().strip('"\'`').strip().rstrip(' .?!')
+ return re.sub(r'\s+',' ',s).casefold()
+
+def symbol(s):
+ s=re.sub(r'(?i)^(?:the|an?)\s+','',s.strip())
+ if not re.fullmatch(ATOM,s) or re.search(r'(?i)\b(?:unless|except|maybe|perhaps|sometimes|either|or|if|then|and)\b',s):
+ raise TaskError('An entity or property has an ambiguous or unsupported modifier.')
+ return clean(s)
+
+def alphabet(n):
+ out=''
+ while True:
+ out=chr(97+n%26)+out;n=n//26-1
+ if n<0:return out
+
+def clauses(text):
+ """Keep decimal points and quoted text intact; every clause remains visible."""
+ out=[];start=0;quote=None
+ for i,ch in enumerate(text):
+ if ch in ('"',"'") and (i==0 or text[i-1]!='\\'):
+ # Apostrophes inside words are not quotation delimiters.
+ if ch=="'" and i and i+1<len(text) and text[i-1].isalnum() and text[i+1].isalnum():continue
+ if quote==ch:quote=None
+ elif quote is None:quote=ch
+ stop=ch in '\n;' or (ch=='.' and not (i and i+1<len(text) and text[i-1].isdigit() and text[i+1].isdigit()))
+ if stop and quote is None:
+ if text[start:i].strip():out.append(text[start:i].strip())
+ start=i+1
+ if text[start:].strip():out.append(text[start:].strip())
+ return out
+
+def spans(text,parts):
+ result=[];offset=0
+ for part in parts:
+ i=text.find(part,offset)
+ if i<0:raise TaskError('Source coverage could not be established.')
+ result.append({'text':part,'span':[i,i+len(part)]});offset=i+len(part)
+ return result
+
+def fraction(s):
+ s=s.strip()
+ if not re.fullmatch(NUMBER,s):raise TaskError('A numeric cell is missing or is not an explicit rational number.')
+ try:v=Fraction(s)
+ except (ValueError,ZeroDivisionError):raise TaskError('A number or denominator is invalid.')
+ if max(v.numerator.bit_length(),v.denominator.bit_length())>512:raise TaskError('The numeric value is outside the checked size limit.')
+ return v
+
+def display(v):
+ if isinstance(v,Fraction):return str(v.numerator) if v.denominator==1 else str(v)
+ return str(v)
+
+def boundary(text):
+ if re.search(r'(?i)\b(?:unless|except|assuming|approximately|probably|maybe|possibly|ignore|disregard|pretend)\b|\bround(?:ed|ing)?\s+(?:to|off|up|down|it|the result)\b',text):
+ raise TaskError('A condition, exception or approximation needs a supported explicit interpretation; it cannot be omitted.')
+
+def strip_request(text):
+ return re.sub(r'(?i)^\s*(?:(?:can|could|would) you\s+)?(?:please\s+)?','',text).strip()
+
+@dataclass
+class Result:
+ value: object
+ family: str
+ program: dict
+ numeric: bool=False
+ exact_text: bool=False
--- /dev/null
+++ b/cael_unified/interpretation_data.py
@@ -0,0 +1,201 @@
+"""Bounded string-operation pipelines and typed table reductions, from source."""
+import csv
+from fractions import Fraction
+import json
+import re
+from .interpretation_common import Result,TaskError,boundary,clauses,clean,fraction,spans,strip_request
+
+def strings(text):
+ t=strip_request(text)
+ if not re.search(r'(?i)\b(?:reverse|backwards|backward|rotate|characters|substring|uppercase|lowercase|swapcase|append|prepend|replace)\b',t):return None
+ if re.match(r'(?i)(?:write|create|implement|define|build|explain) (?:a |the )?(?:python |javascript )?(?:function|script|program|code)\b',t):return None
+ literals=[]
+ def mask(m):
+ raw=m[0]
+ try:value=json.loads(raw) if raw.startswith('"') else raw[1:-1]
+ except ValueError:raise TaskError('A quoted string literal has invalid escaping.')
+ literals.append(value);return f'literalq{len(literals)-1}'
+ source=re.sub(r'''"(?:[^"\\]|\\.)*"|'[^']*' ''',mask,t,flags=re.X)
+ if not literals:return None
+ if not re.search(r'(?i)\b(?:reverse|backwards|backward|rotate|characters|substring|uppercase|lowercase|swapcase|append|prepend|replace)\b',source):return None
+ if not re.match(r'(?i)^(?:from\b|for\b|given\b|using\b|with\b|text\s*:|string\s*:|input\s*:|reverse\b|rotate\b|keep\b|retain\b|select\b|take\b|read\b|write\b|move\b|transfer\b|drop\b|remove\b|delete\b|convert\b|change\b|make\b|uppercase\b|lowercase\b|swapcase\b|append\b|prepend\b|replace\b|number\b|index\b)',source):return None
+ if len(literals[0])>2048 or len(literals)>8:raise TaskError('Use at most eight quoted literals and an input string within 2,048 characters.')
+ boundary(source)
+ source=re.sub(r'(?i)^(?:for|given|using|with)(?: the)? (?:text|string|sequence|characters)\s*(?:is|:)?\s*literalq0\s*[,.:]?\s*','',source)
+ source=re.sub(r'(?i)^(?:text|string|input)\s*:\s*literalq0\s*[,.:]?\s*','',source)
+ source=re.sub(r'(?i)\b(?:the )?(?:string|text) (literalq\d+)\b',r'\1',source)
+ pieces=[]
+ for p in clauses(source):pieces.extend(re.split(r'(?i)\s*,?\s*\b(?:then|after that|next)\b\s*',p))
+ pieces=[p.strip(' ,.:?') for p in pieces if p.strip(' ,.:?')]
+ value=literals[0];ops=[];used={0};base=1
+ arg=r'(?:literalq0|(?:the |its )?(?:entire |resulting |current |original )?(?:string|text|characters|letters|result|sequence)|it)'
+ reverse_words=set('reverse read write take the its all entire resulting current original string text characters letters result sequence it literalq0 in of reverse order backwards backward from last one to first what which is results produces do you obtain choose final'.split())
+ for part in pieces:
+ p=part.casefold()
+ m=re.fullmatch(rf'(?:number|index) (?:the )?characters (?:of |in )?{arg} (?:starting|beginning) (?:at|from) ([01])',p)
+ if m:base=int(m[1]);continue
+ m=re.fullmatch(r'(?:use|using) ([01])[- ]based (?:positions|indexing|indices)',p)
+ if m:base=int(m[1]);continue
+ # Query-only clauses carry no additional transformation.
+ if re.fullmatch(r'(?:what|which)(?: is| do you get| do you obtain)?(?: the)?(?: final| resulting)? (?:string|text|sequence|result)(?: results| remains| do you get| do you obtain)?',p) or p in ('choose the final string','select the resulting string','what remains','which sequence results'):continue
+ op=None
+ m=re.fullmatch(rf'rotate\s+{arg}?\s*(left|right)\s*(?:by )?(\d+)\s*(?:characters?|positions?|places?)?',p)
+ if m:op=('rotate',m[1],int(m[2]))
+ if op is None:
+ m=re.fullmatch(r'(?:move|transfer) (?:the )?(first|last) (\d+) characters (?:of literalq0 )?to (?:its |the )?(end|front|beginning)(?: without (?:reordering|changing their order))?',p)
+ if m and ((m[1]=='first' and m[3]=='end') or (m[1]=='last' and m[3] in ('front','beginning'))):op=('rotate','left' if m[1]=='first' else 'right',int(m[2]))
+ if op is None:
+ m=re.fullmatch(rf'(?:keep|retain|select|take)(?: only)? (?:the )?(even|odd)[- ](?:numbered|positioned) characters(?: (?:of|from|in) {arg})?(?:,? (?:without changing|preserving) their order)?',p)
+ if m:op=('parity',0 if m[1]=='even' else 1,base)
+ if op is None:
+ m=re.fullmatch(rf'(?:from {arg},? )?(?:keep|retain|select|take)(?: only)? (?:the )?characters (?:at|in) positions? ([\d, ]+)(?:,? and so on)?(?: \(([01])[- ]based\))?',p)
+ if m:
+ positions=[int(x) for x in re.findall(r'\d+',m[1])];indexbase=int(m[2]) if m[2] else base
+ if 'and so on' in p:
+ if len(positions)<2 or len(set(b-a for a,b in zip(positions,positions[1:])))!=1 or positions[1]<=positions[0]:raise TaskError('The repeated position pattern is not uniquely specified.')
+ op=('positions_progression',positions[0]-indexbase,positions[1]-positions[0])
+ else:op=('positions',[i-indexbase for i in positions])
+ if op is None:
+ m=re.fullmatch(rf'(?:remove|drop|delete) (?:the )?(first|last) (\d+) characters(?: (?:of|from) {arg})?',p)
+ if m:op=('drop',m[1],int(m[2]))
+ if op is None:
+ m=re.fullmatch(rf'(?:convert|change|make) {arg} (?:to |all )?(upper(?:case)?|lower(?:case)?)(?: letters)?',p) or re.fullmatch(rf'(uppercase|lowercase|swapcase) {arg}',p)
+ if m:op=('case','upper' if m[1].startswith('upper') else 'lower' if m[1].startswith('lower') else 'swapcase')
+ if op is None:
+ m=re.fullmatch(r'(append|prepend) literalq(\d+)(?: to (?:the )?(?:result|string|text|it))?',p)
+ if m:op=(m[1],int(m[2]));used.add(int(m[2]))
+ if op is None:
+ m=re.fullmatch(r'replace (?:every |each |all )?(?:occurrence of )?literalq(\d+) (?:with|by) literalq(\d+)(?: in (?:the )?(?:result|string|text|it))?',p)
+ if m:op=('replace',int(m[1]),int(m[2]));used.update((int(m[1]),int(m[2])))
+ if op is None:
+ words=set(re.findall(r'[a-z0-9]+',p))
+ if (re.search(r'\b(?:reverse|backwards|backward)\b',p) or ('last' in words and 'first' in words and words&{'read','write','take'})) and words<=reverse_words:op=('reverse',)
+ if op is None:raise TaskError('A string operation or indexing instruction is unsupported: '+part[:100])
+ before=value
+ if op[0]=='reverse':value=''.join(reversed(value))
+ elif op[0]=='rotate':
+ k=op[2]%len(value) if value else 0
+ if op[1]=='right':k=(-k)%len(value) if value else 0
+ value=value[k:]+value[:k]
+ elif op[0]=='parity':value=''.join(ch for i,ch in enumerate(value) if (i+op[2])%2==op[1])
+ elif op[0]=='positions':
+ if any(i<0 or i>=len(value) for i in op[1]):raise TaskError('An explicit requested character position is out of bounds.')
+ value=''.join(value[i] for i in op[1])
+ elif op[0]=='positions_progression':
+ if op[1]<0:raise TaskError('A requested position precedes the declared index origin.')
+ value=''.join(value[i] for i in range(op[1],len(value),op[2]))
+ elif op[0]=='drop':value=value[op[2]:] if op[1]=='first' else value[:max(0,len(value)-op[2])]
+ elif op[0]=='case':value=getattr(value,op[1])()
+ elif op[0]=='append':value+=literals[op[1]]
+ elif op[0]=='prepend':value=literals[op[1]]+value
+ else:
+ if not literals[op[1]]:raise TaskError('Replacing an empty substring needs an explicit insertion convention.')
+ value=value.replace(literals[op[1]],literals[op[2]])
+ if len(value)>16384 or len(ops)>=12:raise TaskError('The string program exceeds its checked size bound.')
+ ops.append({'source':part,'operation':op,'before':before,'after':value})
+ if not ops:return None
+ if used!=set(range(len(literals))):raise TaskError('A quoted value was not consumed by the complete string specification.')
+ return Result(value,'strings',{'source_span':[0,len(text)],'literals':literals,'operations':ops,'index_origin':base},exact_text=True)
+
+ALIASES=[{'quantity','qty','units','unit count','amount'}, {'price','unit price','cost','unit cost'},
+ {'group','category','class','type'}, {'name','item','product','entry','identifier','id'}]
+
+def tables(text):
+ lines=[s.strip() for s in text.splitlines() if s.strip()]
+ if len(lines)<3:return None
+ header=lines[0]
+ delimiter='|' if '|' in header else '\t' if '\t' in header else ',' if ',' in header else None
+ if delimiter is None:return None
+ header=re.sub(r'(?i)^(?:table|records|data)\s*:\s*','',header)
+ def cells(line):
+ line=line.strip().strip('|') if delimiter=='|' else line
+ return [x.strip() for x in next(csv.reader([line],delimiter=delimiter))]
+ headers=cells(header);keys=[re.sub(r'[_-]+',' ',clean(x)) for x in headers]
+ if not 2<=len(keys)<=16 or len(set(keys))!=len(keys) or any(not re.fullmatch(r'[a-z][a-z0-9 ]{0,60}',k) for k in keys):return None
+ records=[];qlines=[];data_lines=[]
+ for line in lines[1:]:
+ row=cells(line)
+ if len(row)==len(keys) and all(re.fullmatch(r':?-+:?',x) for x in row):data_lines.append(line);continue
+ if delimiter in line and not qlines:
+ if len(row)!=len(keys):raise TaskError('A table record has a different number of cells from its header.')
+ if any(x=='' for x in row):raise TaskError('A table contains an empty cell; its meaning must be specified.')
+ records.append(row);data_lines.append(line)
+ else:qlines.append(line)
+ if not records or not qlines:return None
+ if len(records)>200:raise TaskError('Use at most 200 explicit table records.')
+ query=' '.join(qlines).strip();boundary(query)
+ if re.search(r'(?i)\b(?:or|either|unless|except)\b',query):raise TaskError('This table query has an unsupported condition or combination.')
+ aliases={}
+ for i,k in enumerate(keys):
+ aliases.setdefault(k,set()).add(i)
+ for group in ALIASES:
+ if k in group:
+ for term in group:aliases.setdefault(term,set()).add(i)
+ def field(label):
+ label=re.sub(r'[_-]+',' ',clean(label))
+ if label in keys:return keys.index(label)
+ found=aliases.get(label,set())
+ if len(found)!=1:raise TaskError('A queried table column is missing or has an ambiguous alias: '+label)
+ return next(iter(found))
+ # "product of X and Y" is an operation, not an inferred name-column alias.
+ if 'product' not in keys:aliases.pop('product',None)
+ all_fields='|'.join(re.escape(k).replace(r'\ ',r'[ _-]+') for k in sorted(aliases,key=len,reverse=True))
+ filters=[]
+ # Conditions use only actual declared fields/aliases. No inferred row labels.
+ condition=rf'(?P<field>{all_fields})\s*(?P<op>is not|is|equals|equal to|!=|>=|<=|=|>|<)?\s+(?P<value>"[^"]*"|\x27[^\x27]*\x27|[A-Za-z0-9_+./-]+)'
+ region=re.search(rf'(?i)\b(?:for|with|where|whose|having|that have|have|has)\s+(?:the )?(?:records?\s+(?:where|with)\s+)?{condition}',query)
+ masked=query
+ if region:
+ idx=field(region['field']);op=(region['op'] or '=').casefold();val=region['value'].strip('"\'') if region['value'].startswith(('"',"'")) else region['value'].rstrip('.?')
+ filters.append((idx,op,val));masked=query[:region.start()]+' FILTER '+query[region.end():]
+ # Additional conjunction conditions must be completely covered too.
+ after_filter=region.start()+len(' FILTER ')
+ while True:
+ m=re.match(rf'(?i)\s*and\s+{condition}',masked[after_filter:])
+ if not m:break
+ val=m['value'].strip('"\'') if m['value'].startswith(('"',"'")) else m['value'].rstrip('.?')
+ filters.append((field(m['field']),(m['op'] or '=').casefold(),val))
+ masked=masked[:after_filter]+' FILTER '+masked[after_filter+m.end():]
+ after_filter+=len(' FILTER ')
+ if re.search(r'(?i)\b(?:where|whose|having)\b',masked):raise TaskError('A table filter could not be fully parsed.')
+ selected=[]
+ for ri,row in enumerate(records):
+ keep=True
+ for col,op,value in filters:
+ actual=row[col]
+ if op in ('>','<','>=','<='):
+ a,b=fraction(actual),fraction(value);accept={'>':a>b,'<':a<b,'>=':a>=b,'<=':a<=b}[op]
+ else:
+ try:a,b=fraction(actual),fraction(value)
+ except TaskError:a,b=actual,value
+ accept=(a!=b) if op in ('is not','!=') else (a==b)
+ keep &= accept
+ if keep:selected.append(ri)
+ # Replace column references with typed variables before lexical coverage.
+ referenced=[]
+ def replace(m):
+ i=field(m[0]);referenced.append(i);return ' FIELD '
+ residual=re.sub(rf'(?i)(?<![\w])(?:{all_fields})(?![\w])',replace,masked)
+ words=set(re.findall(r'[A-Za-z]+',residual.casefold()))
+ vocabulary=set('''filter field what which is are the a an of for with where whose having in per how many number count rows row records record entries entry selected matching all each every their corresponding values value total sum add added adding aggregate combined quantity amounts multiply multiplied by times product products take calculate compute find determine give return choose select obtain get do you result answer these those this that and then to on its together table data please'''.split())
+ vocabulary.update(('minimum','maximum','min','max','average','mean','smallest','largest'))
+ if not words<=vocabulary or re.search(r'[^A-Za-z\s\d,.:?*+/_()=-]',residual):raise TaskError('The complete table query contains an uncompiled operation or qualifier.')
+ q=residual.casefold();fields=list(dict.fromkeys(referenced))
+ if re.search(r'\b(?:count|how many|number of (?:rows|records|entries))\b',q):
+ if fields:raise TaskError('Specify whether to count records or aggregate a column.')
+ value=Fraction(len(selected));operation='count'
+ else:
+ reduce='mean' if re.search(r'\b(?:mean|average)\b',q) else 'min' if re.search(r'\b(?:minimum|min|smallest)\b',q) else 'max' if re.search(r'\b(?:maximum|max|largest)\b',q) else 'sum' if re.search(r'\b(?:sum|total|add|adding|aggregate|combined)\b',q) else None
+ if reduce is None or not fields:raise TaskError('Specify a supported reducer and its numeric column.')
+ product=bool(re.search(r'\b(?:multiply|multiplied|times|product|products)\b|\*',q))
+ if len(fields)!= (2 if product else 1):raise TaskError('The numeric column expression is missing or ambiguous.')
+ values=[]
+ for ri in selected:
+ v=fraction(records[ri][fields[0]])
+ if product:v*=fraction(records[ri][fields[1]])
+ values.append(v)
+ if reduce!='sum' and not values:raise TaskError('The selected table is empty, so this reducer is undefined.')
+ value=sum(values,Fraction(0)) if reduce=='sum' else sum(values,Fraction(0))/len(values) if reduce=='mean' else min(values) if reduce=='min' else max(values)
+ operation=reduce+('_product' if product else '')
+ return Result(value,'tables',{'coverage':spans(text,lines),'headers':headers,'records':records,'filters':filters,
+ 'selected_record_indices':selected,'operation':operation,'numeric_columns':fields,'value':str(value)},True)
--- /dev/null
+++ b/cael_unified/interpretation_relations.py
@@ -0,0 +1,246 @@
+"""Source-covered rule, precedence and chronological event compilation.
+
+Symbolic relations and finite state only. No learned answer table or neural path.
+"""
+import re
+from .interpretation_common import ATOM,Result,TaskError,alphabet,boundary,clauses,clean,spans,symbol
+
+def relation_atom(s):
+ s=re.sub(r'(?i)^(?:(?:the|an?) )?(?:(?:class|category|type|group)\s+)?','',s.strip())
+ return symbol(s)
+
+def membership(text,question=False):
+ t=text.strip().strip('"\'').rstrip(' ?.');negative=False
+ if question and re.match(r'(?i)^is ',t):
+ t=t[3:];m=re.fullmatch(rf'({ATOM}?) (not )?(?:an? |the |in (?:the )?(?:class |category |group )?|of type )(.+)',t,re.I)
+ if m:return symbol(m[1]),relation_atom(m[3]),bool(m[2])
+ m=re.fullmatch(rf'({ATOM}?) (does not belong to|is not a member of|is a member of|is classified as|has type|belongs to|is not|is) (.+)',t,re.I)
+ if not m:return None
+ return symbol(m[1]),relation_atom(m[3]),m[2].casefold() in ('is not','does not belong to','is not a member of')
+
+def _logic_query(q):
+ q=q.strip().rstrip(' ?.');q=re.sub(r'(?i)^(?:question|query)\s*:\s*','',q)
+ q=re.sub(r'(?i)^(?:(?:under|using) open[- ]world (?:logic|assumptions),?\s*)','',q)
+ quoted=re.search(r'''(["'])(.+?)\1''',q)
+ if quoted:
+ tail=q[quoted.end():]
+ if not re.fullmatch(r'(?i)\s*(?:(?:as )?(?:true|false|unknown|undetermined|inconsistent|or|and|,|/|\s)+)?',tail):return None
+ if not re.fullmatch(r'(?i)(?:is|classify|evaluate|judge)(?: the (?:claim|statement|proposition))?\s*',q[:quoted.start()]):return None
+ return membership(quoted[2])
+ q=re.sub(r'(?i)^(?:classify|judge|evaluate|determine)(?: the)? (?:claim|statement|proposition)(?: that)?\s*','',q)
+ q=re.sub(r'(?i)^(?:does (?:it|the information|the evidence) (?:follow|establish)(?: that)?|can (?:we|you) conclude(?: that)?|is it true that|prove(?: that)?|what follows about)\s*','',q)
+ # A truth-value legend must have its complete standard meanings. It is
+ # metadata, not additional facts about the entities.
+ if ':' in q:
+ q,legend=q.split(':',1)
+ words=set(re.findall(r'[a-z]+',legend.casefold()))
+ allowed=set('true false unknown undetermined inconsistent conflicting means proved proven negation its is neither both and or not established supported contradicted the statement claim'.split())
+ if not words<=allowed:raise TaskError('The answer legend contains an unsupported logical convention.')
+ if not {'true','false'}<=words:raise TaskError('State the complete logical answer convention.')
+ standard=re.fullmatch(r'(?i)\s*true means (?:proved|proven|supported),? false means (?:its|the) negation is (?:proved|proven|supported),? unknown means neither,? and (?:inconsistent|conflicting) means both\s*',legend)
+ if not standard:raise TaskError('The truth-value legend must preserve the standard proved/negated/neither/both meanings.')
+ return membership(q,True) or membership(q)
+
+def logic(text,reasoner):
+ parts=clauses(text)
+ if len(parts)<2:return None
+ if not re.search(r'(?i)\b(?:every|all|each|anything|everything|implies|open[- ]world|premises|facts|rules)\b|(?:^|\n)(?:query|question)\s*:|true,? false',text):return None
+ if not re.match(r'(?i)^(?:is\b|under\b|using\b|classify\b|judge\b|evaluate\b|determine\b|question\s*:|query\s*:|does\b|can\b|prove\b|what follows about\b)',parts[-1]):return None
+ if any(re.search(r'(?i)\band\b',p) for p in parts[:-1]) and not re.search(r'(?i)\b(?:class|category|belongs|type)\b',text):return None
+ q=_logic_query(parts[-1])
+ if q is None:return None
+ # A local scenario, not an unsupported attempt to answer general knowledge.
+ if not any(re.search(r'(?i)\b(?:is|has|every|all|each|anything|belongs|implies|classified)\b',p) for p in parts[:-1]):return None
+ facts=[];rules=[];used=[]
+ for raw in parts[:-1]:
+ p=re.sub(r'(?i)^(?:facts|premises|given|rules|scenario|context)\s*:\s*','',raw).strip()
+ if not p:used.append(raw);continue
+ if re.fullmatch(r'(?i)(?:use|consider) only (?:these|the stated|the supplied) (?:facts|statements|premises)(?:,? (?:a )?missing (?:fact|statement) is not false,? and (?:an )?implication cannot be reversed)?',p):used.append(raw);continue
+ if re.fullmatch(r'(?i)(?:no fact implies its converse|use open[- ]world (?:logic|reasoning)|absence (?:of a fact )?(?:is|means) (?:not falsity|unknown))',p):used.append(raw);continue
+ if re.fullmatch(r'(?i)(?:an? )?(?:missing|unstated|absent) (?:fact|statement) (?:is not false|is unknown|does not imply (?:its )?negation)(?:,? and (?:an? )?implication cannot be reversed)?',p):used.append(raw);continue
+ boundary(p)
+ m=re.fullmatch(r'(?i)(?:anything|everything|any entity|any object) (?:in (?:the )?(?:class|category|group)|that is|of type|with type) (.+?) (?:also belongs to|belongs to|is also|is) (.+)',p)
+ if not m:m=re.fullmatch(r'(?i)(?:all|every|each|any) (.+?) (?:are also|is also|are|is|belong to|belongs to|must be) (.+)',p)
+ if not m:m=re.fullmatch(r'(?i)if (?:something|an? (?:object|entity|thing)) (?:is|belongs to) (.+?)(?:,)? then (?:it|that entity|that object) (?:is|belongs to) (.+)',p)
+ if not m:m=re.fullmatch(r'(?i)(.+?) implies (.+)',p)
+ if m:
+ from .reasoning_logic import LogicCA
+ grammar=LogicCA(reasoner().model)
+ source=grammar.noun(relation_atom(m[1]),plural=bool(re.match(r'(?i)^all\b',p)))
+ target=m[2].strip();neg=bool(re.match(r'(?i)^not ',target))
+ target=grammar.noun(relation_atom(re.sub(r'(?i)^not ','',target)),plural=bool(re.search(r'(?i)\bare(?: also)?\b',p)))
+ rules.append((source,target,neg));used.append(raw);continue
+ f=membership(p)
+ if f is None:raise TaskError('A local logical premise could not be compiled in full: '+p[:100])
+ facts.append(f);used.append(raw)
+ if not facts or len(facts)>128 or len(rules)>128:return None
+ mapping={}
+ def bound(kind,v):
+ key=(kind,v)
+ if key not in mapping:mapping[key]='native'+alphabet(len(mapping))+'q'
+ return mapping[key]
+ canonical=[f'{bound("entity",e)} is {"not " if neg else ""}{bound("property",p)}.' for e,p,neg in facts]
+ canonical += [f'Every {bound("property",a)} is {"not " if neg else ""}{bound("property",b)}.' for a,b,neg in rules]
+ query=f'{bound("entity",q[0])} is {"not " if q[2] else ""}{bound("property",q[1])}'
+ from .reasoning_logic import LogicCA,Unparsed
+ try:answer=LogicCA(reasoner().model).query(' '.join(canonical),query)
+ except Unparsed as exc:raise TaskError(str(exc)) from exc
+ return Result(answer['answer'],'logic',{'coverage':spans(text,parts),'facts':facts,'rules':rules,'query':q,
+ 'canonical_premises':canonical,'canonical_query':query,'proof':answer,'symbols':{f'{k[0]}:{k[1]}':v for k,v in mapping.items()}})
+
+def _order_query(q):
+ q=re.sub(r'(?i)^(?:question|query)\s*:\s*','',q.strip()).rstrip(' ?.').casefold()
+ m=re.search(r'\b(?:immediately|directly|right) (after|before|following|preceding) (.+?)(?: in (?:that|the) (?:sequence|order))?$',q)
+ if m:return ('after' if m[1] in ('after','following') else 'before',symbol(m[2]))
+ m=re.fullmatch(r'(?:name|give|identify|find|select|choose|which|what)(?: the| item| object| entry| is| comes| one| earliest| final)* (?:item )?(?:comes |is )?(first|last|earliest|latest|final)(?: item| one)?(?: in (?:that|the) (?:sequence|order))?',q)
+ if m:return ('first' if m[1] in ('first','earliest') else 'last',None)
+ if re.search(r'\b(?:earliest|first|final|last|latest) (?:item|object|entry)\b',q) and re.match(r'(?:name|give|identify|find|select|choose|which|what)\b',q):return ('unsupported',None)
+ m=re.fullmatch(r'(?:which|what) (?:item|object|entry) (?:comes|is) (?:in )?(?:position )?(\d+)(?:st|nd|rd|th)?',q)
+ if m:return ('index',int(m[1])-1)
+ m=re.fullmatch(r'(?:give|what is|find)(?: the)? (?:complete )?(?:order|sequence)',q)
+ if m:return ('all',None)
+ return None
+
+def order(text):
+ parts=clauses(text)
+ if len(parts)<2:return None
+ query=_order_query(parts[-1])
+ if query is None:return None
+ if not any(re.search(r'(?i)\b(?:before|after|ahead of|behind|precedes|follows)\b',p) for p in parts[:-1]):return None
+ boundary(parts[-1])
+ if query[0]=='unsupported':raise TaskError('The complete ordering question contains an unsupported qualifier.')
+ names=[];edges=[]
+ for raw in parts[:-1]:
+ p=raw.strip()
+ listed=re.fullmatch(r'(?i)(?:items|objects|entries|participants)\s*:\s*(.+)',p)
+ if listed:
+ names.extend(symbol(x) for x in re.split(r'\s*,\s*|\s+and\s+',listed[1]));continue
+ if re.fullmatch(r'(?i)(?:all|each) (?:items|objects|entries) (?:occur|occurs|appear|appears) once',p):continue
+ if re.fullmatch(r'(?i)(?:the following|these) (?:constraints|statements|clues) describe (?:their|the) order',p):continue
+ boundary(p)
+ p=re.sub(r'(?i) in the (?:sequence|order)$','',p)
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:comes |is |occurs |appears )?(before|after|ahead of|behind|precedes|follows) ({ATOM})(?: in the (?:sequence|order))?',p)
+ if not m:raise TaskError('An ordering constraint is unsupported or incomplete: '+p[:100])
+ a,b=symbol(m[1]),symbol(m[3]);relation=m[2].casefold()
+ if relation in ('after','behind','follows'):a,b=b,a
+ names.extend((a,b));edges.append((a,b))
+ names=list(dict.fromkeys(names))
+ if not 2<=len(names)<=64 or len(edges)>512:raise TaskError('Use 2–64 distinct items and at most 512 precedence constraints.')
+ reach={a:{b for x,b in edges if x==a} for a in names}
+ # Monotone relation-cell fixed point, not factorial permutation search.
+ for _ in range(len(names)):
+ following={a:reach[a]|set().union(*(reach[b] for b in reach[a])) if reach[a] else set() for a in names}
+ if following==reach:break
+ reach=following
+ if any(a in reach[a] for a in names):raise TaskError('The stated order contains a cycle; no linear order satisfies it.')
+ predecessors={b:{a for a in names if b in reach[a]} for b in names}
+ op,arg=query;possible=[]
+ if op=='first':possible=[a for a in names if not predecessors[a]]
+ elif op=='last':possible=[a for a in names if not reach[a]]
+ elif op=='index':
+ if not 0<=arg<len(names):raise TaskError('The requested position is outside the stated order.')
+ possible=[a for a in names if len(predecessors[a])<=arg<=len(names)-1-len(reach[a])]
+ elif op in ('after','before'):
+ if arg not in names:raise TaskError('The queried item is absent from the constraints.')
+ rel=reach if op=='after' else predecessors
+ # Adjacent candidates are precisely incomparable nodes or cover edges;
+ # if the anchor may be last/first, no next/previous item is guaranteed.
+ if not rel[arg]:possible=[]
+ else:possible=[b for b in names if b!=arg and arg not in rel[b] and not any(x in rel[arg] and b in rel[x] for x in names if x not in (arg,b))]
+ else:
+ if any(not (a in reach[b] or b in reach[a]) for i,a in enumerate(names) for b in names[i+1:]):possible=[]
+ else:possible=[', '.join(sorted(names,key=lambda a:len(predecessors[a])))]
+ value=possible[0] if len(possible)==1 else 'unknown'
+ return Result(value,'ordering',{'coverage':spans(text,parts),'entities':names,'edges':edges,'query':query,
+ 'transitive_relation':{a:sorted(v) for a,v in reach.items()},'possible_answers':possible,'unique':len(possible)==1})
+
+def _state_query(q):
+ q=re.sub(r'(?i)^(?:question|query)\s*:\s*','',q.strip()).rstrip(' ?.').casefold()
+ q=re.sub(r'^(?:after (?:the )?(?:last|final) (?:entry|event|update),?\s*)','',q)
+ m=re.fullmatch(r'(?:where (?:is|was)|(?:give|name|find|state|report|what is)(?: the)? (?:current|latest|final|present|last known) (?:location|position|room) (?:of|for)) (.+?)(?: now| currently| at the end)?',q)
+ if m:return ('location',symbol(m[1]))
+ m=re.fullmatch(r'who (?:has|holds|owns|is carrying) (?:the )?(.+)',q)
+ if m:return ('owner',symbol(m[1]))
+ return None
+
+def state(text,reasoner):
+ parts=clauses(text)
+ if len(parts)<2:return None
+ query=_state_query(parts[-1])
+ if query is None:return None
+ if not any(re.search(r'(?i)\b(?:went|moved|relocated|entered|arrived|walked|travelled|traveled|journeyed|is in|is at|holds|picked up|gave|gives|dropped|location becomes)\b',p) for p in parts[:-1]):return None
+ events=[];reverse=False
+ header_words=set('read this the following movement location log events event entries entry are is listed recorded ordered from earliest latest oldest newest to top bottom each replaces that person s previous position in chronological order timeline record updates update given all information complete'.split())
+ for raw in parts[:-1]:
+ p=re.sub(r'(?i)^(?:facts|events|log|timeline|context)\s*:\s*','',raw).strip()
+ if not p:continue
+ if re.fullmatch(r'(?i)(?:events|entries|updates)(?: are)? (?:listed |recorded )?(?:in )?(?:reverse chronological order|latest first|newest first)',p):reverse=True;continue
+ words=set(re.findall(r'[a-z]+',p.casefold()))
+ if words and words<=header_words and words&{'log','events','entries','chronological','updates'}:continue
+ boundary(p)
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:went|moved|relocated|walked|travelled|traveled|journeyed|returned)(?: back)? (?:to|into) (?:the )?({ATOM})',p)
+ if m:events.append(('move',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:entered|visited) (?:the )?({ATOM})',p)
+ if m:events.append(('move',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:is|was|is currently|was initially)(?: located)? (?:in|at|inside) (?:the )?({ATOM})',p)
+ if m:events.append(('move',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:arrived|arrives) at (?:the )?({ATOM})',p)
+ if m:events.append(('move',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) moved from (?:the )?({ATOM}?) to (?:the )?({ATOM})',p)
+ if m:events.append(('from',symbol(m[1]),symbol(m[2]),symbol(m[3])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:holds|has|got|picked up|takes|took) (?:the )?({ATOM})',p)
+ if m:events.append(('take',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:gave|gives|handed|hands|passed) (?:the )?({ATOM}?) to ({ATOM})',p)
+ if m:events.append(('give',symbol(m[1]),symbol(m[2]),symbol(m[3])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?) (?:dropped|drops|put down) (?:the )?({ATOM})',p)
+ if m:events.append(('drop',symbol(m[1]),symbol(m[2])));continue
+ m=re.fullmatch(rf'(?i)({ATOM}?)\x27s location becomes ({ATOM}?)\x27s current location',p)
+ if m:events.append(('copy',symbol(m[1]),symbol(m[2])));continue
+ raise TaskError('A chronological event could not be compiled in full: '+p[:100])
+ if not events or len(events)>128:raise TaskError('Use a nonempty log of at most 128 explicit events.')
+ if reverse:events.reverse()
+ mapping={};back={}
+ def name(v):
+ if v not in mapping:
+ mapped='native'+alphabet(len(mapping))+'q';mapping[v]=mapped;back[mapped]=v
+ return mapping[v]
+ from .reasoning_world import WorldCA
+ world=WorldCA(reasoner().model);canonical=[];known_actors=set();known_objects=set()
+ for index,event in enumerate(events,1):
+ op,actor,value,*extra=event
+ if actor in ('he','she','they','it'):
+ if len(known_actors)!=1:raise TaskError('A pronoun has more than one possible actor; name the person explicitly.')
+ actor=next(iter(known_actors))
+ known_actors.add(actor)
+ if op in ('take','drop','give'):
+ if value=='it':
+ if len(known_objects)!=1:raise TaskError('The object pronoun has no unique referent.')
+ value=next(iter(known_objects))
+ known_objects.add(value)
+ if op=='give':known_actors.add(extra[0])
+ if op=='copy':
+ cell=world.cells.get(name(value))
+ if cell is None or len(cell.locations)!=1:raise TaskError('A copied location is not uniquely known at that event.')
+ place=next(iter(cell.locations));event_text=f'{name(actor)} went to {place}'
+ elif op=='from':
+ cell=world.cells.get(name(actor))
+ if cell and cell.locations and cell.locations!={name(value)}:raise TaskError('A departure location conflicts with the preceding event state.')
+ event_text=f'{name(actor)} went to {name(extra[0])}'
+ elif op=='move':event_text=f'{name(actor)} went to {name(value)}'
+ elif op=='take':event_text=f'{name(actor)} got {name(value)}'
+ elif op=='drop':event_text=f'{name(actor)} dropped {name(value)}'
+ else:
+ old=world.cells.get(name(value))
+ if old and old.owner not in (None,name(actor)):raise TaskError('The giver is not the established holder of the object.')
+ event_text=f'{name(actor)} gave {name(value)} to {name(extra[0])}'
+ world.apply(world.event(event_text),index);canonical.append(event_text+'.')
+ target_value=query[1]
+ if target_value in ('he','she','they','it'):
+ referents=known_objects if query[0]=='owner' else known_actors
+ if len(referents)!=1:raise TaskError('The question pronoun has no unique referent.')
+ target_value=next(iter(referents))
+ target=name(target_value);q=('Where is '+target if query[0]=='location' else 'Who holds '+target)+'?'
+ result=WorldCA(reasoner().model).query(' '.join(canonical),q)
+ value=back.get(result['answer'],result['answer'])
+ return Result(value,'state',{'coverage':spans(text,parts),'events':events,'reverse_source_order':reverse,
+ 'canonical_events':canonical,'query':query,'proof':result,'symbols':mapping})