12 val decode_term: Proof.context -> |
12 val decode_term: Proof.context -> |
13 Position.report list * term Exn.result -> Position.report list * term Exn.result |
13 Position.report list * term Exn.result -> Position.report list * term Exn.result |
14 val parse_ast_pattern: Proof.context -> string * string -> Ast.ast |
14 val parse_ast_pattern: Proof.context -> string * string -> Ast.ast |
15 val term_of_typ: Proof.context -> typ -> term |
15 val term_of_typ: Proof.context -> typ -> term |
16 val print_checks: Proof.context -> unit |
16 val print_checks: Proof.context -> unit |
17 val context_typ_check: int -> string -> |
|
18 (typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
19 Context.generic -> Context.generic |
|
20 val context_term_check: int -> string -> |
|
21 (term list -> Proof.context -> (term list * Proof.context) option) -> |
|
22 Context.generic -> Context.generic |
|
23 val context_typ_uncheck: int -> string -> |
|
24 (typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
25 Context.generic -> Context.generic |
|
26 val context_term_uncheck: int -> string -> |
|
27 (term list -> Proof.context -> (term list * Proof.context) option) -> |
|
28 Context.generic -> Context.generic |
|
29 val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> |
17 val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> |
30 Context.generic -> Context.generic |
18 Context.generic -> Context.generic |
31 val term_check: int -> string -> (Proof.context -> term list -> term list) -> |
19 val term_check: int -> string -> (Proof.context -> term list -> term list) -> |
32 Context.generic -> Context.generic |
20 Context.generic -> Context.generic |
33 val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> |
21 val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> |
34 Context.generic -> Context.generic |
22 Context.generic -> Context.generic |
35 val term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> |
23 val term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> |
|
24 Context.generic -> Context.generic |
|
25 val typ_check': int -> string -> |
|
26 (typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
27 Context.generic -> Context.generic |
|
28 val term_check': int -> string -> |
|
29 (term list -> Proof.context -> (term list * Proof.context) option) -> |
|
30 Context.generic -> Context.generic |
|
31 val typ_uncheck': int -> string -> |
|
32 (typ list -> Proof.context -> (typ list * Proof.context) option) -> |
|
33 Context.generic -> Context.generic |
|
34 val term_uncheck': int -> string -> |
|
35 (term list -> Proof.context -> (term list * Proof.context) option) -> |
36 Context.generic -> Context.generic |
36 Context.generic -> Context.generic |
37 end |
37 end |
38 |
38 |
39 structure Syntax_Phases: SYNTAX_PHASES = |
39 structure Syntax_Phases: SYNTAX_PHASES = |
40 struct |
40 struct |
761 let val xs' = f ctxt xs |
761 let val xs' = f ctxt xs |
762 in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; |
762 in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; |
763 |
763 |
764 in |
764 in |
765 |
765 |
766 fun context_typ_check stage = context_check apfst (stage, false); |
766 fun typ_check' stage = context_check apfst (stage, false); |
767 fun context_term_check stage = context_check apsnd (stage, false); |
767 fun term_check' stage = context_check apsnd (stage, false); |
768 fun context_typ_uncheck stage = context_check apfst (stage, true); |
768 fun typ_uncheck' stage = context_check apfst (stage, true); |
769 fun context_term_uncheck stage = context_check apsnd (stage, true); |
769 fun term_uncheck' stage = context_check apsnd (stage, true); |
770 |
770 |
771 fun typ_check key name f = context_typ_check key name (simple_check (op =) f); |
771 fun typ_check key name f = typ_check' key name (simple_check (op =) f); |
772 fun term_check key name f = context_term_check key name (simple_check (op aconv) f); |
772 fun term_check key name f = term_check' key name (simple_check (op aconv) f); |
773 fun typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f); |
773 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f); |
774 fun term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f); |
774 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f); |
775 |
775 |
776 end; |
776 end; |
777 |
777 |
778 |
778 |
779 local |
779 local |