Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: misc.xbm Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp

module Dyn = Dyn.Make ()

type 'a substitutivity =
    Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a

type object_name = Libnames.full_path * Names.KerName.t

type 'a object_declaration = {
  object_name : string;
  cache_function : object_name * 'a -> unit;
  load_function : int -> object_name * 'a -> unit;
  open_function : int -> object_name * 'a -> unit;
  classify_function : 'a -> 'a substitutivity;
  subst_function : Mod_subst.substitution * 'a -> 'a;
  discharge_function : object_name * 'a -> 'a option;
  rebuild_function : 'a -> 'a }

let default_object s = {
  object_name = s;
  cache_function = (fun _ -> ());
  load_function = (fun _ _ -> ());
  open_function = (fun _ _ -> ());
  subst_function = (fun _ ->
    CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
  classify_function = (fun obj -> Keep obj);
  discharge_function = (fun _ -> None);
  rebuild_function = (fun x -> x)}

(* The suggested object declaration is the following:

   declare_object { (default_object "MY OBJECT") with
       cache_function = fun (sp,a) -> Mytbl.add sp a}

   and the listed functions are only those which definitions actually
   differ from the default.

   This helps introducing new functions in objects.
*)

let ident_subst_function (_,a) = a

type obj = Dyn.t (* persistent dynamic objects *)

type dynamic_object_declaration = {
  dyn_cache_function : object_name * obj -> unit;
  dyn_load_function : int -> object_name * obj -> unit;
  dyn_open_function : int -> object_name * obj -> unit;
  dyn_subst_function : Mod_subst.substitution * obj -> obj;
  dyn_classify_function : obj -> obj substitutivity;
  dyn_discharge_function : object_name * obj -> obj option;
  dyn_rebuild_function : obj -> obj }

let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t

let cache_tab =
  (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)

let declare_object_full odecl =
  let na = odecl.object_name in
  let (infun, outfun) = Dyn.Easy.make_dyn na in
  let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
  and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
  and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
  and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
  and classifier lobj = match odecl.classify_function (outfun lobj) with
  | Dispose -> Dispose
  | Substitute obj -> Substitute (infun obj)
  | Keep obj -> Keep (infun obj)
  | Anticipate (obj) -> Anticipate (infun obj)
  and discharge (oname,lobj) =
    Option.map infun (odecl.discharge_function (oname,outfun lobj))
  and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
  in
  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
        dyn_load_function = loader;
                             dyn_open_function = opener;
        dyn_subst_function = substituter;
        dyn_classify_function = classifier;
        dyn_discharge_function = discharge;
        dyn_rebuild_function = rebuild };
  (infun,outfun)

let declare_object odecl = fst (declare_object_full odecl)
let declare_object_full odecl = declare_object_full odecl

(* this function describes how the cache, load, open, and export functions
   are triggered. *)

let apply_dyn_fun f lobj =
  let tag = object_tag lobj in
  let dodecl =
    try Hashtbl.find cache_tab tag
    with Not_found -> assert false
  in
  f dodecl

let cache_object ((_,lobj) as node) =
  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj

let load_object i ((_,lobj) as node) =
  apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj

let open_object i ((_,lobj) as node) =
  apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj

let subst_object ((_,lobj) as node) =
  apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj

let classify_object lobj =
  apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj

let discharge_object ((_,lobj) as node) =
  apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj

let rebuild_object lobj =
  apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj

let dump = Dyn.dump

let local_object_nodischarge s ~cache =
  { (default_object s) with
    cache_function = cache;
    classify_function = (fun _ -> Dispose);
  }

let local_object s ~cache ~discharge =
  { (local_object_nodischarge s ~cache) with
    discharge_function = discharge }

let global_object_nodischarge s ~cache ~subst =
  let import i o = if Int.equal i 1 then cache o in
  { (default_object s) with
    cache_function = cache;
    open_function = import;
    subst_function = (match subst with
        | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
        | Some subst -> subst;
      );
    classify_function =
      if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
  }

let global_object s ~cache ~subst ~discharge =
  { (global_object_nodischarge s ~cache ~subst) with
    discharge_function = discharge }

let superglobal_object_nodischarge s ~cache ~subst =
  { (default_object s) with
    load_function = (fun _ x -> cache x);
    cache_function = cache;
    subst_function = (match subst with
        | None -> fun _ -> CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")
        | Some subst -> subst;
      );
    classify_function =
      if Option.has_some subst then (fun o -> Substitute o) else (fun o -> Keep o);
  }

let superglobal_object s ~cache ~subst ~discharge =
  { (superglobal_object_nodischarge s ~cache ~subst) with
    discharge_function = discharge }

¤ Dauer der Verarbeitung: 0.243 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.