SpadLogic.spad

)abbrev package SLOGIC SpadLogic
SpadLogic(EC : SpadEnvCategory) : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> with
    extractPredicates : N -> List(N)
    evaluate : (N, EC) -> N

  Implementation ==> add
    import Printer
    import Logger('Logic)
    import SpadNode
    import SpadNodeFactory
    import SpadNodeTools

    invert (n : N) : N ==
      typeHas? n or typeIs? n =>
        nodeApp(['not], [n])
      apply? n =>
        app := n :: APP 
        app.function = ['and] =>
          -- not ((x > 0) and (S has Foo)) => 
          --   not (x > 0) or not (S has Foo) => nothing useful
          nodeApp(['or], [invert arg for arg in app.args])
        app.function = ['or] =>
          -- not ((x > 0) or (S has Foo)) => 
          --   not (x > 0) and not (S has Foo) => not (S has Foo)
          nodeApp(['and], [invert arg for arg in app.args])
        app.function = ['not] =>
          n
        null
      null

    extractPredicates (n : N) : List(N) ==
      typeHas? n or typeIs? n => [n]
      apply? n =>
        app := n :: APP
        app.function = ['and] =>
          concat [extractPredicates arg for arg in app.args]
        app.function = ['or] => []
        app.function = ['not] and #app.args = 1 =>
          n' := first app.args
          typeHas? n' or typeIs? n' => [n]
          apply? n' => extractPredicates(invert n')
          []
        []
      []

    evalPredicate(p : N, env : EC) : N ==
      key :=
        typeIs? p => (p :: TEI).expr
        typeHas? p => (p :: TEH).expr
        case? p => (p :: SC).expr
        return p
      facts := 
        symbol? key => factsAbout(key :: Symbol, env)
        apply? key => factsAbout(key :: APP, env)
        return p
      for f in facts repeat
        not? f =>
          f := (f :: APP).args.1
          f = p => return ['false]
        f = p => return ['true]
      p

    -- evaluate "n0 is n1" or leave it as is
    evalTypeIs(te : TEI, env : EC) : N ==
      (n0, n1) := (te.expr, te.type)

      hasFreeVars? n0 or hasFreeVars? n1 => [te]

      n0 = n1 => ['true]

      evalPredicate([te], env)

    -- evaluate "n0 has n1" or leave it as is
    evalTypeHas(te : TEH, env : EC) : N ==
      (n0, n1) := (te.expr, te.type)

      hasFreeVars? n0 or hasFreeVars? n1 => [te]

      n1 = baseType() => ['true]

      if symbol? n0 then n0 := symbolType()
      if integer? n0 then n0 := integerType()

      n0 = n1 => ['true]

      n := evalPredicate([te], env)
      true? n or false? n => n

      -- let's find type structure of n0
      ti? :=
        symbol? n0 => fetchType(n0 :: Symbol, env)
        apply? n0 => fetchType(n0 :: APP, env)
        return [te]

      ti? case "failed" => [te]
      ti := ti? :: TI

      -- case "A has B()"
      apply? n1 =>
        (member?(n1, ti.hasList) => ['true]; ['false])

      -- case "A has Join(..)"
      aggregate? n1 =>
        seq := n1 :: AGG
        bs := [evalTypeHas([n0, t]$TEH, env) for t in seq.list]
        every?(true?, bs) => ['true]
        any?(false?, bs) => ['false]
        [te]

      -- case "A has { fn : (..) -> .. }"
      typeDecl? n1 and not(unbound? n0 or unbound? n1) =>
        seq := ti.body :: AGG
        for n in seq.list repeat
          if typeOrigin? n then
            n := (n :: TO).expr
          not typeDecl? n => "iterate"
          n := substitute(n, typeVar() :: TV, n0)
          if n = n1 then
            return ['true]
        ['false]

      [te]

    evaluate(n : N, env : EC) : N ==
      debug ["Evaluate expression:" :: PF, bold(n :: PF)]

      typeHas? n => evalTypeHas(n :: TEH, env)
      typeIs? n => evalTypeIs(n :: TEI, env)
      apply? n =>
        app := n :: APP
        not member?(app.function, [['and], ['or], ['not]]$List(N)) => n
        lst := [evaluate(arg, env) for arg in app.args]
        app.function = ['and] =>
          any?(false?, lst) => ['false]
          lst := remove(true?, lst)
          #lst = 0 => ['true]
          #lst = 1 => first lst
          nodeApp(['and], lst)
        app.function = ['or] =>
          any?(true?, lst) => ['true]
          lst := remove(false?, lst)
          #lst = 0 => ['false]
          #lst = 1 => first lst
          nodeApp(['or], lst)
        app.function = ['not] and #app.args = 1 =>
          n' := evaluate(first app.args, env)
          true? n' => ['false]
          false? n' => ['true]
          n
        n
      true? n or false? n => n
      fail ["Expression" :: PF, bold(n :: PF), "not handled!" :: PF]
      error "evaluate $ SpadLogic"

)abbrev package SLOGICT SpadLogicTest
SpadLogicTest(EC : SpadEnvCategory) : Exports == Implementation where
  N ==> SpadNode
  APP ==> SpadApply(N)
  PF ==> PrintableForm

  Exports ==> with
    test1 : () -> Void
    test2 : () -> Void

  Implementation ==> add
    import SpadNode
    import SpadNodeFactory
    import Printer
    import MainLogger
    import SpadLogic(EC)

    extract (n : N) : Void ==
      println pile([spaces [n :: PF, bold("=>" :: PF)],
                    bracket [p :: PF for p in extractPredicates n]])

    eval (n : N, fs : List(N)) : Void ==
      env := new()
      for f in fs repeat
        addFacts(f, env)
      println pile([spaces [n :: PF, bold("=>" :: PF), evaluate(n, env) :: PF],
                    spaces [bold("when" :: PF), :[f :: PF for f in fs]]])

    test1 () ==
      loggerDefaultLevel "info"
      resetTime()

      a1 := nodeApp(['_>], [['x], [0]])
      a2 := nodeTypeHas(['S], ['Foo])
      a3 := nodeTypeIs(['R], integerType)
      n1 := nodeApp(["and" :: Symbol], [a1, a2, a3])
      n2 := nodeApp(["or" :: Symbol], [a1, a2, a3])

      extract n1
      extract nodeApp(['not], [n1])
      extract n2
      extract nodeApp(['not], [n2])

    test2 () ==
      loggerDefaultLevel "info"
      resetTime()

      a1 := nodeApp(['_>], [['x], [0]])
      a2 := nodeTypeHas(['S], setCategoryType)
      a3 := nodeTypeIs(['R], integerType)

      eval(a3, [a3])
      eval(nodeApp(['not], [a3]), [nodeApp(['not], [a3])])

      n1 := nodeApp(["and" :: Symbol], [a1, a2, a3])
      eval(n1, [nodeApp(['not], [a2])])
      eval(n1, [a2])

      n2 := nodeApp(["or" :: Symbol], [a1, a2, a3])
      eval(n2, [nodeApp(['not], [a3])])
      eval(n2, [a3])