(*  Nominal Function Common
    Author: Christian Urban

    heavily based on the code of Alexander Krauss
    (code forked on 5 June 2011)

Redefinition of config datatype 
*)



structure Nominal_Function_Common =
struct


(* Configuration management *)
datatype nominal_function_opt
  = Sequential
  | Default of string
  | DomIntros
  | No_Partials
  | Invariant of string

datatype nominal_function_config = NominalFunctionConfig of
 {sequential: bool,
  default: string option,
  domintros: bool,
  partials: bool,
  inv: string option}

fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}
  | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}
  | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}
  | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}
  | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
    NominalFunctionConfig 
      {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}

val nominal_default_config =
  NominalFunctionConfig { sequential=false, default=NONE,
    domintros=false, partials=true, inv=NONE}

end