23 val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state |
23 val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state |
24 val prove_interpretation_in_class: tactic -> class * class -> theory -> theory |
24 val prove_interpretation_in_class: tactic -> class * class -> theory -> theory |
25 val intro_classes_tac: thm list -> tactic |
25 val intro_classes_tac: thm list -> tactic |
26 val default_intro_classes_tac: thm list -> tactic |
26 val default_intro_classes_tac: thm list -> tactic |
27 val class_of_locale: theory -> string -> class option |
27 val class_of_locale: theory -> string -> class option |
28 val local_syntax: theory -> class -> bool |
|
29 val print_classes: theory -> unit |
28 val print_classes: theory -> unit |
30 |
29 |
31 val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state |
30 val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state |
32 val instance: arity list -> ((bstring * Attrib.src list) * term) list |
31 val instance: arity list -> ((bstring * Attrib.src list) * term) list |
33 -> (thm list -> theory -> theory) |
32 -> (thm list -> theory -> theory) |
327 (** class data **) |
325 (** class data **) |
328 |
326 |
329 datatype class_data = ClassData of { |
327 datatype class_data = ClassData of { |
330 locale: string, |
328 locale: string, |
331 consts: (string * string) list |
329 consts: (string * string) list |
332 (*locale parameter ~> theory constant name*), |
330 (*locale parameter ~> constant name*), |
333 local_sort: sort, |
331 local_sort: sort, |
334 inst: typ Symtab.table * term Symtab.table |
332 inst: typ Symtab.table * term Symtab.table |
335 (*canonical interpretation*), |
333 (*canonical interpretation*), |
336 intro: thm, |
334 intro: thm, |
337 local_syntax: bool, |
335 local_syntax: bool, |
338 defs: thm list, |
336 defs: thm list, |
339 localized: (string * (term * (class * int))) list |
337 operations: (string * (term * int) option) list |
340 (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*) |
338 (*constant name ~> (locale term, instantiaton index of class typ)*) |
341 }; |
339 }; |
342 |
340 |
343 fun rep_class_data (ClassData d) = d; |
341 fun rep_class_data (ClassData d) = d; |
344 fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) = |
342 fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations)) = |
345 ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro, |
343 ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro, |
346 local_syntax = local_syntax, defs = defs, localized = localized }; |
344 local_syntax = local_syntax, defs = defs, operations = operations }; |
347 fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) = |
345 fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, operations }) = |
348 mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized))) |
346 mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, operations))) |
349 fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, |
347 fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, |
350 intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 }, |
348 intro = intro, local_syntax = local_syntax, defs = defs1, operations = operations1 }, |
351 ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _, |
349 ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _, |
352 defs = defs2, localized = localized2 }) = |
350 defs = defs2, operations = operations2 }) = |
353 mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), |
351 mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), |
354 (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2))); |
352 (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (operations1, operations2))); |
355 |
353 |
356 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); |
354 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); |
357 |
355 |
358 structure ClassData = TheoryDataFun |
356 structure ClassData = TheoryDataFun |
359 ( |
357 ( |
439 |
437 |
440 fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) = |
438 fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) = |
441 ClassData.map (fn (gr, tab) => ( |
439 ClassData.map (fn (gr, tab) => ( |
442 gr |
440 gr |
443 |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst, |
441 |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst, |
444 intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts))) |
442 intro, local_syntax), ([], map (apsnd (SOME o rpair 0 o Free) o swap) consts))) |
445 |> fold (curry Graph.add_edge class) superclasses, |
443 |> fold (curry Graph.add_edge class) superclasses, |
446 tab |
444 tab |
447 |> Symtab.update (locale, class) |
445 |> Symtab.update (locale, class) |
448 )); |
446 )); |
449 |
447 |
450 fun add_class_const_def (class, (entry, def)) = |
448 fun register_const (class, (entry, def)) = |
451 (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) |
449 (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) |
452 (fn (defs, localized) => (def :: defs, (apsnd o apsnd) (pair class) entry :: localized)); |
450 (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations)); |
|
451 |
|
452 fun register_abbrev class abbrev = |
|
453 (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd) |
|
454 (cons (abbrev, NONE)); |
453 |
455 |
454 |
456 |
455 (** rule calculation, tactics and methods **) |
457 (** rule calculation, tactics and methods **) |
456 |
458 |
457 fun class_intro thy locale class sups = |
459 fun class_intro thy locale class sups = |
541 "apply some intro/elim rule")]); |
543 "apply some intro/elim rule")]); |
542 |
544 |
543 |
545 |
544 (** classes and class target **) |
546 (** classes and class target **) |
545 |
547 |
546 (* class context initialization *) |
548 (* class context initialization - experimental *) |
547 |
549 |
548 (*experimental*) |
550 fun get_remove_constraints sort ctxt = |
549 fun get_remove_constraint_ctxt c ctxt = |
551 let |
550 let |
552 val operations = these_operations (ProofContext.theory_of ctxt) sort; |
551 val ty = ProofContext.the_const_constraint ctxt c; |
553 fun get_remove (c, _) ctxt = |
|
554 let |
|
555 val ty = ProofContext.the_const_constraint ctxt c; |
|
556 val _ = tracing c; |
|
557 in |
|
558 ctxt |
|
559 |> ProofContext.add_const_constraint (c, NONE) |
|
560 |> pair (c, ty) |
|
561 end; |
552 in |
562 in |
553 ctxt |
563 ctxt |
554 |> ProofContext.add_const_constraint (c, NONE) |
564 |> fold_map get_remove operations |
555 |> pair (c, ty) |
565 end; |
556 end; |
566 |
557 |
567 fun sort_term_check thy sort constraints = |
558 fun remove_constraints' class thy = |
568 let |
559 thy |> fold_map (get_remove_constraint o fst) (these_localized thy class); |
569 val local_operation = local_operation thy sort; |
560 |
570 fun default_typ consts c = case AList.lookup (op =) constraints c |
561 fun remove_constraints class ctxt = |
571 of SOME ty => SOME ty |
562 ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class); |
572 | NONE => try (Consts.the_constraint consts) c; |
563 |
573 fun infer_constraints ctxt ts = |
564 fun default_typ ctxt constraints c = |
574 TypeInfer.infer_types (ProofContext.pp ctxt) |
565 case AList.lookup (op =) constraints c |
575 (Sign.tsig_of (ProofContext.theory_of ctxt)) |
566 of SOME ty => SOME ty |
576 I (default_typ (ProofContext.consts_of ctxt)) (K NONE) |
567 | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c; |
577 (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts) |
568 |
578 |> fst |> map fst |
569 fun infer_constraints ctxt constraints ts = |
579 handle TYPE (msg, _, _) => error msg; |
570 TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt)) |
580 fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*) |
571 (Syntax.check_typs ctxt) |
581 of TFree (v, _) => v = AxClass.param_tyvarname |
572 (default_typ ctxt constraints) (K NONE) |
582 | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*) |
573 (Variable.names_of ctxt) (Variable.maxidx_of ctxt) (SOME true) (map (rpair dummyT) ts) |
583 | _ => false; |
574 |> #1 |> map #1 |
584 fun subst_operation (t as Const (c, ty)) = (case local_operation c |
575 handle TYPE (msg, _, _) => error msg |
585 of SOME (t', idx) => if check_typ c idx ty then t' else t |
576 |
586 | NONE => t) |
577 fun subst_typ local_sort = |
587 | subst_operation t = t; |
578 map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname |
588 fun subst_operations ts ctxt = |
579 then TFree (v, local_sort) |
589 ts |
580 else t |
590 |> (map o map_aterms) subst_operation |
581 | t => t); |
591 |> infer_constraints ctxt |
582 |
592 |> rpair ctxt; (*FIXME add constraints here*) |
583 fun sort_typ_check thy sort = |
593 in subst_operations end; |
584 let |
594 |
|
595 fun init_exp sort ctxt = |
|
596 let |
|
597 val thy = ProofContext.theory_of ctxt; |
585 val local_sort = (#local_sort o the_class_data thy) (hd sort); |
598 val local_sort = (#local_sort o the_class_data thy) (hd sort); |
586 in |
|
587 pair o map (subst_typ local_sort) |
|
588 end; |
|
589 |
|
590 fun sort_term_check thy sort constraints = |
|
591 let |
|
592 val algebra = Sign.classes_of thy; |
|
593 val local_sort = (#local_sort o the_class_data thy) (hd sort); |
|
594 val v = AxClass.param_tyvarname; |
|
595 val local_param = local_param thy sort; |
|
596 (*FIXME efficiency*) |
|
597 fun class_arg c idx ty = |
|
598 let |
|
599 val typargs = Sign.const_typargs thy (c, ty); |
|
600 fun classtyp (TFree (w, _)) = w = v |
|
601 | classtyp t = false; |
|
602 in classtyp (nth typargs idx) end; |
|
603 fun subst (t as Const (c, ty)) = (case local_param c |
|
604 of NONE => t |
|
605 | SOME (t', (_, idx)) => if class_arg c idx ty |
|
606 then t' else t) |
|
607 | subst t = t; |
|
608 in fn ts => fn ctxt => |
|
609 ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt) |
|
610 end; |
|
611 |
|
612 fun init_default sort ctxt = |
|
613 let |
|
614 val thy = ProofContext.theory_of ctxt; |
|
615 val typ_check = sort_typ_check thy sort; |
|
616 val term_check = sort_term_check thy sort; |
599 val term_check = sort_term_check thy sort; |
617 in |
600 in |
618 ctxt |
601 ctxt |
619 |> remove_constraints sort |
602 |> Variable.declare_term |
620 ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort))) |
603 (Logic.mk_type (TFree (AxClass.param_tyvarname, local_sort))) |
621 ||> Context.proof_map (Syntax.add_typ_check 0 "class" typ_check) |
604 |> get_remove_constraints sort |
622 |-> (fn constraints => |
605 |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class" |
623 Context.proof_map (Syntax.add_term_check 0 "class" (term_check constraints))) |
606 (sort_term_check thy sort constraints))) |
624 end; |
607 end; |
625 |
608 |
626 val init_ref = ref (K I : sort -> Proof.context -> Proof.context); |
609 val init_ref = ref (K I : sort -> Proof.context -> Proof.context); |
627 fun init class = ! init_ref class; |
610 fun init class = ! init_ref class; |
628 |
611 |
643 let |
626 let |
644 val supclasses = map (prep_class thy) raw_supclasses; |
627 val supclasses = map (prep_class thy) raw_supclasses; |
645 val sups = filter (is_some o lookup_class_data thy) supclasses |
628 val sups = filter (is_some o lookup_class_data thy) supclasses |
646 |> Sign.minimize_sort thy; |
629 |> Sign.minimize_sort thy; |
647 val supsort = Sign.minimize_sort thy supclasses; |
630 val supsort = Sign.minimize_sort thy supclasses; |
|
631 val local_sort = case sups |
|
632 of sup :: _ => (#local_sort o the_class_data thy) sup |
|
633 | [] => supsort; |
648 val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups; |
634 val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups; |
649 val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) |
635 val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) |
650 | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); |
636 | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); |
651 val supexpr = Locale.Merge suplocales; |
637 val supexpr = Locale.Merge suplocales; |
652 val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; |
638 val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; |
660 |> Locale.cert_expr supexpr [constrain] |
646 |> Locale.cert_expr supexpr [constrain] |
661 |> snd |
647 |> snd |
662 |> init supsort |
648 |> init supsort |
663 |> process_expr Locale.empty raw_elems |
649 |> process_expr Locale.empty raw_elems |
664 |> fst |
650 |> fst |
665 |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)), |
651 |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)), |
666 (*FIXME*) if null includes then constrain :: elems else elems))) |
652 (*FIXME*) if null includes then constrain :: elems else elems))) |
667 end; |
653 end; |
668 |
654 |
669 val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr; |
655 val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr; |
670 val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr; |
656 val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr; |
671 |
657 |
672 fun gen_class prep_spec prep_param local_syntax bname |
658 fun gen_class prep_spec prep_param local_syntax bname |
673 raw_supclasses raw_includes_elems raw_other_consts thy = |
659 raw_supclasses raw_includes_elems raw_other_consts thy = |
674 let |
660 let |
675 val (((sups, supconsts), (supsort, mergeexpr)), elems) = |
661 val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) = |
676 prep_spec thy raw_supclasses raw_includes_elems; |
662 prep_spec thy raw_supclasses raw_includes_elems; |
677 val other_consts = map (prep_param thy) raw_other_consts; |
663 val other_consts = map (prep_param thy) raw_other_consts; |
678 fun mk_instT class = Symtab.empty |
664 fun mk_instT class = Symtab.empty |
679 |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); |
665 |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); |
680 fun mk_inst class param_names cs = |
666 fun mk_inst class param_names cs = |
719 in |
705 in |
720 thy |
706 thy |
721 |> Locale.add_locale_i (SOME "") bname mergeexpr elems |
707 |> Locale.add_locale_i (SOME "") bname mergeexpr elems |
722 |-> (fn name_locale => ProofContext.theory_result ( |
708 |-> (fn name_locale => ProofContext.theory_result ( |
723 `(fn thy => extract_params thy name_locale) |
709 `(fn thy => extract_params thy name_locale) |
724 #-> (fn (local_sort, (globals, params)) => |
710 #-> (fn (_, (globals, params)) => |
725 AxClass.define_class_params (bname, supsort) params |
711 AxClass.define_class_params (bname, supsort) params |
726 (extract_assumes name_locale params) other_consts |
712 (extract_assumes name_locale params) other_consts |
727 #-> (fn (name_axclass, (consts, axioms)) => |
713 #-> (fn (name_axclass, (consts, axioms)) => |
728 `(fn thy => class_intro thy name_locale name_axclass sups) |
714 `(fn thy => class_intro thy name_locale name_axclass sups) |
729 #-> (fn class_intro => |
715 #-> (fn class_intro => |
793 |> Sign.sticky_prefix prfx |
779 |> Sign.sticky_prefix prfx |
794 |> PureThy.add_defs_i false [(def, [])] |
780 |> PureThy.add_defs_i false [(def, [])] |
795 |-> (fn [def] => interpret def) |
781 |-> (fn [def] => interpret def) |
796 |> Sign.add_const_constraint (c', SOME ty'') |
782 |> Sign.add_const_constraint (c', SOME ty'') |
797 |> Sign.restore_naming thy |
783 |> Sign.restore_naming thy |
|
784 end; |
|
785 |
|
786 fun add_abbrev_in_class class ((c, rhs), syn) thy = |
|
787 let |
|
788 val local_sort = (#local_sort o the_class_data thy) class; |
|
789 val subst_typ = Term.map_type_tfree (fn var as (w, sort) => |
|
790 if w = AxClass.param_tyvarname then TFree (w, local_sort) else TFree var); |
|
791 val ty = fastype_of rhs; |
|
792 val rhs' = map_types subst_typ rhs; |
|
793 in |
|
794 thy |
|
795 |> Sign.parent_path (*FIXME*) |
|
796 |> Sign.add_abbrev Syntax.internalM [] (c, rhs) |
|
797 |-> (fn (lhs as Const (c', _), _) => register_abbrev class c' |
|
798 (*#> Sign.add_const_constraint (c', SOME ty)*) |
|
799 #> pair lhs) |
|
800 ||> Sign.restore_naming thy |
798 end; |
801 end; |
799 |
802 |
800 |
803 |
801 (* interpretation in class target *) |
804 (* interpretation in class target *) |
802 |
805 |