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, i)     -> f (B.LRef (a, i))
  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, v, t) ->
  30       let f tt vv = f (B.Appl (a, vv, tt)) in
  31       let f tt = xlate_term (f tt) v in
  32       xlate_term f t
  33    | D.TProj (_, e, t)  ->
  34       D.shift (xlate_term f) e t
  35    | D.TBind (a, b, t)  ->
  36       xlate_term (xlate_bind f a b) t
  37
  38 and xlate_bind f a b x = match b with
  39    | D.Abst (n, w) ->
  40       let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in
  41       xlate_term f w
  42    | D.Abbr v      ->
  43       let f vv = f (B.Bind (a, B.Abbr vv, x)) in
  44       xlate_term f v
  45    | D.Void        ->
  46       f (B.Bind (a, B.Void, x))
  47
  48 (* internal functions: brg to crg term **************************************)
  49
  50 let rec xlate_bk_term f = function
  51    | B.Sort (a, l)     -> f (D.TSort (a, l))
  52    | B.GRef (a, n)     -> f (D.TGRef (a, n))
  53    | B.LRef (a, i)     -> f (D.TLRef (a, i))
  54    | B.Cast (a, u, t)  ->
  55       let f tt uu = f (D.TCast (a, uu, tt)) in
  56       let f tt = xlate_bk_term (f tt) u in
  57       xlate_bk_term f t
  58    | B.Appl (a, u, t)  ->
  59       let f tt uu = f (D.TAppl (a, uu, tt)) in
  60       let f tt = xlate_bk_term (f tt) u in
  61       xlate_bk_term f t
  62    | B.Bind (a, b, t)  ->
  63       let f tt bb = f (D.TBind (a, bb, tt)) in
  64       let f tt = xlate_bk_bind (f tt) b in
  65       xlate_bk_term f t
  66
  67 and xlate_bk_bind f = function
  68    | B.Abst (n, t) ->
  69       let f tt = f (D.Abst (n, tt)) in
  70       xlate_bk_term f t
  71    | B.Abbr t      ->
  72       let f tt = f (D.Abbr tt) in
  73       xlate_bk_term f t
  74    | B.Void        -> f D.Void
  75
  76 (* interface functions ******************************************************)
  77
  78 let brg_of_crg f t = f (xlate_term C.start t)
  79
  80 let crg_of_brg = xlate_bk_term