1 (* Copyright (C) 2011, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 type t = Stdpp.location * string (* location, name *)
29 let compare = Pervasives.compare
32 module Table = Map.Make (Domain)
34 module Ast = NotationPt
37 let rec aux lastloc acc = function
38 | Ast.AttributedTerm (`Loc l,u) -> aux l acc u
40 List.fold_left (aux lastloc) acc tl
41 | Ast.Binder (k,ty,body) ->
42 let acc' = aux_var lastloc acc ty in
44 | Ast.Case (t,ity,oty,pl) ->
45 (* FIXME: ity contains interpretation info
46 * but we don't have the location for it
47 * this must be rethought
49 let acc = aux lastloc acc t in
50 let acc = match oty with
52 | Some oty' -> aux lastloc acc oty'
54 List.fold_left (aux_pattern lastloc) acc pl
56 aux lastloc (aux lastloc acc v) u
57 | Ast.LetIn (ty,u,v) ->
58 let acc = aux_var lastloc acc ty in
59 let acc = aux lastloc acc u in
61 | Ast.LetRec (ik,l,t) ->
62 let acc = aux lastloc acc t in
63 List.fold_left (aux_letrec lastloc) acc l
64 | Ast.Ident (id,`Uri u) -> Table.add (lastloc,id) u acc
66 and aux_pattern lastloc acc = function
67 | Ast.Pattern (_,_,tys),t ->
68 (* FIXME: patterns may contain disambiguation info
70 let acc = aux lastloc acc t in
71 List.fold_left (aux_var lastloc) acc tys
72 | _,t -> aux lastloc acc t
73 and aux_letrec lastloc acc (args,ty,body,_) =
74 let acc = aux lastloc acc body in
75 let acc = List.fold_left (aux_var lastloc) acc args
77 aux_var lastloc acc ty
78 and aux_var lastloc acc (_,ty) =
81 | Some ty' -> aux lastloc acc ty'
83 in aux Stdpp.dummy_loc (Table.empty)