src/Pure/theory.ML
changeset 24626 85eceef2edc7
parent 24199 8be734b5f59f
child 24666 9885a86f14a8
     1.1 --- a/src/Pure/theory.ML	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -51,10 +51,108 @@
     1.4    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
     1.5  end
     1.6  
     1.7 -structure Theory: THEORY =
     1.8 +signature THEORY_INTERPRETATOR =
     1.9 +sig
    1.10 +  type T
    1.11 +  type interpretator = T list -> theory -> theory
    1.12 +  val add_those: T list -> theory -> theory
    1.13 +  val all_those: theory -> T list
    1.14 +  val add_interpretator: interpretator -> theory -> theory
    1.15 +  val init: theory -> theory
    1.16 +end;
    1.17 +
    1.18 +signature THEORY_INTERPRETATOR_KEY =
    1.19 +sig
    1.20 +  type T
    1.21 +  val eq: T * T -> bool
    1.22 +end;
    1.23 +
    1.24 +structure Theory =
    1.25  struct
    1.26  
    1.27  
    1.28 +(** datatype thy **)
    1.29 +
    1.30 +datatype thy = Thy of
    1.31 + {axioms: term NameSpace.table,
    1.32 +  defs: Defs.T,
    1.33 +  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
    1.34 +  consolidate: theory -> theory};
    1.35 +
    1.36 +fun make_thy (axioms, defs, oracles, consolidate) =
    1.37 +  Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
    1.38 +
    1.39 +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
    1.40 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
    1.41 +
    1.42 +structure ThyData = TheoryDataFun
    1.43 +(
    1.44 +  type T = thy;
    1.45 +  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
    1.46 +  val copy = I;
    1.47 +
    1.48 +  fun extend (Thy {axioms, defs, oracles, consolidate}) =
    1.49 +    make_thy (NameSpace.empty_table, defs, oracles, consolidate);
    1.50 +
    1.51 +  fun merge pp (thy1, thy2) =
    1.52 +    let
    1.53 +      val Thy {axioms = _, defs = defs1, oracles = oracles1,
    1.54 +        consolidate = consolidate1} = thy1;
    1.55 +      val Thy {axioms = _, defs = defs2, oracles = oracles2,
    1.56 +        consolidate = consolidate2} = thy2;
    1.57 +
    1.58 +      val axioms = NameSpace.empty_table;
    1.59 +      val defs = Defs.merge pp (defs1, defs2);
    1.60 +      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    1.61 +        handle Symtab.DUP dup => err_dup_ora dup;
    1.62 +      val consolidate = consolidate1 #> consolidate2;
    1.63 +    in make_thy (axioms, defs, oracles, consolidate) end;
    1.64 +);
    1.65 +
    1.66 +fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
    1.67 +  {axioms = axioms, defs = defs, oracles = oracles});
    1.68 +
    1.69 +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
    1.70 +  make_thy (f (axioms, defs, oracles, consolidate)));
    1.71 +
    1.72 +fun map_axioms f = map_thy
    1.73 +  (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
    1.74 +fun map_defs f = map_thy
    1.75 +  (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
    1.76 +fun map_oracles f = map_thy
    1.77 +  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
    1.78 +
    1.79 +
    1.80 +(* basic operations *)
    1.81 +
    1.82 +val axiom_space = #1 o #axioms o rep_theory;
    1.83 +val axiom_table = #2 o #axioms o rep_theory;
    1.84 +
    1.85 +val oracle_space = #1 o #oracles o rep_theory;
    1.86 +val oracle_table = #2 o #oracles o rep_theory;
    1.87 +
    1.88 +val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    1.89 +
    1.90 +val defs_of = #defs o rep_theory;
    1.91 +
    1.92 +fun requires thy name what =
    1.93 +  if Context.exists_name name thy then ()
    1.94 +  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    1.95 +
    1.96 +
    1.97 +(* interpretators *)
    1.98 +
    1.99 +fun add_consolidate f = map_thy
   1.100 +  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
   1.101 +
   1.102 +fun consolidate thy =
   1.103 +  let
   1.104 +    val Thy {consolidate, ...} = ThyData.get thy;
   1.105 +  in
   1.106 +    thy |> consolidate
   1.107 +  end;
   1.108 +
   1.109 +
   1.110  (** type theory **)
   1.111  
   1.112  (* context operations *)
   1.113 @@ -62,6 +160,10 @@
   1.114  val eq_thy = Context.eq_thy;
   1.115  val subthy = Context.subthy;
   1.116  
   1.117 +fun assert_super thy1 thy2 =
   1.118 +  if subthy (thy1, thy2) then thy2
   1.119 +  else raise THEORY ("Not a super theory", [thy1, thy2]);
   1.120 +
   1.121  val parents_of = Context.parents_of;
   1.122  val ancestors_of = Context.ancestors_of;
   1.123  
   1.124 @@ -73,7 +175,7 @@
   1.125  fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   1.126    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
   1.127  
   1.128 -val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
   1.129 +val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
   1.130  val end_theory = Context.finish_thy;
   1.131  val checkpoint = Context.checkpoint_thy;
   1.132  val copy = Context.copy_thy;
   1.133 @@ -86,73 +188,10 @@
   1.134  
   1.135  
   1.136  
   1.137 -(** datatype thy **)
   1.138 -
   1.139 -datatype thy = Thy of
   1.140 - {axioms: term NameSpace.table,
   1.141 -  defs: Defs.T,
   1.142 -  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table};
   1.143 -
   1.144 -fun make_thy (axioms, defs, oracles) =
   1.145 -  Thy {axioms = axioms, defs = defs, oracles = oracles};
   1.146 -
   1.147 -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
   1.148 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   1.149 -
   1.150 -structure ThyData = TheoryDataFun
   1.151 -(
   1.152 -  type T = thy;
   1.153 -  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
   1.154 -  val copy = I;
   1.155 -
   1.156 -  fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles);
   1.157 -
   1.158 -  fun merge pp (thy1, thy2) =
   1.159 -    let
   1.160 -      val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
   1.161 -      val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
   1.162 +(** axioms **)
   1.163  
   1.164 -      val axioms = NameSpace.empty_table;
   1.165 -      val defs = Defs.merge pp (defs1, defs2);
   1.166 -      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   1.167 -        handle Symtab.DUP dup => err_dup_ora dup;
   1.168 -    in make_thy (axioms, defs, oracles) end;
   1.169 -);
   1.170 -
   1.171 -fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   1.172 -
   1.173 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) =>
   1.174 -  make_thy (f (axioms, defs, oracles)));
   1.175 -
   1.176 -fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles));
   1.177 -fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles));
   1.178 -fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles));
   1.179 -
   1.180 -
   1.181 -(* basic operations *)
   1.182 -
   1.183 -val axiom_space = #1 o #axioms o rep_theory;
   1.184 -val axiom_table = #2 o #axioms o rep_theory;
   1.185 -
   1.186 -val oracle_space = #1 o #oracles o rep_theory;
   1.187 -val oracle_table = #2 o #oracles o rep_theory;
   1.188 -
   1.189 -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   1.190  fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   1.191  
   1.192 -val defs_of = #defs o rep_theory;
   1.193 -
   1.194 -fun requires thy name what =
   1.195 -  if Context.exists_name name thy then ()
   1.196 -  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   1.197 -
   1.198 -fun assert_super thy1 thy2 =
   1.199 -  if subthy (thy1, thy2) then thy2
   1.200 -  else raise THEORY ("Not a super theory", [thy1, thy2]);
   1.201 -
   1.202 -
   1.203 -
   1.204 -(** add axioms **)
   1.205  
   1.206  (* prepare axioms *)
   1.207  
   1.208 @@ -311,5 +350,66 @@
   1.209  
   1.210  end;
   1.211  
   1.212 +functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
   1.213 +struct
   1.214 +
   1.215 +open Key;
   1.216 +
   1.217 +type interpretator = T list -> theory -> theory;
   1.218 +
   1.219 +fun apply ips x = fold_rev (fn (_, f) => f x) ips;
   1.220 +
   1.221 +structure InterpretatorData = TheoryDataFun (
   1.222 +  type T = ((serial * interpretator) list * T list) * (theory -> theory);
   1.223 +  val empty = (([], []), I);
   1.224 +  val extend = I;
   1.225 +  val copy = I;
   1.226 +  fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
   1.227 +    let
   1.228 +      fun diff (interpretators1 : (serial * interpretator) list, done1)
   1.229 +        (interpretators2, done2) = let
   1.230 +          val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
   1.231 +          val undone = subtract eq done2 done1;
   1.232 +        in apply interpretators undone end;
   1.233 +      val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
   1.234 +      val done = Library.merge eq (done1, done2);
   1.235 +      val upd_new = diff (interpretators2, done2) (interpretators1, done1)
   1.236 +        #> diff (interpretators1, done1) (interpretators2, done2);
   1.237 +      val upd = upd1 #> upd2 #> upd_new;
   1.238 +    in ((interpretators, done), upd) end;
   1.239 +);
   1.240 +
   1.241 +fun consolidate thy =
   1.242 +  let
   1.243 +    val (_, upd) = InterpretatorData.get thy;
   1.244 +  in
   1.245 +    thy |> upd |> (InterpretatorData.map o apsnd) (K I)
   1.246 +  end;
   1.247 +
   1.248 +val init = Theory.add_consolidate consolidate;
   1.249 +
   1.250 +fun add_those xs thy =
   1.251 +  let
   1.252 +    val ((interpretators, _), _) = InterpretatorData.get thy;
   1.253 +  in
   1.254 +    thy
   1.255 +    |> apply interpretators xs
   1.256 +    |> (InterpretatorData.map o apfst o apsnd) (append xs)
   1.257 +  end;
   1.258 +
   1.259 +val all_those = snd o fst o InterpretatorData.get;
   1.260 +
   1.261 +fun add_interpretator interpretator thy =
   1.262 +  let
   1.263 +    val ((interpretators, xs), _) = InterpretatorData.get thy;
   1.264 +  in
   1.265 +    thy
   1.266 +    |> interpretator (rev xs)
   1.267 +    |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
   1.268 +  end;
   1.269 +
   1.270 +end;
   1.271 +
   1.272 +structure Theory: THEORY = Theory;
   1.273  structure BasicTheory: BASIC_THEORY = Theory;
   1.274  open BasicTheory;