src/Pure/theory.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50201 c26369c9eda6
child 52696 38466f4f3483
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/theory.ML
     2     Author:     Lawrence C Paulson and Markus Wenzel
     3 
     4 Logical theory content: axioms, definitions, and begin/end wrappers.
     5 *)
     6 
     7 signature THEORY =
     8 sig
     9   val eq_thy: theory * theory -> bool
    10   val subthy: theory * theory -> bool
    11   val assert_super: theory -> theory -> theory
    12   val parents_of: theory -> theory list
    13   val ancestors_of: theory -> theory list
    14   val nodes_of: theory -> theory list
    15   val check_thy: theory -> theory_ref
    16   val deref: theory_ref -> theory
    17   val merge: theory * theory -> theory
    18   val merge_refs: theory_ref * theory_ref -> theory_ref
    19   val merge_list: theory list -> theory
    20   val checkpoint: theory -> theory
    21   val copy: theory -> theory
    22   val requires: theory -> string -> string -> unit
    23   val get_markup: theory -> Markup.T
    24   val axiom_space: theory -> Name_Space.T
    25   val axiom_table: theory -> term Symtab.table
    26   val axioms_of: theory -> (string * term) list
    27   val all_axioms_of: theory -> (string * term) list
    28   val defs_of: theory -> Defs.T
    29   val at_begin: (theory -> theory option) -> theory -> theory
    30   val at_end: (theory -> theory option) -> theory -> theory
    31   val begin_theory: string * Position.T -> theory list -> theory
    32   val end_theory: theory -> theory
    33   val add_axiom: Proof.context -> binding * term -> theory -> theory
    34   val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
    35   val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
    36   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
    37   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    38   val check_overloading: Proof.context -> bool -> string * typ -> unit
    39 end
    40 
    41 structure Theory: THEORY =
    42 struct
    43 
    44 
    45 (** theory context operations **)
    46 
    47 val eq_thy = Context.eq_thy;
    48 val subthy = Context.subthy;
    49 
    50 fun assert_super thy1 thy2 =
    51   if subthy (thy1, thy2) then thy2
    52   else raise THEORY ("Not a super theory", [thy1, thy2]);
    53 
    54 val parents_of = Context.parents_of;
    55 val ancestors_of = Context.ancestors_of;
    56 fun nodes_of thy = thy :: ancestors_of thy;
    57 
    58 val check_thy = Context.check_thy;
    59 val deref = Context.deref;
    60 
    61 val merge = Context.merge;
    62 val merge_refs = Context.merge_refs;
    63 
    64 fun merge_list [] = raise THEORY ("Empty merge of theories", [])
    65   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
    66 
    67 val checkpoint = Context.checkpoint_thy;
    68 val copy = Context.copy_thy;
    69 
    70 fun requires thy name what =
    71   if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
    72   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
    73 
    74 
    75 
    76 (** datatype thy **)
    77 
    78 type wrapper = (theory -> theory option) * stamp;
    79 
    80 fun apply_wrappers (wrappers: wrapper list) =
    81   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
    82 
    83 datatype thy = Thy of
    84  {pos: Position.T,
    85   id: serial,
    86   axioms: term Name_Space.table,
    87   defs: Defs.T,
    88   wrappers: wrapper list * wrapper list};
    89 
    90 fun make_thy (pos, id, axioms, defs, wrappers) =
    91   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
    92 
    93 structure Thy = Theory_Data_PP
    94 (
    95   type T = thy;
    96   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
    97   val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
    98 
    99   fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
   100     make_thy (Position.none, 0, empty_axioms, defs, wrappers);
   101 
   102   fun merge pp (thy1, thy2) =
   103     let
   104       val ctxt = Syntax.init_pretty pp;
   105       val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   106       val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   107 
   108       val axioms' = empty_axioms;
   109       val defs' = Defs.merge ctxt (defs1, defs2);
   110       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   111       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   112     in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
   113 );
   114 
   115 fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
   116 
   117 fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   118   make_thy (f (pos, id, axioms, defs, wrappers)));
   119 
   120 fun map_axioms f =
   121   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
   122 
   123 fun map_defs f =
   124   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
   125 
   126 fun map_wrappers f =
   127   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
   128 
   129 
   130 (* entity markup *)
   131 
   132 fun theory_markup def name id pos =
   133   if id = 0 then Markup.empty
   134   else
   135     Markup.properties (Position.entity_properties_of def id pos)
   136       (Markup.entity Markup.theoryN name);
   137 
   138 fun init_markup (name, pos) thy =
   139   let
   140     val id = serial ();
   141     val _ = Position.report pos (theory_markup true name id pos);
   142   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
   143 
   144 fun get_markup thy =
   145   let val {pos, id, ...} = rep_theory thy
   146   in theory_markup false (Context.theory_name thy) id pos end;
   147 
   148 
   149 (* basic operations *)
   150 
   151 val axiom_space = #1 o #axioms o rep_theory;
   152 val axiom_table = #2 o #axioms o rep_theory;
   153 
   154 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   155 fun all_axioms_of thy = maps axioms_of (nodes_of thy);
   156 
   157 val defs_of = #defs o rep_theory;
   158 
   159 
   160 (* begin/end theory *)
   161 
   162 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
   163 val end_wrappers = rev o #2 o #wrappers o rep_theory;
   164 
   165 fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
   166 fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
   167 
   168 fun begin_theory (name, pos) imports =
   169   if name = Context.PureN then
   170     (case imports of
   171       [thy] => init_markup (name, pos) thy
   172     | _ => error "Bad bootstrapping of theory Pure")
   173   else
   174     let
   175       val thy = Context.begin_thy Context.pretty_global name imports;
   176       val wrappers = begin_wrappers thy;
   177     in
   178       thy
   179       |> init_markup (name, pos)
   180       |> Sign.local_path
   181       |> Sign.map_naming (Name_Space.set_theory_name name)
   182       |> apply_wrappers wrappers
   183       |> tap (Syntax.force_syntax o Sign.syn_of)
   184     end;
   185 
   186 fun end_theory thy =
   187   thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
   188 
   189 
   190 
   191 (** primitive specifications **)
   192 
   193 (* raw axioms *)
   194 
   195 fun cert_axm ctxt (b, raw_tm) =
   196   let
   197     val thy = Proof_Context.theory_of ctxt;
   198     val t = Sign.cert_prop thy raw_tm
   199       handle TYPE (msg, _, _) => error msg
   200         | TERM (msg, _) => error msg;
   201     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   202 
   203     val bad_sorts =
   204       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
   205     val _ = null bad_sorts orelse
   206       error ("Illegal sort constraints in primitive specification: " ^
   207         commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
   208   in (b, Sign.no_vars ctxt t) end
   209   handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
   210 
   211 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   212   let
   213     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
   214     val (_, axioms') = Name_Space.define (Sign.inherit_naming thy ctxt) true axm axioms;
   215   in axioms' end);
   216 
   217 
   218 (* dependencies *)
   219 
   220 fun dependencies ctxt unchecked def description lhs rhs =
   221   let
   222     val thy = Proof_Context.theory_of ctxt;
   223     val consts = Sign.consts_of thy;
   224     fun prep const =
   225       let val Const (c, T) = Sign.no_vars ctxt (Const const)
   226       in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
   227 
   228     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
   229     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
   230       if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
   231     val _ =
   232       if null rhs_extras then ()
   233       else error ("Specification depends on extra type variables: " ^
   234         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
   235         "\nThe error(s) above occurred in " ^ quote description);
   236   in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
   237 
   238 fun add_deps ctxt a raw_lhs raw_rhs thy =
   239   let
   240     val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
   241     val description = if a = "" then #1 lhs ^ " axiom" else a;
   242   in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
   243 
   244 fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
   245 
   246 fun specify_const decl thy =
   247   let val (t as Const const, thy') = Sign.declare_const_global decl thy;
   248   in (t, add_deps_global "" const [] thy') end;
   249 
   250 
   251 (* overloading *)
   252 
   253 fun check_overloading ctxt overloaded (c, T) =
   254   let
   255     val thy = Proof_Context.theory_of ctxt;
   256 
   257     val declT = Sign.the_const_constraint thy c
   258       handle TYPE (msg, _, _) => error msg;
   259     val T' = Logic.varifyT_global T;
   260 
   261     fun message sorts txt =
   262       [Pretty.block [Pretty.str "Specification of constant ",
   263         Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   264         Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
   265         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   266   in
   267     if Sign.typ_instance thy (declT, T') then ()
   268     else if Type.raw_instance (declT, T') then
   269       error (message true "imposes additional sort constraints on the constant declaration")
   270     else if overloaded then ()
   271     else warning (message false "is strictly less general than the declared type")
   272   end;
   273 
   274 
   275 (* definitional axioms *)
   276 
   277 local
   278 
   279 fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   280   let
   281     val name = Sign.full_name thy b;
   282     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   283       handle TERM (msg, _) => error msg;
   284     val lhs_const = Term.dest_Const (Term.head_of lhs);
   285     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   286     val _ = check_overloading ctxt overloaded lhs_const;
   287   in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
   288   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   289    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
   290     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
   291 
   292 in
   293 
   294 fun add_def ctxt unchecked overloaded raw_axm thy =
   295   let val axm = cert_axm ctxt raw_axm in
   296     thy
   297     |> map_defs (check_def ctxt thy unchecked overloaded axm)
   298     |> add_axiom ctxt axm
   299   end;
   300 
   301 end;
   302 
   303 end;