helm/software/lambda-delta/src/basic_rg/brgCrg.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 B = Brg
  18
  19 (* internal functions: crg to brg term **************************************)
  20
  21 let rec lenv_fold_left map1 map2 x = function
  22    | D.ESort            -> x
  23    | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
  24    | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
  25
  26 let rec xlate_term f = function
  27    | D.TSort (a, l)     -> f (B.Sort (a, l))
  28    | D.TGRef (a, n)     -> f (B.GRef (a, n))
  29    | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in E.apix C.err f a
  30    | D.TCast (a, u, t)  ->
  31       let f uu tt = f (B.Cast (a, uu, tt)) in
  32       let f uu = xlate_term (f uu) t in
  33       xlate_term f u
  34    | D.TAppl (a, vs, t) ->
  35       let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
  36       let f tt = C.list_fold_right f map vs tt in
  37       xlate_term f t
  38    | D.TProj (a, e, t)  ->
  39       let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
  40       xlate_term f t
  41    | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
  42       xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
  43    | D.TBind (a, b, t)  ->
  44       let f tt = f (xlate_bind tt a b) in xlate_term f t
  45
  46 and xlate_bind x a b =
  47    let f a ns = a, ns in
  48    let a, ns = E.get_names f a in
  49    match b with
  50       | D.Abst (m, ws) ->
  51          let map x n w =
  52             let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in
  53             xlate_term f w
  54          in
  55          List.fold_left2 map x ns ws
  56       | D.Abbr vs      ->
  57          let map x n v =
  58             let f vv = B.Bind (n :: a, B.Abbr vv, x) in
  59             xlate_term f v
  60          in
  61          List.fold_left2 map x ns vs
  62       | D.Void _       ->
  63          let map x n = B.Bind (n :: a, B.Void, x) in
  64          List.fold_left map x ns
  65
  66 and xlate_proj x _ e =
  67    lenv_fold_left xlate_bind xlate_proj x e
  68
  69 (* internal functions: brg to crg term **************************************)
  70
  71 let rec xlate_bk_term f = function
  72    | B.Sort (a, l)     -> f (D.TSort (a, l))
  73    | B.GRef (a, n)     -> f (D.TGRef (a, n))
  74    | B.LRef (a, i)     -> f (D.TLRef (a, i, 0))
  75    | B.Cast (a, u, t)  ->
  76       let f uu tt = f (D.TCast (a, uu, tt)) in
  77       let f uu = xlate_bk_term (f uu) t in
  78       xlate_bk_term f u
  79    | B.Appl (a, u, t)  ->
  80       let f uu tt = f (D.TAppl (a, [uu], tt)) in
  81       let f uu = xlate_bk_term (f uu) t in
  82       xlate_bk_term f u
  83    | B.Bind (a, b, t)  ->
  84       let f bb tt = f (D.TBind (a, bb, tt)) in
  85       let f bb = xlate_bk_term (f bb) t in
  86       xlate_bk_bind f b
  87
  88 and xlate_bk_bind f = function
  89    | B.Abst (n, t) ->
  90       let f tt = f (D.Abst (n, [tt])) in
  91       xlate_bk_term f t
  92    | B.Abbr t      ->
  93       let f tt = f (D.Abbr [tt]) in
  94       xlate_bk_term f t
  95    | B.Void        -> f (D.Void 1)
  96
  97 (* interface functions ******************************************************)
  98
  99 let brg_of_crg f t =
 100    f (xlate_term C.start t)
 101
 102 let crg_of_brg = xlate_bk_term