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