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 cic_name_of_name = function
  38   | Ast.Ident (n, None) ->  n
  39   | _ -> assert false
  40 ;;
  41
  42 let refine_term metasenv subst context uri term _ ~localization_tbl =
  43   assert (uri=None);
  44   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
  45     (NCicPp.ppterm ~metasenv ~subst ~context term)));
  46   try
  47     let localise t =
  48       try NCicUntrusted.NCicHash.find localization_tbl t
  49       with Not_found -> assert false
  50     in
  51     let metasenv, subst, term, _ =
  52       NCicRefiner.typeof metasenv subst context term None ~localise
  53     in
  54      Disambiguate.Ok (term, metasenv, subst, ())
  55   with
  56   | NCicRefiner.Uncertain loc_msg ->
  57       debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
  58         NCicPp.ppterm ~metasenv ~subst ~context term)) ;
  59       Disambiguate.Uncertain loc_msg
  60   | NCicRefiner.RefineFailure loc_msg ->
  61       debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
  62         (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
  63       Disambiguate.Ko loc_msg
  64 ;;
  65
  66 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
  67         assert false;;
  68 (*
  69   try
  70     snd (Environment.find item env) env num args
  71   with Not_found ->
  72     failwith ("Domain item not found: " ^
  73       (DisambiguateTypes.string_of_domain_item item))
  74 *)
  75
  76   (* TODO move it to Cic *)
  77 let find_in_context name context =
  78   let rec aux acc = function
  79     | [] -> raise Not_found
  80     | Cic.Name hd :: _ when hd = name -> acc
  81     | _ :: tl ->  aux (acc + 1) tl
  82   in
  83   aux 1 context
  84
  85 let interpretate_term
  86   ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl
  87 =
  88   (* create_dummy_ids shouldbe used only for interpretating patterns *)
  89   assert (uri = None);
  90
  91   let rec aux ~localize loc context = function
  92     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
  93         let res = aux ~localize loc context term in
  94          if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
  95          res
  96     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
  97     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
  98         let cic_args = List.map (aux ~localize loc context) args in
  99         resolve env (Symbol (symb, i)) ~args:cic_args ()
 100     | CicNotationPt.Appl terms ->
 101        NCic.Appl (List.map (aux ~localize loc context) terms)
 102     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
 103         let cic_type = aux_option ~localize loc context (Some `Type) typ in
 104         let cic_name = cic_name_of_name var  in
 105         let cic_body = aux ~localize loc (cic_name :: context) body in
 106         (match binder_kind with
 107         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
 108         | `Pi
 109         | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
 110         | `Exists ->
 111             resolve env (Symbol ("exists", 0))
 112               ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
 113     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
 114         let cic_term = aux ~localize loc context term in
 115         let cic_outtype = aux_option ~localize loc context None outtype in
 116         let do_branch ((_, _, args), term) =
 117          let rec do_branch' context = function
 118            | [] -> aux ~localize loc context term
 119            | (name, typ) :: tl ->
 120                let cic_name = cic_name_of_name name in
 121                let cic_body = do_branch' (cic_name :: context) tl in
 122                let typ =
 123                  match typ with
 124                  | None -> NCic.Implicit `Type
 125                  | Some typ -> aux ~localize loc context typ
 126                in
 127                NCic.Lambda (cic_name, typ, cic_body)
 128          in
 129           do_branch' context args
 130         in
 131         let indtype_uri, indtype_no =
 132           if create_dummy_ids then
 133             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
 134           else
 135           match indty_ident with
 136           | Some (indty_ident, _) ->
 137              (match resolve env (Id indty_ident) () with
 138               | NCic.Const (NRef.Ref (uri, NRef.Ind  (_, tyno))) -> (uri, tyno)
 139               | NCic.Implicit _ ->
 140                  raise (Disambiguate.Try_again
 141                   (lazy "The type of the term to be matched is still unknown"))
 142               | _ ->
 143                 raise (DisambiguateTypes.Invalid_choice
 144                   (Some loc,
 145                     lazy "The type of the term to be matched is not (co)inductive!")))
 146           | None ->
 147               let rec fst_constructor =
 148                 function
 149                    (Ast.Pattern (head, _, _), _) :: _ -> head
 150                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
 151                  | [] -> 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"))
 152               in
 153               (match resolve env (Id (fst_constructor branches)) () with
 154               | NCic.MutConstruct (indtype_uri, indtype_no, _, _) ->
 155                   (indtype_uri, indtype_no)
 156               | NCic.Implicit _ ->
 157                  raise (Disambiguate.Try_again (lazy "The type of the term to be matched
 158                   is still unknown"))
 159               | _ ->
 160                 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
 161         in
 162         let branches =
 163          if create_dummy_ids then
 164           List.map
 165            (function
 166                Ast.Wildcard,term -> ("wildcard",None,[]), term
 167              | Ast.Pattern _,_ ->
 168                 raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
 169            ) branches
 170          else
 171          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
 172             NCic.InductiveDefinition (il,_,leftsno,_) ->
 173              let _,_,_,cl =
 174               try
 175                List.nth il indtype_no
 176               with _ -> assert false
 177              in
 178               let rec count_prod t =
 179                 match CicReduction.whd [] t with
 180                     NCic.Prod (_, _, t) -> 1 + (count_prod t)
 181                   | _ -> 0
 182               in
 183               let rec sort branches cl =
 184                match cl with
 185                   [] ->
 186                    let rec analyze unused unrecognized useless =
 187                     function
 188                        [] ->
 189                         if unrecognized != [] then
 190                          raise (DisambiguateTypes.Invalid_choice
 191                           (Some loc,
 192                            lazy
 193                             ("Unrecognized constructors: " ^
 194                              String.concat " " unrecognized)))
 195                         else if useless > 0 then
 196                          raise (DisambiguateTypes.Invalid_choice
 197                           (Some loc,
 198                            lazy
 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                           (Some loc, lazy ("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                            (Some loc,
 236                              lazy ("Wrong number of arguments for " ^ 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         NCic.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         NCic.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 = cic_name_of_name name in
 261         let cic_typ =
 262           match typ with
 263           | None -> NCic.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         NCic.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               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             NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
 279           | NCic.Appl (NCic.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 cic_name_of_name name with
 329                 | NCic.Anonymous ->
 330                     CicNotationPt.fail loc
 331                       "Recursive functions cannot be anonymous"
 332                 | NCic.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 -> NCic.Fix (n,inductiveFuns)
 340           | `CoInductive ->
 341               let coinductiveFuns =
 342                 List.map
 343                  (fun (name, _, typ, body) -> name, typ, body)
 344                  inductiveFuns
 345               in
 346                NCic.CoFix (n,coinductiveFuns)
 347         in
 348          let counter = ref ~-1 in
 349          let build_term _ (var,_,ty,_) t =
 350           incr counter;
 351           NCic.LetIn (NCic.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                  NCic.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 = find_in_context name context in
 371           if subst <> None then
 372             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 373           NCic.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               resolve env (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 (Invalid_choice (Some loc, lazy "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, NCic.Implicit None) uris)
 398           in
 399           (try
 400             match cic with
 401             | NCic.Const (uri, []) ->
 402                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 403                 let uris = CicUtil.params_of_obj o in
 404                 NCic.Const (uri, mk_subst uris)
 405             | NCic.Var (uri, []) ->
 406                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 407                 let uris = CicUtil.params_of_obj o in
 408                 NCic.Var (uri, mk_subst uris)
 409             | NCic.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                  NCic.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                   NCic.MutInd (uri,i,[]))
 423             | NCic.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                 NCic.MutConstruct (uri, i, j, mk_subst uris)
 427             | NCic.Meta _ | NCic.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 (Invalid_choice (Some loc, lazy "??? Can this happen?"))
 440            with
 441              CicEnvironment.CircularDependency _ ->
 442                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
 443     | CicNotationPt.Implicit -> NCic.Implicit None
 444     | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
 445     | CicNotationPt.Num (num, i) -> resolve env (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         NCic.Meta (index, cic_subst)
 455     | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
 456     | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set
 457     | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u)
 458     | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u)
 459     | CicNotationPt.Symbol (symbol, instance) ->
 460         resolve env (Symbol (symbol, instance)) ()
 461     | _ -> assert false (* god bless Bologna *)
 462   and aux_option ~localize loc context annotation = function
 463     | None -> NCic.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_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 469      ~localization_tbl
 470 =
 471   let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
 472   interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
 473 ~localization_tbl
 474 ;;
 475
 476 let domain_of_term ~context =
 477   let context = List.map (fun x -> NCic.Name (fst x)) context in
 478   Disambiguate.domain_of_ast_term ~context
 479 ;;
 480
 481 module Make (C : DisambiguateTypes.Callbacks) = struct
 482  module Disambiguator = Disambiguate.Make(C)
 483
 484  let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
 485     ?(initial_ugraph = ()) ~aliases ~universe
 486     (text,prefix_len,term)
 487   =
 488    let term =
 489      if fresh_instances then CicNotationUtil.freshen_term term else term
 490    in
 491    let localization_tbl = NCic.NCicHash.create 503 in
 492    Disambiguator.disambiguate_thing
 493      ~dbd ~context ~metasenv ~initial_ugraph ~aliases
 494      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
 495      ~domain_of_thing:domain_of_term
 496      ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
 497      ~refine_thing:refine_term (text,prefix_len,term)
 498      ~localization_tbl
 499  ;;
 500
 501 end