Skip to content
Snippets Groups Projects
Commit 90cb7626 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[qed] Removes native:alt-ergo

parent c6c1d1a1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/qed/Makefile
+ 1
− 3
View file @ 90cb7626
......@@ -54,7 +54,6 @@ PLUGIN_CMO:= \
pool kind term \
plib pretty export \
export_whycore \
export_altergo \
export_why3 \
export_coq \
......@@ -67,7 +66,7 @@ PLUGIN_OFLAGS:=
PLUGIN_GENERATED:= $(PLUGIN_DIR)/Qed.mli
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLED)
PLUGIN_DISTRIB_EXTERNAL:= Makefile
PLUGIN_DISTRIB_EXTERNAL:= Makefile
include $(FRAMAC_SHARE)/Makefile.dynamic
......@@ -87,7 +86,6 @@ QED_API= \
pool.mli kind.mli term.mli \
plib.mli pretty.mli engine.mli export.mli \
export_whycore.mli \
export_altergo.mli \
export_why3.mli \
export_coq.mli \
......
src/plugins/qed/export_altergo.ml deleted 100644 → 0
+ 0
− 374
View file @ c6c1d1a1
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2021 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Exportation Engine for Alt-Ergo --- *)
(* -------------------------------------------------------------------------- *)
open Logic
open Format
open Plib
open Engine
open Export
module Make(T : Term) =
struct
open T
module E = Export_whycore.Make(T)
module Env = E.Env
module ADT = T.ADT
module Field = T.Field
module Fun = T.Fun
type trigger = (T.var,Fun.t) ftrigger
type typedef = (tau,Field.t,Fun.t) Engine.ftypedef
class virtual engine =
object(self)
inherit E.engine
(* -------------------------------------------------------------------------- *)
(* --- Types --- *)
(* -------------------------------------------------------------------------- *)
method t_atomic (_:tau) = true
method pp_array fmt data =
fprintf fmt "%a farray" self#pp_tau data
method pp_farray fmt key data =
fprintf fmt "(%a,%a) farray" self#pp_tau key self#pp_tau data
method virtual get_typedef : ADT.t -> tau option
method virtual set_typedef : ADT.t -> tau -> unit
method pp_datatype adt fmt ts =
match self#get_typedef adt with
| Some def ->
let t = Kind.tmap (Array.of_list ts) def in
self#pp_tau fmt t
| None ->
match ts with
| [] -> pp_print_string fmt (self#datatype adt)
| [t] -> fprintf fmt "%a@ %s" self#pp_tau t (self#datatype adt)
| t::ts ->
fprintf fmt "@[<hov 2>(%a" self#pp_tau t ;
List.iter (fun t -> fprintf fmt ",@,%a" self#pp_tau t) ts ;
fprintf fmt ")@ %s@]" (self#datatype adt)
(* -------------------------------------------------------------------------- *)
(* --- Primitives --- *)
(* -------------------------------------------------------------------------- *)
method callstyle = CallVar
method pp_array_cst fmt (key : tau) v =
try
let elt = T.typeof v in
let tau = Array(key,elt) in
fprintf fmt "@[<hov 2>(const(%a)@ : %a)@]"
self#pp_flow v self#pp_tau tau
with Not_found ->
fprintf fmt "const(%a)" self#pp_flow v
(* -------------------------------------------------------------------------- *)
(* --- Arithmetics --- *)
(* -------------------------------------------------------------------------- *)
method pp_int amode fmt z = match amode with
| Aint -> pp_print_string fmt (Z.to_string z)
| Areal -> fprintf fmt "%s.0" (Z.to_string z)
method pp_real fmt r =
if Z.equal r.Q.den Z.one then
self#pp_int Areal fmt r.Q.num
else
fprintf fmt "(%a@ / %a)"
(self#pp_int Areal) r.Q.num
(self#pp_int Areal) r.Q.den
method op_real_of_int = Call "real_of_int"
method op_minus (_:amode) = Op "-"
method op_add (_:amode) = Assoc "+"
method op_sub (_:amode) = Assoc "-"
method op_mul (_:amode) = Assoc "*"
method op_div = function Aint -> Call "div" | Areal -> Op "/"
method op_mod = function Aint -> Call "mod" | Areal -> Call "rmod"
method op_eq cmode _amode =
match cmode with
| Cprop -> Op "="
| Cterm -> Call "eqb"
method op_neq cmode _amode =
match cmode with
| Cprop -> Op "<>"
| Cterm -> Call "neqb"
method op_lt cmode amode =
match cmode , amode with
| Cprop , _ -> Op "<"
| Cterm , Aint -> Call "zlt"
| Cterm , Areal -> Call "rlt"
method op_leq cmode amode =
match cmode , amode with
| Cprop , _ -> Op "<="
| Cterm , Aint -> Call "zleq"
| Cterm , Areal -> Call "rleq"
(* -------------------------------------------------------------------------- *)
(* --- Logical Connectives --- *)
(* -------------------------------------------------------------------------- *)
method e_true _ = "true"
method e_false _ = "false"
method op_not = function Cprop -> Op "not" | Cterm -> Call "notb"
method op_and = function Cprop -> Assoc "and" | Cterm -> Call "andb"
method op_or = function Cprop -> Assoc "or" | Cterm -> Call "orb"
method op_imply = function Cprop -> Assoc "->" | Cterm -> Call "implb"
method op_equiv = function Cprop -> Op "<->" | Cterm -> Call "eqb"
method op_equal = function Cprop -> Op "=" | Cterm -> Call "eqb"
method op_noteq = function Cprop -> Op "<>" | Cterm -> Call "neqb"
(* -------------------------------------------------------------------------- *)
(* --- Conditional --- *)
(* -------------------------------------------------------------------------- *)
method pp_conditional fmt a b c =
match Export.pmode self#mode with
| Negative ->
let cond = T.e_and [T.e_imply [a] b ; T.e_imply [T.e_not a] c] in
self#pp_flow fmt cond
| Positive ->
let cond = T.e_or [T.e_and [a;b] ; T.e_and [T.e_not a;c]] in
self#pp_flow fmt cond
| Boolean ->
begin
fprintf fmt "@[<hov 2>match_bool(" ;
self#with_mode Mterm (fun _ -> self#pp_atom fmt a) ;
fprintf fmt ",@ %a" self#pp_atom b ;
fprintf fmt ",@ %a" self#pp_atom c ;
fprintf fmt ")@]" ;
end
(* -------------------------------------------------------------------------- *)
(* --- Records --- *)
(* -------------------------------------------------------------------------- *)
method op_record = "{" , "}"
(* -------------------------------------------------------------------------- *)
(* --- Atomicity --- *)
(* -------------------------------------------------------------------------- *)
method op_spaced = is_identifier
method is_atomic e =
match T.repr e with
| Kint z -> Z.leq Z.zero z
| Kreal _ -> true
| Apply _ -> true
| Acst _ | Aset _ | Aget _ | Fun _ -> true
| _ -> T.is_simple e
(* -------------------------------------------------------------------------- *)
(* --- Lets --- *)
(* -------------------------------------------------------------------------- *)
method typeof e = T.typeof e
val mutable quantify_let = false
method set_quantify_let e = quantify_let <- e
method pp_let fmt pmode x e =
try
let tau = self#typeof e in
match pmode with
| Positive when quantify_let ->
fprintf fmt "@[<hov 4>forall %s : %a. %s = %a ->@]@ "
x self#pp_tau tau x self#pp_flow e
| Negative when quantify_let ->
fprintf fmt "@[<hov 4>exists %s : %a. %s = %a and@]@ "
x self#pp_tau tau x self#pp_flow e
| _ ->
fprintf fmt "@[<hov 4>let %s = %a : %a in@]@ "
x self#pp_atom e self#pp_tau tau
with Not_found ->
fprintf fmt "@[<hov 4>let %s = %a in@]@ "
x self#pp_flow e
(* -------------------------------------------------------------------------- *)
(* --- Binders --- *)
(* -------------------------------------------------------------------------- *)
method pp_forall tau fmt = function
| [] -> ()
| x::xs ->
fprintf fmt "@[<hov 2>forall %a" self#pp_var x ;
List.iter (fun x -> fprintf fmt ",@,%a" self#pp_var x) xs ;
fprintf fmt "@ : %a.@]" self#pp_tau tau ;
method pp_intros tau fmt = function
| [] -> ()
| x::xs ->
fprintf fmt "@[<hov 2>forall %a" self#pp_var x ;
List.iter (fun x -> fprintf fmt ",@,%a" self#pp_var x) xs ;
fprintf fmt "@ : %a@]" self#pp_tau tau ;
method pp_exists tau fmt = function
| [] -> ()
| x::xs ->
fprintf fmt "@[<hov 2>exists %a" self#pp_var x ;
List.iter (fun x -> fprintf fmt ",@,%a" self#pp_var x) xs ;
fprintf fmt "@ : %a.@]" self#pp_tau tau ;
method pp_trigger fmt t =
let rec pretty fmt = function
| TgAny -> assert false
| TgVar x -> self#pp_var fmt (self#find x)
| TgGet(t,k) -> fprintf fmt "@[<hov 2>%a[%a]@]" pretty t pretty k
| TgSet(t,k,v) -> fprintf fmt "@[<hov 2>%a[%a@ <- %a]@]" pretty t pretty k pretty v
| TgFun(f,ts) -> call Cterm f fmt ts
| TgProp(f,ts) -> call Cprop f fmt ts
and call mode f fmt ts =
match self#link f, mode with
| F_call f, _
| F_bool_prop (f,_), Cterm
| F_bool_prop (_,f), Cprop ->
Plib.pp_call_var ~f pretty fmt ts
| F_left f, _ -> Plib.pp_fold_call ~f pretty fmt ts
| F_right f, _ -> Plib.pp_fold_call_rev ~f pretty fmt (List.rev ts)
| F_assoc op, _ -> Plib.pp_assoc ~e:"?" ~op pretty fmt ts
| F_subst s, _ -> Plib.substitute_list pretty s fmt ts
| F_list(fc,fn) , _ ->
let rec plist fc fn fmt = function
| [] -> pp_print_string fmt fn
| x::xs ->
fprintf fmt "[<hov 2>%s(@,%a,@,%a)@]" fc
pretty x (plist fc fn) xs
in plist fc fn fmt ts
in fprintf fmt "@[<hov 2>%a@]" pretty t
method pp_goal fmt p = self#pp_prop fmt p
(* -------------------------------------------------------------------------- *)
(* --- Declarations --- *)
(* -------------------------------------------------------------------------- *)
method pp_declare_adt fmt adt = function
| 0 -> fprintf fmt "type %s" (self#datatype adt)
| 1 -> fprintf fmt "type %a %s" self#pp_tvar 1 (self#datatype adt)
| n ->
begin
fprintf fmt "type (%a" self#pp_tvar 1 ;
for i=2 to n do fprintf fmt ",%a" self#pp_tvar i done ;
fprintf fmt ") %s" (self#datatype adt) ;
end
method pp_declare_def fmt adt n def =
begin
fprintf fmt "(* @[<hov 4>inlined type " ;
self#pp_declare_adt fmt adt n ;
fprintf fmt "@ = %a@] *)" self#pp_tau def ;
self#set_typedef adt def ;
end
method pp_declare_sum fmt adt n cases =
let is_enum = function (_,[]) -> true | _ -> false in
if List.for_all is_enum cases then
begin
fprintf fmt "@[<hov 4>" ;
self#pp_declare_adt fmt adt n ;
Plib.iteri
(fun index (c,_) -> match index with
| Ifirst | Isingle ->
fprintf fmt " = %s" (link_name (self#link c))
| Imiddle | Ilast ->
fprintf fmt "@ | %s" (link_name (self#link c))
) cases ;
fprintf fmt "@]"
end
else
begin
self#pp_declare_adt fmt adt n ;
pp_print_newline fmt () ;
let result = Data(adt,Kind.type_params n) in
List.iter
(fun (c,ts) ->
self#declare_signature fmt c ts result
) cases ;
let rank = "rank_" ^ self#datatype adt in
fprintf fmt "logic %s : %a -> int@\n" rank self#pp_tau result ;
Plib.iterk
(fun k (c,ts) ->
fprintf fmt "@[<hov 2>axiom %s_%d:@ " rank k ;
let xs = Plib.mapk
(fun k t ->
fprintf fmt "forall x%d:%a.@ " k self#pp_tau t ;
Printf.sprintf "x%d" k) ts
in
let f = link_name (self#link c) in
fprintf fmt "%s(%a)=%d@]@\n" rank
(Plib.pp_call_var ~f pp_print_string)
xs k
) cases ;
end
method declare_signature fmt f ts t =
begin
fprintf fmt "@[<hv 4>logic %s :@ " (link_name (self#link f)) ;
if ts <> [] then
begin
Plib.pp_listcompact ~sep:"," self#pp_tau fmt ts ;
fprintf fmt "@ -> " ;
end ;
fprintf fmt "%a@]@\n" self#pp_tau t
end
method declare_definition fmt f xs t e =
self#global
begin fun () ->
let cmode = Export.ctau t in
fprintf fmt "@[<hv 4>%a@,(" (self#pp_declare_symbol cmode) f ;
Plib.pp_listsep ~sep:","
(fun fmt x ->
let a = self#bind x in
let t = T.tau_of_var x in
fprintf fmt "%a:%a" self#pp_var a self#pp_tau t
) fmt xs ;
match cmode with
| Cprop ->
fprintf fmt ") =@ @[<hov 0>%a@]@]@\n"
self#pp_prop e
| Cterm ->
fprintf fmt ") :@ %a =@ @[<hov 0>%a@]@]@\n"
self#pp_tau t (self#pp_expr t) e
end
end
end
src/plugins/qed/export_altergo.mli deleted 100644 → 0
+ 0
− 74
View file @ c6c1d1a1
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2021 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Logic
open Format
open Plib
open Engine
(** Exportation Engine for Alt-Ergo.
Provides a full {{:Export.S.engine-c.html}engine}
from a {{:Export.S.linker-c.html}linker}. *)
module Make(T : Term) :
sig
open T
module Env : Engine.Env with type term := term
type trigger = (T.var,Fun.t) Engine.ftrigger
type typedef = (tau,Field.t,Fun.t) Engine.ftypedef
class virtual engine :
object
method set_quantify_let : bool -> unit
method virtual get_typedef : ADT.t -> tau option
method virtual set_typedef : ADT.t -> tau -> unit
method typeof : term -> tau (** Defaults to T.typeof *)
inherit [Z.t,ADT.t,Field.t,Fun.t,tau,var,term,Env.t] Engine.engine
method marks : Env.t * T.marks
method op_spaced : string -> bool
method op_record : string * string
method pp_forall : tau -> string list printer
method pp_intros : tau -> string list printer
method pp_exists : tau -> string list printer
method pp_param : (string * tau) printer
method pp_trigger : (var,Fun.t) ftrigger printer
method pp_declare_symbol : cmode -> Fun.t printer
method pp_declare_adt : formatter -> ADT.t -> int -> unit
method pp_declare_def : formatter -> ADT.t -> int -> tau -> unit
method pp_declare_sum : formatter -> ADT.t -> int -> (Fun.t * tau list) list -> unit
method pp_goal : formatter -> term -> unit
method declare_type : formatter -> ADT.t -> int -> typedef -> unit
method declare_prop : kind:string -> formatter -> string -> T.var list -> trigger list list -> term -> unit
method declare_axiom : formatter -> string -> var list -> trigger list list -> term -> unit
method declare_signature : formatter -> Fun.t -> tau list -> tau -> unit
method declare_definition : formatter -> Fun.t -> var list -> tau -> term -> unit
end
end
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