tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

StableConstructorK.hs (8265B)

      1 {-# LANGUAGE BangPatterns #-}
      2 -- Independent finite oracle for constructor-only K pruning. The model stores
      3 -- full free-variable sets (not the portable minimum-index cache). It retains
      4 -- a no-shortcut baseline and checks complete results, not DAG sizes.
      5 module Main where
      6 import Runtime
      7 import Wire
      8 import TreeObservation
      9 import qualified Data.ByteString as BS
     10 import qualified Data.Vector as V
     11 import qualified Data.Text as Text
     12 import qualified Data.Map.Strict as M
     13 import qualified Data.IntSet as S
     14 import Control.Monad
     15 import System.Environment
     16 load path = do
     17  bytes<-BS.readFile path
     18  b<-either error pure(decodeBundle bytes)
     19  either error pure(verifyBundle b)
     20  let ts=reconstructBundleTerms(bundleNodes b)
     21  pure $ M.fromList[(Text.unpack(exportName e),ts V.! fromIntegral(exportRoot e))|e<-manifestExports(bundleManifest b)]
     22 p1(Fork a _)=a
     23 p1 _=error "pair"
     24 p2(Fork _ b)=b
     25 p2 _=error "pair"
     26 result(Fork (Stem Leaf) (Fork v _))=v
     27 result _=error "portable failure"
     28 list=either error id . toList
     29 number t=fromInteger(either error id(toNumber t))::Int
     30 payload=p1.p2
     31 -- Shape -1: unproved computation; -2: opaque value (free variable).
     32 -- 0/1/2: proved Leaf/Stem/Fork. Applications require safe operands and a
     33 -- known Leaf/Stem function; a Fork application is NEVER certified.
     34 data Term = Term !Int !S.IntSet !Int Residual
     35 data Residual = Lit T | Var Int | App Term Term
     36 shape(Term s _ _ _)=s
     37 vars(Term _ v _ _)=v
     38 size(Term _ _ n _)=n
     39 lit t=Term (case t of Leaf->0;Stem _->1;Fork _ _->2) S.empty 1 (Lit t)
     40 var n=Term (-2) (S.singleton n) 1 (Var n)
     41 app a b=Term sh (S.union(vars a)(vars b)) (1+size a+size b) (App a b)
     42  where sh=if shape b/=(-1) && shape a `elem` [0,1] then shape a+1 else -1
     43 foldApp a@(Term _ _ _ (Lit f)) b@(Term _ _ _ (Lit x))=case f of
     44  Leaf->lit(Stem x)
     45  Stem y->lit(Fork y x)
     46  _->app a b
     47 foldApp a b=app a b
     48 k=lit(Stem Leaf)
     49 i=lit(Fork(Stem(Stem Leaf))Leaf)
     50 application l r=foldApp (foldApp (lit Leaf)(foldApp(lit Leaf)l)) r
     51 -- Baseline abstraction deliberately has no K/eta shortcuts.
     52 baseline term@(Term _ _ _ node)=case node of
     53  Lit _->foldApp k term
     54  Var 0->i
     55  Var n->foldApp k(var(n-1))
     56  App a b->application(baseline a)(baseline b)
     57 run(Term _ _ _ node)=case node of
     58  Lit t->t
     59  Var _->error "open output"
     60  App f x->apply(run f)(run x)
     61 lower term@(Term _ _ _ n)=case n of
     62  Lit _->term
     63  Var v->if v>0 then var(v-1) else error "lowered used binder"
     64  App a b->app(lower a)(lower b)
     65 eligible term@(Term sh vs _ node)=case node of
     66  App _ _->sh/=(-1) && not(S.member 0 vs)
     67  _->False
     68 safeBracket term@(Term _ _ _ node)
     69  | eligible term=foldApp k(lower term)
     70  | otherwise=case node of
     71     Lit _->foldApp k term
     72     Var 0->i
     73     Var n->foldApp k(var(n-1))
     74     App a b->application(safeBracket a)(safeBracket b)
     75 encodeTerm (Term _ _ _ n)=case n of
     76  Lit t->node 1 t
     77  Var v->node 2(ofNumber(fromIntegral v))
     78  App a b->node 3(Fork(encodeTerm a)(encodeTerm b))
     79  where node k p=Fork(ofNumber k)(Fork p Leaf)
     80 checkMetadata term annotated=do
     81  let wantedShape=case shape term of -1->0; -2->4; n->n+1
     82      wantedBound=if S.null(vars term) then 0 else S.findMin(vars term)+1
     83  unless(number(p1(p1 annotated))==wantedShape && number(p2(p1 annotated))==wantedBound)(error "cached summary mismatch")
     84  case term of
     85   Term _ _ _ (App a b)->do
     86    let children=payload(p2 annotated)
     87    checkMetadata a(p1 children)
     88    checkMetadata b(p2 children)
     89   _->pure ()
     90 main=do
     91  [bundle,referenceBundle]<-getArgs
     92  portable<-load bundle
     93  let abstract=apply(portable M.! "stableBracket")
     94  forceTreeShared(portable M.! "stableBracket")
     95  let leaf=lit Leaf
     96      unknown=app(var 1)(var 2)
     97      checks=[("open stem",app leaf(var 1),True),
     98              ("open fork",app(app leaf(var 1))(var 2),True),
     99              ("third argument",app(app(app leaf(var 1))(var 2))(var 3),False),
    100              ("unknown function",unknown,False),
    101              ("unsafe child",app leaf unknown,False),
    102              ("used binder",app leaf(var 0),False),
    103              ("known stem",app(lit(Stem Leaf))(var 1),True)]
    104  forM_ checks $ \(name,t,expected)->unless(eligible t==expected)(error name)
    105  let atoms=[var 0,var 1,var 2,leaf,lit(Stem Leaf),lit(Fork Leaf Leaf),i]
    106      level1=atoms++[foldApp a b|a<-atoms,b<-atoms]
    107      terms=filter ((/=(-1)).shape)(atoms++[foldApp a b|a<-level1,b<-level1])
    108      values=[Leaf,Stem Leaf,Fork Leaf Leaf]
    109  forM_ terms $ \body->do
    110    let step expected actual n=do
    111         checkMetadata expected actual
    112         unless(apply(portable M.! "stableCachedToPlain")actual==encodeTerm expected)(error "cached residual mismatch")
    113         when(n>0)(step(safeBracket expected)(apply(portable M.! "stableCachedBracket")actual)(n-1))
    114    step body (apply(portable M.! "stableCachedFromPlain")(encodeTerm body)) (3::Int)
    115    let old=iterate baseline body!!3
    116    forM_ (take 3(iterate safeBracket body)) $ \term ->
    117     unless(abstract(encodeTerm term)==encodeTerm(safeBracket term))(error "portable/model abstraction differs")
    118    let new=iterate safeBracket body!!3
    119        oldTree=run old;newTree=run new
    120    forceTreeShared oldTree
    121    forceTreeShared newTree
    122    forM_ values $ \a->forM_ values $ \b->forM_ values $ \c->
    123     unless(foldl apply oldTree[a,b,c]==foldl apply newTree[a,b,c])(error "nested abstraction changed result")
    124  -- Sparse/high indices and unsafe applications exercise summary maintenance
    125  -- without assuming application termination. Compare cached annotations after
    126  -- each abstraction, not after re-importing ordinary residuals.
    127  let mixed=[app(lit Leaf)(var v)|v<-[0,1,7,63,256]]++
    128            [app(var 7)(var 63),app(lit(Fork Leaf Leaf))(var 7),
    129             app(lit Leaf)(app(var 7)(var 63)),
    130             app(app(lit Leaf)(var 63))(var 0)]
    131  forM_ mixed $ \body->do
    132   let step expected actual n=do
    133        checkMetadata expected actual
    134        unless(apply(portable M.! "stableCachedToPlain")actual==encodeTerm expected)(error "sparse/unsafe residual mismatch")
    135        when(n>0)(step(safeBracket expected)(apply(portable M.! "stableCachedBracket")actual)(n-1))
    136   step body (apply(portable M.! "stableCachedFromPlain")(encodeTerm body)) (4::Int)
    137  -- An opaque variable is only stored, never invoked or forced by a constructor.
    138  let poison=error "opaque argument forced"::T
    139      saved=run(safeBracket(safeBracket(app leaf(var 1))))
    140  case apply(apply saved poison)Leaf of Stem _->pure();_->error "opaque constructor"
    141  -- omega has a Fork function: it must not be evaluated during construction.
    142  let ident=Fork(Stem(Stem Leaf))Leaf
    143      self=Fork(Stem ident)ident
    144      omega=app(lit self)(lit self)
    145  unless(not(eligible omega) && not(eligible(app leaf omega)))(error "omega certified")
    146  forceTreeShared(run(safeBracket omega))
    147  -- Full portable bracket construction, without executing omega.
    148  forceTreeShared(abstract(encodeTerm omega))
    149  -- Demand-sensitive checks run actual portable-produced function trees too.
    150  let node kind value=Fork(ofNumber kind)(Fork value(Fork Leaf Leaf))
    151      lambda body=node 4 body
    152      applyCore a b=node 3(Fork a b)
    153      portableSaved=result(apply(portable M.! "stableCompileCore")
    154        (lambda(lambda(applyCore(node 1 Leaf)(node 2(ofNumber 1))))))
    155  forceTreeShared portableSaved
    156  case apply(apply portableSaved poison)Leaf of Stem _->pure();_->error "portable opaque constructor"
    157  let portableOmega=result(apply(portable M.! "stableCompileCore")
    158        (lambda(applyCore(node 5 self)(node 5 self))))
    159  forceTreeShared portableOmega
    160  let portableEta=result(apply(portable M.! "stableCompileCore")
    161        (lambda(applyCore (applyCore(node 5 self)(node 5 self)) (node 2 Leaf))))
    162  forceTreeShared portableEta
    163  reference<-load referenceBundle
    164  let core kind value=Fork(ofNumber kind)(Fork value(Fork(ofNumber 23)(ofNumber 24)))
    165      badVariable=core 2(ofNumber 3)
    166      invalid=core 99 Leaf
    167      application a b=core 3(Fork a b)
    168  forM_ [badVariable,invalid,application badVariable invalid,application(core 1 Leaf)invalid] $ \input->
    169   unless(apply(portable M.! "stableCompileCore")input==apply(reference M.! "source_stable.stableCompileCore")input)(error "core diagnostic/remainder mismatch")
    170  putStrLn("PASS: "++show(length terms)++" constructor bodies under three nested binders; "++show(length terms*27)++" complete application results; classification, sparse indices, opaque arguments, K/eta construction hazards and diagnostic controls")