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 type attrs = Entity.attrs
  18
  19 type bind = Abst of term list (* domains *)
  20           | Abbr of term list (* bodies  *)
  21           | Void of int       (* number of exclusions *)
  22
  23 and term = Sort of attrs * int              (* attrs, hierarchy index *)
  24          | LRef of attrs * int * int        (* attrs, position indexes *)
  25          | GRef of attrs * uri              (* attrs, reference *)
  26          | Cast of attrs * term * term      (* attrs, domain, element *)
  27          | Appl of attrs * term list * term (* attrs, arguments, function *)
  28          | Proj of attrs * lenv * term      (* attrs, closure, member *)
  29          | Bind of attrs * bind * term      (* attrs, binder, scope *)
  30
  31 and lenv = Null
  32          | Cons of lenv * attrs * bind (* closure, attrs, binder *)
  33
  34 type entity = term Entity.entity
  35
  36 (* helpers ******************************************************************)
  37
  38 let mk_uri root f s =
  39    let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
  40    f str
  41
  42 let empty_lenv = Null
  43
  44 let push f lenv a b = f (Cons (lenv, a, b))
  45
  46 let resolve_lref err f id lenv =
  47    let rec aux f i k = function
  48      | Null            -> err ()
  49      | Cons (tl, a, _) ->
  50         let err kk = aux f (succ i) (k + kk) tl in
  51         let f j = f i j k in
  52         Entity.resolve err f id a
  53    in
  54    aux f 0 0 lenv