(*  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