SpadTypeEvaluator.spad

)abbrev domain STEVAL SpadTypeEvaluator
SpadTypeEvaluator(EC : SpadEnvCategory) : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> CoercibleTo(PF) with
    fetchFunctorType : (Symbol, EC) -> MT
    getTypeInfo : (APP, EC) -> TI
    makeFunctorType : (FT, EC) -> MT

  Implementation ==> add
    import Logger('TypeEval)
    import Printer
    import SpadNode
    import SpadNodeFactory
    import SpadNodeTools
    import SpadTypeDatabase
    import SpadTypeUnifier
    import SpadLogic(EC)

    apply : (APP, MT, EC) -> TI
    flatten : (Symbol, TI, EC) -> TI
    evalTypeGuards : (APP, TI, EC) -> TI
    eraseConstraints : (APP, TI, EC) -> TI

    fetchFunctorType(name : Symbol, env : EC) : MT ==
      n? := search(name, env)
      n? case EVAL => (n? :: EVAL).type :: MT

      info ["getTypeInfo :" :: PF, bold(name :: PF)]

      mt := fetchType name
      ti := flatten(name, mt.result :: TI, env)
      mt := [mt.args, [ti]]
      env(name) := [[mt], []]
      mt

    getTypeInfo(app : APP, env : EC) : TI ==
      n? := search(app, env)
      n? case EVAL => (n? :: EVAL).type :: TI

      name := app.function :: Symbol
      ti := apply(app, fetchFunctorType(name, env), env)
      env(app) := [[ti], []]
      ti := evalTypeGuards(app, ti, env)

      hasFreeVars? [app] => ti

      eraseConstraints(app, ti, env)
      
    makeFunctorType(ft : FT, env : EC) : MT ==
      mt := makeType ft
      ti := flatten(ft.name, mt.result :: TI, env)
      mt := [mt.args, [ti]]
      env(ft.name) := [[mt], []]
      mt

    apply(app : APP, mt : MT, env : EC) : TI ==
      #app.args ~= #mt.args =>
        fail ["wrong number of arguments for:" :: PF, app :: PF]
        error "apply $ SpadTypeEvaluator"
      empty? app.args => mt.result :: TI

      margs := [(arg :: TD).expr for arg in mt.args]
      n1 := nodeTuple margs
      n2 := nodeTuple app.args
      subs := unifyType(n1, setMajor(n2, 1))

      subs case "failed" =>
        fail [paren [a :: PF for a in margs], "~" :: PF, 
              paren [a :: PF for a in app.args]]
        error "apply $ SpadTypeEvaluator"

      subs case SUBS =>
        ti := substitute(mt.result, subs) :: TI
        tds := [substitute(arg, subs) :: TD for arg in mt.args]
        -- constraints have "X has Y $ Z" format, so  in case of failure
        -- we can report which type requires the property to be met
        cs := [nodeTypeOrigin(nodeTypeHas(td.expr, td.type), [app])
               for td in tds]
        cs := concat(cs, ti.constraints)
        setMajor(nodeTypeInfo(ti.body, ti.hasList, cs, ti.superType), 0) :: TI

    flatten(name : Symbol, ti : TI, env : EC) : TI ==
      info ["Flatten" :: PF, bold(name :: PF)]

      origBody := ti.body.list
      flatBody : List(N) := []
      hasLst : AssociationList(APP, N) := [[]]
      constraints := ti.constraints

      while not empty? origBody repeat
        (n, origBody) := (first origBody, rest origBody)

        cond := ['true]
        if typeGuard? n then 
          tg := n :: TG
          if apply? tg.expr then
            -- encountered a functor with constraints
            (n, cond) := (tg.expr, tg.type)

        -- merge functor
        apply? n =>
          app := n :: APP

          -- check if we have already merged a functor
          key?(app, hasLst) => 
            debug ["Skipping:" :: PF, bold(app :: PF), "with" :: PF, bold(hasLst(app) :: PF)]
            -- if true then erase previously remembered constraints
            true? cond =>
              hasLst(app) := cond
            -- if remembered constraints are true then ignore new constraints
            true? hasLst(app) => "iterate"
            hasLstVal := hasLst(app)
            -- BUG: hasLstVal may be a complex logic expression, checks below
            --      assume it's a flat list of statements
            condLst : List(N) :=
              apply? hasLstVal =>
                (hasLstVal :: APP).args
              [hasLstVal]
            member?(cond, condLst) => "iterate"
            hasLst(app) := nodeApp(['or], concat(cond, condLst))

          debug(["Merge" :: PF, bold(true? cond => n :: PF; nodeTypeGuard(n, cond) :: PF),
                 "with" :: PF, name :: PF])

          hasLst(app) := cond
          ti' := apply(app, fetchType(app.function :: Symbol), env)
          -- TODO: does it make sense?
          constraints := concat(ti'.constraints, constraints)

          -- extend original functor's body with included constructor type
          snippet : List(N) := []

          -- TODO: merge both branches
          if true? cond then
            -- case 1: merged functor has no constraints
            for e in ti'.body.list repeat
              e' :=
                cond' := ['true]
                if typeGuard? e then
                  tg := e :: TG
                  (e, cond') := (tg.expr, tg.type)
                apply? e => -- add constraint to merged functor
                  true? cond' => e
                  nodeTypeGuard(e, cond')
                typeDecl? e => -- add origin to function signature
                  e := nodeTypeOrigin(e, n)
                  true? cond' => e
                  nodeTypeGuard(e, cond')
                error "Not handled!"
              snippet := [e', :snippet]
          else
            -- case 2: merged functor has some constraints

            -- INFO: When we merge functor A with %, we know that all what is
            -- within A belongs to % only when "% has A". Hence for each
            -- component of A we remember simple constraint "% has A".
            -- More complex constraints are remembered in hasList.
            --
            -- This allows to add extra options to condition "% has A" in case
            -- we encounter some other (less restrictive) constraints later.

            for e in ti'.body.list repeat
              e' :=
                cond' := nodeTypeHas(typeVar(), [app])
                if typeGuard? e then
                  tg := e :: TG
                  -- add extra constraint to merged functor
                  (e, cond') := (tg.expr, nodeApp(['and], [cond', tg.type]))
                apply? e => -- add constraint to merged functor
                  nodeTypeGuard(e, cond')
                typeDecl? e => -- add origin to function signature
                  e := nodeTypeOrigin(e, n)
                  nodeTypeGuard(e, cond')
                error "Not handled!"
              snippet := [e', :snippet]

          origBody := concat(reverse snippet, origBody)

        -- merge everything else
        typeDecl? n or typeGuard? n or typeOrigin? n =>
          debug ["Copy" :: PF, bold(n :: PF), "to" :: PF, name :: PF]
          flatBody := [n, :flatBody]

        aggregate? n =>
          origBody := concat(n :: List(N), origBody)

        fail ["Flatten" :: PF, bold(n :: PF)]
        error "Not handled!"

      hasLst' : List(N) := []
      for he in entries hasLst repeat
        h := 
          true? he.entry => [he.key]
          nodeTypeGuard([he.key], he.entry)
        hasLst' := [h, :hasLst']

      [[ti.body.kind, reverse flatBody],
       hasLst', removeDuplicates constraints, ti.superType]

    evaluate'(n : N, self : APP, env : EC) : N ==
      evaluate(substitute(n, typeVar() :: TV, [self]), env)

    eraseConstraints(name : APP, ti : TI, env : EC) : TI ==
      info ["Check type constraints for" :: PF, bold(name :: PF)]

      appliesCleanly(n : N) : Boolean ==
        true? evaluate'((n :: TO).expr, name, env)

      ti := [ti.body, ti.hasList, remove(appliesCleanly, ti.constraints),
             ti.superType]
      env(name) := [[ti], []]

      empty? ti.constraints => ti

      fail ["Could not construct type" :: PF, bold(name :: PF)]

      for c in ti.constraints repeat
        to := c :: TO
        te := to.expr :: TEH
        fail [bold blue(to.type :: PF), "requires" :: PF, bold(te.expr :: PF),
              "to have" :: PF, bold(te.type :: PF)]

      error "eraseConstraints $ SpadTypeEvaluator"

    evalTypeGuards(name : APP, ti : TI, env : EC) : TI ==
      info ["Evaluate type guards for" :: PF, bold(name :: PF)]

      -- evaluate type guards on HasList
      continue? := true
      
      while continue? repeat
        newHasList : List(N) := []
        continue? := false

        for n in ti.hasList repeat
          n' := 
            not typeGuard? n => n
            tg := n :: TG
            type' := evaluate'(tg.type, name, env)
            true? type' => (continue? := true; tg.expr)
            nodeTypeGuard(tg.expr, type')
          newHasList := [n', :newHasList]

        ti := [ti.body, reverse newHasList, ti.constraints, ti.superType]
        env(name) := [[ti], []]

      -- with new HasList evaluate type guards in TypeInfo's body
      eval(n : N) : N ==
        not typeGuard? n => n
        tg := n :: TG
        type' := evaluate'(tg.type, name, env)
        true? type' => tg.expr
        nodeTypeGuard(tg.expr, type')

      ti := [[ti.body.kind, map(eval, ti.body.list)],
             ti.hasList, ti.constraints, ti.superType]
      env(name) := [[ti], []]
      ti

)abbrev package TEVALT SpadTypeEvaluatorTest
SpadTypeEvaluatorTest(EC : SpadEnvCategory) : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> with
    test1 : () -> Void
    test2 : () -> Void
    test3 : () -> Void
    test4 : () -> Void
    test5 : () -> Void
    test6 : () -> Void

    fail1 : () -> Void
    fail2 : () -> Void

  Implementation ==> add
    import Printer
    import SpadNodeFactory
    import SpadTypeEvaluator(EC)
    import MainLogger

    initTest : () -> EC
    initTest ==
      loggerDefaultLevel "info"
      loggerLevel('Parser, "notice")
      resetTime()
      new()

    test1 ==
      env := initTest()

      symbols : List(Symbol) := (['Integer, 'List, 'Fraction, 'Expression,
                                  'UnivariateTaylorSeries, 'Matrix])

      for s in symbols repeat
        println [bold blue(s :: PF), "is" :: PF, fetchFunctorType(s, env) :: PF]

      println (env :: PF)

    test2 ==
      env := initTest()

      -- type flattening, type contrains evaluation
      types : List(APP) := (
        [[['NonNegativeInteger], []],
         [['Integer], []],
         [['Symbol], []],
         [['Float], []],
         [['List], [integerType]],
         [['Fraction], [integerType]],
         [['Matrix], [integerType]],
         [['Expression], [integerType]]])

      for t in types repeat
        println [bold blue(t :: PF), "is" :: PF, getTypeInfo(t, env) :: PF]

      println (env :: PF)

    test3 ==
      env := initTest()

      -- check if values as accepted as functor arguments (instead of types)
      println (fetchFunctorType('UnivariateTaylorSeries, env) :: PF)
      t := [['UnivariateTaylorSeries], [integerType(), ['x]$N, [2]$N]]$APP
      println (getTypeInfo(t, env) :: PF)

      println (env :: PF)

    test4 ==
      env := initTest()

      -- TODO: some extremely slow cases to be improved
      println (fetchFunctorType('UnivariateLaurentSeries, env) :: PF)
      --println (fetchFunctorType('UnivariatePuiseuxSeries, env) :: PF)
      --println (fetchFunctorType('ExponentialExpansion, env) :: PF)

      println (env :: PF)

    -- Should I consider following case:
    -- undefinedType() "%undef" passed as a parameter to a functor prevents
    -- contraint evaluation that involves the parameter

    test5 ==
      env := initTest()

      LI := nodeApp(['List], [['Integer]$N])$N

      println (getTypeInfo([['List], [LI]], env) :: PF)

    fail1 ==
      env := initTest()

      -- wrong number of arguments => should fail!
      println (getTypeInfo([['List], []], env) :: PF)

    fail2 ==
      env := initTest()

      -- wrong type parameter => should fail!
      println (getTypeInfo([['List], [nodeApp(['BasicType], [])]], env) :: PF)