src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Wed Nov 09 19:01:50 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 09 20:47:11 2011 +0100
@@ -30,31 +30,6 @@
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
-  val print_checks: Proof.context -> unit
-  val context_typ_check: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_check: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_typ_uncheck: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_uncheck: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val add_typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_check: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val add_typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
-    Context.generic -> Context.generic
-  val add_term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
-    Context.generic -> Context.generic
-  val apply_typ_check: Proof.context -> typ list -> typ list
-  val apply_term_check: Proof.context -> term list -> term list
-  val apply_typ_uncheck: Proof.context -> typ list -> typ list
-  val apply_term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -244,88 +219,7 @@
 val unparse_term = operation #unparse_term;
 
 
-(* context-sensitive (un)checking *)
-
-type key = int * bool;
-
-structure Checks = Generic_Data
-(
-  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
-  type T =
-    ((key * ((string * typ check) * stamp) list) list *
-     (key * ((string * term check) * stamp) list) list);
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
-    (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
-     AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
-);
-
-fun print_checks ctxt =
-  let
-    fun split_checks checks =
-      List.partition (fn ((_, un), _) => not un) checks
-      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
-          #> sort (int_ord o pairself fst));
-    fun pretty_checks kind checks =
-      checks |> map (fn (i, names) => Pretty.block
-        [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
-          Pretty.brk 1, Pretty.strs names]);
-
-    val (typs, terms) = Checks.get (Context.Proof ctxt);
-    val (typ_checks, typ_unchecks) = split_checks typs;
-    val (term_checks, term_unchecks) = split_checks terms;
-  in
-    pretty_checks "typ_checks" typ_checks @
-    pretty_checks "term_checks" term_checks @
-    pretty_checks "typ_unchecks" typ_unchecks @
-    pretty_checks "term_unchecks" term_unchecks
-  end |> Pretty.chunks |> Pretty.writeln;
-
-
-local
-
-fun context_check which (key: key) name f =
-  Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
-
-fun simple_check eq f xs ctxt =
-  let val xs' = f ctxt xs
-  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
-
-in
-
-fun context_typ_check stage = context_check apfst (stage, false);
-fun context_term_check stage = context_check apsnd (stage, false);
-fun context_typ_uncheck stage = context_check apfst (stage, true);
-fun context_term_uncheck stage = context_check apsnd (stage, true);
-
-fun add_typ_check key name f = context_typ_check key name (simple_check (op =) f);
-fun add_term_check key name f = context_term_check key name (simple_check (op aconv) f);
-fun add_typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
-fun add_term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
-
-end;
-
-
-local
-
-fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
-fun check_all fs = perhaps_apply (map check_stage fs);
-
-fun check which uncheck ctxt0 xs0 =
-  let
-    val funs = which (Checks.get (Context.Proof ctxt0))
-      |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
-      |> Library.sort (int_ord o pairself fst) |> map snd
-      |> not uncheck ? map rev;
-  in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
-
-in
-
-val apply_typ_check = check fst false;
-val apply_term_check = check snd false;
-val apply_typ_uncheck = check fst true;
-val apply_term_uncheck = check snd true;
+(* (un)checking *)
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
@@ -338,8 +232,6 @@
 val uncheck_typs = operation #uncheck_typs;
 val uncheck_terms = operation #uncheck_terms;
 
-end;
-
 
 (* derived operations for algebra of sorts *)