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