igor.ey

#!/home/drahflow/elymas/elymas/loaded

{ { _ sys .asm .rawAddress txt .produce .u defv }' scope }
<
  /generate deffd
  0 ==m # placeholder, zero value is never read
  { =m [ m .v keys { m .v -01 . } each ] }' "#dom" defmd
  { =m m .v ==v =*f v keys { v -01 . f }' each } "#each" defmd
  { 0 } "#istart" deffd
  { =m m .v keys len eq }' "#iend" defmd
  { 1 add }" "#istep" deffd
  { =m m .v keys * }' "#itrans" defmd
  { =m m .v -01 sys .asm .rawAddress txt .produce .u .?' }' /has defmd
  { =m m .v ==v "#iclone" | * ==n v keys { _ v -01 . -01 n =[] } each n }' /clone defmd
  { < generate ==v "put" =* > }' _ "#iclone" deffd
> -- /objset deffd

{ ==y ==x 1 y { x mul } rep } /exp deffst

{ 0 }" ==:ANDIF_ZERO
<
  sys .|executeIdentifier "~" deffd
  { quoted { ~ANDIF_ZERO "?" ~ "*" ~ ~not ~not } { { 0 } ? * not not } ? * }
> -- /andif defq

<
  [ ] ==a [ ] ==b
  { =a =b
    a len b len eq {
      1 a dom { _ a * -01 b * eq and }" each
    }" { 0 }" ? *
  }'
> -- /arrEq deffd

{ "}" | *
  { ==f 0 ==running
    { f } { * }" ; { =*f { running not { 1 =running f 0 =running } rep } } ;
  } *
}" "}!" defq

map ==constants
map ==assertions
objset ==blocks
{ # ==parentBlock
  < map ==f map ==e list ==d map ==v _ ==parent >' _ blocks .put
} /childBlock deffd
< > childBlock _ ==emptyBlock ==currentBlock

< map ==:cache { _ cache .has not { _ _ cache =[] }" rep cache * }' > -- /makeUnique deffd

<
  { sys .linux .gettimeofday -- 1000000 mul add } /t deffd
  < { == }' > ==time =*setTime
  < { == }' > ==count =*setCount
  { ==l 0 l setTime 0 l setCount
    { =*f { t ==start f t start sub time l . add l setTime count l . 1 add l setCount } }
    quoted not { * } rep
  }
  {
    time keys _ { ==b ==a time a . time b . lt } order -01* {
      [ -01 ==k
        k time -01 . txt .produce .u " μs "
        k count -01 . txt .produce .u " calls "
        k
      ] |cat fold dump
    } each
  }
> -- /perfstats deffd -- { -- } "τ" defq

{ ==n =*f { n dump f "/" n cat dump } } "δ" deffst

<
  { -- } "$$" defq # { ==name _ "$" name cat " " cat -01 cat dump } "$$" deffd

  txt .consume .|hu "%" defq
  { "2120" "-" | |le "021" "-" | |ge |and } /in defq
  { "Unconfigured peek/take/get/set/noErr/snip" die } -000000 =*peek =*take =*get =*set =*noErr =*snip { } =*setupInput
  { | { ==:f /f sys .executeIdentifier _ * -- } * }" "@" deffd
  str .|infix =*:infix

  # parser generator
  { _ sys .typed .type 1 eq { ==str { 1 ==r str { peek eq r and =r take }' each r _ |noErr rep }' } { }" ? * } /lit deffd
  { lit =*p { get , p { --, ,-- }" { ,--- set }" ? * 1 }' } ",?" deffd
  { lit =*p { { get , p }' { --, ,-- }' loop ,--- set 1 }' } ",*" deffd
  { _ ,* ,; } ",+" deffd
  { lit =*q lit =*p { get , p { --, ,-- 1 }" { ,--- set q }" ? * }' } ",|" deffd
  { lit ==q lit =*p { p q { 0 }" ? * }' } ",;" deffd
  { [ [ }" { ] |lit each ] ",;" | fold }" -01 ",[" deffd ",]" deffd
  { defvst }' =*:defp
  {
    ==name "}'" | * { ,[ }' -01 ; { ,] }' ; { * _ name "_make" cat defp * }_ name "_make" cat defp
    "{" | * name "_make" cat "|" | "*" | "}'" | * name defp
  } "}==" defq
  "{" | "(" defq { 1 "}'" | * }' ")" defq

  { lit =*p lit =*q {
    { get , p { ,--- _ set , 0 }" { ,--- _ set , q }" ? * }' { --, ,-- }' loop ,--- set 1
  }' } /upto deffd

  # compare Specification of the Metamath Language
  { { peek take %24 neq }' { }' loop 1 }" ==sequenceEndingInDollar
  { peek take ==c c %09 eq c %0A eq or c %0C eq or c %0D eq or c %20 eq or } ==whitechar
  { peek take ==c c %41 %5A in c %61 %7A in or c %30 %39 in or c %2D eq or c %5F eq or c %2E eq or } ==labelchar
  { peek take ==c c %41 %5A in c %3F eq or } ==compressedchar
  { peek take ==c c %24 neq c %20 gt and c %7F lt and } ==mathchar

  { "$(" sequenceEndingInDollar ")" upto ")" white }==comment
  { whitechar comment ,| include ,| ,+ }==white
  { "$[" white ( |setupInput get ) mathchar ,* (
    get snip "including: " -1101 cat dump parseFile "finished " -01 cat dump _ =setupInput *
  ) white "$]" white }==include

  { ( get ) mathchar ,+ ( get snip makeUnique ) white }==mathsymbol
  { ( get ) labelchar ,+ ( get snip makeUnique ) white }==label

  { "$c" white ,[ mathsymbol ( $$c 1 -01 constants =[] ) ,] ,+ "$." white }==cstatement
  { "$v" white ,[ mathsymbol ( $$v 1 -01 currentBlock .v =[] ) ,] ,+ "$." white }==vstatement
  { label "$f" white ( $$f [ ) mathsymbol mathsymbol ( ] -01 currentBlock .f =[] ) "$." white }==fstatement
  { label "$e" white ( $$e [ ) mathsymbol mathsymbol ,* ( ] -01 currentBlock .e =[] ) "$." white }==estatement
  { "$d" white ( [ ) mathsymbol mathsymbol ,+ ( ] currentBlock .d .append1 ) "$." white }==dstatement
  { label "$a" white ( $$a [ ) mathsymbol mathsymbol ,* ( ]
    < "a" ==type currentBlock ==ctx ==thm { "Assumption has no proof" die }" =*proof _ ==name
      { mandatoryHypotheses ==hyps }' { mandatoryDisjunct ==disj }' { allDisjunct ==allDisj }' > -01*02*03*0
    -01 assertions =[] ) "$." white
  }==astatement

  { "?" ( "?" ) white }==questionmark
  { ( [ ) label questionmark ,| ,* ( ] { -- }_ ) }==proof
  { "(" white ( [ ) label ,* ( ] ) ")" white ( [ ) ,[ ( get ) ,[ compressedchar ,] ,+ ( get snip ) white ,] ,* ( ] |cat fold
    < ==data _ ==labels len ==labelCount { _ ==hypotheses len ==hypCount
      [ 0 data { ==c
        [
          { c %41 ge c %54 le and } { 20 mul c %40 sub add _ dump ==n
          [
            { n 1 sub hypCount lt } { n 1 sub hypotheses * }
            { n 1 sub hypCount sub labelCount lt } { n 1 sub hypCount sub labels * }
            { 1 } { n 1 sub hypCount sub labelCount sub txt .produce .u "@ " -01 cat }
          ] conds
          0 }
          { c %55 ge c %59 le and } { 5 mul c %54 sub add _ dump }
          { c %5A eq } { -- "!" 0 }
          { c %3F eq } { -- "?" 0 }
          { 1 } { "Invalid compressed proof" die }
        ] conds
      } each -- ]
    } > -- ) }==compressedproof
  { label "$p" white ( $$p [ ) mathsymbol mathsymbol ,* ( ] ) "$="
    white compressedproof proof ,| (
    < "p" ==type currentBlock ==ctx -01 ==thm =*proof _ ==name
      { mandatoryHypotheses ==hyps }' { mandatoryDisjunct ==disj }' { allDisjunct ==allDisj }' > -01*02*03*0
    # -101 "simpl31" eq { perfstats "done" die } rep
    # -101 "vtoclga" eq { perfstats "done" die } rep
    # _ "a17d" eq { -101 verifyProof "done" die } rep # TODO: this line is just debugging
    # -100 verifyProof dump
    -01 assertions =[] ) "$." white
  }==pstatement

  { "${" ( currentBlock childBlock =currentBlock ) white statements ( currentBlock .parent =currentBlock ) "$}" white }==block
  { [ estatement pstatement dstatement block vstatement fstatement astatement cstatement white ] ",|" | fold ,* }==statements

  { ":" via
    "" ==s 0 ==i 0 ==slen 0 ==last 0 ==eof
    {
      {
        i slen lt not {
          eof not {
            s 1024 1024 mul :read cat =s
            s len _ =slen
                    txt .produce .u "Just read to: " -01 cat dump }" rep
        }" rep
        i slen lt { i s * }" { 1 neg 1 =eof }" ? *
      }' =peek
      { i 1 add =i }' =take { i }' =get { =i }' =set { i =last }' =noErr { s infix }' =snip
    } _ =setupInput *

    { statements * { i s len neq { ??metamath.trailing-garbage } rep } { ??metamath } ? * }
      { -- < last s str .postfix ==remaining > ??!' } ?!metamath
  }
> -- /parse deffd

{ sys .file _ ":" via -01 :open parse :close } /parseFile deffd

{ ==ctx ==sym 0 ==found { ctx .?'v found not and }' { sym ctx .v ==v v .has found or =found ctx .parent =ctx }' loop found } /isVar deffd
{ ==ctx ==lbl 0 ==found { ctx .?'e found not and }' { lbl ctx .e ==e e .has found or =found ctx .parent =ctx }' loop found } /isEHyp deffd
{ ==ctx ==lbl 0 ==found { ctx .?'f found not and }' { lbl ctx .f ==f f .has found or =found ctx .parent =ctx }' loop found } /isFHyp deffd
{ -01 ==lbl { _ .e lbl -01 .has not }' { .parent }' loop .e lbl -01 * } /getEHyp deffd
{ -01 ==lbl { _ .f lbl -01 .has not }' { .parent }' loop .f lbl -01 * } /getFHyp deffd
{ constants .has }' /isConst deffd

{ _ ==pstm .ctx ==ctx map _ ==vars # will be returned
  { ==sym [
    { sym ctx isVar }' { 1 sym vars =[] }'
    { sym isConst }' { }'
    { 1 }' { "Undeclared symbol: " sym cat die }'
  ] conds } ==collect

  pstm .thm collect each
  ctx { _ .?'e }' { _ .e { collect each }' each .parent }' loop --
} /mandatoryVariables deffd

{ _ ==pstm mandatoryVariables ==vars list _ ==hyps # will be returned
  [ pstm .ctx { _ .?'e }' { _ .parent }' loop -- ] reverse ==ctxs
  ctxs { _ ==ctx .f dom { _ ==k ctx .f * 1 -01 * vars .has { k hyps .append1 }' rep } each } each
  ctxs { .e dom { hyps .append1 }' each }' each
} /mandatoryHypotheses deffd

{ ==pstm list _ ==disj # will be returned
  [ pstm .ctx { _ .?'d }' { _ .parent }' loop -- ] reverse ==ctxs
  ctxs { .d { _ len ==l ==dstm
    0 l range { ==i
      i 1 add l range { ==j
        [ i dstm * j dstm * ] disj .append1
      } each
    } each
  } each }' each
} /allDisjunct deffd

{ _ ==pstm mandatoryVariables ==vars list _ ==disj # will be returned
  # "Vars: " dump
  # vars dom dump
  [ pstm .ctx { _ .?'d }' { _ .parent }' loop -- ] reverse ==ctxs
  ctxs { .d {
    ==dstm
    0 dstm len range { _ ==i dstm * vars .has {
      i 1 add dstm len range { _ ==j dstm * vars .has {
        [ i dstm * j dstm * ] disj .append1
      }' rep } each
    }' rep } each
  } each }' each
} /mandatoryDisjunct deffd

{ _ ==pstm _ .hyps ==hyps .disj ==disj
  "Mandatory hyps: " dump
  hyps |dump each
  "Mandatory disjunct: " dump
  disj |dump each
  "^^^^^^^^^^^^^^^^^^^" dump

  hyps pstm .proof
} /computeProof deffd

{ _ ==pstm _ .ctx ==ctx computeProof
    list ==stack # the verification stack
    list ==savedTheorems # Z-saved theorems
  { ==lbl
    [
      { lbl ctx isEHyp } { lbl ctx getEHyp stack .append1 }
      { lbl ctx isFHyp } { lbl ctx getFHyp stack .append1 }
      { lbl "!" eq } { stack len 1 sub stack * savedTheorems .append1 }
      { lbl len _ { -- 0 lbl * 0 "@" * eq } rep }
        { 2 lbl str .postfix txt .consume .u savedTheorems * stack .append1 }
      { lbl assertions .has } {
        "Applying: " lbl cat dump

        lbl assertions * _ ==ass .hyps ==hyps
        map ==substitution

        "Mandatory hypotheses:" dump
        hyps dump
        0 hyps len range
          _ { hyps * dump } each
        _ { _ ==i hyps * _ ==h ass .ctx isFHyp {
            h ass .ctx getFHyp ==mask
            stack len hyps len sub i add stack * ==target
            0 mask * 0 target * neq { mask dump target dump "Constant symbol mismatch" die } rep
            [ 1 target len range { target * } each ] 1 mask * substitution =[]
          } rep } each

          substitution dom { ==k k " => " cat k substitution * { " " -01 cat cat } fold cat dump } each

          { _ ==i hyps * _ ==h ass .ctx isEHyp {
              stack len hyps len sub i add stack * ==target
              [ h ass .ctx getEHyp { # ==sym
                _ ass .ctx isVar { substitution * _ len dearray } rep
              } each ] ==mask
              mask target arrEq not { mask dump target dump "Hypthesis does not match stack" die } rep
          } rep } each

        ass .disj { =*d
          "Checking disjunct " 0 d cat " <=> " cat 1 d cat dump
          0 d substitution * { ass .ctx isVar } grep { ==v
            1 d substitution * { ass .ctx isVar } grep { ==w
                v " :=: " w cat cat dump
                v w eq { "Disjunct variable requirement broken" die } rep
                [ pstm .allDisj { =*d 0 d v eq 1 d w eq and 0 d w eq 1 d v eq and or } each ] any not
                  { "Disjunct variable requirement not carried" die } rep
            } each
          } each
        } each

        "All checks ok. Inserting new statement." dump

        hyps len { stack .pop } rep
        [ ass .thm { _ ass .ctx isVar { substitution * _ len dearray } rep } each ] stack .append1
      }
      { 1 } { "Invalid proof step: " lbl cat die }
    ] conds

    "Proof stack" dump
    stack { { " " -01 cat cat } fold dump } each
    "^^^^^^^^^^^" dump
  } each

  [
    { stack len 1 neq } { "Stack not empty after proof." dump 0 }
    { 0 stack * pstm .thm arrEq not } { "Final stack contents: " dump 0 stack * dump "and theorem: " pstm .thm dump "do not match" dump 0 }
    { 1 } { 1 }
  ] conds
} /verifyProof deffd

{
  sys .argv len [ 2 3 ] eq any not { "usage: ./igor input.mm [contination freeze]" die } rep
  1 sys .argv * parseFile
} { _ dump _ keys dump .remaining die } ?!metamath


{ =*f 0 ==computed "" ==?result {
  computed not { 1 =computed f =result }" rep
  result
}' } /memoized deffst

{ map _ ==variables # returned
  blocks { .f _ =*d dom
    { _ ==n d _ 0 -01 * ==nonterminal 1 -01 * ==var
      nonterminal var variables =[]
    } each
  } each
} memoized /variables deffd

{ ==ctx map _ ==result # returned
  [ ctx { _ .?'e }' { _ .parent }' loop -- ] reverse ==ctxs
  ctxs { _ ==c .f _ =*fs dom { _ fs -01 result =[] } each } each
} /collectFHyps deffst

{ ==ctx map _ ==result # returned
  [ ctx { _ .?'e }' { _ .parent }' loop -- ] reverse ==ctxs
  ctxs { _ ==c .e _ =*es dom { _ es -01 result =[] } each } each
} /collectEHyps deffst

{
  map ==nonterminals
  map ==variableNonTerminals # nonterminal -> variable -> theorem name

  blocks { .f _ =*d dom
    { _ ==thm d _ 0 -01 * ==nonterminal 1 -01 * ==var
      nonterminal variableNonTerminals .has not { map nonterminal variableNonTerminals =[] } rep
      nonterminal variableNonTerminals * ==variableTypedefs # variable -> theorem name

      var variableTypedefs .has { var variableTypedefs * len thm len gt } { 1 } ? *
        { thm var variableTypedefs =[] } rep
    } each
  } each

  map ==relevantRules # nonterminal -> [ assertion ... ]
  map ==singularRules # token -> nonterminal (for when only a single token is expanded, this is only an optimization)
  [ "/" ] ==:NONTRIVIALSINGULARTOKENS # / as in [ A / x ] ph is _not_ in fact a class, but / as in 6 / 3 is.
  assertions dom { assertions * ==a
    a .type "a" eq {
      0 a .thm * _ ==nt variableNonTerminals .has {
        a .ctx collectEHyps dom len 0 eq {
          a .thm len 2 eq { 1 a .thm * constants .has } andif
              { 1 a .thm * NONTRIVIALSINGULARTOKENS eq any not } andif {
            a 1 a .thm * singularRules =[]
          } {
            1 a .thm len range a .thm * ==expectedTokens
            nt relevantRules .has not { [ ] nt relevantRules =[] } rep
            nt relevantRules * [ a ] cat nt relevantRules =[]
          } ? *
        } rep
      } rep
    } rep
  } each

  parser .glr ":" via
  map ==parserNonterminals
  variableNonTerminals dom { ==nt nt :nonterminal nt parserNonterminals =[] } each
  variableNonTerminals dom { ==nt
    nt parserNonterminals *
    [ " " nt cat ] # terminal for variable and singularRules tokens
    { :0 }' # keep value
    :rule

    nt relevantRules .has {
      nt relevantRules * { _ ==assertion .thm ==thm
        [ ] ==childParsesToKeep
          nt parserNonterminals *
          [
            1 thm len range { _ ==i thm * ==tok
              tok constants .has { tok }
                                 {
                                   tok variables * parserNonterminals *
                                   childParsesToKeep [ thm len i sub 1 sub ] cat =childParsesToKeep
                                 } ? *
            } each
          ] _ len ==childCount
          { ==s [
            childParsesToKeep { s -01 :child }' each
            s childCount 1 sub :child logicStart
            s :0 logicEnd
            assertion .name
          ] }
        :rule
      } each
    } rep
  } each

  map ==automata # nonterminal -> automaton
  variableNonTerminals dom { _ ==nt parserNonterminals * ==NT
    NT :automaton nt automata =[]
  } each
  [ automata singularRules ]
} memoized /prepareLogicParsers deffd

# generate parser functions
# { ==toks ==start [...] <parse> end success[0/1] }
{ =*variableTranslation
  prepareLogicParsers 2 dearray ==singularRules ==automata
  < "" ==tok [ ] ==value
    { =tok =value
      tok singularRules .has {
        [ 0 value * 1 value * tok singularRules * .name ] " " tok singularRules * .thm 0 -01 * cat
      }' {
        value tok # nothing to do
      }' ? *
    }'
  > -- /singularRulesTranslation deffst
  map ==globalCache # for repeated invocations
  0 ==globalCacheResetCounter # kill global cache once in a while to allow GC
  map _ ==parsers # returned
  automata dom { ==nt {
    ==toks ==start
    [ nt toks { " " } each start txt .produce .hu sys .asmroutines .assemblestr ==cacheKey
    cacheKey globalCache .has not {
      globalCacheResetCounter 1 add _ =globalCacheResetCounter 500 gt {
        0 =globalCacheResetCounter map =globalCache
      } rep
      [
        nt automata * ==automaton
        automaton .run =*consume
        start toks len range { ==i [ i _ 1 add "" ] i toks * singularRulesTranslation variableTranslation consume -- } each
        [ toks len toks len "" ] "" consume automaton .result ==result
        result len 1 gt { result dump "ambiguous grammar" die } rep
        result len 1 eq ==success
        success { 0 result * } rep success
      ] cacheKey globalCache =[]
    } τuncachedParser rep
    cacheKey globalCache * _ len dearray
  } τparsers nt parsers =[] } each
} /generateLogicParsers deffd

< "" ==tok
  { =tok
    tok variables .has {
      " " tok variables * cat
    }' { tok }' ? *
  }'
> -- /noMetaVariables deffst

{ ==tok
  tok len { 0 tok * 0 "$" * eq } andif { tok ".(.*)\\.[0-9]+" regex } andif { =tok } rep
  tok variables .has {
    " " tok variables * cat
  } { tok } ? *
} /alsoMetaVariables deffst

{ "Generating logic parser...\n"      sys .out .writeall |noMetaVariables   generateLogicParsers } memoized /logicParsers deffst
{ "Generating meta-logic parser...\n" sys .out .writeall |alsoMetaVariables generateLogicParsers } memoized /metaLogicParsers deffst

{ ==node node len 3 sub node * } /logicStart deffd
{ ==node node len 2 sub node * } /logicEnd deffd
{ ==node node len _ 3 sub node * -01 2 sub node * range } /logicRange deffd
{ ==node node len 1 sub node * } /logicNonTerminal deffd
{ ==node node len 3 sub } /logicChildCount deffd

sys .argv len 3 eq {
  logicParsers --
  metaLogicParsers --

  { _ { * }_ 2 sys .argv * sys .freeze * } !! *
}" rep

"igor-interactive.ey" include

# vim: syn=elymas