138 end |
138 end |
139 |
139 |
140 |
140 |
141 section {* type definition for the quotient type *} |
141 section {* type definition for the quotient type *} |
142 |
142 |
|
143 (* the auxiliary data for the quotient types *) |
143 use "quotient_info.ML" |
144 use "quotient_info.ML" |
144 use "quotient.ML" |
145 |
|
146 ML {* |
|
147 fun error_msg pre post msg = |
|
148 msg |> quote |
|
149 |> enclose (pre ^ " ") (" " ^ post) |
|
150 |> error |
|
151 *} |
145 |
152 |
146 declare [[map list = (map, LIST_REL)]] |
153 declare [[map list = (map, LIST_REL)]] |
147 declare [[map * = (prod_fun, prod_rel)]] |
154 declare [[map * = (prod_fun, prod_rel)]] |
148 declare [[map "fun" = (fun_map, FUN_REL)]] |
155 declare [[map "fun" = (fun_map, FUN_REL)]] |
149 |
156 |
150 ML {* maps_lookup @{theory} "List.list" *} |
157 ML {* maps_lookup @{theory} "List.list" *} |
151 ML {* maps_lookup @{theory} "*" *} |
158 ML {* maps_lookup @{theory} "*" *} |
152 ML {* maps_lookup @{theory} "fun" *} |
159 ML {* maps_lookup @{theory} "fun" *} |
|
160 |
|
161 |
|
162 (* definition of the quotient types *) |
|
163 use "quotient.ML" |
|
164 |
153 |
165 |
154 text {* FIXME: auxiliary function *} |
166 text {* FIXME: auxiliary function *} |
155 ML {* |
167 ML {* |
156 val no_vars = Thm.rule_attribute (fn context => fn th => |
168 val no_vars = Thm.rule_attribute (fn context => fn th => |
157 let |
169 let |
288 let |
299 let |
289 val otrm_ty = fastype_of otrm |
300 val otrm_ty = fastype_of otrm |
290 val nconst_ty = exchange_ty qenv otrm_ty |
301 val nconst_ty = exchange_ty qenv otrm_ty |
291 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
302 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
292 val def_trm = get_const_def nconst otrm qenv lthy |
303 val def_trm = get_const_def nconst otrm qenv lthy |
293 |
|
294 val _ = print_env qenv lthy |
|
295 val _ = Syntax.string_of_typ lthy otrm_ty |> tracing |
|
296 val _ = Syntax.string_of_typ lthy nconst_ty |> tracing |
|
297 val _ = Syntax.string_of_term lthy def_trm |> tracing |
|
298 in |
304 in |
299 define (nconst_bname, mx, def_trm) lthy |
305 define (nconst_bname, mx, def_trm) lthy |
300 end |
306 end |
301 *} |
307 *} |
302 |
308 |
303 ML {* |
309 ML {* |
304 fun build_qenv lthy qtys = |
310 (* difference of two types *) |
305 let |
311 fun diff (T, S) Ds = |
306 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
312 case (T, S) of |
307 val thy = ProofContext.theory_of lthy |
313 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
308 |
314 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
309 fun find_assoc ((qty', rty')::rest) qty = |
315 | (Type (a, Ts), Type (b, Us)) => |
310 let |
316 if a = b then diffs (Ts, Us) Ds else (T, S)::Ds |
311 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
317 | _ => (T, S)::Ds |
312 in |
318 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
313 (Envir.norm_type inst qty, Envir.norm_type inst rty') |
319 | diffs ([], []) Ds = Ds |
314 end |
320 | diffs _ _ = error "Unequal length of type arguments" |
315 | find_assoc [] qty = |
321 *} |
316 let |
322 |
317 val qtystr = quote (Syntax.string_of_typ lthy qty) |
323 ML {* |
318 in |
324 fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy = |
319 error (implode ["Quotient type ", qtystr, " does not exists"]) |
|
320 end |
|
321 in |
|
322 map (find_assoc qenv) qtys |
|
323 end |
|
324 *} |
|
325 |
|
326 |
|
327 ML {* |
|
328 fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy = |
|
329 let |
325 let |
330 val (lhs_, rhs) = Logic.dest_equals prop |
326 val (_, rhs) = Logic.dest_equals prop |
|
327 val rty = fastype_of rhs |
|
328 val qenv = distinct (op=) (diff (qty, rty) []) |
331 in |
329 in |
332 make_const_def bind rhs mx qenv lthy |
330 make_const_def bind rhs mx qenv lthy |
333 end |
331 end |
334 *} |
332 *} |
335 |
333 |
336 ML {* |
334 ML {* |
|
335 val constdecl = |
|
336 OuterParse.binding -- |
|
337 (OuterParse.$$$ "::" |-- OuterParse.!!! |
|
338 (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_)) |
|
339 >> OuterParse.triple2; |
|
340 *} |
|
341 |
|
342 ML {* |
337 val quotdef_parser = |
343 val quotdef_parser = |
338 Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
344 (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) |
339 (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- |
345 *} |
340 OuterParse.prop)) >> OuterParse.triple2 |
346 |
341 *} |
347 ML {* |
342 |
348 fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy = |
343 ML {* |
|
344 fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = |
|
345 let |
349 let |
346 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs) |
350 val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr |
347 val qenv = build_qenv lthy qtys |
351 val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr |
348 val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr |
|
349 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
|
350 in |
352 in |
351 quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd |
353 quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd |
352 end |
354 end |
353 *} |
355 *} |
354 |
356 |
355 ML {* |
357 ML {* |
356 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
358 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |