helm/software/lambda-delta/toplevel/metaBrg.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 B = Brg
  13 module M = Meta
  14
  15 (* Internal functions *******************************************************)
  16
  17 let map_fold_left f map1 map2 a l =
  18    let f a = Cps.list_fold_left f map2 a l in
  19    map1 f a
  20
  21 let map_args f t v = f (B.Appl (v, t))
  22
  23 let map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t))
  24
  25 let rec xlate_term f = function
  26    | M.Sort s            ->
  27       let f h = f (B.Sort h) in
  28       if s then f 0 else f 1
  29    | M.LRef (l, i)       ->
  30       f (B.LRef (l - succ i))
  31    | M.GRef (_, uri, vs) ->
  32       let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in
  33       Cps.list_map f xlate_term vs
  34    | M.Appl (v, t)       ->
  35       let f v t = f (B.Appl (v, t)) in
  36       let f v = xlate_term (f v) t in
  37       xlate_term f v
  38    | M.Abst (id, w, t)   ->
  39       let f w t = f (B.Bind (id, B.Abst w, t)) in
  40       let f w = xlate_term (f w) t in
  41       xlate_term f w
  42
  43 let xlate_pars f (id, w) =
  44    let f w = f (id, w) in
  45    xlate_term f w
  46
  47 let xlate_entry f = function
  48    | e, pars, uri, u, None        ->
  49       let f u = f (e, uri, B.Abst u) in
  50       let f pars = map_fold_left f xlate_term map_pars u pars in
  51       Cps.list_map f xlate_pars pars
  52    | e, pars, uri, u, Some (_, t) ->
  53       let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in
  54       let f pars u = map_fold_left (f u) xlate_term map_pars t pars in
  55       let f pars = map_fold_left (f pars) xlate_term map_pars u pars in
  56       Cps.list_map f xlate_pars pars
  57
  58 let xlate_item f = function
  59    | None   -> f None
  60    | Some e -> let f e = f (Some e) in xlate_entry f e
  61
  62 (* Interface functions ******************************************************)
  63
  64 let brg_of_meta = xlate_item