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