504 |
504 |
505 |
505 |
506 |
506 |
507 (** concrete syntax for records **) |
507 (** concrete syntax for records **) |
508 |
508 |
|
509 (* decode type *) |
|
510 |
|
511 fun decode_type thy t = |
|
512 let |
|
513 fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); |
|
514 val map_sort = Sign.intern_sort thy; |
|
515 in |
|
516 Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t |
|
517 |> Sign.intern_tycons thy |
|
518 end; |
|
519 |
|
520 |
509 (* parse translations *) |
521 (* parse translations *) |
510 |
522 |
511 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = |
523 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = |
512 if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg) |
524 if c = mark then Syntax.const (suffix sfx name) $ (Syntax.const KN $ arg) |
513 else raise TERM ("gen_field_tr: " ^ mark, [t]) |
525 else raise TERM ("gen_field_tr: " ^ mark, [t]) |
580 else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) |
592 else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) |
581 | splitargs [] (fargs as (_::_)) = ([],fargs) |
593 | splitargs [] (fargs as (_::_)) = ([],fargs) |
582 | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) |
594 | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) |
583 | splitargs _ _ = ([],[]); |
595 | splitargs _ _ = ([],[]); |
584 |
596 |
585 fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); |
|
586 |
|
587 fun to_type t = Sign.certify_typ thy |
|
588 (Sign.intern_typ thy |
|
589 (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)); |
|
590 |
|
591 fun mk_ext (fargs as (name,arg)::_) = |
597 fun mk_ext (fargs as (name,arg)::_) = |
592 (case get_fieldext thy (Sign.intern_const thy name) of |
598 (case get_fieldext thy (Sign.intern_const thy name) of |
593 SOME (ext,alphas) => |
599 SOME (ext,alphas) => |
594 (case get_extfields thy ext of |
600 (case get_extfields thy ext of |
595 SOME flds |
601 SOME flds |
596 => (let |
602 => (let |
597 val flds' = but_last flds; |
603 val flds' = but_last flds; |
598 val types = map snd flds'; |
604 val types = map snd flds'; |
599 val (args,rest) = splitargs (map fst flds') fargs; |
605 val (args,rest) = splitargs (map fst flds') fargs; |
600 val argtypes = map to_type args; |
606 val argtypes = map (Sign.certify_typ thy o decode_type thy) args; |
601 val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) |
607 val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) |
602 argtypes 0; |
608 argtypes 0; |
603 val varifyT = varifyT midx; |
609 val varifyT = varifyT midx; |
604 val vartypes = map varifyT types; |
610 val vartypes = map varifyT types; |
605 |
611 |
744 fun fixT (T as Type (x,[])) = |
750 fun fixT (T as Type (x,[])) = |
745 if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T |
751 if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T |
746 | fixT (Type (x,xs)) = Type (x,map fixT xs) |
752 | fixT (Type (x,xs)) = Type (x,map fixT xs) |
747 | fixT T = T; |
753 | fixT T = T; |
748 |
754 |
749 val T = fixT (Sign.intern_typ thy |
755 val T = fixT (decode_type thy tm); |
750 (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); |
|
751 val midx = maxidx_of_typ T; |
756 val midx = maxidx_of_typ T; |
752 val varifyT = varifyT midx; |
757 val varifyT = varifyT midx; |
753 |
758 |
754 fun mk_type_abbr subst name alphas = |
759 fun mk_type_abbr subst name alphas = |
755 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas); |
760 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas); |
779 fun record_type_tr' sep mark record record_scheme ctxt t = |
784 fun record_type_tr' sep mark record record_scheme ctxt t = |
780 let |
785 let |
781 val thy = ProofContext.theory_of ctxt; |
786 val thy = ProofContext.theory_of ctxt; |
782 fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); |
787 fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy); |
783 |
788 |
784 val T = Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t) |
789 val T = decode_type thy t; |
785 val varifyT = varifyT (Term.maxidx_of_typ T) |
790 val varifyT = varifyT (Term.maxidx_of_typ T); |
786 |
791 |
787 fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T); |
792 fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T); |
788 |
793 |
789 fun field_lst T = |
794 fun field_lst T = |
790 (case T of |
795 (case T of |