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