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