Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: entity.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Isar/entity.ML
    Author:     Makarius

Entity definitions within a global or local theory context.
*)

signature ENTITY =
sig
  type 'a data_ops =
   {get_data: Context.generic -> 'a Name_Space.table,
    put_data: 'a Name_Space.table -> Context.generic -> Context.generic}
  val define_global: 'a data_ops -> binding -> 'a -> theory -> string * theory
  val define: 'a data_ops -> binding -> 'a -> local_theory -> string * local_theory
end;

structure Entity: ENTITY =
struct

(* context data *)

type 'a data_ops =
{get_data: Context.generic -> 'a Name_Space.table,
  put_data: 'a Name_Space.table -> Context.generic -> Context.generic};

(* global definition (foundation) *)

fun define_global {get_data, put_data} b x thy =
  let
    val context = Context.Theory thy;
    val (name, data') = Name_Space.define context true (b, x) (get_data context);
  in (name, Context.the_theory (put_data data' context)) end;

(* local definition *)

fun alias {get_data, put_data} binding name =
  Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    let
      val naming = Name_Space.naming_of context;
      val binding' = Morphism.binding phi binding;
      val data' = Name_Space.alias_table naming binding' name (get_data context);
    in put_data data' context end);

fun transfer {get_data, put_data} ctxt =
  let
    val data0 = get_data (Context.Theory (Proof_Context.theory_of ctxt));
    val data' = Name_Space.merge_tables (data0, get_data (Context.Proof ctxt));
  in Context.proof_map (put_data data') ctxt end;

fun define ops binding x =
  Local_Theory.background_theory_result (define_global ops binding x)
  #-> (fn name =>
    Local_Theory.map_contexts (K (transfer ops))
    #> alias ops binding name
    #> pair name);

end;

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.