helm/software/helena/src/complete_rg/crg.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: complete, relative, global *)
  13 (* note          : fragment of complete \lambda\delta serving as abstract layer *)
  14
  15 module C = Cps
  16 module E = Entity
  17 module N = Level
  18
  19 type uri = E.uri
  20 type id = E.id
  21 type attrs = E.attrs
  22
  23 type bind = Abst of N.level * term      (* level, type *)
  24           | Abbr of term                (* body *)
  25           | Void                        (* *)
  26
  27 and term = TSort of attrs * int         (* attrs, hierarchy index *)
  28          | TLRef of attrs * int         (* attrs, position indexe *)
  29          | TGRef of attrs * uri         (* attrs, reference *)
  30          | TCast of attrs * term * term (* attrs, domain, element *)
  31          | TAppl of attrs * term * term (* attrs, argument, function *)
  32          | TBind of attrs * bind * term (* attrs, binder, scope *)
  33          | TProj of attrs * lenv * term (* attrs, closure, member *)
  34
  35 and lenv = ESort                        (* top *)
  36          | EBind of lenv * attrs * bind (* environment, attrs, binder *)
  37          | EAppl of lenv * attrs * term (* environment, attrs, argument *)
  38          | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
  39
  40 type entity = term E.entity
  41
  42 (* helpers ******************************************************************)
  43
  44 let empty_lenv = ESort
  45
  46 let push_bind f a b lenv = f (EBind (lenv, a, b))
  47
  48 let push_appl f a t lenv = f (EAppl (lenv, a, t))
  49
  50 let push_proj f a e lenv = f (EProj (lenv, a, e))
  51
  52 let add_bind f a b t = f (TBind (a, b, t))
  53
  54 let add_appl f a v t = f (TAppl (a, v, t))
  55
  56 let add_proj f a e t = f (TProj (a, e, t))
  57
  58 let rec shift f c t = match c with
  59    | ESort           -> f t
  60    | EBind (e, a, b) -> add_bind (shift f e) a b t
  61    | EAppl (e, a, v) -> add_appl (shift f e) a v t
  62    | EProj (e, a, d) -> add_proj (shift f e) a d t
  63
  64 let rec append f c = function
  65    | ESort           -> f c
  66    | EBind (e, a, b) -> append (push_bind f a b) c e
  67    | EAppl (e, a, t) -> append (push_appl f a t) c e
  68    | EProj (e, a, d) -> append (push_proj f a d) c e
  69
  70 let resolve_lref err f id lenv =
  71    let rec aux i = function
  72      | ESort             -> err ()
  73      | EAppl (tl, _, _)  -> aux i tl
  74      | EBind (tl, a, _)  ->
  75         let f id0 _ = if id0 = id then f i else aux (succ i) tl in
  76         E.name err f a
  77      | EProj (tl, _, d)  -> append (aux i) tl d
  78    in
  79    aux 0 lenv
  80
  81 let rec get_name err f i = function
  82    | ESort                      -> err i
  83    | EAppl (tl, _, _)           -> get_name err f i tl
  84    | EBind (_, a, _) when i = 0 ->
  85       let err () = err i in
  86       E.name err f a
  87    | EBind (tl, _, _)           -> get_name err f (pred i) tl
  88    | EProj (tl, _, e)           ->
  89       let err i = get_name err f i tl in
  90       get_name err f i e
  91
  92 (*
  93 let push2 err f lenv ?attr ?t () = match lenv, attr, t with
  94    | EBind (e, a, Abst (n, ws)), Some attr, Some t ->
  95       f (EBind (e, (attr :: a), Abst (n, t :: ws)))
  96    | EBind (e, a, Abst (n, ws)), None, Some t      ->
  97       f (EBind (e, a, Abst (n, t :: ws)))
  98    | EBind (e, a, Abbr vs), Some attr, Some t      ->
  99       f (EBind (e, (attr :: a), Abbr (t :: vs)))
 100    | EBind (e, a, Abbr vs), None, Some t           ->
 101       f (EBind (e, a, Abbr (t :: vs)))
 102    | EBind (e, a, Void n), Some attr, None         ->
 103       f (EBind (e, (attr :: a), Void (succ n)))
 104    | EBind (e, a, Void n), None, None              ->
 105       f (EBind (e, a, Void (succ n)))
 106    | _                                             -> err ()
 107
 108 let get_index err f i j lenv =
 109    let rec aux f i k = function
 110       | ESort                      -> err i
 111       | EBind (tl, _, Abst (_, []))
 112       | EBind (tl, _, Abbr [])
 113       | EBind (tl, _, Void 0)      -> aux f i k tl
 114       | EBind (_, a, _) when i = 0 ->
 115          if E.count_names a > j then f (k + j) else err i
 116       | EBind (tl, a, _)           ->
 117          aux f (pred i) (k + E.count_names a) tl
 118       | EProj (tl, _, d)           -> aux f i k (eshift C.start tl d)
 119    in
 120    aux f i 0 lenv
 121 *)
 122 let rec names_of_lenv ns = function
 123    | ESort            -> ns
 124    | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
 125    | EAppl (tl, _, _) -> names_of_lenv ns tl
 126    | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
 127
 128 let rec get e i = match e with
 129    | ESort                      -> ESort, [], Void
 130    | EBind (e, a, b) when i = 0 -> e, a, b
 131    | EBind (e, _, _)            -> get e (pred i)
 132    | EAppl (e, _, _)            -> get e i
 133    | EProj (e, _, d)            -> get (append C.start e d) i
 134
 135 let rec sub_list_strict f e l = match e, l with
 136    | _, []                         -> f e
 137    | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
 138    | _                             -> assert false
 139
 140 let rec fold_attrs f map a0 = function
 141    | ESort                -> f a0
 142    | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e
 143    | _                    -> assert false