equal
deleted
inserted
replaced
58 list_ccomb(%%:(dname^"_when"),map |
58 list_ccomb(%%:(dname^"_when"),map |
59 (fn (con',args) => (List.foldr /\# |
59 (fn (con',args) => (List.foldr /\# |
60 (if con'=con then TT else FF) args)) cons)) |
60 (if con'=con then TT else FF) args)) cons)) |
61 in map ddef cons end; |
61 in map ddef cons end; |
62 |
62 |
63 val mat_defs = let |
63 val mat_defs = |
64 fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == |
64 let |
65 list_ccomb(%%:(dname^"_when"),map |
65 fun mdef (con,_) = |
66 (fn (con',args) => (List.foldr /\# |
66 let |
67 (if con'=con |
67 val k = Bound 0 |
68 then mk_return (mk_ctuple (map (bound_arg args) args)) |
68 val x = Bound 1 |
69 else mk_fail) args)) cons)) |
69 fun one_con (con', args') = |
70 in map mdef cons end; |
70 if con'=con then k else List.foldr /\# mk_fail args' |
|
71 val w = list_ccomb(%%:(dname^"_when"), map one_con cons) |
|
72 val rhs = /\ "x" (/\ "k" (w ` x)) |
|
73 in (mat_name con ^"_def", %%:(mat_name con) == rhs) end |
|
74 in map mdef cons end; |
71 |
75 |
72 val pat_defs = |
76 val pat_defs = |
73 let |
77 let |
74 fun pdef (con,args) = |
78 fun pdef (con,args) = |
75 let |
79 let |