session_itp.mli 18.9 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705

(** New Proof sessions ("Refectoire") *)

type proof_attempt = {
  prover
  timelimit
  memlimit
  proof_state : Call_provers.prover_result option;  (* None means that the call was not done
                                                       or never returned *)
  proof_obsolete : bool;
  proof_script : string option;  (* non empty for external ITP *)
}


(* note: la fonction register des transformations doit permettre de declarer les types des arguments

  type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol | TTlsymbol | TTprsymbol

*)

type trans_arg =
  | TAint of int
  | TAstring of string
  | TAterm of Term.term
  | TAty of ty
  | TAtysymbol of tysymbol
  | ...


type transformation = {
  transf_name : (task Task.string | task Task.tlist)   ou string
  transf_args : trans_arg list
  transf_subtasks : sequence of proof_task
  }

and proof_task =
  {
     why3_task : Task.task
     externals_proofs : collection of proof_attempt
     transf : sequence of transformation
  }


type goal =
  { goal_task : proof_task
    goal_origin : name of goal, its theory, its file
  }


type session =
  {
    goals : collection of goals

    (* autre choix : collection de proof task, chaque task connait son parent

       autrement dit l'arbre est a l'envers

       avantage : recherche d'une task tres rapide, mise a jour des parents faciles

       inconvenient : effacer un noeud demande de savoir effacer tous les descendants.

     *)
  }

val add_proof_attempt : session -> path_to_a_proof_task (int list ?) -> proof_attempt -> session

val add_transf : session -> path_to_a_proof_task (int list ?) -> transformation -> session




(*

  couche au-dessus: "scheduler" cad modifications asynchrones de la session

   - gere une file de travaux de modifications a faire
   - recupere les resultats de travaux , et les applique s'ils sont encore valides

*)


















type theory =
  {
    goals : sequence of task
  }

type file =
  {
    theories = sequence of theories
  }

type session =
  {
    session_files : set of files
  }






















open Stdlib

val debug : Debug.flag
(** The debug flag "session" *)

module PHstr : Exthtbl.Private with type key = string
module PHprover : Exthtbl.Private with type key = Whyconf.prover

(** {2 Proof attempts} *)

(** State of a proof *)
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

type expl
(** An explanation gives hint about how the goal has been produced.
    Allow to reattach proof_attempt to goal when the source file has been
    modified.
*)

type task_option
(** The task can be removed and later reconstructible *)

type 'a hide
(** For internal use *)


type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
  }

type meta_args = Theory.meta_arg list
module Mmeta_args : Extmap.S with type key = meta_args
module Smeta_args : Extset.S with module M = Mmeta_args

type metas_args = Smeta_args.t Mstr.t
module Mmetas_args : Extmap.S with type key = metas_args

type idpos = {
  idpos_ts : ident_path Ty.Mts.t;
  idpos_ls : ident_path Term.Mls.t;
  idpos_pr : ident_path Decl.Mpr.t;
}

(** {2 Session} *)

(** All the element of a session contain a key which can hold whatever
    information the user want. It is generated by the keygen argument
    of the functions of this module *)

type 'a goal = private
    { mutable goal_key  : 'a;
      goal_name : Ident.ident; (** The ident of the task *)
      goal_expl : expl;
      goal_parent : 'a goal_parent;
      mutable goal_checksum : Termcode.checksum option;  (** checksum of the task *)
      mutable goal_shape : Termcode.shape;  (** shape of the task *)
      mutable goal_verified : float option;
      mutable goal_task: task_option;
      mutable goal_expanded : bool;
      goal_external_proofs : 'a proof_attempt PHprover.t;
      goal_transformations : 'a transf PHstr.t;
      mutable goal_metas : 'a metas Mmetas_args.t;
    }

and 'a proof_attempt = private
    { proof_key : 'a;
      mutable proof_prover : Whyconf.prover;
      proof_parent : 'a goal;
      mutable proof_state : proof_attempt_status;
      mutable proof_timelimit : int;
      mutable proof_memlimit : int;
      mutable proof_obsolete : bool;
      mutable proof_archived : bool;
      mutable proof_edited_as : string option;
    }

and 'a goal_parent = private
                     | Parent_theory of 'a theory
                     | Parent_transf of 'a transf
                     | Parent_metas  of 'a metas

and 'a metas =
  { mutable metas_key : 'a;
    metas_added : metas_args;
    metas_idpos : idpos;
    metas_parent : 'a goal;
    mutable metas_verified : float option;
    mutable metas_goal : 'a goal;
    (** Not mutated after the creation *)
    mutable metas_expanded : bool;
  }

and 'a transf = private
    { mutable transf_key : 'a;
      transf_name : string;
      (** Why3 transformation name *)
      transf_parent : 'a goal;
      mutable transf_verified : float option;
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation *)
      mutable transf_expanded : bool;
      mutable transf_detached : 'a detached option;
    }

and 'a detached = private
    { detached_goals: 'a goal list; }

and 'a theory = private
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
      mutable theory_checksum : Termcode.checksum option;
      mutable theory_goals : 'a goal list;
      (** Not mutated after the creation *)
      mutable theory_verified : float option;
      mutable theory_expanded : bool;
      mutable theory_task : Theory.theory hide;
      mutable theory_detached : 'a detached option;
    }

and 'a file = private
    { mutable file_key : 'a;
      file_name : string;
      file_format : string option;
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
      mutable file_verified : float option;
      mutable file_expanded : bool;
      mutable file_for_recovery : Theory.theory Mstr.t hide;
    }

and 'a session = private
    { session_files : 'a file PHstr.t;
      mutable session_shape_version : int;
      session_prover_ids : int PHprover.t;
      session_dir   : string;
    }

val print_session : Format.formatter -> 'a session -> unit
(** Print a session with a pstree format (cf Tree module) *)

val print_attempt_status : Format.formatter -> proof_attempt_status -> unit

val print_external_proof : Format.formatter -> 'key proof_attempt -> unit

val create_session : ?shape_version:int -> string -> 'key session
(** create a new session in the given directory. The directory is
    created if it doesn't exists yet. Don't change the current
    directory of the program if you give a relative path *)

val get_project_dir : string -> string
(** find the session which corresponds to the given file or return
    directly the given directory;
    return [Not_found] if the file or the directory doesn't exists
*)

(** {2 Read/Write} *)

type 'key keygen = ?parent:'key -> unit -> 'key
(** type of functions which can generate keys *)

exception ShapesFileError of string
exception SessionFileError of string

val read_session: string -> unit session * bool
(** Read a session stored on the disk. It returns a session without any
    task attached to goals.

    The returned boolean is set when there was shapes read from disk.

    raises [SessionFileError msg] if the database file cannot be read
    correctly.

    raises [ShapesFileError msg] if the database extra file for shapes
    cannot be read.

*)

val save_session : Whyconf.config -> 'key session -> unit
(** Save a session on disk *)

(** {2 Context of a session} *)

(** A session which contains task and proof_attempt depends on an
    environment and a prover configuration.
    Loaded provers are cached in order to load drivers once *)

type loaded_prover =
    { prover_config : Whyconf.config_prover;
      prover_driver : Driver.driver}

type loaded_provers = loaded_prover option PHprover.t

type 'a env_session = private
    { env : Env.env;
      mutable whyconf : Whyconf.config;
      loaded_provers : loaded_provers;
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
      session : 'a session}

val update_env_session_config : 'a env_session -> Whyconf.config -> unit
(** updates the configuration *)

val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
(** load a prover *)

val unload_provers : 'a env_session -> unit
(** forces unloading of all provers,
    to force reading again the configuration *)

(** {2 Update session} *)

exception OutdatedSession

type 'key update_context =
  { allow_obsolete_goals : bool;
    release_tasks : bool;
    use_shapes_for_pairing_sub_goals : bool;
    keygen : 'key keygen;
  }

val update_session : ctxt:'key update_context -> 'oldkey session ->
  Env.env -> Whyconf.config -> 'key env_session * bool * bool
(** reload the given session with the given environnement :
    - the files are reloaded
    - apply again the transformation
    - if some goals appear try to find to which goal
    in the given session it corresponds.

    The last case meant that the session was obsolete.
    It is authorized if [allow_obsolete] is [true],
    otherwise the exception {!OutdatedSession} is raised.
    If the session was obsolete is indicated by
    the second result.
    If the merge generated new unpaired goals is indicated by
    the third result.

    raises [OutdatedSession] if the session is obsolete and
    [allow_obsolete] is false

*)

(** {2 Copy/Paste } *)

val copy_proof:  'a proof_attempt -> 'a proof_attempt
val copy_transf: 'a transf        -> 'a transf
val copy_metas:  'a metas         -> 'a metas
(** keys are copied *)

val add_proof_to_goal :
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a proof_attempt ->'a proof_attempt
val add_transf_to_goal:
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a transf        -> 'a transf
val add_metas_to_goal :
  keygen:'a keygen -> 'a env_session ->
  'a goal -> 'a metas         -> 'a metas
(** keys are normally generated *)

(** {2 Accessor} *)

exception NoTask
val goal_task : 'key goal -> Task.task
(** Return the task of a goal. Raise {!NoTask} if the goal doesn't contain a task
    (equivalent to ['key = notask] if {!release_task} is not used) *)

val goal_task_option : 'key goal -> Task.task option
(** Return the task of a goal. *)

val goal_expl : 'key goal -> string
(** Return the explication of a goal *)

val proof_verified : 'key proof_attempt -> float option
(** Return [Some t] if the proof is not obsolete and the result is
    valid. [t] is the time needed to solved it *)

val get_used_provers : 'a session -> Whyconf.Sprover.t
(** Get the set of provers which appear in the session *)

(* val metas_of_virtuals : 'a metas -> Theory.Smeta.t *)
(* (\** Get the set of metas added (the parent goal must contain a task) *\) *)

(** {2 Modificator} *)

val set_transf_expanded : 'key transf -> bool -> unit
val set_metas_expanded : 'key metas -> bool -> unit
val set_goal_expanded : 'key goal -> bool -> unit
val set_theory_expanded : 'key theory -> bool -> unit
val set_file_expanded : 'key file -> bool -> unit
(** open one level or close all the sub-level *)

(** {2 General type} *)

type 'a any =
  | File of 'a file
  | Theory of 'a theory
  | Goal of 'a goal
  | Proof_attempt of 'a proof_attempt
  | Transf of 'a transf
  | Metas of 'a metas

val print_any : Format.formatter -> 'a any -> unit
(** Print a subtree with a pstree format (cf Tree module) *)

val key_any : 'a any -> 'a
(** return the key of an element of the tree *)

(** {2 External proof} *)

type 'key notify = 'key any -> unit
(** type of functions which notify modification of the verified field *)

val add_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  obsolete:bool ->
  archived:bool ->
  timelimit:int ->
  memlimit:int ->
  edit:string option ->
  'key goal ->
  Whyconf.prover ->
  proof_attempt_status ->
  'key proof_attempt

val remove_external_proof : ?notify:'key notify -> 'key proof_attempt -> unit

val set_proof_state :
  ?notify:'key notify ->
  obsolete:bool ->
  archived:bool ->
  proof_attempt_status ->
  'key proof_attempt -> unit

val change_prover : 'a proof_attempt -> Whyconf.prover -> unit

val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit

val set_archived : 'key proof_attempt -> bool -> unit

val set_edited_as : string option -> 'key proof_attempt -> unit

val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
(** return the edited filename after concatenation to [session_dir] *)

val update_edit_external_proof :
  cntexample:bool -> 'key env_session -> 'key proof_attempt -> string
(** return the absolute path of the edited file update with the
    current goal *)


val set_timelimit : int -> 'key proof_attempt -> unit
val set_memlimit : int -> 'key proof_attempt -> unit

val copy_external_proof :
  ?notify:'key notify ->
  keygen:'key keygen ->
  ?obsolete:bool ->
  ?archived:bool ->
  ?timelimit:int ->
  ?memlimit:int ->
  ?edit:string option ->
  ?goal:'key goal ->
  ?prover:Whyconf.prover ->
  ?attempt_status:proof_attempt_status ->
  ?env_session:'key env_session ->
  ?session:'key session ->
  'key proof_attempt -> 'key proof_attempt
(** copy an external proof.
    if env_session and session are given only env_session.session is
    taken into account.
    The edited file is copied and an env_session is not required if :
    {ul
    {- the goal is not modified}
    {- the prover is not modified}
    {- a session is given}
    }
    The edited file is regenerated if
    {ul
    {- the external proof contain an edited file}
    {- an env_session is given}
    {- the given goal (or the old one if not modified) contain a task}
    }
    In all the other case the resulting external proof is considered
    not edited.
*)

(** {2 Transformation} *)

val add_transformation :
  ?init:'key notify ->
  ?notify:'key notify ->
  keygen:'key keygen ->
  'key env_session ->
  string ->
  'key goal ->
  Task.task list ->
  'key transf
(** Add a transformation by its subgoals *)

val add_registered_transformation :
  keygen:'key keygen ->
  'key env_session ->
  string ->
  'key goal ->
  'key transf
(** Apply a real transformation by its why3 name,
    raise {!NoTask} if the goal doesn't contain a task.
    If the goal already has a transformation with this name,
    it is returned. *)

val remove_transformation : ?notify:'key notify -> 'key transf -> unit
  (** Remove a transformation *)

(** {2 Metas} *)
val add_registered_metas :
  keygen:'key keygen ->
  'key env_session ->
  (string * Theory.meta_arg list) list ->
  'key goal ->
  'key metas
(** Add some metas to a task. If the goal already contain a {!metas}
    with same metas, the old one is returned.
*)

val remove_metas : ?notify:'key notify -> 'key metas -> unit
(** Remove the addition of metas *)

(** {2 File} *)

val add_file :
  keygen:'key keygen ->
  'key env_session ->
  ?format:string ->
  string ->
  'key file
(** Add a real file by its filename. The filename must be relative to
    session_dir *)

val remove_file : 'key file -> unit
(** Remove a file *)

(** {2 Free and recover task} *)
(** Tasks are stored inside the goals. For releasing memory you can remove
    them. Later you can recompute them *)

val release_task: 'a goal -> unit
  (** remove the task stored in this goal*)

val release_sub_tasks: 'a goal -> unit
  (** apply the previous function on this goal and its its sub-goal *)

val recover_theory_tasks: 'a env_session -> 'a theory -> unit
  (** Recover all the sub-goal (not only strict) of this theory *)

val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
  (** same as goal_task but recover the task goal and all the one of this
      theory if this goal task have been released *)

(** {2 Iterators} *)

(** {3 recursive} *)

val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
(* unused
val transf_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key transf -> unit
*)
val theory_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key theory -> unit
val transf_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key transf -> unit
val file_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key file -> unit
val session_iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key session -> unit
val iter_proof_attempt :
  ('key proof_attempt -> unit) -> 'key any -> unit

val goal_iter_leaf_goal :
  unproved_only:bool -> ('key goal -> unit) -> 'key goal -> unit
(** iter all the goals which are a leaf
    (no transformations are applied on it) *)

val fold_all_sub_goals_of_theory :
  ('a -> 'key goal -> 'a) -> 'a -> 'key theory -> 'a

(** {3 not recursive} *)

val iter_goal :
  ('key proof_attempt -> unit) ->
  ('key transf -> unit) ->
  ('key metas -> unit) ->
  'key goal -> unit
val iter_transf :
  ('key goal -> unit) -> 'key transf -> unit
val iter_metas :
  ('key goal -> unit) -> 'key metas -> unit
val iter_theory : ('key goal -> unit) -> 'key theory -> unit
  (** [iter_theory f th] applies [f] to all root goals of theory [th] *)
val iter_file :
  ('key theory -> unit) -> 'key file -> unit
val iter_session :
  ('key file -> unit) -> 'key session -> unit


val goal_iter : ('key any -> unit) -> 'key goal -> unit
(* unused
val transf_iter : ('key any -> unit) -> 'key transf -> unit
*)
val theory_iter : ('key any -> unit) -> 'key theory -> unit
val transf_iter : ('key any -> unit) -> 'key transf -> unit
val metas_iter : ('key any -> unit) -> 'key metas -> unit
val file_iter : ('key any -> unit) -> 'key file -> unit
val session_iter : ('key any -> unit) -> 'key session -> unit
val iter : ('key any -> unit) -> 'key any -> unit

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
End:
*)







open Session

val add_prover_call : ITP_state -> prover_name -> time limit -> ITP_state

type 'args tactic = 'args -> (task list) trans

val apply_tactic : ITP_state -> 'args tactic -> 'args -> ITP_state

val remove_hyp : prsymbol tactic (* [remove_hyp H] remove the hypothesis H from the context *)

val case_analysis : term tactic
(* [case_analysis P] replaces task [H |- G] by two tasks [H, P |-G]  and [H, not P |- G] *)

val assert_tactic : term tactic
(* [assert_tactic P] replaces task [H |- G] by two tasks [H |- P] and [H,P |- G] *)

val exists : term tactic
(* [exists t] replaces task [H |- exists x. G ] by [ H |- G[x <- t]]  *)

val instantiate : (pr_symbol,term) tactic
(* [instantiate (H,t)] replaces task [....,H:forall x.P,... |- G ] by
[ ....,H:forall x.P,...., P[x <- t] |- G ] *)

val induction_on_nat : lsymbol ->



(* display *)


(* to display an ITP state: we need a driver for printing terms *)

display : ITP_state -> driver -> list of strings (* ? *)