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