helm/ocaml/cic_notation/cicNotationUtil.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open CicNotationPt
  27
  28   (* TODO ensure that names generated by fresh_var do not clash with user's *)
  29 let fresh_name =
  30   let index = ref ~-1 in
  31   fun () ->
  32     incr index;
  33     "fresh" ^ string_of_int !index
  34
  35 let visit_ast ?(special_k = fun _ -> assert false) k =
  36   let rec aux = function
  37
  38     | Appl terms -> Appl (List.map k terms)
  39     | Binder (kind, var, body) ->
  40         Binder (kind, aux_capture_variable var, k body)
  41     | Case (term, indtype, typ, patterns) ->
  42         Case (k term, indtype, aux_opt typ, aux_patterns patterns)
  43     | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
  44     | LetRec (kind, definitions, term) ->
  45         let definitions =
  46           List.map
  47             (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
  48             definitions
  49         in
  50         LetRec (kind, definitions, k term)
  51     | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
  52     | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
  53     | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
  54
  55     | (AttributedTerm _
  56       | Layout _
  57       | Literal _
  58       | Magic _
  59       | Variable _) as t -> special_k t
  60
  61     | (Ident _
  62       | Implicit
  63       | Num _
  64       | Sort _
  65       | Symbol _
  66       | Uri _
  67       | UserInput) as t -> t
  68
  69   and aux_opt = function
  70     | None -> None
  71     | Some term -> Some (k term)
  72
  73   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
  74
  75   and aux_patterns patterns = List.map aux_pattern patterns
  76
  77   and aux_pattern ((head, vars), term) =
  78     ((head, List.map aux_capture_variable vars), k term)
  79
  80   and aux_subst (name, term) = (name, k term)
  81
  82   and aux_substs substs = List.map aux_subst substs
  83
  84   in
  85
  86   aux
  87
  88 let visit_layout k = function
  89   | Sub (t1, t2) -> Sub (k t1, k t2)
  90   | Sup (t1, t2) -> Sup (k t1, k t2)
  91   | Below (t1, t2) -> Below (k t1, k t2)
  92   | Above (t1, t2) -> Above (k t1, k t2)
  93   | Over (t1, t2) -> Over (k t1, k t2)
  94   | Atop (t1, t2) -> Atop (k t1, k t2)
  95   | Frac (t1, t2) -> Frac (k t1, k t2)
  96   | Sqrt t -> Sqrt (k t)
  97   | Root (arg, index) -> Root (k arg, k index)
  98   | Break -> Break
  99   | Box (kind, terms) -> Box (kind, List.map k terms)
 100
 101 let visit_magic k = function
 102   | List0 (t, l) -> List0 (k t, l)
 103   | List1 (t, l) -> List1 (k t, l )
 104   | Opt t -> Opt (k t)
 105   | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
 106   | Default (t1, t2) -> Default (k t1, k t2)
 107
 108 let rec strip_attributes t =
 109   prerr_endline "strip_attributes";
 110   let special_k = function
 111     | AttributedTerm (_, term) -> strip_attributes term
 112     | Magic m -> Magic (visit_magic strip_attributes m)
 113     | Variable _ as t -> t
 114     | t -> assert false
 115   in
 116   visit_ast ~special_k strip_attributes t
 117