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
 357                   Some typ -> typ
 358                 | None-> CicNotationPt.Implicit `JustOne in
 359               let cic_type =
 360                aux_option ~localize loc context (Some `Type)
 361                 (Some (add_binders `Pi typ)) in
 362               let name =
 363                 match CicNotationUtil.cic_name_of_name name with
 364                 | Cic.Anonymous ->
 365                     CicNotationPt.fail loc
 366                       "Recursive functions cannot be anonymous"
 367                 | Cic.Name name -> name
 368               in
 369               (name, decr_idx, cic_type, cic_body))
 370             defs
 371         in
 372         let fix_or_cofix n =
 373          match kind with
 374             `Inductive -> Cic.Fix (n,inductiveFuns)
 375           | `CoInductive ->
 376               let coinductiveFuns =
 377                 List.map
 378                  (fun (name, _, typ, body) -> name, typ, body)
 379                  inductiveFuns
 380               in
 381                Cic.CoFix (n,coinductiveFuns)
 382         in
 383          let counter = ref ~-1 in
 384          let build_term funs (var,_,ty,_) t =
 385           incr counter;
 386           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
 387          in
 388           (match cic_body with
 389               `AvoidLetInNoAppl n ->
 390                 let n' = List.length inductiveFuns - n in
 391                  fix_or_cofix n'
 392             | `AvoidLetIn (n,l) ->
 393                 let n' = List.length inductiveFuns - n in
 394                  Cic.Appl (fix_or_cofix n'::l)
 395             | `AddLetIn cic_body ->
 396                 List.fold_right (build_term inductiveFuns) inductiveFuns
 397                  cic_body)
 398     | CicNotationPt.Ident _
 399     | CicNotationPt.Uri _
 400     | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
 401     | CicNotationPt.NCic _ -> assert false
 402     | CicNotationPt.NRef _ -> assert false
 403     | CicNotationPt.Ident (name,subst)
 404     | CicNotationPt.Uri (name, subst) as ast ->
 405         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
 406         (try
 407           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 408           let index =
 409            Disambiguate.find_in_context name (string_context_of_context context)
 410           in
 411           if subst <> None then
 412             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 413           Cic.Rel index
 414         with Not_found ->
 415           let cic =
 416             if is_uri ast then  (* we have the URI, build the term out of it *)
 417               try
 418                 CicUtil.term_of_uri (UriManager.uri_of_string name)
 419               with UriManager.IllFormedUri _ ->
 420                 CicNotationPt.fail loc "Ill formed URI"
 421             else
 422              try
 423               List.assoc name obj_context
 424              with
 425               Not_found ->
 426                Disambiguate.resolve ~mk_choice ~env
 427                 (DisambiguateTypes.Id name) (`Args [])
 428           in
 429           let mk_subst uris =
 430             let ids_to_uris =
 431               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 432             in
 433             (match subst with
 434             | Some subst ->
 435                 List.map
 436                   (fun (s, term) ->
 437                     (try
 438                       List.assoc s ids_to_uris, aux ~localize loc context term
 439                      with Not_found ->
 440                        raise (DisambiguateTypes.Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
 441                   subst
 442             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
 443           in
 444           (try
 445             match cic with
 446             | Cic.Const (uri, []) ->
 447                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 448                 let uris = CicUtil.params_of_obj o in
 449                 Cic.Const (uri, mk_subst uris)
 450             | Cic.Var (uri, []) ->
 451                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 452                 let uris = CicUtil.params_of_obj o in
 453                 Cic.Var (uri, mk_subst uris)
 454             | Cic.MutInd (uri, i, []) ->
 455                (try
 456                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 457                  let uris = CicUtil.params_of_obj o in
 458                  Cic.MutInd (uri, i, mk_subst uris)
 459                 with
 460                  CicEnvironment.Object_not_found _ ->
 461                   (* if we are here it is probably the case that during the
 462                      definition of a mutual inductive type we have met an
 463                      occurrence of the type in one of its constructors.
 464                      However, the inductive type is not yet in the environment
 465                   *)
 466                   (*here the explicit_named_substituion is assumed to be of length 0 *)
 467                   Cic.MutInd (uri,i,[]))
 468             | Cic.MutConstruct (uri, i, j, []) ->
 469                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 470                 let uris = CicUtil.params_of_obj o in
 471                 Cic.MutConstruct (uri, i, j, mk_subst uris)
 472             | Cic.Meta _ | Cic.Implicit _ as t ->
 473 (*
 474                 debug_print (lazy (sprintf
 475                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 476                   (CicPp.ppterm t)
 477                   (String.concat "; "
 478                     (List.map
 479                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
 480                       subst))));
 481 *)
 482                 t
 483             | _ ->
 484               raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?")))
 485            with
 486              CicEnvironment.CircularDependency _ ->
 487                raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
 488     | CicNotationPt.Implicit `Vector -> assert false
 489     | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
 490     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
 491     | CicNotationPt.Num (num, i) ->
 492        Disambiguate.resolve ~mk_choice ~env
 493         (DisambiguateTypes.Num i) (`Num_arg num)
 494     | CicNotationPt.Meta (index, subst) ->
 495         let cic_subst =
 496           List.map
 497             (function
 498                 None -> None
 499               | Some term -> Some (aux ~localize loc context term))
 500             subst
 501         in
 502         Cic.Meta (index, cic_subst)
 503     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
 504     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
 505     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
 506     | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
 507     | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
 508     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
 509     | CicNotationPt.Symbol (symbol, instance) ->
 510         Disambiguate.resolve ~mk_choice ~env
 511          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
 512     | CicNotationPt.Variable _
 513     | CicNotationPt.Magic _
 514     | CicNotationPt.Layout _
 515     | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
 516   and aux_option ~localize loc context annotation = function
 517     | None -> Cic.Implicit annotation
 518     | Some term -> aux ~localize loc context term
 519   in
 520    aux ~localize:true HExtlib.dummy_floc context ast
 521
 522 let interpretate_path ~context path =
 523  let localization_tbl = Cic.CicHash.create 23 in
 524   (* here we are throwing away useful localization informations!!! *)
 525   fst (
 526    interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
 527     ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
 528     path ~localization_tbl ~obj_context:[], localization_tbl)
 529
 530 let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
 531  ~localization_tbl
 532 =
 533  assert (context = []);
 534  assert (is_path = false);
 535  let interpretate_term ?(obj_context=[]) =
 536   interpretate_term ~mk_choice ~localization_tbl ~obj_context in
 537  match obj with
 538   | CicNotationPt.Inductive (params,tyl) ->
 539      let uri = match uri with Some uri -> uri | None -> assert false in
 540      let context,params =
 541       let context,res =
 542        List.fold_left
 543         (fun (context,res) (name,t) ->
 544           let t =
 545            match t with
 546               None -> CicNotationPt.Implicit `JustOne
 547             | Some t -> t in
 548           let name = CicNotationUtil.cic_name_of_name name in
 549            name::context,(name, interpretate_term context env None false t)::res
 550         ) ([],[]) params
 551       in
 552        context,List.rev res in
 553      let add_params =
 554       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 555      let obj_context =
 556       snd (
 557        List.fold_left
 558         (*here the explicit_named_substituion is assumed to be of length 0 *)
 559         (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
 560         (0,[]) tyl) in
 561      let tyl =
 562       List.map
 563        (fun (name,b,ty,cl) ->
 564          let ty' = add_params (interpretate_term context env None false ty) in
 565          let cl' =
 566           List.map
 567            (fun (name,ty) ->
 568              let ty' =
 569               add_params
 570                (interpretate_term ~obj_context ~context ~env ~uri:None
 571                  ~is_path:false ty)
 572              in
 573               name,ty'
 574            ) cl
 575          in
 576           name,b,ty',cl'
 577        ) tyl
 578      in
 579       Cic.InductiveDefinition (tyl,[],List.length params,[])
 580   | CicNotationPt.Record (params,name,ty,fields) ->
 581      let uri = match uri with Some uri -> uri | None -> assert false in
 582      let context,params =
 583       let context,res =
 584        List.fold_left
 585         (fun (context,res) (name,t) ->
 586           let t =
 587            match t with
 588               None -> CicNotationPt.Implicit `JustOne
 589             | Some t -> t in
 590           let name = CicNotationUtil.cic_name_of_name name in
 591            name::context,(name, interpretate_term context env None false t)::res
 592         ) ([],[]) params
 593       in
 594        context,List.rev res in
 595      let add_params =
 596       List.fold_right
 597        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 598      let ty' = add_params (interpretate_term context env None false ty) in
 599      let fields' =
 600       snd (
 601        List.fold_left
 602         (fun (context,res) (name,ty,_coercion,arity) ->
 603           let context' = Cic.Name name :: context in
 604            context',(name,interpretate_term context env None false ty)::res
 605         ) (context,[]) fields) in
 606      let concl =
 607       (*here the explicit_named_substituion is assumed to be of length 0 *)
 608       let mutind = Cic.MutInd (uri,0,[]) in
 609       if params = [] then mutind
 610       else
 611        Cic.Appl
 612         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
 613      let con =
 614       List.fold_left
 615        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
 616        concl fields' in
 617      let con' = add_params con in
 618      let tyl = [name,true,ty',["mk_" ^ name,con']] in
 619      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
 620       Cic.InductiveDefinition
 621        (tyl,[],List.length params,[`Class (`Record field_names)])
 622   | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
 623      let attrs = [`Flavour flavour] in
 624      let ty' = interpretate_term [] env None false ty in
 625      (match bo,flavour with
 626         None,`Axiom ->
 627          Cic.Constant (name,None,ty',[],attrs)
 628       | Some bo,`Axiom -> assert false
 629       | None,_ ->
 630          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
 631       | Some bo,_ ->
 632          let bo' = Some (interpretate_term [] env None false bo) in
 633           Cic.Constant (name,bo',ty',[],attrs))
 634 ;;
 635
 636 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
 637  ~is_path ast ~localization_tbl
 638 =
 639   let context =
 640    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
 641   in
 642    interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
 643     ast ~localization_tbl ~obj_context:[]
 644 ;;
 645
 646 let string_context_of_context =
 647   List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
 648   (Cic.Anonymous,_) -> Some "_");;
 649
 650 let disambiguate_term ~context ~metasenv ~subst ~expty
 651   ?(initial_ugraph = CicUniv.oblivion_ugraph)
 652   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
 653   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
 654 =
 655   let mk_localization_tbl x = Cic.CicHash.create x in
 656    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
 657     ~initial_ugraph ~aliases ~string_context_of_context
 658     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
 659     ~fix_instance
 660     ~uri:None ~pp_thing:CicNotationPp.pp_term
 661     ~domain_of_thing:Disambiguate.domain_of_term
 662     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
 663     ~refine_thing:refine_term (text,prefix_len,term)
 664     ~mk_localization_tbl
 665     ~expty
 666     ~freshen_thing:CicNotationUtil.freshen_term
 667     ~passes:(MultiPassDisambiguator.passes ())
 668
 669 let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
 670  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 671 =
 672   let mk_localization_tbl x = Cic.CicHash.create x in
 673   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
 674     ~aliases ~universe ~uri ~string_context_of_context
 675     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
 676     ~domain_of_thing:Disambiguate.domain_of_obj
 677     ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
 678     ~initial_ugraph:CicUniv.empty_ugraph
 679     ~interpretate_thing:(interpretate_obj ~mk_choice)
 680     ~refine_thing:refine_obj
 681     ~mk_localization_tbl
 682     ~expty:None
 683     ~passes:(MultiPassDisambiguator.passes ())
 684     ~freshen_thing:CicNotationUtil.freshen_obj
 685     (text,prefix_len,obj)