helm/software/lambda-delta/dual_rg/drg.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 (* kernel version: dual, relative, global *)
  13 (* note          : fragment of dual lambda-delta serving as abstract layer *)
  14
  15 type uri = Entity.uri
  16 type id = Entity.id
  17
  18 type attr = Name of id * bool  (* name, real? *)
  19           | Priv               (* private global definition *)
  20
  21 type attrs = attr list (* attributes *)
  22
  23 type bind = Abst of attrs * term (* attrs, domain *)
  24           | Abbr of attrs * term (* attrs, body   *)
  25           | Void of attrs        (* attrs         *)
  26
  27 and term = Sort of attrs * int              (* attrs, hierarchy index *)
  28          | LRef of attrs * int              (* attrs, position index *)
  29          | GRef of attrs * uri              (* attrs, reference *)
  30          | Cast of attrs * term * term      (* attrs, domain, element *)
  31          | Proj of attrs * lenv * term      (* attrs, closure, scope *)
  32          | Appl of attrs * term list * term (* attrs, arguments, function *)
  33          | Bind of bind * term              (* binder, scope *)
  34
  35 and lenv = bind list (* local environment *)
  36
  37 type entry = bind Entity.entry (* age, uri, binder *)
  38
  39 type entity = bind Entity.entity
  40
  41 (* helpers ******************************************************************)
  42
  43 let mk_uri root f s =
  44    let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
  45    f str
  46
  47 let rec name_of err f = function
  48    | Name (n, r) :: _ -> f n r
  49    | _ :: tl          -> name_of err f tl
  50    | []               -> err ()
  51
  52 let name_of_binder err f = function
  53    | Abst (a, _) -> name_of err f a
  54    | Abbr (a, _) -> name_of err f a
  55    | Void a      -> name_of err f a
  56
  57 let resolve_lref err f id lenv =
  58    let rec aux f i = function
  59      | []      -> err ()
  60      | b :: tl ->
  61         let err () = aux f (succ i) tl in
  62         let f name _ = if name = id then f i else err () in
  63         name_of_binder err f b
  64    in
  65    aux f 0 lenv