# MIT License
# 
# Copyright (c) 2026
# 
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
# 
# The above copyright notice and this permission notice shall be included in all
# copies or substantial portions of the Software.
# 
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.
# 
# Third-party exception: bitmap glyph data derived from Noto Sans CJK is licensed
# under the SIL Open Font License 1.1. See assets/NOTO-LICENSE.txt.

"""すれ違い日記・教材1/5。Python 3.11+、単独実行用。"""
from dataclasses import dataclass, asdict, replace
from itertools import product, combinations
import hashlib, json

def worlds(keys, domains, predicate=lambda w: True):
    return tuple((tuple(sorted(dict(zip(keys, values)).items())) for values in product(*domains) if predicate(dict(zip(keys, values)))))

def claim(**kw):
    return tuple(((k, (v,)) for k, v in kw.items()))

A_W = worlds(('delivered', 'mover', 'dest', 'shelter'), ((0, 1), ('none', 'mina', 'sora'), ('none', 'R', 'K'), (0, 1)), lambda w: w['delivered'] == 0 and w['mover'] == 'none' and (w['dest'] == 'none') or (w['delivered'] == 1 and w['mover'] != 'none' and (w['dest'] != 'none')))

def fits(world, claims):
    w = dict(world)
    return all((w[k] in allowed for k, allowed in claims))

STAGE = 1

# Two disclosed facts from A, used as a PUBLIC experiment, not secret answers.
LAB_FACTS = (claim(mover='sora'), claim(dest='K'))
LAB_LABELS = ('SORA MOVED THE PARCEL', 'THE PARCEL WAS DRIED AT K')
START_MASK = 0

def lab_remaining(mask):
    return tuple(w for w in A_W if all(fits(w, c) for i,c in enumerate(LAB_FACTS) if mask >> i & 1))

def verdict(options, claims):
    matches = [fits(w, claims) for w in options]
    if not any(matches):
        return 'IMPOSSIBLE'
    return 'ENTAILED' if all(matches) else 'POSSIBLE, NOT ENTAILED'

class App:
    def __init__(self):
        self.reset()
    def reset(self):
        self.mask = START_MASK
        self.cursor = 0
        self.gated = False
        self.message = 'TRY EACH FACT SEPARATELY, THEN COMBINE THEM.'
    def snapshot(self):
        return {'mask':self.mask, 'worlds':len(lab_remaining(self.mask)), 'verdict':verdict(lab_remaining(self.mask), claim(mover='sora', dest='K'))}
    def control(self, pressed, held):
        if self.gated:
            if not pressed and not held: self.gated = False
            return
        if len(pressed | held) > 1:
            self.gated = True
            self.message = 'CONFLICT: RELEASE ALL KEYS'
            return
        if len(pressed) != 1: return
        key = next(iter(pressed))
        self.gated = True
        if key == 'R':
            self.reset(); self.gated = True
        elif key in ('LEFT','RIGHT'):
            self.cursor = 1 - self.cursor
        elif key == 'SPACE':
            self.mask ^= 1 << self.cursor
            self.message = 'EVIDENCE CHANGED. NO SINGLE HIDDEN ANSWER IS CHOSEN.'
    def draw(self, p):
        p.cls(1)
        p.text(16, 14, '064 CROSSED DIARIES / 01 FINITE WORLD LAB', 10)
        p.text(16, 40, 'A PUBLIC EXPERIMENT: TWO FACTS ARE ALREADY DISCLOSED.', 6)
        for i,label in enumerate(LAB_LABELS):
            y = 76 + i*34
            p.rect(14, y-8, 612, 26, 3 if self.cursor == i else 2)
            p.text(24, y, ('[USED] ' if self.mask >> i & 1 else '[ -- ] ')+label, 11 if self.mask >> i & 1 else 7)
        options = lab_remaining(self.mask)
        p.text(16, 158, 'REMAINING WORLDS: '+str(len(options))+' / '+str(len(A_W)), 10)
        p.text(16, 180, 'CLAIM: SORA MOVED THE PARCEL TO K', 7)
        p.text(16, 198, verdict(options, claim(mover='sora', dest='K')), 11)
        p.text(16, 230, 'EVERY REMAINING WORLD MUST SATISFY A CLAIM TO ENTAIL IT.', 6)
        p.text(16, 252, 'MOVER AND DESTINATION IN THE REMAINING HYPOTHESES:', 7)
        pairs = sorted({(dict(w)['mover'], dict(w)['dest']) for w in options})
        for i,(who,where) in enumerate(pairs):
            p.text(24 + (i//4)*300, 276+(i%4)*22, who.upper()+' -> '+where, 7)
        p.text(16, 382, 'Different SHELTER values can remain after proof.', 13)
        p.text(16, 408, self.message, 10)
        p.text(16, 454, 'LEFT/RIGHT SELECT FACT   SPACE USE/REMOVE   R RESET', 7)
        p.text(16, 476, 'ESC QUIT / SAVE CODE, QUIT, THEN RERUN TO SEE EDITS', 6)

def demo_keys():
    return ('SPACE', 'RIGHT', 'SPACE')

def main(headless=False, screenshot=None, demo=False, state_json=None):
    # Pyxel changes cwd during import/init. Resolve EVERY output first.
    from pathlib import Path
    if demo and not headless:
        raise ValueError('demo requires --headless-smoke')
    outputs = []
    for value, suffix in ((screenshot, '.png'), (state_json, '.json')):
        if value is None:
            outputs.append(None)
            continue
        target = Path(value).resolve()
        if not headless or target.suffix.lower() != suffix or not target.parent.is_dir() or target.exists():
            raise ValueError('output needs headless mode, matching suffix, existing parent, and a new file')
        outputs.append(str(target))
    screenshot, state_json = outputs
    import pyxel as p
    p.init(640, 500, title='Crossed diaries / lesson '+str(STAGE), fps=30, display_scale=1, headless=headless)
    app = App()
    sequence = demo_keys() if demo else ()
    names = ('UP','DOWN','LEFT','RIGHT','Z','SPACE','RETURN','TAB','H','X','R','1','2','3')
    keys = {name: getattr(p, 'KEY_'+name) for name in names}
    limit = max(12, len(sequence)*2+6)
    def update():
        if p.btnp(p.KEY_ESCAPE) or headless and p.frame_count >= limit:
            if screenshot:
                app.draw(p)
                p.screen.save(screenshot, 1)
            if state_json:
                # x mode is also a last-moment overwrite guard.
                with open(state_json, 'x', encoding='utf-8') as stream:
                    json.dump(app.snapshot(), stream, ensure_ascii=False, indent=2)
            p.quit()
            return
        if headless:
            index = p.frame_count//2
            pressed = {sequence[index]} if p.frame_count%2 == 0 and index < len(sequence) else set()
            app.control(pressed, pressed)
        else:
            app.control({k for k,v in keys.items() if p.btnp(v)}, {k for k,v in keys.items() if p.btn(v)})
    p.run(update, lambda: app.draw(p))

if __name__ == '__main__':
    import argparse
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--headless-smoke', action='store_true')
    parser.add_argument('--demo-checkpoint', action='store_true')
    parser.add_argument('--screenshot')
    parser.add_argument('--state-json')
    args = parser.parse_args()
    try:
        main(args.headless_smoke, args.screenshot, args.demo_checkpoint, args.state_json)
    except ValueError as error:
        parser.error(str(error))