helm/software/helena/src/basic_ag/bagCrg.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 P = Marks
  14 module N = Layer
  15 module E = Entity
  16 module D = Crg
  17 module Z = Bag
  18
  19 (* internal functions: crg to bag term **************************************)
  20
  21 let rec xlate_term st f c = function
  22    | D.TSort k         -> f (Z.Sort k)
  23    | D.TGRef (_, s)    -> f (Z.GRef s)
  24    | D.TLRef (_, i)    ->
  25       let _, l, _ = List.nth c i in f (Z.LRef l)
  26    | D.TCast (u, t)    ->
  27       let f tt uu = f (Z.Cast (uu, tt)) in
  28       let f tt = xlate_term st (f tt) c u in
  29       xlate_term st f c t
  30    | D.TAppl (_, v, t) ->
  31       let f tt vv = f (Z.Appl (vv, tt)) in
  32       let f tt = xlate_term st (f tt) c v in
  33       xlate_term st f c t
  34    | D.TProj (e, t)    ->
  35       D.shift (xlate_term st f c) e t
  36 (* this case should be removed by improving alpha-conversion *)
  37    | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) ->
  38       xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t)))
  39    | D.TBind (y, b, t) ->
  40       let f cc =
  41          let a, l, b = List.hd cc in
  42          let f tt = f (Z.Bind (a, l, b, tt)) in
  43          xlate_term st f cc t
  44       in
  45       xlate_bind st f c y b
  46
  47 and xlate_bind st f c y = function
  48    | D.Abst (_, _, w) ->
  49       let f ww = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abst ww) in
  50       xlate_term st f c w
  51    | D.Abbr v         ->
  52       let f vv = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abbr vv) in
  53       xlate_term st f c v
  54    | D.Void           ->
  55       Z.push "xlate_bind" f c y (P.new_mark ()) Z.Void
  56
  57 (* internal functions: bag to crg term **************************************)
  58
  59 let rec xlate_bk_term f c = function
  60    | Z.Sort k            -> f (D.TSort k)
  61    | Z.GRef s            -> f (D.TGRef (E.empty_node, s))
  62    | Z.LRef l            ->
  63        let f i = f (D.TLRef (E.empty_node, i)) in
  64        Z.nth C.err f l c
  65    | Z.Cast (u, t)  ->
  66       let f tt uu = f (D.TCast (uu, tt)) in
  67       let f tt = xlate_bk_term (f tt) c u in
  68       xlate_bk_term f c t
  69    | Z.Appl (u, t)       ->
  70       let f tt uu = f (D.TAppl (E.appl_attrs false, uu, tt)) in
  71       let f tt = xlate_bk_term (f tt) c u in
  72       xlate_bk_term f c t
  73    | Z.Bind (y, l, b, t) ->
  74       let f tt bb = f (D.TBind (y, bb, tt)) in
  75       let f tt = xlate_bk_bind (f tt) c b in
  76       let cc = Z.push "xlate_bk_term" C.start c y l b in
  77       xlate_bk_term f cc t
  78
  79 and xlate_bk_bind f c = function
  80    | Z.Abst t ->
  81       let f tt = f (D.Abst (false, N.infinity, tt)) in
  82       xlate_bk_term f c t
  83    | Z.Abbr t ->
  84       let f tt = f (D.Abbr tt) in
  85       xlate_bk_term f c t
  86    | Z.Void   -> f D.Void
  87
  88 (* interface functions ******************************************************)
  89
  90 let bag_of_crg st f t =
  91    xlate_term st f Z.empty_lenv t
  92
  93 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t