helm/ocaml/cic_proof_checking/cicEnvironment.ml

   1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 (*****************************************************************************)
  27 (*                                                                           *)
  28 (*                              PROJECT HELM                                 *)
  29 (*                                                                           *)
  30 (*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                24/01/2000                                 *)
  32 (*                                                                           *)
  33 (* This module implements a trival cache system (an hash-table) for cic      *)
  34 (* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)        *)
  35 (*                                                                           *)
  36 (*****************************************************************************)
  37
  38
  39 let cleanup_tmp = true;;
  40
  41 let trust = ref  (fun _ -> true);;
  42 let set_trust f = trust := f
  43 let trust_obj uri = !trust uri
  44
  45 type type_checked_obj =
  46    CheckedObj of (Cic.obj * CicUniv.universe_graph)    (* cooked obj *)
  47  | UncheckedObj of Cic.obj   (* uncooked obj to proof-check *)
  48 ;;
  49
  50
  51 exception AlreadyCooked of string;;
  52 exception CircularDependency of string;;
  53 exception CouldNotFreeze of string;;
  54 exception CouldNotUnfreeze of string;;
  55 exception Term_not_found of UriManager.uri;;
  56
  57 (* Cache that uses == instead of = for testing equality *)
  58 (* Invariant: an object is always in at most one of the *)
  59 (* following states: unchecked, frozen and cooked.      *)
  60 module Cache :
  61   sig
  62    val find_or_add_unchecked :
  63      UriManager.uri ->
  64      get_object_to_add:(unit -> Cic.obj * CicUniv.universe_graph option) ->
  65      Cic.obj * CicUniv.universe_graph
  66    val can_be_cooked:
  67      UriManager.uri -> bool
  68    val unchecked_to_frozen :
  69      UriManager.uri -> unit
  70    val frozen_to_cooked :
  71      uri:UriManager.uri -> unit
  72    val hack_univ:
  73      UriManager.uri -> CicUniv.universe_graph -> unit
  74    val find_cooked :
  75      key:UriManager.uri -> Cic.obj * CicUniv.universe_graph
  76    val add_cooked :
  77      key:UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
  78    val not_jet_cooked:
  79      UriManager.uri -> Cic.obj * CicUniv.universe_graph
  80    val remove: UriManager.uri -> unit
  81
  82    val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
  83    val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
  84    val empty : unit -> unit
  85    val is_in_frozen: UriManager.uri -> bool
  86    val is_in_unchecked: UriManager.uri -> bool
  87   end
  88 =
  89   struct
  90    (*************************************************************************
  91      TASSI: invariant
  92      The CacheOfCookedObjects will contain only objects with a valid universe
  93      graph. valid means that non None (used if there is no universe file
  94      in the universe generation phase).
  95    **************************************************************************)
  96    module CacheOfCookedObjects :
  97     sig
  98      val mem  : UriManager.uri -> bool
  99      val find : UriManager.uri -> Cic.obj * CicUniv.universe_graph
 100      val add  : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
 101      val remove : UriManager.uri -> unit
 102
 103       (** (de)serialization of type checker cache *)
 104      val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
 105      val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
 106      val empty : unit -> unit
 107     end
 108    =
 109     struct
 110      module HashedType =
 111       struct
 112        type t = UriManager.uri
 113        let equal = UriManager.eq
 114        let hash = Hashtbl.hash
 115       end
 116      ;;
 117      module HT = Hashtbl.Make(HashedType);;
 118      let hashtable = HT.create 1009;;
 119      let mem uri =
 120       try
 121        HT.mem hashtable uri
 122       with
 123        Not_found -> false
 124      ;;
 125      let find uri = HT.find hashtable uri ;;
 126      let add uri (obj,ugraph) =
 127        HT.add hashtable uri (obj,ugraph)
 128      ;;
 129      let remove uri =
 130        if mem uri then
 131          HT.remove hashtable uri
 132        else
 133          raise (Term_not_found uri);
 134      ;;
 135
 136       (* used to hash cons uris on restore to grant URI structure unicity *)
 137      let restore_uris =
 138        let module C = Cic in
 139        let recons uri =
 140          UriManager.uri_of_string (UriManager.string_of_uri uri)
 141        in
 142        let rec restore_in_term =
 143          function
 144             (C.Rel _) as t -> t
 145           | C.Var (uri,exp_named_subst) ->
 146              let uri' = recons uri in
 147              let exp_named_subst' =
 148               List.map
 149                (function (uri,t) ->(recons uri,restore_in_term t))
 150                 exp_named_subst
 151              in
 152               C.Var (uri',exp_named_subst')
 153           | C.Meta (i,l) ->
 154              let l' =
 155               List.map
 156                (function
 157                    None -> None
 158                  | Some t -> Some (restore_in_term t)
 159                ) l
 160              in
 161               C.Meta(i,l')
 162           | C.Sort _ as t -> t
 163           | C.Implicit _ as t -> t
 164           | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
 165           | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
 166           | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
 167           | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t)
 168           | C.Appl l -> C.Appl (List.map restore_in_term l)
 169           | C.Const (uri,exp_named_subst) ->
 170              let uri' = recons uri in
 171              let exp_named_subst' =
 172               List.map
 173                (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 174              in
 175               C.Const (uri',exp_named_subst')
 176           | C.MutInd (uri,tyno,exp_named_subst) ->
 177              let uri' = recons uri in
 178              let exp_named_subst' =
 179               List.map
 180                (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 181              in
 182               C.MutInd (uri',tyno,exp_named_subst')
 183           | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 184              let uri' = recons uri in
 185              let exp_named_subst' =
 186               List.map
 187                (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 188              in
 189               C.MutConstruct (uri',tyno,consno,exp_named_subst')
 190           | C.MutCase (uri,i,outty,t,pl) ->
 191              C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
 192               List.map restore_in_term pl)
 193           | C.Fix (i, fl) ->
 194              let len = List.length fl in
 195              let liftedfl =
 196               List.map
 197                (fun (name, i, ty, bo) ->
 198                  (name, i, restore_in_term ty, restore_in_term bo))
 199                 fl
 200              in
 201               C.Fix (i, liftedfl)
 202           | C.CoFix (i, fl) ->
 203              let len = List.length fl in
 204              let liftedfl =
 205               List.map
 206                (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo))
 207                 fl
 208              in
 209               C.CoFix (i, liftedfl)
 210        in
 211        function
 212           C.Constant (name,bo,ty,params) ->
 213             let bo' =
 214               match bo with
 215                 None -> None
 216               | Some bo -> Some (restore_in_term bo)
 217             in
 218             let ty' = restore_in_term ty in
 219             let params' = List.map recons params in
 220             C.Constant (name, bo', ty', params')
 221         | C.CurrentProof (name,conjs,bo,ty,params) ->
 222             let conjs' =
 223               List.map
 224                 (function (i,hyps,ty) ->
 225                   (i,
 226                   List.map (function
 227                       None -> None
 228                     | Some (name,C.Decl t) ->
 229                         Some (name,C.Decl (restore_in_term t))
 230                     | Some (name,C.Def (bo,ty)) ->
 231                         let ty' =
 232                           match ty with
 233                             None -> None
 234                           | Some ty'' -> Some (restore_in_term ty'')
 235                         in
 236                         Some (name,C.Def (restore_in_term bo, ty'))) hyps,
 237                   restore_in_term ty))
 238                 conjs
 239             in
 240             let bo' = restore_in_term bo in
 241             let ty' = restore_in_term ty in
 242             let params' = List.map recons params in
 243             C.CurrentProof (name, conjs', bo', ty', params')
 244         | C.Variable (name,bo,ty,params) ->
 245             let bo' =
 246               match bo with
 247                 None -> None
 248               | Some bo -> Some (restore_in_term bo)
 249             in
 250             let ty' = restore_in_term ty in
 251             let params' = List.map recons params in
 252             C.Variable (name, bo', ty', params')
 253         | C.InductiveDefinition (tl,params,paramsno) ->
 254             let params' = List.map recons params in
 255             let tl' =
 256               List.map (function (name, inductive, ty, constructors) ->
 257                 name,
 258                 inductive,
 259                 restore_in_term ty,
 260                 (List.map
 261                   (function (name, ty) -> name, restore_in_term ty)
 262                   constructors))
 263                 tl
 264             in
 265             C.InductiveDefinition (tl', params', paramsno)
 266
 267      let dump_to_channel ?(callback = ignore) oc =
 268        HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) hashtable;
 269        Marshal.to_channel oc hashtable [] ;;
 270      let empty () = HT.clear hashtable ;;
 271      let restore_from_channel ?(callback = ignore) ic =
 272        let restored = Marshal.from_channel ic in
 273        empty ();
 274        HT.iter
 275         (fun k v ->
 276           callback (UriManager.string_of_uri k);
 277           HT.add hashtable
 278             (UriManager.uri_of_string (UriManager.string_of_uri k))
 279
 280 (************************************************
 281    TASSI: FIXME add channel stuff for universes
 282 *************************************************)
 283
 284             ((restore_uris v),CicUniv.empty_ugraph))
 285         restored
 286      ;;
 287
 288     end
 289    ;;
 290    let frozen_list = ref [];;
 291    let unchecked_list = ref [];;
 292
 293    let is_in_frozen uri =
 294      List.mem_assoc uri !frozen_list
 295    ;;
 296
 297    let is_in_unchecked uri =
 298      List.mem_assoc uri !unchecked_list
 299    ;;
 300    (*******************************************************************
 301      TASSI: invariant
 302      we need, in the universe generation phase, to traverse objects
 303      that are not jet committed, so we search them in the frozen list.
 304      Only uncommitted objects without a universe file (see the assertion)
 305      can be searched with method
 306    *******************************************************************)
 307    let not_jet_cooked uri =
 308      try
 309        let o,u = List.assoc uri !frozen_list in
 310          match u with
 311              None -> o, CicUniv.empty_ugraph
 312            | Some _ -> assert false (* only univ_maker ca use this *)
 313      with Not_found ->
 314        CacheOfCookedObjects.find uri
 315    ;;
 316    let find_or_add_unchecked uri ~get_object_to_add =
 317      try
 318        let o,g = List.assq uri !unchecked_list in
 319          match g with
 320              None -> o,CicUniv.empty_ugraph
 321            | Some g' -> o,g'
 322      with
 323          Not_found ->
 324            if List.mem_assq uri !frozen_list then
 325              begin
 326                print_endline "\nCircularDependency!\nfrozen list: \n";
 327                List.iter (
 328                  fun (u,(_,o)) ->
 329                    let su = UriManager.string_of_uri u in
 330                    let univ = if o = None then "NO_UNIV" else "" in
 331                    print_endline (su^" "^univ))
 332                  !frozen_list;
 333                raise (CircularDependency (UriManager.string_of_uri uri))
 334              end
 335            else
 336              if CacheOfCookedObjects.mem uri then
 337                raise (AlreadyCooked (UriManager.string_of_uri uri))
 338              else
 339                (* OK, it is not already frozen nor cooked *)
 340                let obj,ugraph = get_object_to_add () in
 341                let ugraph_real =
 342                  match ugraph with
 343                      None -> CicUniv.empty_ugraph
 344                    | Some g -> g
 345                in
 346                  unchecked_list := (uri,(obj,ugraph))::!unchecked_list ;
 347                  obj,ugraph_real
 348    ;;
 349    let unchecked_to_frozen uri =
 350     try
 351      let obj,ugraph = List.assq uri !unchecked_list in
 352       unchecked_list := List.remove_assq uri !unchecked_list ;
 353       frozen_list := (uri,(obj,ugraph))::!frozen_list
 354     with
 355      Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 356    ;;
 357    (************************************************************
 358      TASSI: invariant
 359      only object with a valid universe graph can be committed
 360    *************************************************************)
 361    let frozen_to_cooked ~uri =
 362     try
 363       let obj,ugraph = List.assq uri !frozen_list in
 364         match ugraph with
 365             None ->
 366               assert false (* only non dummy universes can be committed *)
 367           | Some g ->
 368               frozen_list := List.remove_assq uri !frozen_list ;
 369               CacheOfCookedObjects.add uri (obj,g)
 370     with
 371         Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 372    ;;
 373    let can_be_cooked uri =
 374      try
 375        let obj,ugraph = List.assq uri !frozen_list in
 376          match ugraph with
 377              None -> false
 378            | Some _ -> true
 379      with
 380          Not_found -> false
 381    ;;
 382    let hack_univ uri real_ugraph =
 383      try
 384        let o,g = List.assq uri !frozen_list in
 385          match g with
 386              None ->
 387                frozen_list := List.remove_assoc uri !frozen_list;
 388                frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
 389            | Some g ->
 390                prerr_endline (
 391                  "You are probably hacking an object already hacked or an"^
 392                  " object that has the universe file but is not"^
 393                  " jet committed");
 394                assert false
 395      with
 396          Not_found ->
 397            prerr_endline (
 398              "You are hacking an object that is not in the"^
 399              " frozen_list, this means you are probably generating an"^
 400              " universe file for an object that already as an universe file");
 401            assert false
 402    ;;
 403    let find_cooked ~key:uri = CacheOfCookedObjects.find uri;;
 404    let add_cooked ~key:uri (obj,ugraph) =
 405      CacheOfCookedObjects.add uri (obj,ugraph);;
 406    let remove uri =
 407      if (!unchecked_list <> []) || (!frozen_list <> []) then
 408        failwith "CicEnvironment.remove while type checking"
 409      else
 410        CacheOfCookedObjects.remove uri
 411    ;;
 412    let dump_to_channel = CacheOfCookedObjects.dump_to_channel;;
 413    let restore_from_channel = CacheOfCookedObjects.restore_from_channel;;
 414    let empty () =
 415      CacheOfCookedObjects.empty ();
 416      unchecked_list := [] ;
 417      frozen_list := []
 418    ;;
 419   end
 420 ;;
 421
 422 let dump_to_channel = Cache.dump_to_channel;;
 423 let restore_from_channel = Cache.restore_from_channel;;
 424 let empty = Cache.empty;;
 425
 426 let find_or_add_unchecked_to_cache uri =
 427  Cache.find_or_add_unchecked uri
 428   ~get_object_to_add:
 429    (function () ->
 430      let filename = Http_getter.getxml' uri in
 431      let bodyfilename =
 432       match UriManager.bodyuri_of_uri uri with
 433          None -> None
 434        | Some bodyuri ->
 435           try
 436            ignore (Http_getter.resolve' bodyuri) ;
 437            (* The body exists ==> it is not an axiom *)
 438            Some (Http_getter.getxml' bodyuri)
 439           with
 440            Http_getter_types.Key_not_found _ ->
 441             (* The body does not exist ==> we consider it an axiom *)
 442             None
 443      in
 444
 445        (*
 446           maybe this is not the right place to do this.. but I think
 447           obj_of_xml is called only here
 448        *)
 449      (* this brakes something : let _ = CicUniv.restart_numbering () in *)
 450      let obj = CicParser.obj_of_xml filename bodyfilename in
 451      let ugraph,filename_univ =
 452        (*
 453        try
 454          let filename_univ =
 455            Http_getter.getxml' (
 456              UriManager.uri_of_string (
 457                (UriManager.string_of_uri uri) ^ ".univ"))
 458          in
 459            (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
 460        with Failure s ->
 461
 462          prerr_endline (
 463            "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
 464          None,None
 465          *)
 466          (**********************************************
 467            TASSI: should fail when universes will be ON
 468          ***********************************************)
 469          (Some CicUniv.empty_ugraph,None)
 470      in
 471      let cleanup () =
 472        Unix.unlink filename ;
 473        begin
 474          match filename_univ with
 475              Some f -> Unix.unlink f
 476            | None -> ()
 477        end;
 478        begin
 479          match bodyfilename with
 480              Some f -> Unix.unlink f
 481            | None -> ()
 482        end
 483      in
 484        cleanup();
 485        obj,ugraph)
 486 ;;
 487
 488 (* set_type_checking_info uri                               *)
 489 (* must be called once the type-checking of uri is finished *)
 490 (* The object whose uri is uri is unfreezed                 *)
 491 let set_type_checking_info ?(replace_ugraph=None) uri =
 492   if Cache.can_be_cooked uri && replace_ugraph <> None then
 493     invalid_arg (
 494       "?replace_ugraph must be None if you are not committing an "^
 495       "object that has an no universe graph associated "^
 496       "(can happen only in the fase of universes graphs generation).");
 497   if not (Cache.can_be_cooked uri) && replace_ugraph = None then
 498     invalid_arg (
 499       "?replace_ugraph must be (Some ugraph) when committing an object that "^
 500       "has no associated universe graph. If this is in make_univ phase you "^
 501       "should drop this exception and let univ_make commit thi object with "^
 502       "proper arguments");
 503   begin
 504     match replace_ugraph with
 505         None -> ()
 506       | Some g -> Cache.hack_univ uri g
 507   end;
 508   Cache.frozen_to_cooked uri
 509 ;;
 510
 511
 512 (* is_type_checked uri                                                *)
 513 (* CSC: commento falso ed obsoleto *)
 514 (* returns a CheckedObj if the term has been type-checked             *)
 515 (* otherwise it freezes the term for type-checking and returns
 516  it *)
 517 (* set_type_checking_info must be called to unfreeze the term         *)
 518 let is_type_checked ?(trust=true) uri base_univ =
 519  try
 520    let o,u = Cache.find_cooked uri in
 521      CheckedObj (o,CicUniv.merge_ugraphs u base_univ)
 522  with
 523      Not_found ->
 524        let obj,ugraph = find_or_add_unchecked_to_cache uri in
 525          Cache.unchecked_to_frozen uri ;
 526          if trust && trust_obj uri then
 527            begin
 528              CicLogger.log (`Trusting uri) ;
 529              set_type_checking_info uri  ;
 530              let o,u = Cache.find_cooked uri in
 531              let u' = CicUniv.merge_ugraphs base_univ ugraph in
 532                CheckedObj (o,u')
 533            end
 534          else
 535            begin
 536              UncheckedObj obj
 537            end
 538 ;;
 539
 540 (* get_cooked_obj ~trust uri *)
 541 (* returns the object if it is already type-checked or if it can be *)
 542 (* trusted (if [trust] = true and the trusting function accepts it) *)
 543 (* Otherwise it raises Not_found                                    *)
 544 let get_cooked_obj ?(trust=true) uri base_univ =
 545  try
 546    let o,u = Cache.find_cooked uri in
 547      o,(CicUniv.merge_ugraphs base_univ u)
 548  with Not_found ->
 549   if trust && trust_obj uri then
 550    begin
 551     match is_type_checked uri base_univ with
 552         CheckedObj (obj,ugraph) -> obj,(CicUniv.merge_ugraphs ugraph base_univ)
 553       | _ -> assert false
 554    end
 555   else
 556     begin
 557       prerr_endline (
 558         "@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^
 559         ") raises Not_found since the object is not type-checked"^
 560         " nor trusted.");
 561       raise Not_found
 562     end
 563 ;;
 564
 565 (* get_obj uri                                                               *)
 566 (* returns the cic object whose uri is uri. If the term is not just in cache,*)
 567 (* then it is parsed via CicParser.term_of_xml from the file whose name is   *)
 568 (* the result of Getter.getxml uri                                           *)
 569 let get_obj ?(not_jet_cooked=false) uri base_univ =
 570   if not_jet_cooked then
 571     let o,u = Cache.not_jet_cooked uri in
 572       o,(CicUniv.merge_ugraphs base_univ u)
 573   else
 574     try
 575       get_cooked_obj uri base_univ
 576     with
 577         Not_found ->
 578           let s = ( UriManager.string_of_uri uri) in
 579           let o,u = find_or_add_unchecked_to_cache uri in
 580             o,(CicUniv.merge_ugraphs base_univ u)
 581 ;;
 582
 583 exception OnlyPutOfInductiveDefinitionsIsAllowed
 584
 585 let put_inductive_definition uri (obj,ugraph) =
 586  match obj with
 587     Cic.InductiveDefinition _ -> Cache.add_cooked uri (obj,ugraph)
 588   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 589 ;;
 590
 591 let in_cache uri =
 592  try
 593    ignore (Cache.find_cooked uri);
 594    prerr_endline "TROVATO NELLA CHECKED";true
 595  with Not_found ->
 596    if Cache.is_in_frozen uri then
 597      (prerr_endline "TROVATO NELLA FROZEN";true)
 598    else
 599      if Cache.is_in_unchecked uri then
 600        (prerr_endline "TROVATO NELLA UNCHECKED";true)
 601      else
 602        (prerr_endline ("NON TROVATO:" ^ (UriManager.string_of_uri uri) );false)
 603 ;;
 604
 605 let add_type_checked_term uri (obj,ugraph) =
 606   match obj with
 607       Cic.Constant (s,(Some bo),ty,ul) ->
 608         Cache.add_cooked ~key:uri (obj,ugraph)
 609     | _ ->
 610         assert false
 611 ;;
 612
 613 let remove_term = Cache.remove
 614