1 (* Copyright (C) 2004-2005, 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 (* let meta_names_of term = *)
29 (* let rec names = ref [] in *)
30 (* let add_name n = *)
31 (* if List.mem n !names then () *)
32 (* else names := n :: !names *)
34 (* let rec aux = function *)
35 (* | AttributedTerm (_, term) -> aux term *)
36 (* | Appl terms -> List.iter aux terms *)
37 (* | Binder (_, _, body) -> aux body *)
38 (* | Case (term, indty, outty_opt, patterns) -> *)
40 (* aux_opt outty_opt ; *)
41 (* List.iter aux_branch patterns *)
42 (* | LetIn (_, t1, t2) -> *)
45 (* | LetRec (_, definitions, body) -> *)
46 (* List.iter aux_definition definitions ; *)
48 (* | Uri (_, Some substs) -> aux_substs substs *)
49 (* | Ident (_, Some substs) -> aux_substs substs *)
50 (* | Meta (_, substs) -> aux_meta_substs substs *)
58 (* | UserInput -> () *)
60 (* | Magic magic -> aux_magic magic *)
61 (* | Variable var -> aux_variable var *)
63 (* | _ -> assert false *)
64 (* and aux_opt = function *)
65 (* | Some term -> aux term *)
67 (* and aux_capture_var (_, ty_opt) = aux_opt ty_opt *)
68 (* and aux_branch (pattern, term) = *)
69 (* aux_pattern pattern ; *)
71 (* and aux_pattern (head, vars) = *)
72 (* List.iter aux_capture_var vars *)
73 (* and aux_definition (var, term, i) = *)
74 (* aux_capture_var var ; *)
76 (* and aux_substs substs = List.iter (fun (_, term) -> aux term) substs *)
77 (* and aux_meta_substs meta_substs = List.iter aux_opt meta_substs *)
78 (* and aux_variable = function *)
79 (* | NumVar name -> add_name name *)
80 (* | IdentVar name -> add_name name *)
81 (* | TermVar name -> add_name name *)
82 (* | FreshVar _ -> () *)
83 (* | Ascription _ -> assert false *)
84 (* and aux_magic = function *)
85 (* | Default (t1, t2) *)
86 (* | Fold (_, t1, _, t2) -> *)
89 (* | _ -> assert false *)
94 let visit_ast ?(special_k = fun _ -> assert false) k =
95 let rec aux = function
96 | Appl terms -> Appl (List.map k terms)
97 | Binder (kind, var, body) ->
98 Binder (kind, aux_capture_variable var, k body)
99 | Case (term, indtype, typ, patterns) ->
100 Case (k term, indtype, aux_opt typ, aux_patterns patterns)
101 | Cast (t1, t2) -> Cast (k t1, k t2)
102 | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
103 | LetRec (kind, definitions, term) ->
106 (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
109 LetRec (kind, definitions, k term)
110 | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
111 | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
112 | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
117 | Variable _) as t -> special_k t
124 | UserInput) as t -> t
125 and aux_opt = function
127 | Some term -> Some (k term)
128 and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
129 and aux_patterns patterns = List.map aux_pattern patterns
130 and aux_pattern ((head, vars), term) =
131 ((head, List.map aux_capture_variable vars), k term)
132 and aux_subst (name, term) = (name, k term)
133 and aux_substs substs = List.map aux_subst substs
137 let visit_layout k = function
138 | Sub (t1, t2) -> Sub (k t1, k t2)
139 | Sup (t1, t2) -> Sup (k t1, k t2)
140 | Below (t1, t2) -> Below (k t1, k t2)
141 | Above (t1, t2) -> Above (k t1, k t2)
142 | Over (t1, t2) -> Over (k t1, k t2)
143 | Atop (t1, t2) -> Atop (k t1, k t2)
144 | Frac (t1, t2) -> Frac (k t1, k t2)
145 | Sqrt t -> Sqrt (k t)
146 | Root (arg, index) -> Root (k arg, k index)
148 | Box (kind, terms) -> Box (kind, List.map k terms)
149 | Group terms -> Group (List.map k terms)
151 let visit_magic k = function
152 | List0 (t, l) -> List0 (k t, l)
153 | List1 (t, l) -> List1 (k t, l)
155 | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
156 | Default (t1, t2) -> Default (k t1, k t2)
157 | If (t1, t2, t3) -> If (k t1, k t2, k t3)
160 let variables_of_term t =
161 let rec vars = ref [] in
163 if List.mem v !vars then ()
164 else vars := v :: !vars
166 let rec aux = function
167 | Magic m -> Magic (visit_magic aux m)
168 | Layout l -> Layout (visit_layout aux l)
169 | Variable v -> Variable (aux_variable v)
170 | Literal _ as t -> t
171 | AttributedTerm (_, t) -> aux t
172 | t -> visit_ast aux t
173 and aux_variable = function
179 | FreshVar _ as t -> t
180 | Ascription _ -> assert false
185 let names_of_term t =
192 List.map aux (variables_of_term t)
194 let keywords_of_term t =
195 let rec keywords = ref [] in
196 let add_keyword k = keywords := k :: !keywords in
197 let rec aux = function
198 | AttributedTerm (_, t) -> aux t
199 | Layout l -> Layout (visit_layout aux l)
200 | Literal (`Keyword k) as t ->
203 | Literal _ as t -> t
204 | Magic m -> Magic (visit_magic aux m)
205 | Variable _ as v -> v
206 | t -> visit_ast aux t
211 let rec strip_attributes t =
212 let special_k = function
213 | AttributedTerm (_, term) -> strip_attributes term
214 | Magic m -> Magic (visit_magic strip_attributes m)
215 | Variable _ as t -> t
218 visit_ast ~special_k strip_attributes t
220 let meta_names_of_term term =
221 let rec names = ref [] in
223 if List.mem n !names then ()
224 else names := n :: !names
226 let rec aux = function
227 | AttributedTerm (_, term) -> aux term
228 | Appl terms -> List.iter aux terms
229 | Binder (_, _, body) -> aux body
230 | Case (term, indty, outty_opt, patterns) ->
233 List.iter aux_branch patterns
234 | LetIn (_, t1, t2) ->
237 | LetRec (_, definitions, body) ->
238 List.iter aux_definition definitions ;
240 | Uri (_, Some substs) -> aux_substs substs
241 | Ident (_, Some substs) -> aux_substs substs
242 | Meta (_, substs) -> aux_meta_substs substs
252 | Magic magic -> aux_magic magic
253 | Variable var -> aux_variable var
256 and aux_opt = function
257 | Some term -> aux term
259 and aux_capture_var (_, ty_opt) = aux_opt ty_opt
260 and aux_branch (pattern, term) =
261 aux_pattern pattern ;
263 and aux_pattern (head, vars) =
264 List.iter aux_capture_var vars
265 and aux_definition (var, term, i) =
266 aux_capture_var var ;
268 and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
269 and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
270 and aux_variable = function
271 | NumVar name -> add_name name
272 | IdentVar name -> add_name name
273 | TermVar name -> add_name name
275 | Ascription _ -> assert false
276 and aux_magic = function
278 | Fold (_, t1, _, t2) ->
291 let rectangular matrix =
292 let columns = Array.length matrix.(0) in
294 Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix;
299 let matrix = Array.of_list (List.map Array.of_list ll) in
300 assert (rectangular matrix);
301 let rows = Array.length matrix in
302 let columns = Array.length matrix.(0) in
303 let lists = ref [] in
304 for j = 0 to columns - 1 do
306 for i = 0 to rows - 1 do
307 l := matrix.(i).(j) :: !l
309 lists := List.rev !l :: !lists
313 let string_of_literal = function
318 let boxify = function
320 | l -> Layout (Box ((H, false, false), l))
322 let unboxify = function
323 | Layout (Box ((H, false, false), [ a ])) -> a
328 | l -> Layout (Group l)
334 | Layout (Group terms) :: terms' -> aux acc (terms @ terms')
335 | term :: terms -> aux (term :: acc) terms
344 | hd :: tl -> hd :: sauce :: aux tl
348 let find_appl_pattern_uris ap =
353 ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
355 with Not_found -> uri :: acc)
357 | VarPattern _ -> acc
358 | ApplPattern apl -> List.fold_left aux acc apl
362 let rec find_branch =
364 Magic (If (_, Magic Fail, t)) -> find_branch t
365 | Magic (If (_, t, _)) -> find_branch t
368 let cic_name_of_name = function
369 | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
370 | CicNotationPt.Ident (name, None) -> Cic.Name name
373 let name_of_cic_name = function
374 | Cic.Name s -> CicNotationPt.Ident (s, None)
375 | Cic.Anonymous -> CicNotationPt.Ident ("_", None)
377 let fresh_index = ref ~-1
379 type notation_id = int
385 (* TODO ensure that names generated by fresh_var do not clash with user's *)
386 let fresh_name () = "fresh" ^ string_of_int (fresh_id ())