src/Pure/Syntax/syntax.ML
changeset 42402 c7139609b67d
parent 42383 0ae4ad40d7b5
child 42403 38b29c9fc742
     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