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