helm/software/components/ng_disambiguation/nDisambiguate.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id: disambiguate.ml 9178 2008-11-12 12:09:52Z tassi $ *)
  27
  28 open Printf
  29
  30 open DisambiguateTypes
  31 open UriManager
  32
  33 module Ast = CicNotationPt
  34
  35 let debug_print _ = ();;
  36
  37 let refine_term metasenv subst context uri term _ ~localization_tbl =
  38   assert (uri=None);
  39   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
  40     (NCicPp.ppterm ~metasenv ~subst ~context term)));
  41   try
  42     let localise t =
  43       try NCicUntrusted.NCicHash.find localization_tbl t
  44       with Not_found -> assert false
  45     in
  46     let metasenv, subst, term, _ =
  47       NCicRefiner.typeof metasenv subst context term None ~localise
  48     in
  49      Disambiguate.Ok (term, metasenv, subst, ())
  50   with
  51   | NCicRefiner.Uncertain (msg) ->
  52       debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^
  53         NCicPp.ppterm ~metasenv ~subst ~context term)) ;
  54       Disambiguate.Uncertain (loc,msg)
  55   | NCicRefiner.RefineFailure (msg) ->
  56       debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
  57         (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg))));
  58       Disambiguate.Ko (loc,msg,())
  59 ;;
  60
  61 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
  62   try
  63     snd (Environment.find item env) env num args
  64   with Not_found ->
  65     failwith ("Domain item not found: " ^
  66       (DisambiguateTypes.string_of_domain_item item))
  67
  68   (* TODO move it to Cic *)
  69 let find_in_context name context =
  70   let rec aux acc = function
  71     | [] -> raise Not_found
  72     | Cic.Name hd :: _ when hd = name -> acc
  73     | _ :: tl ->  aux (acc + 1) tl
  74   in
  75   aux 1 context
  76
  77 let interpretate_term
  78   ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl
  79 =
  80   (* create_dummy_ids shouldbe used only for interpretating patterns *)
  81   assert (uri = None);
  82
  83   let rec aux ~localize loc context = function
  84     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
  85         let res = aux ~localize loc context term in
  86          if localize then NCic.NCicHash.add localization_tbl res loc;
  87          res
  88     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
  89     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
  90         let cic_args = List.map (aux ~localize loc context) args in
  91         resolve env (Symbol (symb, i)) ~args:cic_args ()
  92     | CicNotationPt.Appl terms ->
  93        NCic.Appl (List.map (aux ~localize loc context) terms)
  94     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
  95         let cic_type = aux_option ~localize loc context (Some `Type) typ in
  96         let cic_name = CicNotationUtil.cic_name_of_name var in
  97         let cic_body = aux ~localize loc (cic_name :: context) body in
  98         (match binder_kind with
  99         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
 100         | `Pi
 101         | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
 102         | `Exists ->
 103             resolve env (Symbol ("exists", 0))
 104               ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
 105     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
 106         let cic_term = aux ~localize loc context term in
 107         let cic_outtype = aux_option ~localize loc context None outtype in
 108         let do_branch ((_, _, args), term) =
 109          let rec do_branch' context = function
 110            | [] -> aux ~localize loc context term
 111            | (name, typ) :: tl ->
 112                let cic_name = CicNotationUtil.cic_name_of_name name in
 113                let cic_body = do_branch' (cic_name :: context) tl in
 114                let typ =
 115                  match typ with
 116                  | None -> NCic.Implicit (Some `Type)
 117                  | Some typ -> aux ~localize loc context typ
 118                in
 119                NCic.Lambda (cic_name, typ, cic_body)
 120          in
 121           do_branch' context args
 122         in
 123         let indtype_uri, indtype_no =
 124           if create_dummy_ids then
 125             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
 126           else
 127           match indty_ident with
 128           | Some (indty_ident, _) ->
 129              (match resolve env (Id indty_ident) () with
 130               | NCic.MutInd (uri, tyno, _) -> (uri, tyno)
 131               | NCic.Implicit _ ->
 132                  raise (Disambiguate.Try_again (lazy "The type of the term to be matched
 133                   is still unknown"))
 134               | _ ->
 135                 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
 136           | None ->
 137               let rec fst_constructor =
 138                 function
 139                    (Ast.Pattern (head, _, _), _) :: _ -> head
 140                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
 141                  | [] -> raise (Invalid_choice (Some loc, lazy "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"))
 142               in
 143               (match resolve env (Id (fst_constructor branches)) () with
 144               | NCic.MutConstruct (indtype_uri, indtype_no, _, _) ->
 145                   (indtype_uri, indtype_no)
 146               | NCic.Implicit _ ->
 147                  raise (Disambiguate.Try_again (lazy "The type of the term to be matched
 148                   is still unknown"))
 149               | _ ->
 150                 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
 151         in
 152         let branches =
 153          if create_dummy_ids then
 154           List.map
 155            (function
 156                Ast.Wildcard,term -> ("wildcard",None,[]), term
 157              | Ast.Pattern _,_ ->
 158                 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
 159            ) branches
 160          else
 161          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
 162             NCic.InductiveDefinition (il,_,leftsno,_) ->
 163              let _,_,_,cl =
 164               try
 165                List.nth il indtype_no
 166               with _ -> assert false
 167              in
 168               let rec count_prod t =
 169                 match CicReduction.whd [] t with
 170                     NCic.Prod (_, _, t) -> 1 + (count_prod t)
 171                   | _ -> 0
 172               in
 173               let rec sort branches cl =
 174                match cl with
 175                   [] ->
 176                    let rec analyze unused unrecognized useless =
 177                     function
 178                        [] ->
 179                         if unrecognized != [] then
 180                          raise (DisambiguateTypes.Invalid_choice
 181                           (Some loc,
 182                            lazy
 183                             ("Unrecognized constructors: " ^
 184                              String.concat " " unrecognized)))
 185                         else if useless > 0 then
 186                          raise (DisambiguateTypes.Invalid_choice
 187                           (Some loc,
 188                            lazy
 189                             ("The last " ^ string_of_int useless ^
 190                              "case" ^ if useless > 1 then "s are" else " is" ^
 191                              " unused")))
 192                         else
 193                          []
 194                      | (Ast.Wildcard,_)::tl when not unused ->
 195                          analyze true unrecognized useless tl
 196                      | (Ast.Pattern (head,_,_),_)::tl when not unused ->
 197                          analyze unused (head::unrecognized) useless tl
 198                      | _::tl -> analyze unused unrecognized (useless + 1) tl
 199                    in
 200                     analyze false [] 0 branches
 201                 | (name,ty)::cltl ->
 202                    let rec find_and_remove =
 203                     function
 204                        [] ->
 205                         raise
 206                          (DisambiguateTypes.Invalid_choice
 207                           (Some loc, lazy ("Missing case: " ^ name)))
 208                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
 209                          branch, branches
 210                      | (Ast.Pattern (name',_,_),_) as branch :: tl
 211                         when name = name' ->
 212                          branch,tl
 213                      | branch::tl ->
 214                         let found,rest = find_and_remove tl in
 215                          found, branch::rest
 216                    in
 217                     let branch,tl = find_and_remove branches in
 218                     match branch with
 219                        Ast.Pattern (name,y,args),term ->
 220                         if List.length args = count_prod ty - leftsno then
 221                          ((name,y,args),term)::sort tl cltl
 222                         else
 223                          raise
 224                           (DisambiguateTypes.Invalid_choice
 225                            (Some loc,
 226                              lazy ("Wrong number of arguments for " ^ name)))
 227                      | Ast.Wildcard,term ->
 228                         let rec mk_lambdas =
 229                          function
 230                             0 -> term
 231                           | n ->
 232                              CicNotationPt.Binder
 233                               (`Lambda, (CicNotationPt.Ident ("_", None), None),
 234                                 mk_lambdas (n - 1))
 235                         in
 236                          (("wildcard",None,[]),
 237                           mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
 238               in
 239                sort branches cl
 240           | _ -> assert false
 241         in
 242         NCic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 243           (List.map do_branch branches))
 244     | CicNotationPt.Cast (t1, t2) ->
 245         let cic_t1 = aux ~localize loc context t1 in
 246         let cic_t2 = aux ~localize loc context t2 in
 247         NCic.Cast (cic_t1, cic_t2)
 248     | CicNotationPt.LetIn ((name, typ), def, body) ->
 249         let cic_def = aux ~localize loc context def in
 250         let cic_name = CicNotationUtil.cic_name_of_name name in
 251         let cic_typ =
 252           match typ with
 253           | None -> NCic.Implicit (Some `Type)
 254           | Some t -> aux ~localize loc context t
 255         in
 256         let cic_body = aux ~localize loc (cic_name :: context) body in
 257         NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
 258     | CicNotationPt.LetRec (kind, defs, body) ->
 259         let context' =
 260           List.fold_left
 261             (fun acc (_, (name, _), _, _) ->
 262               CicNotationUtil.cic_name_of_name name :: acc)
 263             context defs
 264         in
 265         let cic_body =
 266          let unlocalized_body = aux ~localize:false loc context' body in
 267          match unlocalized_body with
 268             NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
 269           | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
 270              (try
 271                let l' =
 272                 List.map
 273                  (function t ->
 274                    let t',subst,metasenv =
 275                     CicMetaSubst.delift_rels [] [] (List.length defs) t
 276                    in
 277                     assert (subst=[]);
 278                     assert (metasenv=[]);
 279                     t') l
 280                in
 281                 (* We can avoid the LetIn. But maybe we need to recompute l'
 282                    so that it is localized *)
 283                 if localize then
 284                  match body with
 285                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
 286                      (* since we avoid the letin, the context has no
 287                       * recfuns in it *)
 288                      let l' = List.map (aux ~localize loc context) l in
 289                       `AvoidLetIn (n,l')
 290                   | _ -> assert false
 291                 else
 292                  `AvoidLetIn (n,l')
 293               with
 294                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 295                 if localize then
 296                  `AddLetIn (aux ~localize loc context' body)
 297                 else
 298                  `AddLetIn unlocalized_body)
 299           | _ ->
 300              if localize then
 301               `AddLetIn (aux ~localize loc context' body)
 302              else
 303               `AddLetIn unlocalized_body
 304         in
 305         let inductiveFuns =
 306           List.map
 307             (fun (params, (name, typ), body, decr_idx) ->
 308               let add_binders kind t =
 309                List.fold_right
 310                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
 311               in
 312               let cic_body =
 313                aux ~localize loc context' (add_binders `Lambda body) in
 314               let cic_type =
 315                aux_option ~localize loc context (Some `Type)
 316                 (HExtlib.map_option (add_binders `Pi) typ) in
 317               let name =
 318                 match CicNotationUtil.cic_name_of_name name with
 319                 | NCic.Anonymous ->
 320                     CicNotationPt.fail loc
 321                       "Recursive functions cannot be anonymous"
 322                 | NCic.Name name -> name
 323               in
 324               (name, decr_idx, cic_type, cic_body))
 325             defs
 326         in
 327         let fix_or_cofix n =
 328          match kind with
 329             `Inductive -> NCic.Fix (n,inductiveFuns)
 330           | `CoInductive ->
 331               let coinductiveFuns =
 332                 List.map
 333                  (fun (name, _, typ, body) -> name, typ, body)
 334                  inductiveFuns
 335               in
 336                NCic.CoFix (n,coinductiveFuns)
 337         in
 338          let counter = ref ~-1 in
 339          let build_term _ (var,_,ty,_) t =
 340           incr counter;
 341           NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
 342          in
 343           (match cic_body with
 344               `AvoidLetInNoAppl n ->
 345                 let n' = List.length inductiveFuns - n in
 346                  fix_or_cofix n'
 347             | `AvoidLetIn (n,l) ->
 348                 let n' = List.length inductiveFuns - n in
 349                  NCic.Appl (fix_or_cofix n'::l)
 350             | `AddLetIn cic_body ->
 351                 List.fold_right (build_term inductiveFuns) inductiveFuns
 352                  cic_body)
 353     | CicNotationPt.Ident _
 354     | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
 355     | CicNotationPt.Ident (name, subst)
 356     | CicNotationPt.Uri (name, subst) as ast ->
 357         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
 358         (try
 359           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 360           let index = find_in_context name context in
 361           if subst <> None then
 362             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 363           NCic.Rel index
 364         with Not_found ->
 365           let cic =
 366             if is_uri ast then  (* we have the URI, build the term out of it *)
 367               try
 368                 CicUtil.term_of_uri (UriManager.uri_of_string name)
 369               with UriManager.IllFormedUri _ ->
 370                 CicNotationPt.fail loc "Ill formed URI"
 371             else
 372               resolve env (Id name) ()
 373           in
 374           let mk_subst uris =
 375             let ids_to_uris =
 376               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 377             in
 378             (match subst with
 379             | Some subst ->
 380                 List.map
 381                   (fun (s, term) ->
 382                     (try
 383                       List.assoc s ids_to_uris, aux ~localize loc context term
 384                      with Not_found ->
 385                        raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
 386                   subst
 387             | None -> List.map (fun uri -> uri, NCic.Implicit None) uris)
 388           in
 389           (try
 390             match cic with
 391             | NCic.Const (uri, []) ->
 392                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 393                 let uris = CicUtil.params_of_obj o in
 394                 NCic.Const (uri, mk_subst uris)
 395             | NCic.Var (uri, []) ->
 396                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 397                 let uris = CicUtil.params_of_obj o in
 398                 NCic.Var (uri, mk_subst uris)
 399             | NCic.MutInd (uri, i, []) ->
 400                (try
 401                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 402                  let uris = CicUtil.params_of_obj o in
 403                  NCic.MutInd (uri, i, mk_subst uris)
 404                 with
 405                  CicEnvironment.Object_not_found _ ->
 406                   (* if we are here it is probably the case that during the
 407                      definition of a mutual inductive type we have met an
 408                      occurrence of the type in one of its constructors.
 409                      However, the inductive type is not yet in the environment
 410                   *)
 411                   (*here the explicit_named_substituion is assumed to be of length 0 *)
 412                   NCic.MutInd (uri,i,[]))
 413             | NCic.MutConstruct (uri, i, j, []) ->
 414                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 415                 let uris = CicUtil.params_of_obj o in
 416                 NCic.MutConstruct (uri, i, j, mk_subst uris)
 417             | NCic.Meta _ | NCic.Implicit _ as t ->
 418 (*
 419                 debug_print (lazy (sprintf
 420                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 421                   (CicPp.ppterm t)
 422                   (String.concat "; "
 423                     (List.map
 424                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
 425                       subst))));
 426 *)
 427                 t
 428             | _ ->
 429               raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
 430            with
 431              CicEnvironment.CircularDependency _ ->
 432                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
 433     | CicNotationPt.Implicit -> NCic.Implicit None
 434     | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
 435     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
 436     | CicNotationPt.Meta (index, subst) ->
 437         let cic_subst =
 438           List.map
 439             (function
 440                 None -> None
 441               | Some term -> Some (aux ~localize loc context term))
 442             subst
 443         in
 444         NCic.Meta (index, cic_subst)
 445     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
 446     | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set
 447     | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u)
 448     | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u)
 449     | CicNotationPt.Symbol (symbol, instance) ->
 450         resolve env (Symbol (symbol, instance)) ()
 451     | _ -> assert false (* god bless Bologna *)
 452   and aux_option ~localize loc context annotation = function
 453     | None -> NCic.Implicit annotation
 454     | Some term -> aux ~localize loc context term
 455   in
 456    aux ~localize:true HExtlib.dummy_floc context ast
 457
 458 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 459      ~localization_tbl
 460 =
 461   let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
 462   interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
 463 ~localization_tbl
 464 ;;
 465
 466 let domain_of_term ~context =
 467   let context = List.map (fun x -> NCic.Name (fst x)) context in
 468   Disambiguate.domain_of_ast_term ~context
 469 ;;
 470
 471 module Make (C : DisambiguateTypes.Callbacks) = struct
 472  module Disambiguator = Disambiguate.Make(C)
 473
 474  let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
 475     ?(initial_ugraph = ()) ~aliases ~universe
 476     (text,prefix_len,term)
 477   =
 478    let term =
 479      if fresh_instances then CicNotationUtil.freshen_term term else term
 480    in
 481    let localization_tbl = NCic.NCicHash.create 503 in
 482    Disambiguator.disambiguate_thing
 483      ~dbd ~context ~metasenv ~initial_ugraph ~aliases
 484      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
 485      ~domain_of_thing:domain_of_term
 486      ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
 487      ~refine_thing:refine_term (text,prefix_len,term)
 488      ~localization_tbl
 489  ;;
 490
 491 end