Commit 3e857fa1 authored by MARCHE Claude's avatar MARCHE Claude

db

parent f8e88c7e
This diff is collapsed.
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** Proof database *)
(** {1 data types} *)
(** prover info *)
type prover
val prover_from_id : string -> prover
(** status of an external proof attempt *)
type proof_status =
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| Failure (** external prover call failed *)
type proof_attempt
type goal
type transf
type theory
type file
type goal_parent =
| Theory of theory
| Transf of transf
(** proof_attempt accessors *)
val prover : proof_attempt -> prover
val proof_goal : proof_attempt -> goal
val status : proof_attempt -> proof_status
val proof_obsolete : proof_attempt -> bool
val time : proof_attempt -> float
val edited_as : proof_attempt -> string
(** goal accessors *)
val parent : goal -> goal_parent
val task : goal -> string (* checksum *)
val proved : goal -> bool
val external_proofs: (string, proof_attempt) Hashtbl.t
val transformations : (string, transf) Hashtbl.t
(** transf accessors *)
val parent_goal : transf -> goal
val transf_name : transf -> string
val subgoals : transf -> goal list
(** theory accessors *)
val theory_name : theory -> string
val goals : theory -> goal list
val verified : theory -> bool
(** file accessors *)
val file_name : file -> string
val theories : file -> theory list
(** {1 The persistent database} *)
val init_base : string -> unit
(** opens or creates the current database, from given file name *)
val files : unit -> file list
(** returns the current set of files *)
(** {1 Updates} *)
......@@ -991,7 +991,7 @@ let (_ : GtkSignal.id) =
match goals_view#selection#get_selected_rows with
| [p] -> select_row p
| [] -> ()
| _ -> assert false (* multi-selection is disabled *)
| _ -> ()
end
let () = w#add_accel_group accel_group
......
theory Test
theory TestInt
use import int.Int
......@@ -19,6 +19,11 @@ theory Test
goal Test6: 2+3 = 5 and forall x:int. x*x >= 0
end
theory TestDiv
use import int.Int
use int.EuclideanDivision
goal EDiv1: EuclideanDivision.div 1 2 = 0
......@@ -31,6 +36,10 @@ theory Test
goal CDiv2: ComputerDivision.div (-1) 2 = 0
end
theory TestReal
use import real.Real
goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0
......@@ -39,6 +48,10 @@ theory Test
goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
end
theory TestFloat
use import floating_point.Rounding
use floating_point.Single
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment