]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/content_pres/termContentPres.ml
Added new syntax Type[n] where n is a number.
[helm.git] / helm / software / components / content_pres / termContentPres.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 (* $Id$ *)
27
28 open Printf
29
30 module Ast = CicNotationPt
31 module Env = CicNotationEnv
32
33 let debug = false
34 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
35
36 type pattern_id = int
37 type pretty_printer_id = pattern_id
38
39 let resolve_binder = function
40   | `Lambda -> "\\lambda"
41   | `Pi -> "\\Pi"
42   | `Forall -> "\\forall"
43   | `Exists -> "\\exists"
44
45 let add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
46
47 let rec top_pos t = add_level_info ~-1 t
48
49 let rec remove_level_info =
50   function
51   | Ast.AttributedTerm (`Level _, t) -> remove_level_info t
52   | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t)
53   | t -> t
54
55 let add_xml_attrs attrs t =
56   if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t)
57
58 let add_keyword_attrs =
59   add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
60
61 let box kind spacing indent content =
62   Ast.Layout (Ast.Box ((kind, spacing, indent), content))
63
64 let hbox = box Ast.H
65 let vbox = box Ast.V
66 let hvbox = box Ast.HV
67 let hovbox = box Ast.HOV
68 let break = Ast.Layout Ast.Break
69 let space = Ast.Literal (`Symbol " ")
70 let builtin_symbol s = Ast.Literal (`Symbol s)
71 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
72
73 let number s =
74   add_xml_attrs (RenderingAttrs.number_attributes `MathML)
75     (Ast.Literal (`Number s))
76
77 let ident i =
78   add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
79
80 let ident_w_href href i =
81   match href with
82   | None -> ident i
83   | Some href ->
84       let href = UriManager.string_of_uri href in
85       add_xml_attrs [Some "xlink", "href", href] (ident i)
86
87 let binder_symbol s =
88   add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
89     (builtin_symbol s)
90
91 let string_of_sort_kind = function
92   | `Prop -> "Prop"
93   | `Set -> "Set"
94   | `CProp _ -> "CProp"
95   | `Type _ -> "Type"
96   | `NType s -> "Type[" ^ s ^ "]"
97
98 let pp_ast0 t k =
99   let rec aux =
100     function
101     | Ast.Appl ts ->
102         let rec aux_args level =
103           function
104           | [] -> []
105           | [ last ] ->
106               [ Ast.AttributedTerm (`Level level,k last) ]
107           | hd :: tl ->
108               (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
109         in
110         add_level_info Ast.apply_prec 
111           (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
112     | Ast.Binder (binder_kind, (id, ty), body) ->
113         add_level_info Ast.binder_prec
114           (hvbox false true
115             [ binder_symbol (resolve_binder binder_kind);
116               k id; builtin_symbol ":"; aux_ty ty; break;
117               builtin_symbol "."; k body ])
118     | Ast.Case (what, indty_opt, outty_opt, patterns) ->
119         let outty_box =
120           match outty_opt with
121           | None -> []
122           | Some outty ->
123               [ space; keyword "return"; space; break; remove_level_info (k outty)]
124         in
125         let indty_box =
126           match indty_opt with
127           | None -> []
128           | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ]
129         in
130         let match_box =
131           hvbox false false [
132            hvbox false true [
133             hvbox false true [keyword "match"; space; break; top_pos (k what)];
134             break;
135             hvbox false true indty_box;
136             break;
137             hvbox false true outty_box
138            ];
139            break;
140            space;
141            keyword "with";
142            space
143          ]
144         in
145         let mk_case_pattern =
146          function
147             Ast.Pattern (head, href, vars) ->
148              hvbox true false (ident_w_href href head :: List.map aux_var vars)
149           | Ast.Wildcard -> builtin_symbol "_"
150         in
151         let patterns' =
152           List.map
153             (fun (lhs, rhs) ->
154               remove_level_info
155                 (hvbox false true [
156                   hbox false true [
157                     mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ];
158                   break; top_pos (k rhs) ]))
159             patterns
160         in
161         let patterns'' =
162           let rec aux_patterns = function
163             | [] -> assert false
164             | [ last ] ->
165                 [ break; 
166                   hbox false false [
167                     builtin_symbol "|";
168                     last; builtin_symbol "]" ] ]
169             | hd :: tl ->
170                 [ break; hbox false false [ builtin_symbol "|"; hd ] ]
171                 @ aux_patterns tl
172           in
173           match patterns' with
174           | [] ->
175               [ hbox false false [ builtin_symbol "["; builtin_symbol "]" ] ]
176           | [ one ] ->
177               [ hbox false false [
178                 builtin_symbol "["; one; builtin_symbol "]" ] ]
179           | hd :: tl ->
180               hbox false false [ builtin_symbol "["; hd ]
181               :: aux_patterns tl
182         in
183         add_level_info Ast.simple_prec
184           (hvbox false false [
185             hvbox false false ([match_box]); break;
186             hbox false false [ hvbox false false patterns'' ] ])
187     | Ast.Cast (bo, ty) ->
188         add_level_info Ast.simple_prec
189           (hvbox false true [
190             builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":";
191             top_pos (k ty); builtin_symbol ")"])
192     | Ast.LetIn (var, s, t) ->
193         add_level_info Ast.let_in_prec 
194           (hvbox false true [
195             hvbox false true [
196               keyword "let"; space;
197               hvbox false true [
198                 aux_var var; space;
199                 builtin_symbol "\\def"; break; top_pos (k s) ];
200               break; space; keyword "in"; space ];
201             break;
202             k t ])
203     | Ast.LetRec (rec_kind, funs, where) ->
204         let rec_op =
205           match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
206         in
207         let mk_fun (args, (name,ty), body, rec_param) =
208          List.map aux_var args ,k name, HExtlib.map_option k ty, k body,  
209            fst (List.nth args rec_param)
210         in
211         let mk_funs = List.map mk_fun in
212         let fst_fun, tl_funs =
213           match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false
214         in
215         let fst_row =
216           let (params, name, ty, body, rec_param) = fst_fun in
217           hvbox false true ([
218             keyword "let";
219             space;
220             keyword rec_op;
221             space;
222             name] @
223             params @
224             [space; keyword "on" ; space ; rec_param ;space ] @
225             (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
226             [ builtin_symbol "\\def";
227             break;
228             top_pos body ])
229         in
230         let tl_rows =
231           List.map
232             (fun (params, name, ty, body, rec_param) ->
233               [ break;
234                 hvbox false true ([
235                   keyword "and";
236                   name] @
237                   params @
238                   [space; keyword "on" ; space; rec_param ;space ] @
239                   (match ty with
240                       None -> []
241                     | Some ty -> [builtin_symbol ":"; ty]) @
242                   [ builtin_symbol "\\def"; break; body ])])
243             tl_funs
244         in
245         add_level_info Ast.let_in_prec
246           ((hvbox false false
247             (fst_row :: List.flatten tl_rows
248              @ [ break; keyword "in"; break; k where ])))
249     | Ast.Implicit -> builtin_symbol "?"
250     | Ast.Meta (n, l) ->
251         let local_context l =
252             List.map (function None -> None | Some t -> Some (k t)) l
253         in
254         Ast.Meta(n, local_context l)
255     | Ast.Sort sort -> aux_sort sort
256     | Ast.Num _
257     | Ast.Symbol _
258     | Ast.Ident (_, None) | Ast.Ident (_, Some [])
259     | Ast.Uri (_, None) | Ast.Uri (_, Some [])
260     | Ast.Literal _
261     | Ast.UserInput as leaf -> leaf
262     | t -> CicNotationUtil.visit_ast ~special_k k t
263   and aux_sort sort_kind =
264     add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
265       (Ast.Ident (string_of_sort_kind sort_kind, None))
266   and aux_ty = function
267     | None -> builtin_symbol "?"
268     | Some ty -> k ty
269   and aux_var = function
270     | name, Some ty ->
271         hvbox false true [
272           builtin_symbol "("; name; builtin_symbol ":"; break; k ty;
273           builtin_symbol ")" ]
274     | name, None -> name
275   and special_k = function
276     | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
277     | t ->
278         prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t);
279         assert false
280   in
281   aux t
282
283   (* persistent state *)
284
285 let initial_level1_patterns21 () = Hashtbl.create 211
286 let level1_patterns21 = ref (initial_level1_patterns21 ())
287 let compiled21 = ref None
288 let pattern21_matrix = ref []
289 let counter = ref ~-1 
290
291 let stack = ref [];;
292
293 let push () =
294   stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack;
295   counter := ~-1;
296   level1_patterns21 := initial_level1_patterns21 ();
297   compiled21 := None;
298   pattern21_matrix := []
299 ;;
300
301 let pop () =
302  match !stack with
303     [] -> assert false
304   | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old ->
305      stack := old;
306      counter := ocounter;
307      level1_patterns21 := olevel1_patterns21;
308      compiled21 := ocompiled21;
309      pattern21_matrix := opatterns21_matrix
310 ;;
311
312 let get_compiled21 () =
313   match !compiled21 with
314   | None -> assert false
315   | Some f -> Lazy.force f
316
317 let set_compiled21 f = compiled21 := Some f
318
319 let add_idrefs =
320   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
321
322 let instantiate21 idrefs env l1 =
323   let rec subst_singleton pos env =
324     function
325       Ast.AttributedTerm (attr, t) ->
326         Ast.AttributedTerm (attr, subst_singleton pos env t)
327     | t -> CicNotationUtil.group (subst pos env t)
328   and subst pos env = function
329     | Ast.AttributedTerm (attr, t) ->
330 (*         prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
331         subst pos env t
332     | Ast.Variable var ->
333         let name, expected_ty = CicNotationEnv.declaration_of_var var in
334         let ty, value =
335           try
336             List.assoc name env
337           with Not_found ->
338             prerr_endline ("name " ^ name ^ " not found in environment");
339             assert false
340         in
341         assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
342         (* following assertion should be a conditional that makes this
343          * instantiation fail *)
344         if not (CicNotationEnv.well_typed expected_ty value) then
345          begin
346           prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration");
347           assert false
348          end;
349         let value = CicNotationEnv.term_of_value value in
350         let value = 
351           match expected_ty with
352           | Env.TermType l -> Ast.AttributedTerm (`Level l,value) 
353           | _ -> value
354         in
355         [ value ]
356     | Ast.Magic m -> subst_magic pos env m
357     | Ast.Literal l as t ->
358         let t = add_idrefs idrefs t in
359         (match l with
360         | `Keyword k -> [ add_keyword_attrs t ]
361         | _ -> [ t ])
362     | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
363     | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ]
364   and subst_magic pos env = function
365     | Ast.List0 (p, sep_opt)
366     | Ast.List1 (p, sep_opt) ->
367         let rec_decls = CicNotationEnv.declarations_of_term p in
368         let rec_values =
369           List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
370         in
371         let values = CicNotationUtil.ncombine rec_values in
372         let sep =
373           match sep_opt with
374             | None -> []
375             | Some l -> [ Ast.Literal l; break; space ]
376         in
377         let rec instantiate_list acc = function
378           | [] -> List.rev acc
379           | value_set :: [] ->
380               let env = CicNotationEnv.combine rec_decls value_set in
381               instantiate_list (CicNotationUtil.group (subst pos env p) :: acc)
382                 []
383           | value_set :: tl ->
384               let env = CicNotationEnv.combine rec_decls value_set in
385               let terms = subst pos env p in
386               instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
387         in
388         if values = [] then []
389         else [hovbox false false (instantiate_list [] values)]
390     | Ast.Opt p ->
391         let opt_decls = CicNotationEnv.declarations_of_term p in
392         let env =
393           let rec build_env = function
394             | [] -> []
395             | (name, ty) :: tl ->
396                   (* assumption: if one of the value is None then all are *)
397                 (match CicNotationEnv.lookup_opt env name with
398                 | None -> raise Exit
399                 | Some v -> (name, (ty, v)) :: build_env tl)
400           in
401           try build_env opt_decls with Exit -> []
402         in
403           begin
404             match env with
405               | [] -> []
406               | _ -> subst pos env p
407           end
408     | _ -> assert false (* impossible *)
409   and subst_layout pos env = function
410     | Ast.Box (kind, tl) ->
411         let tl' = subst_children pos env tl in
412         Ast.Box (kind, List.concat tl')
413     | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
414   and subst_children pos env =
415     function
416     | [] -> []
417     | [ child ] ->
418         let pos' =
419           match pos with
420           | `Inner -> `Right
421           | `Left -> `Left
422 (*           | `None -> assert false *)
423           | `Right -> `Right
424         in
425         [ subst pos' env child ]
426     | hd :: tl ->
427         let pos' =
428           match pos with
429           | `Inner -> `Inner
430           | `Left -> `Inner
431 (*           | `None -> assert false *)
432           | `Right -> `Right
433         in
434         (subst pos env hd) :: subst_children pos' env tl
435   in
436     subst_singleton `Left env l1
437
438 let rec pp_ast1 term = 
439   let rec pp_value = function
440     | CicNotationEnv.NumValue _ as v -> v
441     | CicNotationEnv.StringValue _ as v -> v
442 (*     | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
443     | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
444     | CicNotationEnv.OptValue None as v -> v
445     | CicNotationEnv.OptValue (Some v) -> 
446         CicNotationEnv.OptValue (Some (pp_value v))
447     | CicNotationEnv.ListValue vl ->
448         CicNotationEnv.ListValue (List.map pp_value vl)
449   in
450   let ast_env_of_env env =
451     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
452   in
453 (* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
454   match term with
455   | Ast.AttributedTerm (attrs, term') ->
456       Ast.AttributedTerm (attrs, pp_ast1 term')
457   | _ ->
458       (match (get_compiled21 ()) term with
459       | None -> pp_ast0 term pp_ast1
460       | Some (env, ctors, pid) ->
461           let idrefs =
462             List.flatten (List.map CicNotationUtil.get_idrefs ctors)
463           in
464           let l1 =
465             try
466               Hashtbl.find !level1_patterns21 pid
467             with Not_found -> assert false
468           in
469           instantiate21 idrefs (ast_env_of_env env) l1)
470
471 let load_patterns21 t =
472   set_compiled21 (lazy (Content2presMatcher.Matcher21.compiler t))
473
474 let pp_ast ast =
475   debug_print (lazy "pp_ast <-");
476   let ast' = pp_ast1 ast in
477   debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
478   ast'
479
480 exception Pretty_printer_not_found
481
482 let fill_pos_info l1_pattern = l1_pattern
483 (*   let rec aux toplevel pos =
484     function
485     | Ast.Layout l ->
486         (match l 
487
488     | Ast.Magic m ->
489         Ast.Box (
490     | Ast.Variable _ as t -> add_pos_info pos t
491     | t -> t
492   in
493   aux true l1_pattern *)
494
495 let fresh_id =
496   fun () ->
497     incr counter;
498     !counter
499
500 let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
501   let id = fresh_id () in
502   let l1' = add_level_info precedence (fill_pos_info l1) in
503   let l2' = CicNotationUtil.strip_attributes l2 in
504   Hashtbl.add !level1_patterns21 id l1';
505   pattern21_matrix := (l2', id) :: !pattern21_matrix;
506   load_patterns21 !pattern21_matrix;
507   id
508
509 let remove_pretty_printer id =
510   (try
511     Hashtbl.remove !level1_patterns21 id;
512   with Not_found -> raise Pretty_printer_not_found);
513   pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
514   load_patterns21 !pattern21_matrix
515
516   (* presentation -> content *)
517
518 let unopt_names names env =
519   let rec aux acc = function
520     | (name, (ty, v)) :: tl when List.mem name names ->
521         (match ty, v with
522         | Env.OptType ty, Env.OptValue (Some v) ->
523             aux ((name, (ty, v)) :: acc) tl
524         | _ -> assert false)
525     | hd :: tl -> aux (hd :: acc) tl
526     | [] -> acc
527   in
528   aux [] env
529
530 let head_names names env =
531   let rec aux acc = function
532     | (name, (ty, v)) :: tl when List.mem name names ->
533         (match ty, v with
534         | Env.ListType ty, Env.ListValue (v :: _) ->
535             aux ((name, (ty, v)) :: acc) tl
536         | Env.TermType _, Env.TermValue _  ->
537             aux ((name, (ty, v)) :: acc) tl
538         | _ -> assert false)
539     | _ :: tl -> aux acc tl
540       (* base pattern may contain only meta names, thus we trash all others *)
541     | [] -> acc
542   in
543   aux [] env
544
545 let tail_names names env =
546   let rec aux acc = function
547     | (name, (ty, v)) :: tl when List.mem name names ->
548         (match ty, v with
549         | Env.ListType ty, Env.ListValue (_ :: vtl) ->
550             aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
551         | Env.TermType _, Env.TermValue _  ->
552             aux ((name, (ty, v)) :: acc) tl
553         | _ -> assert false)
554     | binding :: tl -> aux (binding :: acc) tl
555     | [] -> acc
556   in
557   aux [] env
558
559 let instantiate_level2 env term =
560 (*   prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *)
561   let fresh_env = ref [] in
562   let lookup_fresh_name n =
563     try
564       List.assoc n !fresh_env
565     with Not_found ->
566       let new_name = CicNotationUtil.fresh_name () in
567       fresh_env := (n, new_name) :: !fresh_env;
568       new_name
569   in
570   let rec aux env term =
571 (*    prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
572     match term with
573     | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
574     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
575     | Ast.Binder (binder, var, body) ->
576         Ast.Binder (binder, aux_capture_var env var, aux env body)
577     | Ast.Case (term, indty, outty_opt, patterns) ->
578         Ast.Case (aux env term, indty, aux_opt env outty_opt,
579           List.map (aux_branch env) patterns)
580     | Ast.LetIn (var, t1, t3) ->
581         Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
582     | Ast.LetRec (kind, definitions, body) ->
583         Ast.LetRec (kind, List.map (aux_definition env) definitions,
584           aux env body)
585     | Ast.Uri (name, None) -> Ast.Uri (name, None)
586     | Ast.Uri (name, Some substs) ->
587         Ast.Uri (name, Some (aux_substs env substs))
588     | Ast.Ident (name, Some substs) ->
589         Ast.Ident (name, Some (aux_substs env substs))
590     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
591
592     | Ast.Implicit
593     | Ast.Ident _
594     | Ast.Num _
595     | Ast.Sort _
596     | Ast.Symbol _
597     | Ast.UserInput -> term
598
599     | Ast.Magic magic -> aux_magic env magic
600     | Ast.Variable var -> aux_variable env var
601
602     | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
603
604     | _ -> assert false
605   and aux_opt env = function
606     | Some term -> Some (aux env term)
607     | None -> None
608   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
609   and aux_branch env (pattern, term) =
610     (aux_pattern env pattern, aux env term)
611   and aux_pattern env =
612    function
613       Ast.Pattern (head, hrefs, vars) ->
614        Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
615     | Ast.Wildcard -> Ast.Wildcard
616   and aux_definition env (params, var, term, i) =
617     (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
618   and aux_substs env substs =
619     List.map (fun (name, term) -> (name, aux env term)) substs
620   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
621   and aux_variable env = function
622     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
623     | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
624     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
625         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
626     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
627     | Ast.Ascription (term, name) -> assert false
628   and aux_magic env = function
629     | Ast.Default (some_pattern, none_pattern) ->
630         let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
631         let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
632         let opt_names =
633           List.filter
634             (fun name -> not (List.mem name none_pattern_names))
635             some_pattern_names
636         in
637         (match opt_names with
638         | [] -> assert false (* some pattern must contain at least 1 name *)
639         | (name :: _) as names ->
640             (match Env.lookup_value env name with
641             | Env.OptValue (Some _) ->
642                 (* assumption: if "name" above is bound to Some _, then all
643                  * names returned by "meta_names_of" are bound to Some _ as well
644                  *)
645                 aux (unopt_names names env) some_pattern
646             | Env.OptValue None -> aux env none_pattern
647             | _ ->
648                 prerr_endline (sprintf
649                   "lookup of %s in env %s did not return an optional value"
650                   name (CicNotationPp.pp_env env));
651                 assert false))
652     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
653         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
654         let meta_names =
655           List.filter ((<>) acc_name)
656             (CicNotationUtil.names_of_term rec_pattern)
657         in
658         (match meta_names with
659         | [] -> assert false (* as above *)
660         | (name :: _) as names ->
661             let rec instantiate_fold_left acc env' =
662               match Env.lookup_value env' name with
663               | Env.ListValue (_ :: _) ->
664                   instantiate_fold_left 
665                     (let acc_binding =
666                       acc_name, (Env.TermType 0, Env.TermValue acc)
667                      in
668                      aux (acc_binding :: head_names names env') rec_pattern)
669                     (tail_names names env')
670               | Env.ListValue [] -> acc
671               | _ -> assert false
672             in
673             instantiate_fold_left (aux env base_pattern) env)
674     | Ast.Fold (`Right, base_pattern, names, rec_pattern) ->
675         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
676         let meta_names =
677           List.filter ((<>) acc_name)
678             (CicNotationUtil.names_of_term rec_pattern)
679         in
680         (match meta_names with
681         | [] -> assert false (* as above *)
682         | (name :: _) as names ->
683             let rec instantiate_fold_right env' =
684               match Env.lookup_value env' name with
685               | Env.ListValue (_ :: _) ->
686                   let acc = instantiate_fold_right (tail_names names env') in
687                   let acc_binding =
688                     acc_name, (Env.TermType 0, Env.TermValue acc)
689                   in
690                   aux (acc_binding :: head_names names env') rec_pattern
691               | Env.ListValue [] -> aux env base_pattern
692               | _ -> assert false
693             in
694             instantiate_fold_right env)
695     | Ast.If (_, p_true, p_false) as t ->
696         aux env (CicNotationUtil.find_branch (Ast.Magic t))
697     | Ast.Fail -> assert false
698     | _ -> assert false
699   in
700   aux env term
701
702   (* initialization *)
703
704 let _ = load_patterns21 []
705
706
707