563 val cert_prop_pats = map o gen_cert cert_prop_sg true; |
563 val cert_prop_pats = map o gen_cert cert_prop_sg true; |
564 |
564 |
565 |
565 |
566 (* declare terms *) |
566 (* declare terms *) |
567 |
567 |
|
568 local |
|
569 |
568 val ins_types = foldl_aterms |
570 val ins_types = foldl_aterms |
569 (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types) |
571 (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types) |
570 | (types, Var v) => Vartab.update (v, types) |
572 | (types, Var v) => Vartab.update (v, types) |
571 | (types, _) => types); |
573 | (types, _) => types); |
572 |
574 |
586 | None => types)); |
588 | None => types)); |
587 |
589 |
588 fun map_defaults f = map_context (fn (thy, data, asms, binds, thms, cases, defs) => |
590 fun map_defaults f = map_context (fn (thy, data, asms, binds, thms, cases, defs) => |
589 (thy, data, asms, binds, thms, cases, f defs)); |
591 (thy, data, asms, binds, thms, cases, f defs)); |
590 |
592 |
591 fun declare (ctxt as Context {asms = (_, (fixes, _)), ...}, t) = |
593 fun declare_syn (ctxt, t) = |
592 ctxt |
594 ctxt |
593 |> map_defaults (fn (types, sorts, used) => (ins_types (types, t), sorts, used)) |
595 |> map_defaults (fn (types, sorts, used) => (ins_types (types, t), sorts, used)) |
594 |> map_defaults (fn (types, sorts, used) => (types, ins_sorts (sorts, t), used)) |
596 |> map_defaults (fn (types, sorts, used) => (types, ins_sorts (sorts, t), used)); |
|
597 |
|
598 fun declare_occ (ctxt as Context {asms = (_, (fixes, _)), ...}, t) = |
|
599 declare_syn (ctxt, t) |
595 |> map_defaults (fn (types, sorts, used) => (types, sorts, ins_used (used, t))) |
600 |> map_defaults (fn (types, sorts, used) => (types, sorts, ins_used (used, t))) |
596 |> map_defaults (fn (types, sorts, used) => |
601 |> map_defaults (fn (types, sorts, used) => |
597 (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used)); |
602 (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used)); |
598 |
603 |
599 |
604 in |
600 fun declare_term t ctxt = declare (ctxt, t); |
605 |
601 fun declare_terms ts ctxt = foldl declare (ctxt, ts); |
606 fun declare_term t ctxt = declare_occ (ctxt, t); |
|
607 fun declare_terms ts ctxt = foldl declare_occ (ctxt, ts); |
|
608 fun predeclare_terms ts ctxt = foldl declare_syn (ctxt, ts); |
|
609 |
|
610 end; |
602 |
611 |
603 |
612 |
604 |
613 |
605 (** Hindley-Milner polymorphism **) |
614 (** Hindley-Milner polymorphism **) |
606 |
615 |
944 end; |
953 end; |
945 |
954 |
946 |
955 |
947 (* variables *) |
956 (* variables *) |
948 |
957 |
|
958 local |
|
959 |
949 fun prep_vars prep_typ (ctxt, (xs, raw_T)) = |
960 fun prep_vars prep_typ (ctxt, (xs, raw_T)) = |
950 let |
961 let |
951 val _ = (case filter (not o Syntax.is_identifier) (map (no_skolem false ctxt) xs) of |
962 val _ = (case filter (not o Syntax.is_identifier) (map (no_skolem false ctxt) xs) of |
952 [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); |
963 [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); |
953 |
964 |
954 val opt_T = apsome (prep_typ ctxt) raw_T; |
965 val opt_T = apsome (prep_typ ctxt) raw_T; |
955 val T = if_none opt_T TypeInfer.logicT; |
966 val T = if_none opt_T TypeInfer.logicT; |
956 val ctxt' = ctxt |> declare_terms (map (fn x => Free (x, T)) xs); |
967 val ctxt' = ctxt |> predeclare_terms (map (fn x => Free (x, T)) xs); |
957 in (ctxt', (xs, opt_T)) end; |
968 in (ctxt', (xs, opt_T)) end; |
|
969 |
|
970 in |
958 |
971 |
959 val read_vars = prep_vars read_typ; |
972 val read_vars = prep_vars read_typ; |
960 val cert_vars = prep_vars cert_typ; |
973 val cert_vars = prep_vars cert_typ; |
|
974 |
|
975 end; |
961 |
976 |
962 |
977 |
963 (* fix *) |
978 (* fix *) |
964 |
979 |
965 local |
980 local |