SpadTypeTreeCreator.spad

)abbrev package STRFAC SpadTypeRuleFactory
SpadTypeRuleFactory() : Exports == Implementation where
)include SpadTypeDefs.inc

  OTN ==> Union(TN, "none")

  Exports ==> with
    ruleAssign : (TN, TN) -> TR
    ruleAssignFresh : (TN, TN, TN) -> TR
    ruleApply : (TN, List(TN)) -> TR
    ruleApply : (TN, List(TN), List(TN)) -> TR
    ruleCase : (TN, TN) -> TR
    ruleCoerce : (TN, List(TN), N) -> TR
    ruleCondExpr : (TN, TN, TN) -> TR
    ruleIfThen : (TN, TN) -> TR
    ruleFun : (FN, List(TN), TN, TN) -> TR
    ruleFunDef : (TN, TN) -> TR
    ruleFtor : (FT, List(TN), TN, TN, TN) -> TR
    ruleLoopIter : (TN, TN, TN) -> TR
    ruleLoop : (Union("loop", "collect", "repeat"), 
                List(TN), List(TN), Union(TN, "none"), TN) -> TR
    ruleRef : (List(TN), TN) -> TR
    ruleTypeIs : (TN, TN) -> TR
    ruleTypeIs : (List(TN), TN, TN) -> TR
    ruleSeg : (TN, OTN) -> TR
    ruleAgg : (Union("Domain", "Package", "Join", "Capsule", "Sequence",
                     "Tuple", "List"), TN, List(TN)) -> TR
    ruleCapsule : List(TN) -> TR
    ruleTypeCoerce : (TN, TN) -> TR
    ruleTypeSelect : (TN, TN) -> TR
    ruleTypeOrigin : (TN, TN) -> TR
    ruleSubType : (TN, TN) -> TR
    ruleSubType : (List(TN), TN, TN) -> TR
    ruleSuperType : (TN, TN) -> TR

  Implementation ==> add
    import SpadNodeFactory

    -- for assignment "L := R" do:
    -- compute "L, R"; if "L := R" then solution is "L := R"
    ruleAssign (L', R') ==
      (L, R) := (nodeRef(L'), nodeRef(R'))
      [[L, R, nodeAssign(L, R)], nodeAssign(L, R)]

    ruleAssignFresh (D', L', R') ==
      (D, L, R) := (nodeRef(D'), nodeRef(L'), nodeRef(R'))
      [[D, L, R, nodeAssign(L, R)], nodeSeq [D, nodeAssign(L, R)]]

    ruleApply (fun, args) ==
      (funRef, argRefs) := (nodeRef(fun), [nodeRef(arg) for arg in args])
      [[funRef, :argRefs, nodeApp(funRef, argRefs)],
       nodeApp(funRef, argRefs)]

    ruleApply (fun, args, extras) ==
      (funRef, argRefs) := (nodeRef(fun), [nodeRef(arg) for arg in args])
      extraRefs := [nodeRef(extra) for extra in extras]
      [[:extraRefs, funRef, :argRefs, nodeApp(funRef, argRefs)],
       nodeApp(funRef, argRefs)]

    ruleCase (S', T') ==
      (S, T) := (nodeRef(S'), nodeRef(T'))
      [[S, T, nodeCase(S, T)], nodeCase(S, T)]

    ruleCoerce (fun, args, rtyp) ==
      (funRef, argRefs) := (nodeRef(fun), [nodeRef(arg) for arg in args])
      [[funRef, :argRefs, nodeApp(funRef, argRefs)],
       nodeTypeSelect(nodeApp(funRef, argRefs), rtyp)]

    ruleCondExpr (C', T', F') ==
      (C, T, F) := (nodeRef(C'), nodeRef(T'), nodeRef(F'))
      [[C, T, F, nodeCondExpr(C, T, F)], nodeCondExpr(C, T, F)]

    ruleIfThen (C', T') ==
      (C, T) := (nodeRef(C'), nodeRef(T'))
      [[C, T, nodeCondExpr(C, T, null)], nodeCondExpr(C, T, null)]

    -- for function "fn (a1 : A1, ..., an : An) : T == B" do:
    -- compute "A1, ..., An, T, B"; if "T is B" then solution is "fn"
    ruleFun (fn, As', T', B') ==
      (As, T, B) := ([nodeRef(a) for a in As'], nodeRef(T'), nodeRef(B'))
      [[:As, T, B, nodeSubType(B, T)], nodeFun(fn.name, As, T, B)]

    ruleFunDef (S', T') ==
      (S, T) := (nodeRef(S'), nodeRef(T'))
      [[S, nodeTypeIs(S, T)], S]

    -- for functor "ft (a1 : A1, ..., an : An) : T == E add B" do:
    -- compute "A1, ..., An, T, B"; if "B <: T" then solution is "ft"
    ruleFtor (ft, As', E', T', B') ==
      As := [nodeRef(a) for a in As']
      (E, T, B) := (nodeRef(E'), nodeRef(T'), nodeRef(B'))
      [[:As, E, T, B, nodeSubType(B, T)], nodeFtor(ft.name, ft.args, T, E, B)]

    ruleLoopIter (var, seq, iter) == 
      (varRef, seqRef, iterRef) := (nodeRef(var), nodeRef(seq), nodeRef(iter))
      [[varRef, seqRef], nodeIterator(var.node :: Symbol, seqRef)]

    ruleLoop (kind, itors, guards, bodyType, body) ==
      itorRefs := [nodeRef(itor) for itor in itors]
      guardRefs := [nodeRef(guard) for guard in guards]
      bodyRef := nodeRef(body)
      formulas :=
        bodyType case TN =>
          [:itorRefs, :guardRefs, nodeRef(bodyType), bodyRef]
        [:itorRefs, :guardRefs, bodyRef]
      [formulas, nodeLoop(kind, itorRefs, guardRefs, bodyRef)]

    ruleRef (deps, body) ==
      depRefs := [nodeRef(dep) for dep in deps]
      bodyRef := nodeRef(body)
      [depRefs, bodyRef]

    ruleSeg (start, end) ==
      startRef := nodeRef(start)
      formulas := [startRef]$List(N)
      if end case TN then
        endRef := nodeRef(end)
        concat!(formulas, endRef)
      else
        endRef := null
      [formulas, nodeSeg(startRef, endRef)]

    ruleAgg (kind, seq, exprs) ==
      (seqRef, exprRefs) := (nodeRef(seq), [nodeRef(expr) for expr in exprs])
      [[:exprRefs, nodeTypeIs(last exprRefs, seqRef)], nodeAgg(kind, exprRefs)]

    ruleCapsule exprList ==
      exprRefList := [nodeRef(expr) for expr in exprList | not done? expr]
      [exprRefList, nodeCapsule exprRefList]

    ruleTypeOrigin (expr, origin) ==
      (exprRef, originRef) := (nodeRef(expr), nodeRef(origin))
      [[exprRef, originRef, nodeTypeOrigin(exprRef, originRef)],
       nodeTypeOrigin(exprRef, originRef)]

    ruleTypeCoerce (S', T') ==
      (S, T) := (nodeRef(S'), nodeRef(T'))
      [[S, T, nodeTypeCoerce(S, T)], nodeTypeCoerce(S, T)]

    ruleTypeSelect (S', T') ==
      (S, T) := (nodeRef(S'), nodeRef(T'))
      [[S, T, nodeTypeSelect(S, T)], nodeTypeSelect(S, T)]

    ruleSuperType (superType, type) ==
      (superTypeRef, typeRef) := (nodeRef(superType), nodeRef(type))
      [[typeRef, nodeSubType(superTypeRef, typeRef)], nodeRef(type)]

    -- compute "S"; if "S is T" then solution is "S"
    ruleTypeIs (S', T') ==
      ruleTypeIs ([], S', T')

    -- compute "P1, ..., Pn, S"; if "S is T" then solution is "S"
    ruleTypeIs (Ps', S', T') ==
      (Ps, S, T) := ([nodeRef(p) for p in Ps'], nodeRef(S'), nodeRef(T'))
      [[:Ps, S, nodeTypeIs(S, T)], S]

    -- compute "S"; if "S <: T" then solution is "S"
    ruleSubType (S', T') ==
      ruleSubType ([], S', T')

    -- compute "P1, ..., Pn, S"; if "S <: T" then solution is "S"
    ruleSubType (Ps', S', T') ==
      (Ps, S, T) := ([nodeRef(p) for p in Ps'], nodeRef(S'), nodeRef(T'))
      [[:Ps, S, nodeSubType(S, T)], S]


)abbrev package STEXCAPT SpadTreeExtractCapsuleType
SpadTreeExtractCapsuleType(find : NR -> TN) : SNR == Implementation where
)include SpadTypeDefs.inc

  Implementation ==> add
    import Logger('Capsule)

    walk (s : AGG) : N ==
      ns := [walk(coerce(n)@NR) for n in s.list | nodeRef? n]
      nodeJoin [n for n in ns | not null? n]

    walk (ass : ASS) : N == null
    walk (td : TD) : N == null

    walk (nr : NR) : N ==
      tn := find(nr)
      tn.node = [nr] =>
        fail pile ["Self reference detected:" :: PF, tn :: PF]
        error ""
      -- nodes that have no rules are leaves and we accept them
      empty? tn.rules => walk tn.node
      n := first(tn.rules).solution
      -- for functions take definition type
      function? n =>
        fn : FN := coerce(n)
        fnName : Symbol := coerce(fn.name)
        nodeTypeDecl([fnName], tn.type)
      -- for conditional expression add type guards to the content of branches
      condExpr? n =>
        ce : CE := coerce(n)
        cond := walk(ce.cond)
        truebr := nodeTypeGuard(walk ce.truebr, cond)
        falsebr := nodeTypeGuard(walk ce.falsebr, nodeApp(['not], [cond]))
        nodeJoin [truebr, falsebr]
      walk n

)abbrev package STTCREAT SpadTypeTreeCreator
SpadTypeTreeCreator() : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> with
    walk : (N, CTX, ENV) -> TN

  Implementation ==> add
    import SpadNode
    import SpadNodeFactory
    import SpadNodeTools
    import SpadEnvironment
    import SpadTypeRuleFactory
    import SpadTypeNodeArray
    import SpadTypeDatabase
    import SpadTypeUnifier
    import SpadLogic(SpadEnvironment)
    import SpadTypeEvaluator(SpadEnvironment)
    import Printer
    import Logger('Creator)

    walkApp (a : APP, ctx : CTX, env : ENV) : TN ==
      -- treat QUOTE(symbol) application as a symbol value
      a.function = ['QUOTE] and #a.args = 1 =>
        this := addNode!(ctx, [a], env)
        bindNode!(ctx, this, symbolType)
        this

      debug ["Processing function application." :: PF]

      this := addNode!(ctx, [a], env)

      -- First case: just a function call.
      funExpr := walk(a.function, ctx, env)
      argExprList := [walk(arg, ctx, env) for arg in a.args]

      -- Second case: element indexing or record field access.
      eltFunList : List(N) := []
      eltFunTypeList : List(MT) := []
      if a.function ~= ['elt] and a.function ~= ['return] then
        for n in typesOf('elt, env) | typeOrigin? n repeat
          eltFunType := (n :: TO).expr :: MT
          if #eltFunType.args = #a.args + 1 then
            eltFunList := [n, :eltFunList]
            eltFunTypeList := [eltFunType, :eltFunTypeList]

      if not empty? eltFunList then
        eltFunExpr := addNode!(ctx, ['elt], env)
        eltFunExpr.node := nodeTypeOrigin(eltFunExpr.node, typeRef(eltFunExpr))
        setTypeOf!(ctx, eltFunExpr, eltFunList)
        this.rules :=
          [:this.rules, ruleApply(eltFunExpr, [funExpr, :argExprList])]

      -- Add origin to function expression.
      if not(funExpr.node = ['return] or funExpr.node = ['error]) then
        funExpr.node := nodeTypeOrigin(funExpr.node, typeRef(funExpr))

      -- First case with a twist: arbitrary list construction.
      if stripOrigin(a.function) = ['construct] then
        item := addNode!(ctx, null, env)
        item.node := item.type
        setTypeOf!(ctx, item, dropSubTypes [argExpr.type for argExpr in argExprList])
        ctorArgs := [item.type for i in 1..#a.args]
        ctorRes := nodeApp(['List], [item.type])
        ctorType := nodeMappingType(ctorArgs, ctorRes)
        ctorNode := addNode!(ctx, ['construct], env)
        bindNode!(ctx, ctorNode, ctorType)
        this.rules := [:this.rules, ruleApply(ctorNode, argExprList, [item])]

      this.rules := [ruleApply(funExpr, argExprList), :this.rules]
      this

    walkAssign (a : ASS, ctx : CTX, env : ENV) : TN ==
      apply? a.lval =>
        app := a.lval :: APP
        this := walk(nodeApp(['setelt!], [app.function, :app.args, a.rval]), ctx, env)
        this.node := [a]
        this

      this := addNode!(ctx, null)
      right := walk(a.rval, ctx, env)

      fresh? :=
        symbol? a.lval =>
          s := a.lval :: Symbol
          -- user can overload a symbol of function that belong to any capsule,
          -- to check if overloading takes place and fresh symbol must be
          -- introduced we need to filter out mappings with origin
          ts := [t for t in typesOf(s, env) | not typeOrigin? t]
          empty? ts
        false

      decl : TN

      if fresh? then
        debug ["Processing fresh assignment" :: PF, string(a.lval :: PF)]
        -- introduce type declaration and propagate type through environment
        decl := walk(nodeTypeDecl(a.lval, right.type), ctx, env)
        env := decl.env

      left := walk(a.lval, ctx, env)

      -- Only left-value environment is propagated!
      this.env := left.env
      if fresh? then
        this.rules := [ruleAssignFresh(decl, left, right)]
      else
        this.rules := [ruleAssign(left, right)]
      this

    walkCondExpr (ce : CE, ctx : CTX, env : ENV) : TN ==
      debug ["Processing conditional expression." :: PF]
      this := addNode!(ctx, [ce])

      cond := walk(ce.cond, ctx, env)
      trueEnv := createScope cond.env
      addFacts(ce.cond, trueEnv)
      truebr := walk(ce.truebr, ctx, trueEnv)

      null? ce.falsebr =>
        this.env := env
        this.rules := [ruleIfThen(cond, truebr)]
        this

      falseEnv := createScope (case? ce.cond => env; cond.env)
      addFacts(nodeApp(['not], [ce.cond]), falseEnv)
      falsebr := walk(ce.falsebr, ctx, falseEnv)

      env := merge(env, trueEnv, falseEnv)

      -- TODO: "truebr.env" and "falsebr.env" should be merged and passed
      -- forward instead of just "env". Merging means that if the same variable
      -- was introduced in both branches then it should be present in the final
      -- environment.
      --
      -- Q: What if a variable "x : T" is defined only in one branch?
      -- A: In merged envrionment introduce "x" with type Union(T, "undefined"),
      --    and emit a warning when subtyping rule is applied.
      this.env := env
      this.rules := [ruleCondExpr(cond, truebr, falsebr)]
      this

    walkFun (fn : FN, ctx : CTX, env : ENV) : TN ==
      funName := (fn.name case "lambda" => '_+_-_>; fn.name :: Symbol)
      funDeclNode := addNode!(ctx, null, env)

      if fn.name case "lambda" then
        debug ("Processing lambda expression." :: PF)
      else
        debug ["Processing function" :: PF, string(funName :: PF)]

      addSubTree!(ctx)
      env' := createScope env

      -- It's vitally important that result type is represented by "%2" type
      -- variable (e.g. 'return' refers to "%2").
      funDefNode := addNode!(ctx, null, env')
      resNode := addNode!(ctx, null, env')
      argNodeList := [addNode!(ctx, null, env') for n in fn.args]

      resNode.node := resNode.type
      for argNode in argNodeList for n in fn.args repeat
        argNode.node :=
          typeDecl? n => nodeTypeDecl((n :: TD).expr, argNode.type)
          string? n => n
          error "walkApp: unexpected argument format"

      -- Take the type of function and replace those components, that were not
      -- specified, with type variables.
      fnType : MT := signature fn

      for argNode in argNodeList for argType in fnType.args repeat
        if not unbound? argType then
          bindNode!(ctx, argNode, argType)

      if not unbound? fnType.result then
        bindNode!(ctx, resNode, fnType.result)

      typeList : List(N) :=
        ([(null?(t) => n.type; t)
          for n in [resNode, :argNodeList] for t in [fnType.result, :fnType.args]])

      fnType' := nodeMappingType(rest typeList, first typeList)
      bindNode!(ctx, funDefNode, fnType')

      if fn.name case "lambda" then
        debug(["Lambda expression has" :: PF, bold(fnType' :: PF),
               "type based on definition." :: PF])
      else
        debug(["Function" :: PF, string(bold (funName :: PF)), "has" :: PF,
               bold(fnType' :: PF), "type based on definition." :: PF])

      -- Fetch signatures from the environment, including those defined by
      -- the domain / package / function. Filter out those that don't match
      -- the type calculated above.
      candidateList : List(MT) := []

      dom := first typesOf("$" :: Symbol, env)

      if fn.name case Symbol then
        for n in typesOf(fn.name :: Symbol, env') repeat
          candidate := null

          if typeGuard? n then
            tg := n :: TG
            if true? evaluate(tg.type, env) then
              candidate := tg.expr
          if typeOrigin? n then
            to := n :: TO
            if to.type = dom and mappingType? to.expr then
              candidate := to.expr
          if mappingType? n then
            candidate := n

          if not null? candidate then
            ures := unifyType(fnType', candidate)
            ures case "failed" => "iterate"
            candidate := substitute(fnType', ures :: SUBS)
            candidateList := [candidate :: MT, :candidateList]

      for c in candidateList repeat 
        for type in c.args | not unbound? type repeat
          addType(type, env')
        if not unbound? c.result then
          addType(c.result, env')

      -- TODO: Filter out function which have been already defined.
      if not empty? candidateList then
        info(["Environment contains" :: PF, string bold(funName :: PF),
              "from" :: PF, bold("$" :: PF), "with matching signatures:" :: PF,
              bold bracket [c :: PF for c in candidateList]])

        extendTypeOf!(ctx, funDeclNode, [[c] for c in candidateList])
        extendTypeOf!(ctx, resNode, [c.result for c in candidateList])
        for argNode in argNodeList for i in 1.. repeat
          extendTypeOf!(ctx, argNode, [c.args.i for c in candidateList])
      else
        info(["Considering" :: PF, string bold(funName :: PF),
              "of type" :: PF, bold(fnType :: PF),
              "to be a local function!" :: PF])

      fresh? := empty? candidateList

      for n in fn.args for argNode in argNodeList repeat
        typeDecl? n =>
          td := n :: TD
          addTypeOf(td.expr :: Symbol, argNode.type, env')
        string? n =>
          s := n :: String
          addTypeOf(s :: Symbol, n, env')
        error "walkFun: unexpected argument format"

      if fresh? and fn.name case Symbol then
        -- add the type to environment visible inside function's body
        -- to enable recursion
        addTypeOf(fn.name :: Symbol, funDefNode.type, env')

      bodyNode := walk(fn.body, ctx, env')

      leaveSubTree!(ctx)

      -- lambda is an expression so it must have a type (of its definiton)
      funDeclType := (fn.name case "lambda" => funDefNode.type; undefinedType)
      bindNode!(ctx, funDeclNode, funDeclType)

      funDeclNode.node := nodeRef(funDefNode)
      if fresh? and fn.name case Symbol then
        -- propagate function's declaration
        addTypeOf(fn.name :: Symbol, funDefNode.type, funDeclNode.env)
      funDefNode.rules := [ruleFun(fn, argNodeList, resNode, bodyNode)]
      funDefNode.node := funDefNode.rules.1.solution

      return funDeclNode

    walkFtor (ft : FT, ctx : CTX, env : ENV) : TN ==
      sig := signature ft
      -- sig is unchecked and may contain invalid types
      ftorApp := nodeApp([ft.name], [[td] for td in ft.args])

      debug pile([spaces ["Processing functor" :: PF, bold(ftorApp :: PF),
                          "with:" :: PF], ft.type :: PF])

      addSubTree!(ctx)

      this := addNode!(ctx, [ft.name], env)

      resNode := addNode!(ctx, ft.type, env)
      resType := resNode.type

      argSub := [[]]$Table(Symbol, N)
      argNodeList : List(TN) := []

      -- process functor's arguments
      for arg in ft.args repeat
        name := arg.expr :: Symbol
        argNode := addNode!(ctx, arg.expr, env)
        bindNode!(ctx, argNode, arg.type)
        addDomainAs(arg.type :: APP, name, env)
        importDomain(name, env)
        argSub(name) := argNode.type
        argNodeList := [argNode, :argNodeList]

      makeFunctorType(ft, env)

      argNodeList := reverse argNodeList
      argList := [argNode.node for argNode in argNodeList]
      ftType := nodeApp([ft.name], argList)
      addDomain(ftType :: APP, env)
      addTypeOf("$" :: Symbol, ftType, env)
      bindNode!(ctx, this, nodeMappingType(argList, resType))

      -- add functor's type info to the environment
      importDomain(ftType :: APP, env)
      ftRealType := 
        substitute(first typesOf(ftType :: APP, env), typeVar() :: TV, ftType)
      ftRes :=
        ft.type = categoryType => categoryType()
        -- FIXME: Functor's return type is not of "Join" node!
        nodeJoin (ftRealType :: TI).body.list
      bindNode!(ctx, resNode, ftRes)

      extNode := addNode!(ctx, ft.extends, env)
      bindNode!(ctx, extNode,
                (null? ft.extends => undefinedType(); ft.extends))

      bodyNode := walk(ft.capsule, ctx, env)

      capsuleType := nodeJoin [extNode.type, bodyNode.type]

      leaveSubTree!(ctx)

      this.rules := [ruleFtor(ft, argNodeList, extNode, resNode, bodyNode)]
      this

    walkImport (im : IM, ctx : CTX, env : ENV) : TN ==
      debug ["Importing" :: PF, bold(im.type :: PF)]
      addType(im.type, env)
      if apply? im.type then
        importDomain (im.type :: APP, env)
      tn := addNode!(ctx, [im], env)
      bindNode!(ctx, tn, undefinedType)
      done! tn

    walkLoop (lp : LP, ctx : CTX, env : ENV) : TN ==
      debug ["Loop statement." :: PF]

      this := addNode!(ctx, [lp], env)
      env' := env

      debug ["Processing" :: PF, #(lp.itors) :: PF, "iterator(s)." :: PF]
      itorList : List(TN) := []
      for n in lp.itors repeat
        itor := n :: IT

        itorExpr := addNode!(ctx, n, env)
        varExpr := addNode!(ctx, [itor.var], env)
        seqType := addNode!(ctx, null, env)
        seqExpr := walk(itor.seq, ctx, env)

        setTypeOf!(ctx, seqType,
            [nodeApp(['List], [varExpr.type]),
             nodeApp(['UniversalSegment], [varExpr.type])])
        seqType.rules := [ruleTypeIs(seqExpr, seqType), ruleSubType(seqExpr, seqType)]

        -- Iterator variable is added to loop's body environment,
        -- but is also known to guards.
        addTypeOf(itor.var, varExpr.type, env')

        bindNode!(ctx, itorExpr, undefinedType)

        itorExpr.rules := [ruleLoopIter(varExpr, seqType, itorExpr)]
        itorList := [itorExpr, :itorList]

      debug ["Processing" :: PF, #(lp.guards) :: PF, "guard(s)." :: PF]
      guardList : List(TN) := []
      for guard in lp.guards repeat
        guardExpr := walk(guard, ctx, env')
        bindNode!(ctx, guardExpr, booleanType)
        guardList := [guardExpr, :guardList]

      debug ["Processing loop body." :: PF]
      maybeBodyType : Union(TN, "none") := "none"
      body : TN
      if lp.kind case "collect" then
        bodyType := addNode!(ctx, null, env)
        body := walk(lp.body, ctx, env')
        bodyType.node := bodyType.type
        bodyType.rules := [ruleSubType(body, bodyType)]
        bindNode!(ctx, body, bodyType.type)
        bindNode!(ctx, this, nodeApp(['List], [bodyType.type]))
        maybeBodyType := bodyType
      else
        body := walk(lp.body, ctx, env')
        if hasUnknownType?(ctx, body) then
          bindNode!(ctx, body, undefinedType)
        bindNode!(ctx, this, undefinedType)

      this.rules := 
        [ruleLoop(lp.kind, itorList, guardList, maybeBodyType, body)]
      this

    walkSeg (seg : SEG, ctx : CTX, env : ENV) : TN ==
      debug ["Processing segment:" :: PF, string(seg :: PF)]
      this := addNode!(ctx, [seg], env)

      startExpr := walk(seg.start, ctx, env)

      endExpr' : Union(TN, "none") :=
        not null? seg.end =>
          endExpr := walk(seg.end, ctx, env)
          setTypeOf!(ctx, endExpr, [startExpr.type])
          endExpr
        "none"

      bindNode!(ctx, this, nodeApp(['UniversalSegment], [startExpr.type]))
      this.rules := [ruleSeg(startExpr, endExpr')]
      this

    walkAgg (s : AGG, ctx : CTX, env : ENV) : TN ==
      import List(TN)

      debug ["Found sequence of" :: PF, #(s.list) :: PF, "expressions." :: PF]
      this := addNode!(ctx, [s])

      exprList : List(TN) := [(n := walk(e, ctx, env); env := n.env; n) for e in s.list]

      if s.kind = "Capsule" then
        rule := ruleCapsule(exprList)
        findTypeNode := ((nr : NR) : TN +-> node(ctx, nr))
        capsuleType := walk(rule.solution)$SpadTreeExtractCapsuleType(findTypeNode)
        bindNode!(ctx, this, capsuleType)
        this.rules := [rule]
      else
        this.rules := [ruleAgg(s.kind, this, exprList)]
      this.env := (last exprList).env
      this

    walkSym (s : Symbol, ctx : CTX, env : ENV) : TN ==
      debug ["Symbol lookup for" :: PF, string bold(s :: PF)]

      this := addNode!(ctx, [s], env)

      types := typesOf(s, env)

      -- BUG: parseTran uses true and false as "Boolean" and not as "() -> Boolean"
      -- workaround for Boolean constants
      if s = 'true or s = 'false then
        types := [booleanType, :types]
      if s = '_$NoValue then
        types := [voidType, :types]
      if s = 'leave then
        leaveType := nodeMappingType([integerType, voidType], undefinedType) 
        types := [leaveType, :types]
      if s = 'error then
        errorType := nodeMappingType([stringType], undefinedType)
        types := [errorType, :types]
      if s = 'return then
        resType := node(ctx, 2).type
        returnType := nodeMappingType([resType], undefinedType)
        types := [returnType, :types]

      -- handle a symbol which is a type constructor
      if inDatabase? s then
        mt := fetchFunctorType(s, env)

        ftorArgList : List(N) := []
        ftorArgNodeList : List(TN) := []
        ftorArgRenames : SUBS := empty()

        for arg in mt.args repeat
          ftorArg := (arg :: TD).expr
          ftorArgType := (arg :: TD).type

          if typeVar? ftorArg then
            origFtorArg := ftorArg
            ftorArgType := substitute(ftorArgType, ftorArgRenames)

            ftorArgTypeNode := addNode!(ctx, ftorArgType, env)
            bindNode!(ctx, ftorArgTypeNode, ftorArgType)

            ftorArgNode := addNode!(ctx, ftorArg, env)
            ftorArg := ftorArgNode.type
            ftorArgRenames(origFtorArg :: TV) := [ftorArg]
            ftorArgNodeList := [ftorArgNode, :ftorArgNodeList]
            ftorArgNode.rules := [ruleSuperType(ftorArgNode, ftorArgTypeNode)]

          ftorArgList := [ftorArg, :ftorArgList]

        ftorResType := nodeTypeValue(baseType, nodeApp([s], ftorArgList))
        ftorType := nodeMappingType(reverse ftorArgList, ftorResType)
        -- BUG? ftorType should be nodeTypeValue(baseType, ftorType)
        types := [ftorType, :types]

        if not empty? ftorArgNodeList then
          this.rules := [[[nodeRef(n) for n in ftorArgNodeList], [s]]]

      empty? types =>
        fail ["Undefined symbol:" :: PF, bold red string (s :: PF), "!" :: PF]
        error ""
      
      info(["Found" :: PF, string bold(s :: PF), "with type :" :: PF,
            bold bracket [t :: PF for t in types]])
      #types = 1 =>
        bindNode!(ctx, this, types.1)
        this
      setTypeOf!(ctx, this, types)
      this 

    walkTypeDecl (td : TD, ctx : CTX, env : ENV) : TN ==
      debug(["Expression" :: PF, td.expr :: PF, "has type" :: PF, td.type :: PF])

      not symbol? td.expr =>
        fail ["Type annotation works only for symbols!" :: PF]
        error ""

      -- Type definition for a symbol.
      s := td.expr :: Symbol
      ts := [t for t in typesOf(s, env) | not typeOrigin? t]

      -- Add type to the environment or crash if already defined,
      -- this behaviour is supressed for mappings that have origin.
      not empty? ts and not member?(td.type, ts) =>
        fail([bold red ("Error!" :: PF), "Symbol" :: PF, string(s :: PF),
              "already defined as" :: PF, bracket [t :: PF for t in ts], "!" :: PF])
        error ""

      addTypeOf(s, td.type, env)
      tn := addNode!(ctx, [td], env)
      bindNode!(ctx, tn, undefinedType)
      tn

    walkTypeSelect (ts : TS, ctx : CTX, env : ENV) : TN ==
      debug(["Expression" :: PF, ts.expr :: PF,
             "has to return type" :: PF, ts.type :: PF])

      not symbol? ts.expr =>
        fail ["Type cut operator works only for function symbols!" :: PF]
        error ""

      addType(ts.type, env)
      this := addNode!(ctx, [ts], env)
      ntype := walk(ts.type, ctx, env)
      nexpr := walk(ts.expr, ctx, ntype.env)
      this.rules := [ruleTypeSelect(nexpr, ntype)]
      this

    walkTypeCoerce (tc : TC, ctx : CTX, env : ENV) : TN ==
      debug ["Expression" :: PF, tc.expr :: PF, "have to coerce to" :: PF, tc.type :: PF]

      addType(tc.type, env)
      this := addNode!(ctx, [tc], env)
      ntype := walk(tc.type, ctx, env)
      nexpr := walk(tc.expr, ctx, ntype.env)

      rs := [ruleTypeCoerce(nexpr, ntype)]$List(TR)
      if not empty? typesOf('coerce, env) then
        coerceFun := walk(['coerce], ctx, env)
        rs := [:rs, ruleApply(coerceFun, [nexpr])]
      this.rules := rs
      this

    walkTypeHas (te : TEH, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [te], env)
      bindNode!(ctx, this, booleanType)
      this

    walkTypeIs (te : TEI, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [te], env)
      bindNode!(ctx, this, booleanType)
      this
    
    walkTypeOrigin (to : TO, ctx : CTX, env : ENV) : TN ==
      not symbol? to.expr =>
        fail ("Type origin selector works only for symbols!" :: PF)
        error ""

      debug(["Symbol" :: PF, string bold(to.expr :: PF),
             "must originate from" :: PF, bold(to.type :: PF),
             "type!" :: PF])

      addType(to.type, env)
      this := addNode!(ctx, [to], env)
      ntype := walk(to.type, ctx, env)
      nexpr := walk(to.expr, ctx, ntype.env)
      bindNode!(ctx, this, nexpr.type)
      this.rules := [ruleTypeOrigin(nexpr, ntype)]
      this.env := ntype.env
      this

    walkCase (sc : SC, ctx : CTX, env : ENV) : TN ==
      addType(sc.type, env)

      this := addNode!(ctx, [sc], env)
      ntype := walk(sc.type, ctx, env)
      nexpr := walk(sc.expr, ctx, ntype.env)

      bindNode!(ctx, this, booleanType)
      this.rules := [ruleCase(nexpr, ntype)]
      this.env := ntype.env
      this

    walkInt (i : Integer, ctx : CTX, env : ENV) : TN ==
      type :=
        i > 0 => nodeApp(['PositiveInteger], []) 
        i >= 0 => nodeApp(['NonNegativeInteger], [])
        nodeApp(['Integer], [])
      this := addNode!(ctx, [i], env)
      bindNode!(ctx, this, type)
      done! this

    walkFlt (f : DoubleFloat, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [f], env)
      bindNode!(ctx, this, floatType)
      done! this

    walkStr (s : String, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [s], env)
      ts := typesOf(s :: Symbol, env)
      setTypeOf!(ctx, this, [stringType, :map(stripOrigin, ts)])
      this

    walkRecord (rt : RT, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [rt], env)
      bindNode!(ctx, this, nodeTypeValue(baseType, [rt]))
      this

    walkUnion (ut : UT, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, [ut], env)
      bindNode!(ctx, this, nodeTypeValue(baseType, [ut]))
      this

    walkEmpty (e : N, ctx : CTX, env : ENV) : TN ==
      this := addNode!(ctx, e, env)
      bindNode!(ctx, this, undefinedType)
      done! this

    walk (n, ctx, env) ==
      apply? n => walkApp(n :: APP, ctx, env)
      assign? n => walkAssign(n :: ASS, ctx, env)
      case? n => walkCase(n :: SC, ctx, env)
      condExpr? n => walkCondExpr(n :: CE, ctx, env)
      float? n => walkFlt(n :: DoubleFloat, ctx, env)
      functor? n => walkFtor(n :: FT, ctx, env)
      import? n => walkImport(n :: IM, ctx, env)
      integer? n => walkInt(n :: Integer, ctx, env)
      loop? n => walkLoop(n :: LP, ctx, env)
      segment? n => walkSeg(n :: SEG, ctx, env)
      aggregate? n => walkAgg(n :: AGG, ctx, env)
      string? n => walkStr(n :: String, ctx, env)
      symbol? n => walkSym(n :: Symbol, ctx, env)
      typeCoerce? n => walkTypeCoerce(n :: TC, ctx, env)
      typeDecl? n => walkTypeDecl(n :: TD, ctx, env)
      typeHas? n => walkTypeHas(n :: TEH, ctx, env)
      typeIs? n => walkTypeIs(n :: TEI, ctx, env)
      typeOrigin? n => walkTypeOrigin(n :: TO, ctx, env)
      typeSelect? n => walkTypeSelect(n :: TS, ctx, env)
      function? n or lambda? n => walkFun(n :: FN, ctx, env)
      recordType? n => walkRecord(n :: RT, ctx, env)
      unionType? n => walkUnion(n :: UT, ctx, env)
      null? n => walkEmpty(n, ctx, env)
      -- namedType, mappingType, recordType, sumType, unionType, macro, where
      fail ["Expression" :: PF, bold red paren(n :: PF), "not handled yet!" :: PF]
      error ""