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.node_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 a 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 let rec get e i = match e with
  93    | ESort                      -> ESort, E.empty_node, Void
  94    | EBind (e, a, b) when i = 0 -> e, a, b
  95    | EBind (e, _, _)            -> get e (pred i)
  96    | EAppl (e, _, _)            -> get e i
  97    | EProj (e, _, d)            -> get (append C.start e d) i
  98
  99 let rec sub_list_strict f e l = match e, l with
 100    | _, []                         -> f e
 101    | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
 102    | _                             -> assert false
 103
 104 let rec fold_names f map x = function
 105    | ESort                                  -> f x
 106    | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e
 107    | _                                      -> assert false
 108
 109 let rec mem err f e b = match e with
 110    | ESort           -> err ()
 111    | EBind (e, a, _) ->
 112       if a.E.n_name = b.E.n_name then f () else mem err f e b
 113    | EAppl (e, _, _) -> mem err f e b
 114    | EProj (e, _, d) ->
 115       let err () = mem err f e b in mem err f d b
 116
 117 let rec sta f = function
 118    | ESort                     -> f ESort
 119    | EBind (e, a, Abst (_, w)) -> sta (push_bind f a (Abst (N.one, w))) e
 120    | EBind (e, a, b)           -> sta (push_bind f a b) e
 121    | EAppl (e, a, v)           -> sta (push_appl f a v) e
 122    | EProj (e, a, d)           -> let f d = sta (push_proj f a d) e in sta f d