53 val cert_typ: Proof.context -> typ -> typ |
53 val cert_typ: Proof.context -> typ -> typ |
54 val cert_typ_syntax: Proof.context -> typ -> typ |
54 val cert_typ_syntax: Proof.context -> typ -> typ |
55 val cert_typ_abbrev: Proof.context -> typ -> typ |
55 val cert_typ_abbrev: Proof.context -> typ -> typ |
56 val get_skolem: Proof.context -> string -> string |
56 val get_skolem: Proof.context -> string -> string |
57 val revert_skolem: Proof.context -> string -> string |
57 val revert_skolem: Proof.context -> string -> string |
58 val infer_type: Proof.context -> string -> typ |
58 val infer_type: Proof.context -> string * typ -> typ |
59 val inferred_param: string -> Proof.context -> typ * Proof.context |
59 val inferred_param: string -> Proof.context -> typ * Proof.context |
60 val inferred_fixes: Proof.context -> (string * typ) list * Proof.context |
60 val inferred_fixes: Proof.context -> (string * typ) list * Proof.context |
61 val read_type_name: Proof.context -> bool -> string -> typ |
61 val read_type_name: Proof.context -> bool -> string -> typ |
62 val read_type_name_proper: Proof.context -> bool -> string -> typ |
62 val read_type_name_proper: Proof.context -> bool -> string -> typ |
63 val read_const_proper: Proof.context -> bool -> string -> term |
63 val read_const_proper: Proof.context -> bool -> string -> term |
64 val read_const: Proof.context -> bool -> string -> term |
64 val read_const: Proof.context -> bool -> typ -> string -> term |
65 val allow_dummies: Proof.context -> Proof.context |
65 val allow_dummies: Proof.context -> Proof.context |
66 val check_tvar: Proof.context -> indexname * sort -> indexname * sort |
66 val check_tvar: Proof.context -> indexname * sort -> indexname * sort |
67 val check_tfree: Proof.context -> string * sort -> string * sort |
67 val check_tfree: Proof.context -> string * sort -> string * sort |
68 val decode_term: Proof.context -> term -> term |
68 val decode_term: Proof.context -> term -> term |
69 val standard_infer_types: Proof.context -> term list -> term list |
69 val standard_infer_types: Proof.context -> term list -> term list |
436 (** prepare terms and propositions **) |
436 (** prepare terms and propositions **) |
437 |
437 |
438 (* inferred types of parameters *) |
438 (* inferred types of parameters *) |
439 |
439 |
440 fun infer_type ctxt x = |
440 fun infer_type ctxt x = |
441 Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) |
441 Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); |
442 (Free (x, dummyT))); |
|
443 |
442 |
444 fun inferred_param x ctxt = |
443 fun inferred_param x ctxt = |
445 let val T = infer_type ctxt x |
444 let val T = infer_type ctxt (x, dummyT) |
446 in (T, ctxt |> Variable.declare_term (Free (x, T))) end; |
445 in (T, ctxt |> Variable.declare_term (Free (x, T))) end; |
447 |
446 |
448 fun inferred_fixes ctxt = |
447 fun inferred_fixes ctxt = |
449 let |
448 let |
450 val xs = rev (map #2 (Variable.fixes_of ctxt)); |
449 val xs = rev (map #2 (Variable.fixes_of ctxt)); |
503 | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T)); |
502 | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T)); |
504 |
503 |
505 |
504 |
506 fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content; |
505 fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content; |
507 |
506 |
508 fun read_const ctxt strict text = |
507 fun read_const ctxt strict ty text = |
509 let val (c, pos) = token_content text in |
508 let val (c, pos) = token_content text in |
510 (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of |
509 (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of |
511 (SOME x, false) => |
510 (SOME x, false) => |
512 (Position.report (Markup.name x |
511 (Position.report (Markup.name x |
513 (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos; |
512 (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos; |
514 Free (x, infer_type ctxt x)) |
513 Free (x, infer_type ctxt (x, ty))) |
515 | _ => prep_const_proper ctxt strict (c, pos)) |
514 | _ => prep_const_proper ctxt strict (c, pos)) |
516 end; |
515 end; |
517 |
516 |
518 end; |
517 end; |
519 |
518 |