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