defpackage firrtl/errors :
   import core
   import verse
   import firrtl/ir2
   import firrtl/ir-utils
   import firrtl/primops
   import firrtl/passes
   import firrtl-main

; TODO
; make sure it compiles, write tests, look over code to make sure its right
;========== ALL CHECKS =================
;PARSER CHECK
; * No nested modules <- parser
; * Only modules in circuit (no statements or expressions) <- parser
; * Module must be a reference in inst declaration

;AFTER GENDER INFERENCE
; o Nodes always male
; o Accessors only have one gender, unless rdwr
; o output/input only one gender
; o correctly check for the base bundle

;AFTER WIDTH INFERENCE
; o No names
; o No Unknowns
; o All widths are positive
; o Pad's width is greater than value's width
; o pad's width is greater than value's width
; o widths are large enough to contain value

;AFTER LOWERING
; o All things connect to once
; o no reg
; o no accessors

;AFTER ??????
; o No combinational loops
; o cannot connect to a pad, or a register. only connct to a reference

;================= High Form Check ==========================
; * Subexps of Subfield and Index can only be subfields, index, or refs
; * Can only connect to a Ref or Subfield or Index or WritePort
; * A module has the same name as main of circuit
; * mems cannot be a bundle with flips
; * instance module must have the same name as a defined module
; * reset must be UInt<1>
; * Unique names per module
; * No name can be a prefix of any other name.
; * all references are declared
; * UInt only has positive ints

;----------------- Errors ------------------------
defn NotUnique (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Reference " name " does not have a unique name."]

defn IsPrefix (info:FileInfo, name1:Symbol, name2:Symbol) :
   PassException $ string-join $
   [info ": Reference " name1 " and " name2 " share a prefix."]
   
defn InvalidLOC (info:FileInfo) :
   PassException $ string-join $
   [info ": Invalid connect to an expression that is not a reference or a WritePort."]
   
defn NegUInt (info:FileInfo) :
   PassException $ string-join $
   [info ": UIntValue cannot be negative."]

defn UndeclaredReference (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Reference " name " is not declared."]

defn MemWithFlip (info:FileInfo, name:Symbol) : 
   PassException $ string-join $
   [info ": Memory " name " cannot be a bundle type with flips."]

defn InvalidSubfield (info:FileInfo) :
   PassException $ string-join $
   [info ": Invalid subfield access to non-reference."]

defn InvalidIndex (info:FileInfo) :
   PassException $ string-join $
   [info ": Invalid index access to non-reference."]
   
defn NoTopModule (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": A single module must be named " name "."]

defn ModuleNotDefined (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Module " name " is not defined."]

defn WrongReset (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Module " name " has a reset that is not of type UInt<1>."]

;---------------- Helper Functions --------------
defn has-flip? (t:Type) -> True|False :
   var has? = false
   defn find-flip (t:Type) -> Type :
      match(t) : 
         (t:BundleType) : 
            for f in fields(t) do : 
               if flip(f) == REVERSE : has? = true
            t
         (t) : t
   find-flip(t)
   map(find-flip,t)
   has?

defn contains?<?T> (c:?T,cs:Streamable<?T>) -> True|False : 
   label<True|False> myret :
      for x in cs do :
         if x == c : myret(true)
      false

defn is-prefix? (s:Symbol,v:Vector<Symbol>) -> Symbol|False :
   label<Symbol|False> myret :
      for x in v do :
         if is-prefix?(x,s) : myret(x)
      false

defn is-prefix? (s1:Symbol,s2:Symbol) -> True|False :
   var is? = true
   val s1* = to-string(s1)
   val s2* = to-string(s2)
   for (x in s1*, y in s2*) do :
      if x != y : is? = false
   if length(s1*) > length(s2*) :
      if s1*[length(s2*)] != '$' : is? = false
   if length(s1*) < length(s2*) :
      if s2*[length(s1*)] != '$' : is? = false
   if length(s1*) == length(s2*) :
      is? = false
   is?

;--------------- Check High Form Pass -------------------
public defn check-high-form (c:Circuit) -> Circuit : 
   val errors = Vector<PassException>()

   defn check-valid-loc (info:FileInfo,e:Expression) -> False :
      match(e) : 
         (e:UIntValue|SIntValue|DoPrim|ReadPort|Register|Pad) :
            add(errors,InvalidLOC(info))
         (e) : false

   defn check-high-form-e (info:FileInfo,e:Expression,names:Vector<Symbol>) -> Expression :
      match(map(check-high-form-e{info,_,names},e)) :
         (e:Ref) : 
            if not contains?(name(e),names) : 
               add(errors,UndeclaredReference(info,name(e)))
         (e:Subfield) : 
            match(exp(e)) :
               (e:Ref|Subfield|Index) : false
               (e) : add(errors,InvalidSubfield(info))
         (e:Index) : 
            match(exp(e)) :
               (e:Ref|Subfield|Index) : false
               (e) : add(errors,InvalidIndex(info))
         ;; (e:UIntValue) :
         ;; if value(e) < 0 : 
         ;;    add(errors,NegUInt(info))
         (e) : false
      e

   defn check-high-form-s (s:Stmt,names:Vector<Symbol>) -> Stmt :
      defn check-name (info:FileInfo,name:Symbol) -> False :
         if contains?(name,names) : add(errors,NotUnique(info,name))
         val prefix = is-prefix?(name,names)
         if prefix typeof Symbol : add(errors,IsPrefix(info,name,prefix as Symbol))

      map{check-high-form-s{_,names},_} $ { 
         match(map(check-high-form-e{info(s),_,names},s)) :
            (s:DefWire|DefRegister) :
               check-name(info(s),name(s))
               add(names,name(s))
            (s:DefMemory) : 
               check-name(info(s),name(s))
               add(names,name(s))
               if has-flip?(type(s)) : add(errors, MemWithFlip(info(s), name(s)))
            (s:DefInstance) : 
               if not contains?(name(module(s) as Ref),map(name,modules(c))) : 
                  add(errors, ModuleNotDefined(info(s),name(module(s) as Ref)))
               add(names,name(s))
            (s:DefNode) : 
               add(names,name(s))
            (s:DefAccessor) :
               add(names,name(s))
            (s:Connect) : 
               check-valid-loc(info(s),loc(s))
            (s) : false
         s }()

   defn check-high-form-m (m:Module) -> False :
      val names = Vector<Symbol>()
      for m in modules(c) do :
         add(names,name(m))
      for p in ports(m) do :
         add(names,name(p))
         if name(p) == `reset :
            if direction(p) == OUTPUT : 
               add(errors,WrongReset(info!(m),name(m)))
            else :
               if type(p) typeof UIntType :
                  if width(type(p) as UIntType) != IntWidth(1) : 
                     add(errors,WrongReset(info!(m),name(m)))
               else :
                  add(errors,WrongReset(info!(m),name(m)))

      
      add(names,`reset)
      check-high-form-s(body(m),names)
      false
   
   var number-top-m = 0
   for m in modules(c) do :
      if name(m) == main(c) : number-top-m = number-top-m + 1
      check-high-form-m(m)
   if number-top-m != 1 : add(errors,NoTopModule(info!(c),main(c)))
   throw(PassExceptions(errors)) when not empty?(errors)
   c

;================= KIND CHECK  ==========================
; o Cannot connect directly to a mem ever
; o onreset can only handle a register
; o Cannot use a mem in anything except an accessor, Readport, or Writeport

;----------------- Errors ---------------------
defn NotMem (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Reference " name " must be a mem."]

defn IsMem (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Reference " name " cannot be a mem."]

defn OnResetNotReg (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Illegal on-reset to non-reg reference " name "."]

;----------------- Check Kinds Pass ---------------------
; I may have been overeager in looking for places where mems can't be, as mems are guaranteed to have a vector
;   type, and this will get caught in the type check pass
public defn check-kinds (c:Circuit) -> Circuit : 
   val errors = Vector<PassException>()
   defn check-not-mem (info:FileInfo,e:Expression) -> False :
      do(check-not-mem{info,_},e) 
      match(e) :
         (e:WRef) : if kind(e) == MemKind() : add(errors,IsMem(info,name(e)))
         (e:WSubfield) : check-not-mem(info,exp(e))
         (e:WIndex) : check-not-mem(info,exp(e))
         (e) : false
   defn check-is-reg (info:FileInfo,e:Expression) -> False :
      do(check-is-reg{info,_},e) 
      match(e) :
         (e:WRef) : if kind(e) != RegKind() : add(errors,OnResetNotReg(info,name(e)))
         (e:WSubfield) : check-is-reg(info,exp(e))
         (e:WIndex) : check-is-reg(info,exp(e))
         (e) : false
   defn check-is-mem (info:FileInfo,e:Expression) -> False :
      do(check-is-mem{info,_},e) 
      match(e) :
         (e:WRef) : if kind(e) != MemKind() : add(errors,NotMem(info,name(e)))
         (e:WSubfield) : check-is-mem(info,exp(e))
         (e:WIndex) : check-is-mem(info,exp(e))
         (e) : false

   defn check-kinds-e (info:FileInfo,e:Expression) -> False :
      do(check-kinds-e{info,_},e)
      match(e) :
         (e:ReadPort) : 
            check-is-mem(info,mem(e))
            check-not-mem(info,index(e))
            check-not-mem(info,enable(e))
         (e:WritePort) : 
            check-is-mem(info,mem(e))
            check-not-mem(info,index(e))
            check-not-mem(info,enable(e))
         (e:Pad) :
            check-not-mem(info,value(e))
         (e) : do(check-not-mem{info,_},e)
   defn check-kinds-s (s:Stmt) -> False :
      do(check-kinds-e{info(s),_:Expression},s)
      match(s) : 
         (s:DefNode) : check-not-mem(info(s),value(s))
         (s:DefAccessor) : check-not-mem(info(s),index(s))
         (s:Conditionally) : check-not-mem(info(s),pred(s))
         (s:Connect) : 
            check-not-mem(info(s),loc(s))
            check-not-mem(info(s),exp(s))
         (s:OnReset) : 
            check-is-reg(info(s),loc(s))
            check-not-mem(info(s),exp(s))
         (s) : false
      do(check-kinds-s,s)
   
   for m in modules(c) do :
      check-kinds-s(body(m))
   throw(PassExceptions(errors)) when not empty?(errors)
   c


;==================== CHECK TYPES =====================
; o expression in pad must be a ground type
; o Subfields are only on bundles, before type inference <- need to not error, just do unknown-type
; o Indexes are only on vectors
; o pred in conditionally must be of type UInt
; o enable/index in read/writeports must be UInt
; o node's value cannot be a bundle with a flip in it
; o := has same types
; o 2nd arg in dshr/l must be UInt, in general do primops

;----------------- Errors ---------------------
defn SubfieldNotInBundle (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Subfield " name " is not in bundle."]

defn SubfieldOnNonBundle (info:FileInfo, name:Symbol) :
   PassException $ string-join $
   [info ": Subfield " name " is accessed on a non-bundle."]

defn IndexTooLarge (info:FileInfo, value:Int) :
   PassException $ string-join $
   [info ": Index with value " value " is too large."]

defn IndexOnNonVector (info:FileInfo) :
   PassException $ string-join $
   [info ": Index illegal on non-vector type."]

defn IndexNotUInt (info:FileInfo) :
   PassException $ string-join $
   [info ": Index is not of UIntType."]

defn EnableNotUInt (info:FileInfo) :
   PassException $ string-join $
   [info ": Enable is not of UIntType."]

defn PadNotGround (info:FileInfo) :
   PassException $ string-join $
   [info ": Illegal Pad on non-ground type."]

defn InvalidConnect (info:FileInfo) :
   PassException $ string-join $
   [info ": Type mismatch."]

defn PredNotUInt (info:FileInfo) :
   PassException $ string-join $
   [info ": Predicate not a UIntType."]

;---------------- Helper Functions --------------
defmethod equal? (t1:Type,t2:Type) -> True|False :
   match(t1,t2) : 
      (t1:UIntType,t2:UIntType) : true
      (t1:SIntType,t2:SIntType) : true
      (t1:BundleType,t2:BundleType) : 
         var same? = true
         for (f1 in fields(t1),f2 in fields(t2)) do :
            if flip(f1) != flip(f2) : same? = false
            if name(f1) != name(f2) : same? = false
            if type(f1) != type(f2) : same? = false
         same?
      (t1:VectorType,t2:VectorType) :
         if type(t1) == type(t2) and size(t1) == size(t2) : true
         else : false
      (t1,t2) : false
            
defn u () -> UIntType : UIntType(UnknownWidth())
defn s () -> SIntType : SIntType(UnknownWidth())

;----------------- Check Types Pass ---------------------
public defn check-types (c:Circuit) -> Circuit : 
   val errors = Vector<PassException>()
   defn check-types-e (info:FileInfo,e:Expression) -> Expression :
      match(map(check-types-e{info,_},e)) :
         (e:WRef) : e
         (e:WSubfield) : 
            match(type(exp(e))) : 
               (t:BundleType) : 
                  val ft = for p in fields(t) find : name(p) == name(e)
                  if ft == false : add(errors,SubfieldNotInBundle(info,name(e)))
               (t) : add(errors,SubfieldOnNonBundle(info,name(e)))
         (e:WIndex) : 
            match(type(exp(e))) :
               (t:VectorType) : 
                  if value(e) >= size(t) : add(errors,IndexTooLarge(info,value(e)))
               (t) : add(errors,IndexOnNonVector(info))
         (e:DoPrim) : false ;check-types-primop(e)
         (e:ReadPort|WritePort) : 
            if type(index(e)) != u() : add(errors,IndexNotUInt(info))
            if type(enable(e)) != u() : add(errors,EnableNotUInt(info))
         (e:Register) :
            if type(enable(e)) != u() : add(errors,EnableNotUInt(info))
         (e:Pad) :
            val t = type(value(e))
            if not (t == u() or t == s()) : add(errors,PadNotGround(info))
         (e:UIntValue|SIntValue) : false
      e
   defn check-types-s (s:Stmt) -> Stmt :
      map{check-types-s,_} $ 
      match(map(check-types-e{info(s),_},s)) : 
         (s:Connect) : 
            if type(loc(s)) != type(exp(s)) : add(errors,InvalidConnect(info(s)))
            s
         (s:OnReset) : 
            if type(loc(s)) != type(exp(s)) : add(errors,InvalidConnect(info(s)))
            s
         (s:Conditionally) :
            if type(pred(s)) != u() : add(errors,PredNotUInt(info(s)))
            s
         (s) : s
   
   for m in modules(c) do :
      check-types-s(body(m))
   throw(PassExceptions(errors)) when not empty?(errors)
   c

;================= GENDER CHECK  ==========================
; o Nodes always male
; o Accessors only have one gender, unless rdwr
; o output/input only one gender
; o correctly check for the base bundle

;----------------- Errors ---------------------
defn WrongGender (info:FileInfo,expr:Symbol,wrong:Symbol,right:Symbol) :
   PassException $ string-join $
   [info ": Expression " expr "has gender " wrong " but requires gender " right "."]

defn UnknownGenders (info:FileInfo,name:Symbol) : 
   PassException $ string-join $
   [info ": Accessor " name " has an unknown gender."]

;---------------- Helper Functions --------------
defn dir-to-gender (d:Direction) -> Gender :
   switch {_ == d} :
      INPUT : MALE
      OUTPUT : FEMALE

;----------------- Check Genders Pass ---------------------

public defn check-genders (c:Circuit) -> Circuit :
   val errors = Vector<PassException>()
   defn check-gender (info:FileInfo,genders:HashTable<Symbol,Gender>,e:Expression,right:Gender) -> False :
      val gender = get-gender(e,genders)
      if gender != right and gender != BI-GENDER:
         add(errors,WrongGender(info,to-symbol(e),to-symbol(gender),to-symbol(right)))

   defn get-gender (e:Expression,genders:HashTable<Symbol,Gender>) -> Gender :
      match(e) :
         (e:WRef) : genders[name(e)]
         (e:WSubfield) : 
            val f = {_ as Field} $ for f in fields(type(exp(e)) as BundleType) find : name(f) == name(e)
            get-gender(exp(e),genders) * flip(f)
         (e:WIndex) : get-gender(exp(e),genders)
         (e:Pad) : MALE
         (e:DoPrim) : MALE
         (e:UIntValue) : MALE
         (e:SIntValue) : MALE
         (e:ReadPort) : MALE
         (e:WritePort) : FEMALE
         (e:Register) : MALE

   defn check-genders-e (info:FileInfo,e:Expression,genders:HashTable<Symbol,Gender>) -> False :
      do(check-genders-e{info,_,genders},e)
      match(e) :
         (e:WRef) : false
         (e:WSubfield) : false
         (e:WIndex) : false
         (e:Pad) : check-gender(info,genders,value(e),MALE)
         (e:DoPrim) : 
            for e in args(e) do :
               check-gender(info,genders,e,MALE)
         (e:UIntValue) : false
         (e:SIntValue) : false
         (e:ReadPort) : do(check-gender{info,genders,_,MALE},e)
         (e:WritePort) : do(check-gender{info,genders,_,MALE},e)
         (e:Register) : do(check-gender{info,genders,_,MALE},e)
     
   defn check-genders-s (s:Stmt,genders:HashTable<Symbol,Gender>) -> False :
      do(check-genders-e{info(s),_:Expression,genders},s)
      match(s) :
         (s:DefWire) : genders[name(s)] = BI-GENDER
         (s:DefRegister) : genders[name(s)] = BI-GENDER
         (s:DefNode) : 
            check-gender(info(s),genders,value(s),MALE)
            genders[name(s)] = MALE
         (s:DefMemory) : genders[name(s)] = BI-GENDER
         (s:DefInstance) : genders[name(s)] = MALE
         (s:WDefAccessor) : 
            if gender(s) == UNKNOWN-GENDER : add(errors,UnknownGenders(info(s),name(s)))
            check-gender(info(s),genders,index(s),MALE)
            check-gender(info(s),genders,source(s),gender(s))
            genders[name(s)] = gender(s)
         (s:Connect) : 
            check-gender(info(s),genders,loc(s),FEMALE)
            check-gender(info(s),genders,exp(s),MALE)
         (s:OnReset) : 
            check-gender(info(s),genders,loc(s),FEMALE)
            check-gender(info(s),genders,exp(s),MALE)
         (s:Conditionally) :
            check-gender(info(s),genders,pred(s),MALE)
         (s:EmptyStmt) : false
         (s:Begin) : false


   for m in modules(c) do :
      val genders = HashTable<Symbol,Gender>(symbol-hash)
      for p in ports(m) do :
         genders[name(p)] = dir-to-gender(direction(p))
      check-genders-s(body(m),genders)
   throw(PassExceptions(errors)) when not empty?(errors)
   c