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 (`CProp u) -> Cic.Sort (Cic.CProp u)
 488     | CicNotationPt.Symbol (symbol, instance) ->
 489         Disambiguate.resolve ~mk_choice ~env
 490          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
 491     | _ -> assert false (* god bless Bologna *)
 492   and aux_option ~localize loc context annotation = function
 493     | None -> Cic.Implicit annotation
 494     | Some term -> aux ~localize loc context term
 495   in
 496    aux ~localize:true HExtlib.dummy_floc context ast
 497
 498 let interpretate_path ~context path =
 499  let localization_tbl = Cic.CicHash.create 23 in
 500   (* here we are throwing away useful localization informations!!! *)
 501   fst (
 502    interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
 503     ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
 504     path ~localization_tbl ~obj_context:[], localization_tbl)
 505
 506 let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
 507  ~localization_tbl
 508 =
 509  assert (context = []);
 510  assert (is_path = false);
 511  let interpretate_term ?(obj_context=[]) =
 512   interpretate_term ~mk_choice ~localization_tbl ~obj_context in
 513  match obj with
 514   | CicNotationPt.Inductive (params,tyl) ->
 515      let uri = match uri with Some uri -> uri | None -> assert false in
 516      let context,params =
 517       let context,res =
 518        List.fold_left
 519         (fun (context,res) (name,t) ->
 520           let t =
 521            match t with
 522               None -> CicNotationPt.Implicit
 523             | Some t -> t in
 524           let name = CicNotationUtil.cic_name_of_name name in
 525            name::context,(name, interpretate_term context env None false t)::res
 526         ) ([],[]) params
 527       in
 528        context,List.rev res in
 529      let add_params =
 530       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 531      let obj_context =
 532       snd (
 533        List.fold_left
 534         (*here the explicit_named_substituion is assumed to be of length 0 *)
 535         (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
 536         (0,[]) tyl) in
 537      let tyl =
 538       List.map
 539        (fun (name,b,ty,cl) ->
 540          let ty' = add_params (interpretate_term context env None false ty) in
 541          let cl' =
 542           List.map
 543            (fun (name,ty) ->
 544              let ty' =
 545               add_params
 546                (interpretate_term ~obj_context ~context ~env ~uri:None
 547                  ~is_path:false ty)
 548              in
 549               name,ty'
 550            ) cl
 551          in
 552           name,b,ty',cl'
 553        ) tyl
 554      in
 555       Cic.InductiveDefinition (tyl,[],List.length params,[])
 556   | CicNotationPt.Record (params,name,ty,fields) ->
 557      let uri = match uri with Some uri -> uri | None -> assert false in
 558      let context,params =
 559       let context,res =
 560        List.fold_left
 561         (fun (context,res) (name,t) ->
 562           let t =
 563            match t with
 564               None -> CicNotationPt.Implicit
 565             | Some t -> t in
 566           let name = CicNotationUtil.cic_name_of_name name in
 567            name::context,(name, interpretate_term context env None false t)::res
 568         ) ([],[]) params
 569       in
 570        context,List.rev res in
 571      let add_params =
 572       List.fold_right
 573        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 574      let ty' = add_params (interpretate_term context env None false ty) in
 575      let fields' =
 576       snd (
 577        List.fold_left
 578         (fun (context,res) (name,ty,_coercion,arity) ->
 579           let context' = Cic.Name name :: context in
 580            context',(name,interpretate_term context env None false ty)::res
 581         ) (context,[]) fields) in
 582      let concl =
 583       (*here the explicit_named_substituion is assumed to be of length 0 *)
 584       let mutind = Cic.MutInd (uri,0,[]) in
 585       if params = [] then mutind
 586       else
 587        Cic.Appl
 588         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
 589      let con =
 590       List.fold_left
 591        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
 592        concl fields' in
 593      let con' = add_params con in
 594      let tyl = [name,true,ty',["mk_" ^ name,con']] in
 595      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
 596       Cic.InductiveDefinition
 597        (tyl,[],List.length params,[`Class (`Record field_names)])
 598   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
 599      let attrs = [`Flavour flavour] in
 600      let ty' = interpretate_term [] env None false ty in
 601      (match bo,flavour with
 602         None,`Axiom ->
 603          Cic.Constant (name,None,ty',[],attrs)
 604       | Some bo,`Axiom -> assert false
 605       | None,_ ->
 606          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
 607       | Some bo,_ ->
 608          let bo' = Some (interpretate_term [] env None false bo) in
 609           Cic.Constant (name,bo',ty',[],attrs))
 610 ;;
 611
 612 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
 613  ~is_path ast ~localization_tbl
 614 =
 615   let context =
 616    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
 617   in
 618    interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
 619     ast ~localization_tbl ~obj_context:[]
 620 ;;
 621
 622 let string_context_of_context =
 623   List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
 624   (Cic.Anonymous,_) -> Some "_");;
 625
 626 let disambiguate_term ~context ~metasenv ~subst ?goal
 627   ?(initial_ugraph = CicUniv.oblivion_ugraph)
 628   ~mk_implicit ~description_of_alias ~mk_choice
 629   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
 630 =
 631   let hint = match goal with
 632     | None -> (fun _ x -> x), fun k -> k
 633     | Some i ->
 634         (fun metasenv t ->
 635           let _,c,ty = CicUtil.lookup_meta i metasenv in
 636           assert(c=context);
 637           Cic.Cast(t,ty)),
 638         function
 639         | Disambiguate.Ok (t,m,s,ug) ->
 640             (match t with
 641             | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
 642             | _ -> assert false)
 643         | k -> k
 644   in
 645   let localization_tbl = Cic.CicHash.create 503 in
 646    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
 647     ~initial_ugraph ~aliases ~string_context_of_context
 648     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
 649     ~uri:None ~pp_thing:CicNotationPp.pp_term
 650     ~domain_of_thing:Disambiguate.domain_of_term
 651     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
 652     ~refine_thing:refine_term (text,prefix_len,term)
 653     ~localization_tbl
 654     ~hint
 655     ~freshen_thing:CicNotationUtil.freshen_term
 656     ~passes:(MultiPassDisambiguator.passes ())
 657
 658 let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
 659  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 660 =
 661   let hint = (fun _ x -> x), fun k -> k in
 662   let localization_tbl = Cic.CicHash.create 503 in
 663   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
 664     ~aliases ~universe ~uri ~string_context_of_context
 665     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
 666     ~domain_of_thing:Disambiguate.domain_of_obj
 667     ~lookup_in_library ~mk_implicit ~description_of_alias
 668     ~initial_ugraph:CicUniv.empty_ugraph
 669     ~interpretate_thing:(interpretate_obj ~mk_choice)
 670     ~refine_thing:refine_obj
 671     ~localization_tbl
 672     ~hint
 673     ~passes:(MultiPassDisambiguator.passes ())
 674     ~freshen_thing:CicNotationUtil.freshen_obj
 675     (text,prefix_len,obj)