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 N = Layer
  17 module E = Entity
  18
  19 type uri = E.uri
  20 type id = E.id
  21 type attrs = E.node_attrs
  22
  23 type bind = Abst of bool * N.layer * term       (* x-reduced?, layer, 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 * bool * term * term  (* attrs, extended?, 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 * bool * term  (* environment, attrs, extended?, 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 x t lenv = f (EAppl (lenv, a, x, 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 x v t = f (TAppl (a, x, 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, x, v) -> add_appl (shift f e) a x 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, x, t) -> append (push_appl f a x 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         let err () = aux (succ i) tl in
  77         E.name err f a
  78      | EProj (tl, _, d)     -> append (aux i) tl d
  79    in
  80    aux 0 lenv
  81
  82 let rec get_name err f i = function
  83    | ESort                      -> err i
  84    | EAppl (tl, _, _, _)        -> get_name err f i tl
  85    | EBind (_, a, _) when i = 0 ->
  86       let err () = err i in
  87       E.name err f a
  88    | EBind (tl, _, _)           -> get_name err f (pred i) tl
  89    | EProj (tl, _, e)           ->
  90       let err i = get_name err f i tl in
  91       get_name err f i e
  92
  93 let rec get e i = match e with
  94    | ESort                      -> ESort, E.empty_node, Void
  95    | EBind (e, a, b) when i = 0 -> e, a, b
  96    | EBind (e, _, _)            -> get e (pred i)
  97    | EAppl (e, _, _, _)         -> get e i
  98    | EProj (e, _, d)            -> get (append C.start e d) i
  99
 100 let rec sub_list_strict f e l = match e, l with
 101    | _, []                         -> f e
 102    | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
 103    | _                             -> assert false
 104
 105 let rec fold_names f map x = function
 106    | ESort                                  -> f x
 107    | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e
 108    | _                                      -> assert false
 109
 110 let rec mem err f e b = match e with
 111    | ESort              -> err ()
 112    | EBind (e, a, _)    ->
 113       if a.E.n_name = b.E.n_name then f () else mem err f e b
 114    | EAppl (e, _, _, _) -> mem err f e b
 115    | EProj (e, _, d)    ->
 116       let err () = mem err f e b in mem err f d b
 117
 118 let set_layer f n0 e =
 119    let rec aux f = function
 120       | ESort                        -> f ESort
 121       | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
 122       | EBind (e, a, b)              -> aux (push_bind f a b) e
 123       | EAppl (e, a, x, v)           -> aux (push_appl f a x v) e
 124       | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
 125    in
 126    aux f e
 127
 128 let set_attrs f a0 e =
 129    let rec aux f = function
 130       | ESort              -> f ESort
 131       | EBind (e, a, b)    ->
 132          let a = E.compose a a0 in
 133          aux (push_bind f a b) e
 134       | EAppl (e, a, x, v) ->
 135          let a = E.compose a a0 in
 136          aux (push_appl f a x v) e
 137       | EProj (e, a, d)    ->
 138          let a = E.compose a a0 in
 139          let f d = aux (push_proj f a d) e in
 140          aux f d
 141    in
 142    aux f e