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)