1(* Title: Pure/defs.ML 2 Author: Makarius 3 4Global well-formedness checks for overloaded definitions (mixed constants and 5types). Recall that constant definitions may be explained syntactically within 6Pure, but type definitions require particular set-theoretic semantics. 7*) 8 9signature DEFS = 10sig 11 datatype item_kind = Const | Type 12 type item = item_kind * string 13 type entry = item * typ list 14 val item_kind_ord: item_kind ord 15 val plain_args: typ list -> bool 16 type context = Proof.context * (Name_Space.T * Name_Space.T) 17 val global_context: theory -> context 18 val space: context -> item_kind -> Name_Space.T 19 val pretty_item: context -> item -> Pretty.T 20 val pretty_args: Proof.context -> typ list -> Pretty.T list 21 val pretty_entry: context -> entry -> Pretty.T 22 type T 23 type spec = 24 {def: string option, 25 description: string, 26 pos: Position.T, 27 lhs: typ list, 28 rhs: entry list} 29 val all_specifications_of: T -> (item * spec list) list 30 val specifications_of: T -> item -> spec list 31 val dest: T -> 32 {restricts: (entry * string) list, 33 reducts: (entry * entry list) list} 34 val dest_constdefs: T list -> T -> (string * string) list 35 val empty: T 36 val merge: context -> T * T -> T 37 val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T 38 val get_deps: T -> item -> (typ list * entry list) list 39end; 40 41structure Defs: DEFS = 42struct 43 44(* specification items *) 45 46datatype item_kind = Const | Type; 47type item = item_kind * string; 48type entry = item * typ list; 49 50fun item_kind_ord (Const, Type) = LESS 51 | item_kind_ord (Type, Const) = GREATER 52 | item_kind_ord _ = EQUAL; 53 54structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord); 55 56 57(* pretty printing *) 58 59type context = Proof.context * (Name_Space.T * Name_Space.T); 60 61fun global_context thy = 62 (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy)); 63 64fun space ((_, spaces): context) kind = 65 if kind = Const then #1 spaces else #2 spaces; 66 67fun pretty_item (context as (ctxt, _)) (kind, name) = 68 let val prt_name = Name_Space.pretty ctxt (space context kind) name in 69 if kind = Const then prt_name 70 else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name] 71 end; 72 73fun pretty_args ctxt args = 74 if null args then [] 75 else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; 76 77fun pretty_entry context (c, args) = 78 Pretty.block (pretty_item context c :: pretty_args (#1 context) args); 79 80 81(* type arguments *) 82 83fun plain_args args = 84 forall Term.is_TVar args andalso not (has_duplicates (op =) args); 85 86fun disjoint_args (Ts, Us) = 87 not (Type.could_unifys (Ts, Us)) orelse 88 ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false) 89 handle Type.TUNIFY => true); 90 91fun match_args (Ts, Us) = 92 if Type.could_matches (Ts, Us) then 93 Option.map Envir.subst_type 94 (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE) 95 else NONE; 96 97 98(* datatype defs *) 99 100type spec = 101 {def: string option, 102 description: string, 103 pos: Position.T, 104 lhs: typ list, 105 rhs: entry list}; 106 107type def = 108 {specs: spec Inttab.table, (*source specifications*) 109 restricts: (typ list * string) list, (*global restrictions imposed by incomplete patterns*) 110 reducts: (typ list * entry list) list}; (*specifications as reduction system*) 111 112fun make_def (specs, restricts, reducts) = 113 {specs = specs, restricts = restricts, reducts = reducts}: def; 114 115fun map_def c f = 116 Itemtab.default (c, make_def (Inttab.empty, [], [])) #> 117 Itemtab.map_entry c (fn {specs, restricts, reducts}: def => 118 make_def (f (specs, restricts, reducts))); 119 120 121datatype T = Defs of def Itemtab.table; 122 123fun lookup_list which defs c = 124 (case Itemtab.lookup defs c of 125 SOME (def: def) => which def 126 | NONE => []); 127 128fun all_specifications_of (Defs defs) = 129 (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs); 130 131fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; 132 133val restricts_of = lookup_list #restricts; 134val reducts_of = lookup_list #reducts; 135 136fun dest (Defs defs) = 137 let 138 val restricts = Itemtab.fold (fn (c, {restricts, ...}) => 139 fold (fn (args, description) => cons ((c, args), description)) restricts) defs []; 140 val reducts = Itemtab.fold (fn (c, {reducts, ...}) => 141 fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; 142 in {restricts = restricts, reducts = reducts} end; 143 144fun dest_constdefs prevs (Defs defs) = 145 let 146 fun prev_spec c i = prevs |> exists (fn Defs prev_defs => 147 (case Itemtab.lookup prev_defs c of 148 NONE => false 149 | SOME {specs, ...} => Inttab.defined specs i)); 150 in 151 (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) => 152 specs |> Inttab.fold (fn (i, spec) => 153 if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i) 154 then cons (#2 c, the (#def spec)) else I)) 155 end; 156 157val empty = Defs Itemtab.empty; 158 159 160(* specifications *) 161 162fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = 163 Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => 164 i = j orelse disjoint_args (Ts, Us) orelse 165 error ("Clash of specifications for " ^ 166 Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^ 167 " " ^ quote a ^ Position.here pos_a ^ "\n" ^ 168 " " ^ quote b ^ Position.here pos_b)); 169 170fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = 171 let 172 val specs' = 173 Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2)) 174 specs2 specs1; 175 in make_def (specs', restricts, reducts) end; 176 177fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) => 178 (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts))); 179 180 181(* normalized dependencies: reduction with well-formedness check *) 182 183local 184 185val prt = Pretty.string_of oo pretty_entry; 186 187fun err context (c, Ts) (d, Us) s1 s2 = 188 error (s1 ^ " dependency of " ^ prt context (c, Ts) ^ " -> " ^ prt context (d, Us) ^ s2); 189 190fun acyclic context (c, Ts) (d, Us) = 191 c <> d orelse 192 is_none (match_args (Ts, Us)) orelse 193 err context (c, Ts) (d, Us) "Circular" ""; 194 195fun reduction context defs const deps = 196 let 197 fun reduct Us (Ts, rhs) = 198 (case match_args (Ts, Us) of 199 NONE => NONE 200 | SOME subst => SOME (map (apsnd (map subst)) rhs)); 201 fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d); 202 203 val reds = map (`reducts) deps; 204 val deps' = 205 if forall (is_none o #1) reds then NONE 206 else SOME (fold_rev 207 (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); 208 val _ = forall (acyclic context const) (the_default deps deps'); 209 in deps' end; 210 211fun restriction context defs (c, Ts) (d, Us) = 212 plain_args Us orelse 213 (case find_first (fn (Rs, _) => not (disjoint_args (Rs, Us))) (restricts_of defs d) of 214 SOME (Rs, description) => 215 err context (c, Ts) (d, Us) "Malformed" 216 ("\n(restriction " ^ prt context (d, Rs) ^ " from " ^ quote description ^ ")") 217 | NONE => true); 218 219in 220 221fun normalize context = 222 let 223 fun check_def defs (c, {reducts, ...}: def) = 224 reducts |> forall (fn (Ts, deps) => forall (restriction context defs (c, Ts)) deps); 225 fun check_defs defs = Itemtab.forall (check_def defs) defs; 226 227 fun norm_update (c, {reducts, ...}: def) (changed, defs) = 228 let 229 val reducts' = reducts |> map (fn (Ts, deps) => 230 (Ts, perhaps (reduction context defs (c, Ts)) deps)); 231 in 232 if reducts = reducts' then (changed, defs) 233 else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) 234 end; 235 fun norm_loop defs = 236 (case Itemtab.fold norm_update defs (false, defs) of 237 (true, defs') => norm_loop defs' 238 | (false, _) => defs); 239 in norm_loop #> tap check_defs end; 240 241fun dependencies context (c, args) restr deps = 242 map_def c (fn (specs, restricts, reducts) => 243 let 244 val restricts' = Library.merge (op =) (restricts, restr); 245 val reducts' = insert (op =) (args, deps) reducts; 246 in (specs, restricts', reducts') end) 247 #> normalize context; 248 249end; 250 251 252(* merge *) 253 254fun merge context (Defs defs1, Defs defs2) = 255 let 256 fun add_deps (c, args) restr deps defs = 257 if AList.defined (op =) (reducts_of defs c) args then defs 258 else dependencies context (c, args) restr deps defs; 259 fun add_def (c, {restricts, reducts, ...}: def) = 260 fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; 261 in 262 Defs (Itemtab.join (join_specs context) (defs1, defs2) 263 |> normalize context |> Itemtab.fold add_def defs2) 264 end; 265 266 267(* define *) 268 269fun define context unchecked def description (c, args) deps (Defs defs) = 270 let 271 val pos = Position.thread_data (); 272 val restr = 273 if plain_args args orelse 274 (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false) 275 then [] else [(args, description)]; 276 val spec = 277 (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); 278 val defs' = defs |> update_specs context c spec; 279 in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end; 280 281fun get_deps (Defs defs) c = reducts_of defs c; 282 283end; 284