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