9 

    10 

    11 structure Nominal_Function_Common =

    12 struct

    13 

    14 

    15 (* Configuration management *)

    16 datatype nominal_function_opt

    17   = Sequential

    18   | Default of string

    19   | DomIntros

    20   | No_Partials

    21   | Invariant of string

    22 

    23 datatype nominal_function_config = NominalFunctionConfig of

    24  {sequential: bool,

    25   default: string option,

    26   domintros: bool,

    27   partials: bool,

    28   inv: string option}

    29 

    30 fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =

    31     NominalFunctionConfig 

    32       {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}

    33   | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =

    34     NominalFunctionConfig 

    35       {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}

    36   | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =

    37     NominalFunctionConfig 

    38       {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}

    39   | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =

    40     NominalFunctionConfig 

    41       {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}

    42   | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =

    43     NominalFunctionConfig 

    44       {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}

    45 

    46 val nominal_default_config =

    47   NominalFunctionConfig { sequential=false, default=NONE,

    48     domintros=false, partials=true, inv=NONE}

    49 

    50 end