(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)

(*******************

This file builds some goals using the API and calls
the alt-ergo prover to check them

Note: the comments of the form BEGIN{id} and END{id} are there for automatic extraction
of the chapter "The Why3 API" of the manual
******************)

(* BEGIN{opening} *)
(* opening the Why3 library *)
open Why3

(* a ground propositional goal: true or false *)
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false
(* END{opening} *)

(* BEGIN{printformula} *)
(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
(* END{printformula} *)


(* a propositional goal: A and B implies A *)

(* BEGIN{declarepropvars} *)
let prop_var_A : Term.lsymbol =
  Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol =
  Term.create_psymbol (Ident.id_fresh "B") []
(* END{declarepropvars} *)
(* BEGIN{declarepropatoms} *)
let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term =
  Term.t_implies (Term.t_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
(* END{declarepropatoms} *)

(* BEGIN{buildtask} *)
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
(* END{buildtask} *)

(* BEGIN{printtask} *)
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
(* END{printtask} *)

(* BEGIN{buildtask2} *)
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
(* END{buildtask2} *)



(* To call a prover, we need to access the Why configuration *)

(* BEGIN{getconf} *)
(* reads the default config file *)
let config : Whyconf.config = Whyconf.init_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config
(* default resource limits *)
let limits =
  Call_provers.{empty_limits with
                limit_time = Whyconf.timelimit main;
                limit_mem = Whyconf.memlimit main }
(* END{getconf} *)

(* BEGIN{getanyaltergo} *)
(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
  (* all provers that have the name "Alt-Ergo" *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
      eprintf "Prover Alt-Ergo not installed or not configured@.";
      exit 1
    end else begin
      printf "Versions of Alt-Ergo found:";
      Whyconf.(Mprover.iter (fun k _ -> printf " %s" k.prover_version) provers);
      printf "@.";
      (* returning an arbitrary one *)
      snd (Whyconf.Mprover.max_binding provers)
    end
(* END{getanyaltergo} *)

(* BEGIN{getaltergo200} *)
(* Specific version 2.5.4 of Alt-Ergo in the config file *)
let _ : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.5.4" in
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
      eprintf "Prover Alt-Ergo 2.5.4 not installed or not configured, using version %s instead@."
        Whyconf.(alt_ergo.prover.prover_version) ;
    alt_ergo (* we don't want to fail this time *)
  end else
    snd (Whyconf.Mprover.max_binding provers)
(* END{getaltergo200} *)

(* BEGIN{getdriver} *)
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)

(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
  try
    Driver.load_driver_for_prover main env alt_ergo
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1
(* END{getdriver} *)

(* BEGIN{callprover} *)
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~limits
       ~config:main
       ~command:alt_ergo.Whyconf.command
       alt_ergo_driver
       task1)

(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, Alt-Ergo answers %a@]@."
    (Call_provers.print_prover_result ?json:None) result1
(* END{callprover} *)

(* BEGIN{calltimelimit} *)
let result2 : Call_provers.prover_result =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~command:alt_ergo.Whyconf.command
       ~config:main
       ~limits:{ limits with Call_provers.limit_time = 10. }
       alt_ergo_driver
       task2)

let () = printf "@[On task 2, Alt-Ergo answers %a in %.2f seconds, %d steps@]@."
  Call_provers.print_prover_answer result1.Call_provers.pr_answer
  result1.Call_provers.pr_time result1.Call_provers.pr_steps
(* END{calltimelimit} *)




(*

An arithmetic goal: 2+2 = 4

*)

(* BEGIN{buildfmla} *)
let two  : Term.term = Term.t_nat_const 2
let four : Term.term = Term.t_nat_const 4
let int_theory : Theory.theory = Env.read_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.term = Term.t_equ two_plus_two four
(* END{buildfmla} *)

(* BEGIN{buildtermalt} *)
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
(* END{buildtermalt} *)

(* BEGIN{buildtaskimport} *)
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
(* END{buildtaskimport} *)

(*
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
*)
let () = printf "@[task 3 created@]@."

let result3 =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~limits
       ~config:main
       ~command:alt_ergo.Whyconf.command
       alt_ergo_driver
       task3)

let () = printf "@[On task 3, Alt-Ergo answers %a@]@."
  (Call_provers.print_prover_result ?json:None) result3

(* quantifiers: let's build "forall x:int. x*x >= 0" *)
(* BEGIN{quantfmla1} *)
let zero : Term.term = Term.t_nat_const 0
let mult_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
(* END{quantfmla1} *)

(* BEGIN{quantfmla2} *)
let var_x : Term.vsymbol =
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
(* END{quantfmla2} *)

(* BEGIN{quantfmla3} *)
let x : Term.term = Term.t_var var_x
let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero]
(* END{quantfmla3} *)

(* BEGIN{quantfmla4} *)
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
(* END{quantfmla4} *)

let task4 = None
let task4 = Task.use_export task4 int_theory
let goal_id4 = Decl.create_prsymbol (Ident.id_fresh "goal4")
let task4 = Task.add_prop_decl task4 Decl.Pgoal goal_id4 fmla4

let result4 =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~limits
       ~config:main
       ~command:alt_ergo.Whyconf.command
       alt_ergo_driver
       task4)

let () = printf "@[On task 4, Alt-Ergo answers %a@]@."
  (Call_provers.print_prover_result ?json:None) result4

(* build a theory with all these goals *)

(* create a theory *)
let () = printf "@[creating theory 'My_theory'@]@."

(* BEGIN{buildth1} *)
let my_theory : Theory.theory_uc =
  Theory.create_theory (Ident.id_fresh "My_theory")
(* END{buildth1} *)

(* add declarations of goals *)

let () = printf "@[adding goal 1@]@."
(* BEGIN{buildth2} *)
let decl_goal1 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1
(* END{buildth2} *)

let () = printf "@[adding goal 2@]@."
(* BEGIN{buildth3} *)
let my_theory : Theory.theory_uc =
  Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc =
  Theory.add_param_decl my_theory prop_var_B
let decl_goal2 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2
(* END{buildth3} *)

(* BEGIN{buildth4} *)
(* helper function: [use th1 th2] insert the equivalent of a
   "use import th2" in theory th1 under construction *)
let use th1 th2 =
  let name = th2.Theory.th_name in
  Theory.close_scope
    (Theory.use_export (Theory.open_scope th1 name.Ident.id_string) th2)
    ~import:true
(* END{buildth4} *)

let () = printf "@[adding goal 3@]@."
(* use import int.Int *)
(* BEGIN{buildth5} *)
let my_theory : Theory.theory_uc = use my_theory int_theory
let decl_goal3 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal3
(* END{buildth5} *)

let () = printf "@[adding goal 4@]@."
(* BEGIN{buildth6} *)
let decl_goal4 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal4
(* END{buildth6} *)

(* closing the theory *)
(* BEGIN{buildth7} *)
let my_theory : Theory.theory = Theory.close_theory my_theory
(* END{buildth7} *)

(* printing the result *)
(* BEGIN{printtheory} *)
let () = printf "@[my new theory is as follows:@\n@\n%a@]@."
                Pretty.print_theory my_theory
(* END{printtheory} *)

(* getting set of task from a theory *)
(* BEGIN{splittheory} *)
let my_tasks : Task.task list =
  List.rev (Task.split_theory my_theory None None)
(* END{splittheory} *)

(* BEGIN{printalltasks} *)
let () =
  printf "Tasks are:@.";
  let _ =
    List.fold_left
      (fun i t -> printf "@[<v 0>== Task %d ==@\n@\n%a@]@." i Pretty.print_task t; i+1)
      1 my_tasks
  in ()
(* END{printalltasks} *)







(*
Local Variables:
compile-command: "make -C ../.. test-api-logic.byte"
End:
*)