NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Monomorphisation for using BDDs/analysis #30

Open nickgian opened 4 years ago

nickgian commented 4 years ago

A function that uses BDDs (or some analyses that requires the types) may have polymorphic type which causes the interpreter to fail. For instance, the type of transFailure depends on transProt, and type inference gives the most general type for this which includes type quantifiers.

let transFailure transProt e x =
  let x = mapIf (fun e1 -> e = e1) (fun v -> None) x in
  mapIf (fun e1 -> !(e=e1)) (fun v -> transProt e v) x

The workaround for now is to inline and hence the type of transProt will be visible in the body of transFailure. Another option would be to have a monomorphisation pass which creates specialized version of transFailure with the type of each different transProt that it's called with. This is less intrusive than inlining.