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