module Bpl

module Transformation
  class StaticSegments < Bpl::Pass
    def self.description
      "I don’t know what this does."
    end

    def run! program
    end
  end
end

module AST
  class Program
    def static_segments_sequentialize!

      globals = global_variables
      gs = globals.map{|d| d.idents}.flatten
      return if gs.empty?

      threads = []
      @declarations.each do |proc|
        next unless proc.is_a?(ProcedureDeclaration) && proc.body
        proc.replace do |call|
          next call unless call.is_a?(CallStatement) && \
            call.attributes.include?(:async)
          abort "static thread creation only allowed in entry points." \
            unless proc.is_entrypoint?
          threads << call
          nil
        end
      end

      @declarations << bpl("var #s: int;")
      @declarations << bpl("var #d: int;")
      @declarations += globals.map do |decl|
        bpl "const #{decl.names.map{|g| "$S.#{g}"} * ", "}: [int] #{decl.type};"
      end

      @declarations << bpl("function $pos(int) returns (int);")
      @declarations << bpl("axiom $pos(0) == 0;")
      @declarations << bpl("axiom (forall i: int :: i > 0 ==> $pos(i) > 0);")
      @declarations << bpl("axiom (forall i: int :: i < #S ==> $pos(i) < #S);")
      @declarations << bpl("axiom (forall i,j: int :: $pos(i) == $pos(j) ==> i == j);")

      @declarations << bpl("const #S: int;")
      @declarations << bpl("const #DELAYS: int;")
      @declarations << bpl("const #ROUNDS: int;")

      @declarations.each do |decl|
        case decl
        when ProcedureDeclaration
          next unless decl.body

          mods = gs - decl.modifies
          decl.specifications << bpl("modifies #s, #d;")
          decl.specifications << bpl("modifies #{mods * ", "};") unless mods.empty?

          decl.body.replace do |elem|
            case elem
            when AssumeStatement
              if elem.attributes.include? :startpoint
                next [
                  bpl("#s := 0;"),
                  bpl("#d := 0;"),
                  elem
                ]

              elsif elem.attributes.include? :endpoint
                next [
                  elem,
                  gs.map{|g| bpl("assume #{g} == $S.#{g}[$pos(#s)+1];")},
                  threads.map.with_index do |call,i|
                    seq_number = call.attributes[:async].first
                    call.attributes.delete :async
                    bpl(<<-end
                      if (true) {
                        #s := #s + 1;
                        assume $pos(#s) == #{seq_number || "#s-#d"};
                        #{gs.map{|g| bpl("#{g} := $S.#{g}[$pos(#s)];")} * "\n"}
                        #{call}
                        #{gs.map{|g| bpl("assume #{g} == $S.#{g}[$pos(#s)+1];")} * "\n"}
                      }
                    end
                    )
                  end,
                  bpl("assume #s+1 == #S;")
                ].flatten

              elsif elem.attributes.include? :yield
                seq_number = elem.attributes[:yield].first
                next bpl(<<-end
                  if (#{seq_number ? "true" : "*"}) {
                    assume #d < #DELAYS;
                    #{gs.map{|g| bpl("assume #{g} == $S.#{g}[$pos(#s)+1];")} * "\n"}
                    assume $pos(#s) < $pos(#s+1);
                    #d := #d + 1;
                    #s := #s + 1;
                    // Q: how to determine the scheduler here?
                    assume $pos(#s) == #{seq_number || "$pos(#s)"};
                    #{gs.map{|g| bpl("#{g} := $S.#{g}[$pos(#s)];")} * "\n"}
                  }
                end
                )

              end
            end

            elem
          end
        end
      end
    end
  end

end

end