1.1 --- a/src/Pure/Syntax/syntax.ML Tue Apr 19 10:50:54 2011 +0200
1.2 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 19 14:57:09 2011 +0200
1.3 @@ -31,18 +31,26 @@
1.4 val unparse_typ: Proof.context -> typ -> Pretty.T
1.5 val unparse_term: Proof.context -> term -> Pretty.T
1.6 val print_checks: Proof.context -> unit
1.7 - val add_typ_check: int -> string ->
1.8 + val context_typ_check: int -> string ->
1.9 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
1.10 Context.generic -> Context.generic
1.11 - val add_term_check: int -> string ->
1.12 + val context_term_check: int -> string ->
1.13 (term list -> Proof.context -> (term list * Proof.context) option) ->
1.14 Context.generic -> Context.generic
1.15 - val add_typ_uncheck: int -> string ->
1.16 + val context_typ_uncheck: int -> string ->
1.17 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
1.18 Context.generic -> Context.generic
1.19 - val add_term_uncheck: int -> string ->
1.20 + val context_term_uncheck: int -> string ->
1.21 (term list -> Proof.context -> (term list * Proof.context) option) ->
1.22 Context.generic -> Context.generic
1.23 + val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
1.24 + Context.generic -> Context.generic
1.25 + val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
1.26 + Context.generic -> Context.generic
1.27 + val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
1.28 + Context.generic -> Context.generic
1.29 + val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
1.30 + Context.generic -> Context.generic
1.31 val typ_check: Proof.context -> typ list -> typ list
1.32 val term_check: Proof.context -> term list -> term list
1.33 val typ_uncheck: Proof.context -> typ list -> typ list
1.34 @@ -224,13 +232,11 @@
1.35
1.36 (* context-sensitive (un)checking *)
1.37
1.38 -local
1.39 -
1.40 type key = int * bool;
1.41 -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
1.42
1.43 structure Checks = Generic_Data
1.44 (
1.45 + type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
1.46 type T =
1.47 ((key * ((string * typ check) * stamp) list) list *
1.48 (key * ((string * term check) * stamp) list) list);
1.49 @@ -241,27 +247,6 @@
1.50 AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
1.51 );
1.52
1.53 -fun gen_add which (key: key) name f =
1.54 - Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
1.55 -
1.56 -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
1.57 -
1.58 -fun gen_check which uncheck ctxt0 xs0 =
1.59 - let
1.60 - val funs = which (Checks.get (Context.Proof ctxt0))
1.61 - |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
1.62 - |> Library.sort (int_ord o pairself fst) |> map snd
1.63 - |> not uncheck ? map rev;
1.64 - val check_all = perhaps_apply (map check_stage funs);
1.65 - in #1 (perhaps check_all (xs0, ctxt0)) end;
1.66 -
1.67 -fun map_sort f S =
1.68 - (case f (TFree ("", S)) of
1.69 - TFree ("", S') => S'
1.70 - | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
1.71 -
1.72 -in
1.73 -
1.74 fun print_checks ctxt =
1.75 let
1.76 fun split_checks checks =
1.77 @@ -283,15 +268,52 @@
1.78 pretty_checks "term_unchecks" term_unchecks
1.79 end |> Pretty.chunks |> Pretty.writeln;
1.80
1.81 -fun add_typ_check stage = gen_add apfst (stage, false);
1.82 -fun add_term_check stage = gen_add apsnd (stage, false);
1.83 -fun add_typ_uncheck stage = gen_add apfst (stage, true);
1.84 -fun add_term_uncheck stage = gen_add apsnd (stage, true);
1.85 +
1.86 +local
1.87 +
1.88 +fun context_check which (key: key) name f =
1.89 + Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
1.90 +
1.91 +fun simple_check eq f xs ctxt =
1.92 + let val xs' = f ctxt xs in
1.93 + if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
1.94 + else SOME (xs', ctxt)
1.95 + end;
1.96 +
1.97 +in
1.98 +
1.99 +fun context_typ_check stage = context_check apfst (stage, false);
1.100 +fun context_term_check stage = context_check apsnd (stage, false);
1.101 +fun context_typ_uncheck stage = context_check apfst (stage, true);
1.102 +fun context_term_uncheck stage = context_check apsnd (stage, true);
1.103
1.104 -val typ_check = gen_check fst false;
1.105 -val term_check = gen_check snd false;
1.106 -val typ_uncheck = gen_check fst true;
1.107 -val term_uncheck = gen_check snd true;
1.108 +fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
1.109 +fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
1.110 +fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
1.111 +fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
1.112 +
1.113 +end;
1.114 +
1.115 +
1.116 +local
1.117 +
1.118 +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
1.119 +fun check_all fs = perhaps_apply (map check_stage fs);
1.120 +
1.121 +fun check which uncheck ctxt0 xs0 =
1.122 + let
1.123 + val funs = which (Checks.get (Context.Proof ctxt0))
1.124 + |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
1.125 + |> Library.sort (int_ord o pairself fst) |> map snd
1.126 + |> not uncheck ? map rev;
1.127 + in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
1.128 +
1.129 +in
1.130 +
1.131 +val typ_check = check fst false;
1.132 +val term_check = check snd false;
1.133 +val typ_uncheck = check fst true;
1.134 +val term_uncheck = check snd true;
1.135
1.136 val check_typs = operation #check_typs;
1.137 val check_terms = operation #check_terms;
1.138 @@ -300,17 +322,30 @@
1.139 val check_typ = singleton o check_typs;
1.140 val check_term = singleton o check_terms;
1.141 val check_prop = singleton o check_props;
1.142 -val check_sort = map_sort o check_typ;
1.143
1.144 val uncheck_typs = operation #uncheck_typs;
1.145 val uncheck_terms = operation #uncheck_terms;
1.146 +
1.147 +end;
1.148 +
1.149 +
1.150 +(* derived operations for algebra of sorts *)
1.151 +
1.152 +local
1.153 +
1.154 +fun map_sort f S =
1.155 + (case f (TFree ("", S)) of
1.156 + TFree ("", S') => S'
1.157 + | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
1.158 +
1.159 +in
1.160 +
1.161 +val check_sort = map_sort o check_typ;
1.162 val uncheck_sort = map_sort o singleton o uncheck_typs;
1.163
1.164 end;
1.165
1.166
1.167 -(* derived operations for classrel and arity *)
1.168 -
1.169 val uncheck_classrel = map o singleton o uncheck_sort;
1.170
1.171 fun unparse_classrel ctxt cs = Pretty.block (flat