helm/software/lambda-delta/dual_rg/drgOutput.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 X = Library
  13 module D = Drg
  14
  15 (* this is not tail recursive *)
  16 let rec list_iter map l f = match l with
  17    | []       -> f
  18    | hd :: tl -> map hd (list_iter map tl f)
  19
  20 let rec lenv_iter map1 map2 l f = match l with
  21    | D.ESort              -> f
  22    | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f)
  23    | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f)
  24
  25 (* these are not tail recursive *)
  26 let rec exp_term t f = match t with
  27    | D.TSort (a, h)       ->
  28       let attrs = [X.position h; X.name a] in
  29       X.tag X.sort attrs f
  30    | D.TLRef (a, i, j)    ->
  31       let attrs = [X.position i; X.offset j; X.name a] in
  32       X.tag X.lref attrs f
  33    | D.TGRef (a, n)       ->
  34       let attrs = [X.uri n; X.name a] in
  35       X.tag X.gref attrs f
  36    | D.TCast (a, u, t)    ->
  37       let attrs = [] in
  38       X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
  39    | D.TAppl (a, vs, t)   ->
  40       let attrs = [X.arity (List.length vs)] in
  41       X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
  42    | D.TProj (a, lenv, t) ->
  43       let attrs = [] in
  44       X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv)
  45    | D.TBind (a, b, t) ->
  46       exp_bind a b (exp_term t f)
  47
  48 and exp_bind a b f = match b with
  49    | D.Abst ws ->
  50       let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
  51       X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
  52    | D.Abbr vs ->
  53       let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
  54       X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
  55    | D.Void n ->
  56       let attrs = [X.name a; X.mark a; X.arity n] in
  57       X.tag X.void attrs f
  58
  59 and exp_eproj a lenv f =
  60    let attrs = [] in
  61    X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv)
  62
  63 let export_term = exp_term