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