helm/software/helena/src/basic_ag/bagCrg.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 module C = Cps
  13 module E = Entity
  14 module J = Marks
  15 module N = Level
  16 module D = Crg
  17 module Z = Bag
  18
  19 (* internal functions: crg to bag term **************************************)
  20
  21 let rec shift t = function
  22    | _, []                    -> t
  23    | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns)
  24    | _                        -> assert false
  25
  26 let rec xlate_term xlate_bind f c = function
  27    | D.TSort (_, h)     -> f (Z.Sort h)
  28    | D.TGRef (_, s)     -> f (Z.GRef s)
  29    | D.TLRef (a, _, _)  ->
  30       let f i =
  31          let _, l, _ = List.nth c i in
  32          f (Z.LRef l)
  33       in
  34       E.apix C.err f a
  35    | D.TCast (_, u, t)  ->
  36       let f tt uu = f (Z.Cast (uu, tt)) in
  37       let f tt = xlate_term xlate_bind (f tt) c u in
  38       xlate_term xlate_bind f c t
  39    | D.TAppl (_, vs, t) ->
  40       let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in
  41       let f tt = C.list_fold_right f map vs tt in
  42       xlate_term xlate_bind f c t
  43    | D.TProj (_, e, t)  ->
  44       xlate_term xlate_bind f c (D.tshift e t)
  45 (* this case should be removed by improving alpha-conversion *)
  46    | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
  47       xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
  48    | D.TBind (a, b, t)  ->
  49       let g _ ns = ns in
  50       let ns = E.get_names g a in
  51       let cc = xlate_bind C.start c ns b in
  52       let f tt = f (shift tt (cc, ns)) in
  53       xlate_term xlate_bind f cc t
  54
  55 let rec xlate_bind f c ns = function
  56    | D.Abst (_, ws) ->
  57       let map f n w c =
  58          let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in
  59          xlate_term xlate_bind f c w
  60       in
  61       C.list_fold_right2 f map ns ws c
  62    | D.Abbr vs      ->
  63       let map f n v c =
  64          let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in
  65          xlate_term xlate_bind f c v
  66       in
  67       C.list_fold_right2 f map ns vs c
  68    | D.Void _       ->
  69       let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in
  70       C.list_fold_right f map ns c
  71
  72 (* internal functions: bag to crg term **************************************)
  73
  74 let rec xlate_bk_term f c = function
  75    | Z.Sort h            -> f (D.TSort ([], h))
  76    | Z.GRef s            -> f (D.TGRef ([], s))
  77    | Z.LRef l            ->
  78        let f i = f (D.TLRef ([], i, 0)) in
  79        Z.nth C.err f l c
  80    | Z.Cast (u, t)  ->
  81       let f tt uu = f (D.TCast ([], uu, tt)) in
  82       let f tt = xlate_bk_term (f tt) c u in
  83       xlate_bk_term f c t
  84    | Z.Appl (u, t)       ->
  85       let f tt uu = f (D.TAppl ([], [uu], tt)) in
  86       let f tt = xlate_bk_term (f tt) c u in
  87       xlate_bk_term f c t
  88    | Z.Bind (a, l, b, t) ->
  89       let f tt bb = f (D.TBind (a, bb, tt)) in
  90       let f tt = xlate_bk_bind (f tt) c b in
  91       let cc = Z.push "xlate_bk_term" C.start c a l b in
  92       xlate_bk_term f cc t
  93
  94 and xlate_bk_bind f c = function
  95    | Z.Abst t ->
  96       let f tt = f (D.Abst (N.infinite, [tt])) in
  97       xlate_bk_term f c t
  98    | Z.Abbr t ->
  99       let f tt = f (D.Abbr [tt]) in
 100       xlate_bk_term f c t
 101    | Z.Void   -> f (D.Void 1)
 102
 103 (* interface functions ******************************************************)
 104
 105 let bag_of_crg f t =
 106    xlate_term xlate_bind f Z.empty_lenv t
 107
 108 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t