helm/software/lambda-delta/dual_rg/drgBrg.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 Y = Entity
  14 module D = Drg
  15 module B = Brg
  16
  17 let rec lenv_fold_left map1 map2 x = function
  18    | D.ESort            -> x
  19    | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
  20    | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
  21
  22 let rec xlate_term f = function
  23    | D.TSort (a, l)     -> f (B.Sort (a, l))
  24    | D.TGRef (a, n)     -> f (B.GRef (a, n))
  25    | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
  26    | D.TCast (a, u, t)  ->
  27       let f uu tt = f (B.Cast (a, uu, tt)) in
  28       let f uu = xlate_term (f uu) t in
  29       xlate_term f t
  30    | D.TAppl (a, vs, t) ->
  31       let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
  32       let f tt = C.list_fold_right f map vs tt in
  33       xlate_term f t
  34    | D.TProj (ap, e, D.TCast (ac, u, t)) ->
  35       xlate_term f (D.TCast (ac, D.TProj (ap, e, u), D.TProj (ap, e, t)))
  36    | D.TProj (a, e, t)  ->
  37       let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
  38       xlate_term f t
  39    | D.TBind (a, b, t)  ->
  40       let f tt = f (xlate_bind tt a b) in xlate_term f t
  41
  42 and xlate_bind x a b = assert false
  43
  44 and xlate_proj x _ e =
  45    lenv_fold_left xlate_bind xlate_proj x e
  46
  47 let brg_of_drg f t =
  48    f (xlate_term C.start t)