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          | Appl of attrs * term list * term (* attrs, arguments, function *)
  32          | Bind of lenv * term              (* closure, scope *)
  33
  34 and lenv = bind list (* local environment *)
  35
  36 type entry = bind Entity.entry (* age, uri, binder *)
  37
  38 type entity = bind Entity.entity
  39
  40 (* helpers ******************************************************************)
  41
  42 let mk_uri root f s =
  43    let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
  44    f str
  45
  46 let rec name_of err f = function
  47    | Name (n, r) :: _ -> f n r
  48    | _ :: tl          -> name_of err f tl
  49    | []               -> err ()
  50
  51 let name_of_binder err f = function
  52    | Abst (a, _) -> name_of err f a
  53    | Abbr (a, _) -> name_of err f a
  54    | Void a      -> name_of err f a
  55
  56 let resolve_lref err f id lenv =
  57    let rec aux f i = function
  58      | []      -> err ()
  59      | b :: tl ->
  60         let err () = aux f (succ i) tl in
  61         let f name _ = if name = id then f i else err () in
  62         name_of_binder err f b
  63    in
  64    aux f 0 lenv