]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_disambiguation/cicDisambiguate.ml
Temporary (and partially broken) patch for Ferruccio: I duplicate
[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml
1 (*
2 Copyright (C) 1999-2006, HELM Team.
3
4 This file is part of HELM, an Hypertextual, Electronic
5 Library of Mathematics, developed at the Computer Science
6 Department, University of Bologna, Italy.
7
8 HELM is free software; you can redistribute it and/or
9 modify it under the terms of the GNU General Public License
10 as published by the Free Software Foundation; either version 2
11 of the License, or (at your option) any later version.
12
13 HELM is distributed in the hope that it will be useful,
14 but WITHOUT ANY WARRANTY; without even the implied warranty of
15 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16 GNU General Public License for more details.
17
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software
20 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21 02110-1301 USA.
22
23 For details, see the HELM web site: http://helm.cs.unibo.it/
24 *)
25
26 open Printf
27 module Ast = CicNotationPt
28
29 let debug = false
30 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
31
32 let rec string_context_of_context =
33  List.map
34   (function
35    | Cic.Name n -> Some n
36    | Cic.Anonymous -> Some "_")
37 ;;
38
39 let refine_term metasenv subst context uri ~use_coercions
40  term expty ugraph ~localization_tbl =
41 (*   if benchmark then incr actual_refinements; *)
42   assert (uri=None);
43   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
44   let saved_use_coercions = !CicRefine.insert_coercions in
45   try
46     CicRefine.insert_coercions := use_coercions;
47     let term = 
48       match expty with
49       | None -> term
50       | Some ty -> Cic.Cast(term,ty)
51     in
52     let term', _, metasenv',ugraph1 = 
53             CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
54     in
55     let term' = 
56       match expty, term' with
57       | None,_ -> term'
58       | Some _,Cic.Cast (term',_) -> term'
59       | _ -> assert false 
60     in
61      CicRefine.insert_coercions := saved_use_coercions;
62      (Disambiguate.Ok (term', metasenv',[],ugraph1))
63   with
64    exn ->
65     CicRefine.insert_coercions := saved_use_coercions;
66     let rec process_exn loc =
67      function
68         HExtlib.Localized (loc,exn) -> process_exn loc exn
69       | CicRefine.Uncertain msg ->
70           debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
71           Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
72       | CicRefine.RefineFailure msg ->
73           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
74             (CicPp.ppterm term) (Lazy.force msg)));
75           Disambiguate.Ko (lazy (loc,Lazy.force msg))
76      | exn -> raise exn
77     in
78      process_exn Stdpp.dummy_loc exn
79
80 let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
81  ~localization_tbl =
82    assert (context = []);
83    assert (metasenv = []);
84    assert (subst = []);
85    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
86    let saved_use_coercions = !CicRefine.insert_coercions in
87    try
88      CicRefine.insert_coercions := use_coercions;
89      let obj', metasenv,ugraph =
90        CicRefine.typecheck metasenv uri obj ~localization_tbl
91      in
92       CicRefine.insert_coercions := saved_use_coercions;
93       (Disambiguate.Ok (obj', metasenv,[],ugraph))
94    with
95      exn ->
96       CicRefine.insert_coercions := saved_use_coercions;
97       let rec process_exn loc =
98        function
99           HExtlib.Localized (loc,exn) -> process_exn loc exn
100         | CicRefine.Uncertain msg ->
101             debug_print (lazy ("UNCERTAIN!!! [" ^ 
102               (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
103             Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
104         | CicRefine.RefineFailure msg ->
105             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
106               (CicPp.ppobj obj) (Lazy.force msg))) ;
107             Disambiguate.Ko (lazy (loc,Lazy.force msg))
108        | exn -> raise exn
109       in
110        process_exn Stdpp.dummy_loc exn
111 ;;
112
113 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
114  ~is_path ast ~localization_tbl ~obj_context
115 =
116   (* create_dummy_ids shouldbe used only for interpretating patterns *)
117   assert (uri = None);
118   let rec aux ~localize loc context = function
119     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
120         let res = aux ~localize loc context term in
121          if localize then Cic.CicHash.add localization_tbl res loc;
122          res
123     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
124     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
125         let cic_args = List.map (aux ~localize loc context) args in
126         Disambiguate.resolve ~mk_choice ~env 
127           (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args)
128     | CicNotationPt.Appl terms ->
129        Cic.Appl (List.map (aux ~localize loc context) terms)
130     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
131         let cic_type = aux_option ~localize loc context (Some `Type) typ in
132         let cic_name = CicNotationUtil.cic_name_of_name var in
133         let cic_body = aux ~localize loc (cic_name :: context) body in
134         (match binder_kind with
135         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
136         | `Pi
137         | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
138         | `Exists ->
139             Disambiguate.resolve ~mk_choice ~env
140              (DisambiguateTypes.Symbol ("exists", 0))
141              (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ]))
142     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
143         let cic_term = aux ~localize loc context term in
144         let cic_outtype = aux_option ~localize loc context None outtype in
145         let do_branch ((head, _, args), term) =
146          let rec do_branch' context = function
147            | [] -> aux ~localize loc context term
148            | (name, typ) :: tl ->
149                let cic_name = CicNotationUtil.cic_name_of_name name in
150                let cic_body = do_branch' (cic_name :: context) tl in
151                let typ =
152                  match typ with
153                  | None -> Cic.Implicit (Some `Type)
154                  | Some typ -> aux ~localize loc context typ
155                in
156                Cic.Lambda (cic_name, typ, cic_body)
157          in
158           do_branch' context args
159         in
160         let indtype_uri, indtype_no =
161           if create_dummy_ids then
162             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
163           else
164           match indty_ident with
165           | Some (indty_ident, _) ->
166              (match 
167                Disambiguate.resolve ~mk_choice ~env 
168                 (DisambiguateTypes.Id indty_ident) (`Args [])
169               with
170               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
171               | Cic.Implicit _ ->
172                  raise (Disambiguate.Try_again 
173                    (lazy "The type of the term to be matched
174                   is still unknown"))
175               | _ ->
176                 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
177           | None ->
178               let rec fst_constructor =
179                 function
180                    (Ast.Pattern (head, _, _), _) :: _ -> head
181                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
182                  | [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")))
183               in
184               (match Disambiguate.resolve ~mk_choice ~env
185                 (DisambiguateTypes.Id (fst_constructor branches))
186                 (`Args []) with
187               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
188                   (indtype_uri, indtype_no)
189               | Cic.Implicit _ ->
190                  raise (Disambiguate.Try_again (lazy "The type of the term to be matched
191                   is still unknown"))
192               | _ ->
193                 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
194         in
195         let branches =
196          if create_dummy_ids then
197           List.map
198            (function
199                Ast.Wildcard,term -> ("wildcard",None,[]), term
200              | Ast.Pattern _,_ ->
201                 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\"")))
202            ) branches
203          else
204          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
205             Cic.InductiveDefinition (il,_,leftsno,_) ->
206              let _,_,_,cl =
207               try
208                List.nth il indtype_no
209               with _ -> assert false
210              in
211               let rec count_prod t =
212                 match CicReduction.whd [] t with
213                     Cic.Prod (_, _, t) -> 1 + (count_prod t)
214                   | _ -> 0 
215               in 
216               let rec sort branches cl =
217                match cl with
218                   [] ->
219                    let rec analyze unused unrecognized useless =
220                     function
221                        [] ->
222                         if unrecognized != [] then
223                          raise (DisambiguateTypes.Invalid_choice
224                           (lazy (loc,
225                             ("Unrecognized constructors: " ^
226                              String.concat " " unrecognized))))
227                         else if useless > 0 then
228                          raise (DisambiguateTypes.Invalid_choice
229                            (lazy (loc,
230                             ("The last " ^ string_of_int useless ^
231                              "case" ^ if useless > 1 then "s are" else " is" ^
232                              " unused"))))
233                         else
234                          []
235                      | (Ast.Wildcard,_)::tl when not unused ->
236                          analyze true unrecognized useless tl
237                      | (Ast.Pattern (head,_,_),_)::tl when not unused ->
238                          analyze unused (head::unrecognized) useless tl
239                      | _::tl -> analyze unused unrecognized (useless + 1) tl
240                    in
241                     analyze false [] 0 branches
242                 | (name,ty)::cltl ->
243                    let rec find_and_remove =
244                     function
245                        [] ->
246                         raise
247                          (DisambiguateTypes.Invalid_choice
248                           (lazy (loc, ("Missing case: " ^ name))))
249                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
250                          branch, branches
251                      | (Ast.Pattern (name',_,_),_) as branch :: tl
252                         when name = name' ->
253                          branch,tl
254                      | branch::tl ->
255                         let found,rest = find_and_remove tl in
256                          found, branch::rest
257                    in
258                     let branch,tl = find_and_remove branches in
259                     match branch with
260                        Ast.Pattern (name,y,args),term ->
261                         if List.length args = count_prod ty - leftsno then
262                          ((name,y,args),term)::sort tl cltl
263                         else
264                          raise
265                           (DisambiguateTypes.Invalid_choice
266                             (lazy (loc,"Wrong number of arguments for " ^
267                             name)))
268                      | Ast.Wildcard,term ->
269                         let rec mk_lambdas =
270                          function
271                             0 -> term
272                           | n ->
273                              CicNotationPt.Binder
274                               (`Lambda, (CicNotationPt.Ident ("_", None), None),
275                                 mk_lambdas (n - 1))
276                         in
277                          (("wildcard",None,[]),
278                           mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
279               in
280                sort branches cl
281           | _ -> assert false
282         in
283         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
284           (List.map do_branch branches))
285     | CicNotationPt.Cast (t1, t2) ->
286         let cic_t1 = aux ~localize loc context t1 in
287         let cic_t2 = aux ~localize loc context t2 in
288         Cic.Cast (cic_t1, cic_t2)
289     | CicNotationPt.LetIn ((name, typ), def, body) ->
290         let cic_def = aux ~localize loc context def in
291         let cic_name = CicNotationUtil.cic_name_of_name name in
292         let cic_typ =
293           match typ with
294           | None -> Cic.Implicit (Some `Type)
295           | Some t -> aux ~localize loc context t
296         in
297         let cic_body = aux ~localize loc (cic_name :: context) body in
298         Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
299     | CicNotationPt.LetRec (kind, defs, body) ->
300         let context' =
301           List.fold_left
302             (fun acc (_, (name, _), _, _) ->
303               CicNotationUtil.cic_name_of_name name :: acc)
304             context defs
305         in
306         let cic_body =
307          let unlocalized_body = aux ~localize:false loc context' body in
308          match unlocalized_body with
309             Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
310           | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
311              (try
312                let l' =
313                 List.map
314                  (function t ->
315                    let t',subst,metasenv =
316                     CicMetaSubst.delift_rels [] [] (List.length defs) t
317                    in
318                     assert (subst=[]);
319                     assert (metasenv=[]);
320                     t') l
321                in
322                 (* We can avoid the LetIn. But maybe we need to recompute l'
323                    so that it is localized *)
324                 if localize then
325                  match body with
326                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
327                      (* since we avoid the letin, the context has no
328                       * recfuns in it *)
329                      let l' = List.map (aux ~localize loc context) l in
330                       `AvoidLetIn (n,l')
331                   | _ -> assert false
332                 else
333                  `AvoidLetIn (n,l')
334               with
335                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
336                 if localize then
337                  `AddLetIn (aux ~localize loc context' body)
338                 else
339                  `AddLetIn unlocalized_body)
340           | _ ->
341              if localize then
342               `AddLetIn (aux ~localize loc context' body)
343              else
344               `AddLetIn unlocalized_body
345         in
346         let inductiveFuns =
347           List.map
348             (fun (params, (name, typ), body, decr_idx) ->
349               let add_binders kind t =
350                List.fold_right
351                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
352               in
353               let cic_body =
354                aux ~localize loc context' (add_binders `Lambda body) in
355               let typ =
356                match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
357               let cic_type =
358                aux_option ~localize loc context (Some `Type)
359                 (Some (add_binders `Pi typ)) in
360               let name =
361                 match CicNotationUtil.cic_name_of_name name with
362                 | Cic.Anonymous ->
363                     CicNotationPt.fail loc
364                       "Recursive functions cannot be anonymous"
365                 | Cic.Name name -> name
366               in
367               (name, decr_idx, cic_type, cic_body))
368             defs
369         in
370         let fix_or_cofix n =
371          match kind with
372             `Inductive -> Cic.Fix (n,inductiveFuns)
373           | `CoInductive ->
374               let coinductiveFuns =
375                 List.map
376                  (fun (name, _, typ, body) -> name, typ, body)
377                  inductiveFuns
378               in
379                Cic.CoFix (n,coinductiveFuns)
380         in
381          let counter = ref ~-1 in
382          let build_term funs (var,_,ty,_) t =
383           incr counter;
384           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
385          in
386           (match cic_body with
387               `AvoidLetInNoAppl n ->
388                 let n' = List.length inductiveFuns - n in
389                  fix_or_cofix n'
390             | `AvoidLetIn (n,l) ->
391                 let n' = List.length inductiveFuns - n in
392                  Cic.Appl (fix_or_cofix n'::l)
393             | `AddLetIn cic_body ->         
394                 List.fold_right (build_term inductiveFuns) inductiveFuns
395                  cic_body)
396     | CicNotationPt.Ident _
397     | CicNotationPt.Uri _
398     | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
399     | CicNotationPt.NRef _ -> assert false
400     | CicNotationPt.Ident (name,subst)
401     | CicNotationPt.Uri (name, subst) as ast ->
402         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
403         (try
404           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
405           let index =
406            Disambiguate.find_in_context name (string_context_of_context context)
407           in
408           if subst <> None then
409             CicNotationPt.fail loc "Explicit substitutions not allowed here";
410           Cic.Rel index
411         with Not_found ->
412           let cic =
413             if is_uri ast then  (* we have the URI, build the term out of it *)
414               try
415                 CicUtil.term_of_uri (UriManager.uri_of_string name)
416               with UriManager.IllFormedUri _ ->
417                 CicNotationPt.fail loc "Ill formed URI"
418             else
419              try
420               List.assoc name obj_context
421              with
422               Not_found ->
423                Disambiguate.resolve ~mk_choice ~env
424                 (DisambiguateTypes.Id name) (`Args [])
425           in
426           let mk_subst uris =
427             let ids_to_uris =
428               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
429             in
430             (match subst with
431             | Some subst ->
432                 List.map
433                   (fun (s, term) ->
434                     (try
435                       List.assoc s ids_to_uris, aux ~localize loc context term
436                      with Not_found ->
437                        raise (DisambiguateTypes.Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
438                   subst
439             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
440           in
441           (try 
442             match cic with
443             | Cic.Const (uri, []) ->
444                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
445                 let uris = CicUtil.params_of_obj o in
446                 Cic.Const (uri, mk_subst uris)
447             | Cic.Var (uri, []) ->
448                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
449                 let uris = CicUtil.params_of_obj o in
450                 Cic.Var (uri, mk_subst uris)
451             | Cic.MutInd (uri, i, []) ->
452                (try
453                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
454                  let uris = CicUtil.params_of_obj o in
455                  Cic.MutInd (uri, i, mk_subst uris)
456                 with
457                  CicEnvironment.Object_not_found _ ->
458                   (* if we are here it is probably the case that during the
459                      definition of a mutual inductive type we have met an
460                      occurrence of the type in one of its constructors.
461                      However, the inductive type is not yet in the environment
462                   *)
463                   (*here the explicit_named_substituion is assumed to be of length 0 *)
464                   Cic.MutInd (uri,i,[]))
465             | Cic.MutConstruct (uri, i, j, []) ->
466                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
467                 let uris = CicUtil.params_of_obj o in
468                 Cic.MutConstruct (uri, i, j, mk_subst uris)
469             | Cic.Meta _ | Cic.Implicit _ as t ->
470 (*
471                 debug_print (lazy (sprintf
472                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
473                   (CicPp.ppterm t)
474                   (String.concat "; "
475                     (List.map
476                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
477                       subst))));
478 *)
479                 t
480             | _ ->
481               raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?")))
482            with 
483              CicEnvironment.CircularDependency _ -> 
484                raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
485     | CicNotationPt.Implicit -> Cic.Implicit None
486     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
487     | CicNotationPt.Num (num, i) ->
488        Disambiguate.resolve ~mk_choice ~env
489         (DisambiguateTypes.Num i) (`Num_arg num)
490     | CicNotationPt.Meta (index, subst) ->
491         let cic_subst =
492           List.map
493             (function
494                 None -> None
495               | Some term -> Some (aux ~localize loc context term))
496             subst
497         in
498         Cic.Meta (index, cic_subst)
499     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
500     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
501     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
502     | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
503     | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
504     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
505     | CicNotationPt.Symbol (symbol, instance) ->
506         Disambiguate.resolve ~mk_choice ~env
507          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
508     | CicNotationPt.Variable _
509     | CicNotationPt.Magic _
510     | CicNotationPt.Layout _
511     | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
512   and aux_option ~localize loc context annotation = function
513     | None -> Cic.Implicit annotation
514     | Some term -> aux ~localize loc context term
515   in
516    aux ~localize:true HExtlib.dummy_floc context ast
517
518 let interpretate_path ~context path =
519  let localization_tbl = Cic.CicHash.create 23 in
520   (* here we are throwing away useful localization informations!!! *)
521   fst (
522    interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true 
523     ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
524     path ~localization_tbl ~obj_context:[], localization_tbl)
525
526 let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
527  ~localization_tbl
528 =
529  assert (context = []);
530  assert (is_path = false);
531  let interpretate_term ?(obj_context=[]) =
532   interpretate_term ~mk_choice ~localization_tbl ~obj_context in
533  match obj with
534   | CicNotationPt.Inductive (params,tyl) ->
535      let uri = match uri with Some uri -> uri | None -> assert false in
536      let context,params =
537       let context,res =
538        List.fold_left
539         (fun (context,res) (name,t) ->
540           let t =
541            match t with
542               None -> CicNotationPt.Implicit
543             | Some t -> t in
544           let name = CicNotationUtil.cic_name_of_name name in
545            name::context,(name, interpretate_term context env None false t)::res
546         ) ([],[]) params
547       in
548        context,List.rev res in
549      let add_params =
550       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
551      let obj_context =
552       snd (
553        List.fold_left
554         (*here the explicit_named_substituion is assumed to be of length 0 *)
555         (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
556         (0,[]) tyl) in
557      let tyl =
558       List.map
559        (fun (name,b,ty,cl) ->
560          let ty' = add_params (interpretate_term context env None false ty) in
561          let cl' =
562           List.map
563            (fun (name,ty) ->
564              let ty' =
565               add_params
566                (interpretate_term ~obj_context ~context ~env ~uri:None
567                  ~is_path:false ty)
568              in
569               name,ty'
570            ) cl
571          in
572           name,b,ty',cl'
573        ) tyl
574      in
575       Cic.InductiveDefinition (tyl,[],List.length params,[])
576   | CicNotationPt.Record (params,name,ty,fields) ->
577      let uri = match uri with Some uri -> uri | None -> assert false in
578      let context,params =
579       let context,res =
580        List.fold_left
581         (fun (context,res) (name,t) ->
582           let t =
583            match t with
584               None -> CicNotationPt.Implicit
585             | Some t -> t in
586           let name = CicNotationUtil.cic_name_of_name name in
587            name::context,(name, interpretate_term context env None false t)::res
588         ) ([],[]) params
589       in
590        context,List.rev res in
591      let add_params =
592       List.fold_right
593        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
594      let ty' = add_params (interpretate_term context env None false ty) in
595      let fields' =
596       snd (
597        List.fold_left
598         (fun (context,res) (name,ty,_coercion,arity) ->
599           let context' = Cic.Name name :: context in
600            context',(name,interpretate_term context env None false ty)::res
601         ) (context,[]) fields) in
602      let concl =
603       (*here the explicit_named_substituion is assumed to be of length 0 *)
604       let mutind = Cic.MutInd (uri,0,[]) in
605       if params = [] then mutind
606       else
607        Cic.Appl
608         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
609      let con =
610       List.fold_left
611        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
612        concl fields' in
613      let con' = add_params con in
614      let tyl = [name,true,ty',["mk_" ^ name,con']] in
615      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
616       Cic.InductiveDefinition
617        (tyl,[],List.length params,[`Class (`Record field_names)])
618   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
619      let attrs = [`Flavour flavour] in
620      let ty' = interpretate_term [] env None false ty in
621      (match bo,flavour with
622         None,`Axiom ->
623          Cic.Constant (name,None,ty',[],attrs)
624       | Some bo,`Axiom -> assert false
625       | None,_ ->
626          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
627       | Some bo,_ ->
628          let bo' = Some (interpretate_term [] env None false bo) in
629           Cic.Constant (name,bo',ty',[],attrs))
630 ;;
631
632 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
633  ~is_path ast ~localization_tbl
634 =
635   let context =
636    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
637   in
638    interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
639     ast ~localization_tbl ~obj_context:[]
640 ;;
641
642 let string_context_of_context =
643   List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
644   (Cic.Anonymous,_) -> Some "_");;
645
646 let disambiguate_term ~context ~metasenv ~subst ~expty 
647   ?(initial_ugraph = CicUniv.oblivion_ugraph)
648   ~mk_implicit ~description_of_alias ~mk_choice
649   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
650 =
651   let mk_localization_tbl x = Cic.CicHash.create x in
652    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
653     ~initial_ugraph ~aliases ~string_context_of_context
654     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
655     ~uri:None ~pp_thing:CicNotationPp.pp_term
656     ~domain_of_thing:Disambiguate.domain_of_term
657     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
658     ~refine_thing:refine_term (text,prefix_len,term)
659     ~mk_localization_tbl
660     ~expty
661     ~freshen_thing:CicNotationUtil.freshen_term
662     ~passes:(MultiPassDisambiguator.passes ())
663
664 let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
665  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
666 =
667   let mk_localization_tbl x = Cic.CicHash.create x in
668   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] 
669     ~aliases ~universe ~uri ~string_context_of_context
670     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
671     ~domain_of_thing:Disambiguate.domain_of_obj
672     ~lookup_in_library ~mk_implicit ~description_of_alias
673     ~initial_ugraph:CicUniv.empty_ugraph
674     ~interpretate_thing:(interpretate_obj ~mk_choice)
675     ~refine_thing:refine_obj
676     ~mk_localization_tbl
677     ~expty:None
678     ~passes:(MultiPassDisambiguator.passes ())
679     ~freshen_thing:CicNotationUtil.freshen_obj
680     (text,prefix_len,obj)