src/metis/mlibModel.sml

60 type fix = int -> {func : (string * int list) -> int option,
65     val {func = func1, pred = pred1} = fix1 N
66     val {func = func2, pred = pred2} = fix2 N
67     fun func x = case func1 x of NONE => func2 x | sn => sn
70     {func = func, pred = pred}
77     val {func,pred} = fix N
78     fun func' (f,a) = case map_fn f of NONE => NONE | SOME f' => func (f',a)
81     {func = func', pred = pred'}
85   fn _ => {func = K NONE, pred = fn ("=",[m,n]) => SOME (m = n) | _ => NONE};
89     fun func ("id",[n]) = SOME n
90       | func ("fst",[n,_]) = SOME n
91       | func ("snd",[_,n]) = SOME n
92       | func ("#1",n::_) = SOME n
93       | func ("#2",_::n::_) = SOME n
94       | func ("#3",_::_::n::_) = SOME n
95       | func _ = NONE
99     K {func = func, pred = pred}
116       fun func ("0",[]) = SOME zero
117         | func ("1",[]) = SOME one
118         | func ("2",[]) = SOME two
119         | func ("suc",[n]) = SOME (f (n + one))
120         | func ("pre",[n]) = SOME (f (n - one))
121         | func ("~",[n]) = SOME (f (~n))
122         | func ("+",[m,n]) = SOME (f (m + n))
123         | func ("-",[m,n]) = SOME (f (m - n))
124         | func ("*",[m,n]) = SOME (f (m * n))
125         | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one)
126         | func ("mod",[m,n]) = SOME (if n = zero then m else m mod n)
127         | func _ = NONE
138       {func = func, pred = pred}
147     fun func ("0",[]) = SOME zero
148       | func ("1",[]) = SOME one
149       | func ("2",[]) = SOME two
150       | func ("suc",[m]) = SOME (f (m + one))
151       | func ("pre",[m]) = SOME (f (m - one))
152       | func ("+",[m,n]) = SOME (f (m + n))
153       | func ("-",[m,n]) = SOME (f (m - n))
154       | func ("*",[m,n]) = SOME (f (m * n))
155       | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one)
156       | func _ = NONE
164     {func = func, pred = pred}
180     fun func ("empty",[]) = SOME (from_set empty)
181       | func ("univ",[]) = SOME (from_set univ)
182       | func ("union",[m,n]) = SOME (from_set (union (to_set m) (to_set n)))
183       | func ("inter",[m,n]) = SOME (from_set (inter (to_set m) (to_set n)))
184       | func ("compl",[n]) = SOME (from_set (compl (to_set n)))
185       | func ("card",[n]) = SOME (count_bits (to_set n))
186       | func _ = NONE
197     {func = func, pred = pred}
309       val {func = fixf, pred = fixp} = r n