109 |
109 |
110 (* normalized dependencies: reduction with well-formedness check *) |
110 (* normalized dependencies: reduction with well-formedness check *) |
111 |
111 |
112 local |
112 local |
113 |
113 |
|
114 val prt = Pretty.string_of oo pretty_const; |
|
115 fun err pp (c, args) (d, Us) s1 s2 = |
|
116 error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2); |
|
117 |
114 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts |
118 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts |
115 | contained _ _ = false; |
119 | contained _ _ = false; |
116 |
120 |
|
121 fun acyclic pp defs (c, args) (d, Us) = |
|
122 c <> d orelse |
|
123 exists (fn U => exists (contained U) args) Us orelse |
|
124 is_none (match_args (args, Us)) orelse |
|
125 err pp (c, args) (d, Us) "Circular" ""; |
|
126 |
117 fun wellformed pp defs (c, args) (d, Us) = |
127 fun wellformed pp defs (c, args) (d, Us) = |
118 let |
128 forall is_TVar Us orelse |
119 val prt = Pretty.string_of o pretty_const pp; |
129 (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of |
120 fun err s1 s2 = |
130 SOME (Ts, name) => |
121 error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " -> " ^ prt (d, Us) ^ s2); |
131 err pp (c, args) (d, Us) "Malformed" |
122 in |
132 ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")") |
123 exists (fn U => exists (contained U) args) Us orelse |
133 | NONE => true); |
124 (c <> d andalso forall is_TVar Us) orelse |
|
125 (if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else |
|
126 (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of |
|
127 SOME (Ts, name) => |
|
128 is_some (match_args (Ts, Us)) orelse |
|
129 err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")") |
|
130 | NONE => true)) |
|
131 end; |
|
132 |
134 |
133 fun reduction pp defs const deps = |
135 fun reduction pp defs const deps = |
134 let |
136 let |
135 fun reduct Us (Ts, rhs) = |
137 fun reduct Us (Ts, rhs) = |
136 (case match_args (Ts, Us) of |
138 (case match_args (Ts, Us) of |
142 | add (SOME dps, _) = fold (insert (op =)) dps; |
144 | add (SOME dps, _) = fold (insert (op =)) dps; |
143 val reds = map (`reducts) deps; |
145 val reds = map (`reducts) deps; |
144 val deps' = |
146 val deps' = |
145 if forall (is_none o #1) reds then NONE |
147 if forall (is_none o #1) reds then NONE |
146 else SOME (fold_rev add reds []); |
148 else SOME (fold_rev add reds []); |
147 val _ = forall (wellformed pp defs const) (the_default deps deps'); |
149 val _ = forall (acyclic pp defs const) (the_default deps deps'); |
148 in deps' end; |
150 in deps' end; |
149 |
151 |
150 fun normalize pp = |
152 fun normalize pp = |
151 let |
153 let |
152 fun norm_update (c, {reducts, ...}: def) (changed, defs) = |
154 fun norm_update (c, {reducts, ...}: def) (changed, defs) = |
160 end; |
162 end; |
161 fun norm_all defs = |
163 fun norm_all defs = |
162 (case Symtab.fold norm_update defs (false, defs) of |
164 (case Symtab.fold norm_update defs (false, defs) of |
163 (true, defs') => norm_all defs' |
165 (true, defs') => norm_all defs' |
164 | (false, _) => defs); |
166 | (false, _) => defs); |
165 in norm_all end; |
167 fun check defs (c, {reducts, ...}: def) = |
|
168 reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps); |
|
169 in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end; |
166 |
170 |
167 in |
171 in |
168 |
172 |
169 fun dependencies pp (c, args) restr deps = |
173 fun dependencies pp (c, args) restr deps = |
170 map_def c (fn (specs, restricts, reducts) => |
174 map_def c (fn (specs, restricts, reducts) => |