helm/software/helena/src/common/entity.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module U = NUri
  13 module N = Layer
  14
  15 type uri = U.uri
  16
  17 type id = string (* identifier *)
  18
  19 type name = id * bool (* token, real? *)
  20
  21 type arity = int * int (* sort, degree *)
  22
  23 type meta = Main     (* main object *)
  24           | InProp   (* inhabitant of a proposition *)
  25           | Progress (* uncompleted object *)
  26           | Private  (* private global definition *)
  27
  28 type node_attrs = {
  29    n_apix: int; (* additional position index *)
  30 }
  31
  32 type appl_attrs = {
  33    a_rest: bool;  (* restricted application? *)
  34    a_main: arity; (* main arity *)
  35    a_side: arity; (* side arity *)
  36 }
  37
  38 type bind_attrs = {
  39    b_name: name option; (* name *)
  40    b_main: arity;       (* main arity *)
  41    b_side: arity;       (* side arity *)
  42 }
  43
  44 type root_attrs = {
  45    r_meta: meta list;                (* metaliguistic classification *)
  46    r_info: (string * string) option; (* metaliguistic annotation: language (defaults to "en-US"), text *)
  47 }
  48
  49 type env_attrs = {
  50    e_side: arity; (* arity *)
  51 }
  52
  53
  54 type 'term bind = Abst of env_attrs * 'term (* declaration: attrs, domain *)
  55                 | Abbr of env_attrs * 'term (* definition: attrs, body    *)
  56                 | Void                      (* exclusion                  *)
  57
  58 type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, binder *)
  59
  60 (* helpers ******************************************************************)
  61
  62 let node_attrs ?(apix=0) () = {
  63    n_apix = apix;
  64 }
  65
  66 let appl_attrs ?(main=(0,0)) ?(side=(0,0)) rest = {
  67    a_rest = rest; a_main = main; a_side = side;
  68 }
  69
  70 let bind_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = {
  71    b_name = name; b_main = main; b_side = side;
  72 }
  73
  74 let root_attrs ?(meta=[]) ?info () = {
  75    r_meta = meta; r_info = info;
  76 }
  77
  78 let env_attrs ?(side=(0,0)) () = {
  79    e_side = side;
  80 }
  81
  82 let empty_node = node_attrs ()
  83
  84 let empty_bind = bind_attrs ()
  85
  86 let empty_root = root_attrs ()
  87
  88 let empty_env = env_attrs ()
  89
  90 let abst a t = Abst (a, t)
  91
  92 let abbr a t = Abbr (a, t)
  93
  94 let common f (ra, na, u, _) = f ra na u
  95
  96 let succ (sort, degr) = sort, succ degr
  97
  98 let compose av yt = {av with b_main = yt}
  99
 100 let rec name err f a = match a.b_name with
 101    | Some (n, r) -> f n r
 102    | None        -> err ()
 103
 104 let rec info err f a = match a.r_info with
 105    | Some (lg, tx) -> f lg tx
 106    | None          -> err ()
 107
 108 let xlate f xlate_term = function
 109    | ra, na, uri, Abst (a, t) ->
 110       let f t = f (ra, na, uri, abst a t) in xlate_term f t
 111    | ra, na, uri, Abbr (a, t) ->
 112       let f t = f (ra, na, uri, abbr a t) in xlate_term f t
 113    | _, _, _, Void            ->
 114       assert false