diff --git a/src/lib/dune b/src/lib/dune index f91c8ecea..34898b491 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -46,7 +46,7 @@ ; modules that make up the lib (modules ; frontend - Translate D_loop D_state_option Frontend Parsed_interface Models + Translate D_loop D_state_option Frontend Models ; reasoners Ac Arith Arrays_rel Bitv Ccx Shostak Relation Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel @@ -56,7 +56,7 @@ Sig Sig_rel Theory Uf Use Domains Domains_intf Rel_utils Bitlist ; structures Commands Errors Explanation Fpa_rounding - Parsed Profiling Satml_types Symbols + Profiling Satml_types Symbols Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal ; util Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml deleted file mode 100644 index c34012d9b..000000000 --- a/src/lib/frontend/parsed_interface.ml +++ /dev/null @@ -1,338 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -open Parsed - -(* helper functions *) - -let mk_localized pp_loc pp_desc = { pp_loc ; pp_desc } - -let mk_infix e1 op e2 = PPinfix (e1, op, e2) - -let mk_prefix op e = PPprefix (op, e) - -(** Declaration of types **) - -let mk_non_rec_type_decl loc ty_vars ty ty_kind = - TypeDecl [ loc, ty_vars, ty, ty_kind ] - -let mk_rec_type_decl l = - TypeDecl l - -let mk_abstract_type_decl loc ty_vars ty = - mk_non_rec_type_decl loc ty_vars ty Abstract - -let mk_enum_type_decl loc ty_vars ty enums = - mk_non_rec_type_decl loc ty_vars ty (Enum enums) - -let mk_algebraic_type_decl loc ty_vars ty enums = - try - let l = - List.rev_map - (fun (c, l) -> - if l != [] then raise Exit; - c - )enums - in - mk_non_rec_type_decl loc ty_vars ty (Enum (List.rev l)) - with Exit -> - mk_non_rec_type_decl loc ty_vars ty (Algebraic enums) - -let mk_record_type_decl loc ty_vars ty ?(constr="{") fields = - mk_non_rec_type_decl loc ty_vars ty (Record (constr, fields)) - - -(** Declaration of symbols, functions, predicates, and goals *) - -let mk_logic loc is_ac named_idents ty = - Logic (loc , is_ac, named_idents, ty) - -let mk_function_def loc named_ident args ty expr = - Function_def (loc, named_ident, args, ty, expr) - -let mk_mut_rec_def l = - MutRecDefs l - -let mk_ground_predicate_def loc named_ident expr = - Predicate_def (loc, named_ident, [], expr) - -let mk_non_ground_predicate_def loc named_ident args expr = - Predicate_def (loc, named_ident, args, expr) - -let mk_goal loc name expr = - Goal (loc, name, expr) - -let mk_check_sat loc name expr = - Check_sat (loc, name, expr) - -(** Declaration of theories, generic axioms and rewriting rules **) - -let mk_theory loc name ext expr = - Theory (loc, name, ext, expr) - -let mk_generic_axiom loc name expr = - Axiom (loc, name, Util.Default, expr) - -let mk_rewriting loc name expr = - Rewriting (loc, name, expr) - - -(** Declaration of theory axioms and case-splits **) - -let mk_theory_axiom loc name expr = - Axiom (loc, name, Util.Propagator, expr) - -let mk_theory_case_split loc name expr = - Axiom (loc, name, Util.Default, expr) - -(** Declaration of stack assertions commands *) - -let mk_push loc n = - Push (loc, n) - -let mk_pop loc n = - Pop (loc, n) - -(** Declaration of optimization of objective functions. *) - -let mk_optimize loc expr is_max = - Optimize (loc, expr, is_max) - -(** Making pure and logic types *) - -let int_type = PPTint - -let bool_type = PPTbool - -let real_type = PPTreal - -let unit_type = PPTunit - -let mk_bitv_type size = - PPTbitv(int_of_string size) - -let mk_external_type loc args ty = - PPTexternal (args, ty, loc) - -let mk_logic_type args_ty res_ty = - match res_ty with - | None -> PPredicate args_ty - | Some res -> PFunction (args_ty, res) - -let mk_var_type loc alpha = - PPTvarid (alpha, loc) - - -(** Making arithmetic expressions and predicates **) - -let mk_int_const loc n = - mk_localized loc (PPconst (ConstInt n)) - -let mk_real_const loc r = - mk_localized loc (PPconst (ConstReal r)) - -let mk_add loc e1 e2 = - mk_localized loc (mk_infix e1 PPadd e2) - -let mk_sub loc e1 e2 = - mk_localized loc (mk_infix e1 PPsub e2) - - -let mk_mul loc e1 e2 = - mk_localized loc (mk_infix e1 PPmul e2) - -let mk_div loc e1 e2 = - mk_localized loc (mk_infix e1 PPdiv e2) - -let mk_mod loc e1 e2 = - mk_localized loc (mk_infix e1 PPmod e2) - -let mk_pow_int loc e1 e2 = - mk_localized loc (mk_infix e1 PPpow_int e2) - -let mk_pow_real loc e1 e2 = - mk_localized loc (mk_infix e1 PPpow_real e2) - -let mk_minus loc e = - mk_localized loc (mk_prefix PPneg e) - -let mk_pred_lt loc e1 e2 = - mk_localized loc (mk_infix e1 PPlt e2) - -let mk_pred_le loc e1 e2 = - mk_localized loc (mk_infix e1 PPle e2) - -let mk_pred_gt loc e1 e2 = - mk_localized loc (mk_infix e1 PPgt e2) - -let mk_pred_ge loc e1 e2 = - mk_localized loc (mk_infix e1 PPge e2) - - -(** Making Record expressions **) - -let mk_record loc fields = - mk_localized loc (PPrecord fields) - -let mk_with_record loc e fields = - mk_localized loc (PPwith(e, fields)) - -let mk_dot_record loc e label = - mk_localized loc (PPdot(e, label)) - - -(** Making Array expressions **) - -let mk_array_get loc e1 e2 = - mk_localized loc (PPget(e1, e2)) - -let mk_array_set loc e1 e2 e3 = - mk_localized loc (PPset(e1, e2, e3)) - - -(** Making Bit-vector expressions **) - -let mk_bitv_const = - let check_binary_mode s = - String.iter - (fun x -> - match x with - | '0' | '1' -> () - | _ -> raise Parsing.Parse_error) s; - s - in fun loc const -> - mk_localized loc (PPconst (ConstBitv (check_binary_mode const))) - -let mk_bitv_extract loc e i j = - mk_localized loc (PPextract (e, int_of_string i, int_of_string j)) - -let mk_bitv_concat loc e1 e2 = - mk_localized loc (PPconcat(e1, e2)) - - -(** Making Boolean / Propositional expressions **) - -let mk_true_const loc = - mk_localized loc (PPconst ConstTrue) - -let mk_false_const loc = - mk_localized loc (PPconst ConstFalse) - -let mk_and loc e1 e2 = - mk_localized loc (mk_infix e1 PPand e2) - -let mk_or loc e1 e2 = - mk_localized loc (mk_infix e1 PPor e2) - -let mk_xor loc e1 e2 = - mk_localized loc (mk_infix e1 PPxor e2) - -let mk_iff loc e1 e2 = - mk_localized loc (mk_infix e1 PPiff e2) - -let mk_implies loc e1 e2 = - mk_localized loc (mk_infix e1 PPimplies e2) - -let mk_not loc e = - mk_localized loc (mk_prefix PPnot e) - -let mk_pred_eq loc e1 e2 = - mk_localized loc (mk_infix e1 PPeq e2) - -let mk_pred_not_eq loc e1 e2 = - mk_localized loc (mk_infix e1 PPneq e2) - -let mk_distinct loc e2 = - match e2 with - | [a; b] -> mk_pred_not_eq loc a b - | _ -> mk_localized loc (PPdistinct e2) - -(** Making quantified formulas **) - -let mk_forall loc vs_ty triggers filters expr = - mk_localized loc (PPforall_named (vs_ty, triggers, filters, expr)) - -let mk_exists loc vs_ty triggers filters expr = - mk_localized loc (PPexists_named (vs_ty, triggers, filters, expr)) - - -(** Naming and casting types of expressions **) - -let mk_named loc name e = - mk_localized loc (PPnamed (name, e)) - - -let mk_type_cast loc e ty = - mk_localized loc (PPcast(e,ty)) - - -(** Making vars, applications, if-then-else, and let expressions **) - -let mk_var loc var = - mk_localized loc (PPvar var) - -let mk_application loc app args = - mk_localized loc (PPapp (app, args)) - -let mk_pattern pat_loc pat_app args = - { pat_loc ; pat_desc = (pat_app, args) } - -let mk_ite loc cond th el = - mk_localized loc (PPif (cond, th, el)) - -let mk_let loc binders e = - mk_localized loc (PPlet (binders, e)) - -let mk_void loc = - mk_localized loc (PPconst ConstVoid) - - -(** Making particular expression used in semantic triggers **) - -let mk_in_interval loc expr low_br ei ej up_br = - mk_localized loc (PPinInterval (expr, not low_br, ei ,ej, up_br)) - -let mk_maps_to loc v expr = - mk_localized loc (PPmapsTo (v, expr)) - - -(** Making cuts and checks **) - -let mk_check loc expr = - mk_localized loc (PPcheck expr) - -let mk_cut loc expr = - mk_localized loc (PPcut expr) - -let mk_match loc expr cases = - mk_localized loc (PPmatch (expr, cases)) - -let mk_algebraic_test loc expr constr = - mk_localized loc (PPisConstr (expr, constr)) - -let mk_algebraic_project loc expr constr = - mk_localized loc (PPproject (expr, constr)) diff --git a/src/lib/frontend/parsed_interface.mli b/src/lib/frontend/parsed_interface.mli deleted file mode 100644 index ea45881c2..000000000 --- a/src/lib/frontend/parsed_interface.mli +++ /dev/null @@ -1,258 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -open Parsed - -(** Declaration of types **) - -val mk_abstract_type_decl : - Loc.t -> string list -> string -> decl - [@ocaml.ppwarning "TODO: add documentation for every function in this file"] - -val mk_enum_type_decl : Loc.t -> string list -> string -> string list -> decl - -val mk_algebraic_type_decl : - Loc.t -> string list -> string -> - (string * (string * ppure_type) list) list -> decl - -val mk_record_type_decl : - Loc.t -> string list -> string -> ?constr : string -> - (string * ppure_type) list -> decl - -val mk_rec_type_decl : Parsed.type_decl list -> decl - -(** Declaration of symbols, functions, predicates, and goals *) - -val mk_logic : - Loc.t -> Symbols.name_kind -> (string * string) list -> plogic_type -> decl - -val mk_function_def : - Loc.t -> - string * string -> - (Loc.t * string * ppure_type) list -> - ppure_type -> lexpr -> decl - -val mk_ground_predicate_def : - Loc.t -> string * string -> lexpr -> decl - -val mk_non_ground_predicate_def : - Loc.t -> - string * string -> - (Loc.t * string * ppure_type) list -> lexpr -> decl - -val mk_mut_rec_def : - (Loc.t - * (string * string) - * (Loc.t * string * ppure_type) list - * ppure_type option - * lexpr - ) list -> decl - -val mk_goal : Loc.t -> string -> lexpr -> decl - -val mk_check_sat : Loc.t -> string -> lexpr -> decl - -(** Declaration of theories, generic axioms and rewriting rules **) - -val mk_theory : Loc.t -> string -> string -> decl list -> decl - -val mk_generic_axiom : Loc.t -> string -> lexpr -> decl - -val mk_rewriting : Loc.t -> string -> lexpr list -> decl - - -(** Declaration of theory axioms and case-splits **) - -val mk_theory_axiom : Loc.t -> string -> lexpr -> decl - -val mk_theory_case_split : Loc.t -> string -> lexpr -> decl - -(** Declaration of stack assertions commands *) - -val mk_push : Loc.t -> int -> decl - -val mk_pop : Loc.t -> int -> decl - -(** Declaration of optimization of objective functions. *) - -val mk_optimize : Loc.t -> lexpr -> bool -> decl - -(** Making pure and logic types *) - -val int_type : ppure_type - -val bool_type : ppure_type - -val real_type : ppure_type - -val unit_type : ppure_type - -val mk_bitv_type : string -> ppure_type - -val mk_external_type : Loc.t -> ppure_type list -> string -> ppure_type - -val mk_var_type : Loc.t -> string -> ppure_type - -val mk_logic_type : ppure_type list -> ppure_type option -> plogic_type - - -(** Making arithmetic expressions and predicates **) - -val mk_int_const : Loc.t -> string -> lexpr - -val mk_real_const : Loc.t -> Numbers.Q.t -> lexpr - -val mk_add : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_sub : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_mul : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_div : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_mod : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_pow_int : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_pow_real : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_minus : Loc.t -> lexpr -> lexpr - -val mk_pred_lt : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_pred_le : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_pred_gt : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_pred_ge : Loc.t -> lexpr -> lexpr -> lexpr - - -(** Making Record expressions **) - -val mk_record : Loc.t -> (string * lexpr) list -> lexpr - -val mk_with_record : Loc.t -> lexpr -> (string * lexpr) list -> lexpr - -val mk_dot_record : Loc.t -> lexpr -> string -> lexpr - - -(** Making Array expressions **) - -val mk_array_get : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_array_set : - Loc.t -> lexpr -> lexpr -> lexpr -> lexpr - - -(** Making Bit-vector expressions **) - -val mk_bitv_const : Loc.t -> string -> lexpr - -val mk_bitv_extract : Loc.t -> lexpr -> string -> string -> lexpr - -val mk_bitv_concat : Loc.t -> lexpr -> lexpr -> lexpr - - -(** Making Boolean / Propositional expressions **) - -val mk_true_const : Loc.t -> lexpr - -val mk_false_const : Loc.t -> lexpr - -val mk_and : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_or : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_xor : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_iff : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_implies : Loc.t -> lexpr -> lexpr -> lexpr - -val mk_not : Loc.t -> lexpr -> lexpr - -val mk_distinct : Loc.t -> lexpr list -> lexpr - -val mk_pred_eq : Loc.t -> lexpr -> lexpr -> lexpr -val mk_pred_not_eq : Loc.t -> lexpr -> lexpr -> lexpr - - -(** Making quantified formulas **) - -val mk_forall : - Loc.t -> - (string * string * ppure_type) list -> - (lexpr list * bool) list -> - lexpr list -> lexpr -> lexpr - -val mk_exists : - Loc.t -> - (string * string * ppure_type) list -> - (lexpr list * bool) list -> - lexpr list -> lexpr -> lexpr - - -(** Naming and casting types of expressions **) - -val mk_type_cast : Loc.t -> lexpr -> ppure_type -> lexpr - -val mk_named : Loc.t -> string -> lexpr -> lexpr - - -(** Making vars, applications, if-then-else, and let expressions **) - -val mk_var : Loc.t -> string -> lexpr - -val mk_application : Loc.t -> string -> lexpr list -> lexpr - -val mk_pattern : Loc.t -> string -> string list -> pattern - -val mk_ite : Loc.t -> lexpr -> lexpr -> lexpr -> lexpr - -val mk_let : Loc.t -> (string * lexpr) list -> lexpr -> lexpr - -val mk_void : Loc.t -> lexpr - - -(** Making particular expression used in semantic triggers **) - -val mk_in_interval : Loc.t -> lexpr -> bool -> lexpr -> lexpr -> bool -> lexpr - -val mk_maps_to : Loc.t -> string -> lexpr -> lexpr - - -(** Making cuts and checks **) - -val mk_check : Loc.t -> lexpr -> lexpr - -val mk_cut : Loc.t -> lexpr -> lexpr - -val mk_match : Loc.t -> lexpr -> (pattern * lexpr) list -> lexpr - -val mk_algebraic_test : Loc.t -> lexpr -> string -> lexpr - -val mk_algebraic_project : Loc.t -> lexpr -> string -> lexpr diff --git a/src/lib/structures/parsed.ml b/src/lib/structures/parsed.ml deleted file mode 100644 index d58dde682..000000000 --- a/src/lib/structures/parsed.ml +++ /dev/null @@ -1,280 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type constant = - | ConstBitv of string - | ConstInt of string - | ConstReal of Numbers.Q.t - | ConstTrue - | ConstFalse - | ConstVoid - -let pp_const fmt = - let open Format in - function - | ConstBitv s -> fprintf fmt "%s" s - | ConstInt s -> fprintf fmt "%s" s - | ConstReal v -> fprintf fmt "%s" (Numbers.Q.to_string v) - | ConstTrue -> fprintf fmt "true" - | ConstFalse -> fprintf fmt "false" - | ConstVoid -> fprintf fmt "void" - -type pp_infix = - | PPand | PPor | PPxor | PPimplies | PPiff - | PPlt | PPle | PPgt | PPge | PPeq | PPneq - | PPadd | PPsub | PPmul | PPdiv | PPmod - | PPpow_int | PPpow_real - -let pp_inf_op fmt = - let open Format in - function - | PPand -> fprintf fmt "and" - | PPor -> fprintf fmt "or" - | PPxor -> fprintf fmt "xor" - | PPimplies -> fprintf fmt "implies" - | PPiff -> fprintf fmt "iff" - | PPlt -> fprintf fmt "lt" - | PPle -> fprintf fmt "le" - | PPgt -> fprintf fmt "gt" - | PPge -> fprintf fmt "ge" - | PPeq -> fprintf fmt "eq" - | PPneq -> fprintf fmt "neq" - | PPadd -> fprintf fmt "add" - | PPsub -> fprintf fmt "sub" - | PPmul -> fprintf fmt "mul" - | PPdiv -> fprintf fmt "div" - | PPmod -> fprintf fmt "mod" - | PPpow_int -> fprintf fmt "pow_int" - | PPpow_real -> fprintf fmt "pow_real" - -type pp_prefix = - | PPneg | PPnot - -let pp_pre_op fmt = - let open Format in - function - | PPneg -> fprintf fmt "-" - | PPnot -> fprintf fmt "not" - -type ppure_type = - | PPTint - | PPTbool - | PPTreal - | PPTunit - | PPTbitv of int - | PPTvarid of string * Loc.t - | PPTexternal of ppure_type list * string * Loc.t - -let pp_sep_comma fmt () = Format.fprintf fmt "," - -let pp_sep_space fmt () = Format.fprintf fmt " " - -let rec pp_ppure_type fmt t = - Format.fprintf fmt "%s" - (match t with - | PPTint -> "int" - | PPTbool -> "bool" - | PPTreal -> "real" - | PPTunit -> "unit" - | PPTbitv i -> Format.asprintf "bitv[%d]" i - | PPTvarid (s, _) -> Format.asprintf "varid[%s]" s - | PPTexternal (ppl, s, _) -> - Format.asprintf "%a %s" pp_ppure_type_list ppl s - ) - -and pp_ppure_type_list fmt tl = - Format.fprintf fmt "@[%a@]" - (Format.pp_print_list ~pp_sep:pp_sep_comma (fun fmt t -> - Format.fprintf fmt "%a" pp_ppure_type t)) tl - -and pp_str_ppure_type_list fmt tl = - Format.fprintf fmt "@[%a@]" - (Format.pp_print_list ~pp_sep:pp_sep_comma (fun fmt (s, t) -> - Format.fprintf fmt "(%s, %a)" s pp_ppure_type t)) tl - -and pp_str_str_ppure_type_list fmt tl = - Format.fprintf fmt "@[%a@]" - (Format.pp_print_list ~pp_sep:pp_sep_comma (fun fmt (s1, s2, t) -> - Format.fprintf fmt "(%s, %s, %a)" s1 s2 pp_ppure_type t)) tl - -type pattern = - { pat_loc : Loc.t; pat_desc : string * string list } - -type lexpr = - { pp_loc : Loc.t; pp_desc : pp_desc } - -and pp_desc = - | PPvar of string - | PPapp of string * lexpr list - | PPmapsTo of string * lexpr - | PPinInterval of lexpr * bool * lexpr * lexpr * bool - (* bool = true <-> interval is_open *) - - | PPdistinct of lexpr list - | PPconst of constant - | PPinfix of lexpr * pp_infix * lexpr - | PPprefix of pp_prefix * lexpr - | PPget of lexpr * lexpr - | PPset of lexpr * lexpr * lexpr - | PPdot of lexpr * string - | PPrecord of (string * lexpr) list - | PPwith of lexpr * (string * lexpr) list - | PPextract of lexpr * int * int - | PPconcat of lexpr * lexpr - | PPif of lexpr * lexpr * lexpr - | PPforall of - (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr - | PPexists of - (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr - | PPforall_named of - (string * string * ppure_type) list * (lexpr list * bool) list * - lexpr list * lexpr - | PPexists_named of - (string * string * ppure_type) list * (lexpr list * bool) list * - lexpr list * lexpr - | PPnamed of string * lexpr - | PPlet of (string * lexpr) list * lexpr - | PPcheck of lexpr - | PPcut of lexpr - | PPcast of lexpr * ppure_type - | PPmatch of lexpr * (pattern * lexpr) list - | PPisConstr of lexpr * string - | PPproject of lexpr * string - -let rec pp_lexpr fmt {pp_desc; _} = - let open Format in - match pp_desc with - | PPvar s -> - fprintf fmt "%s" s - | PPapp (s, lel) -> - fprintf fmt "PPapp(%s, %a)" s - (pp_print_list ~pp_sep:pp_sep_space pp_lexpr) lel - | PPmapsTo (s, le) -> - fprintf fmt "[%s -> %a]" s pp_lexpr le - | PPinInterval (le, b1, le1, le2, b2) -> - fprintf fmt "%a in %c %a, %a %c" - pp_lexpr le - (if b1 then ']' else '[') - pp_lexpr le1 - pp_lexpr le2 - (if b2 then ']' else '[') - | PPdistinct lel -> - fprintf fmt "distincts (%a)" (pp_print_list pp_lexpr) lel - | PPconst c-> - fprintf fmt "%a" pp_const c - | PPinfix (le1, op, le2) -> - fprintf fmt "inf: (%a %a %a)" pp_lexpr le1 pp_inf_op op pp_lexpr le2 - | PPprefix (op, le) -> - fprintf fmt "pre: %a %a" pp_pre_op op pp_lexpr le - | PPget (arr, ind) -> - fprintf fmt "%a[%a]" pp_lexpr arr pp_lexpr ind - | PPset (arr, ind, v) -> - fprintf fmt "%a[%a] <- %a" pp_lexpr arr pp_lexpr ind pp_lexpr v - | PPdot (le, s) -> - fprintf fmt "%a.%s" pp_lexpr le s - | PPrecord l -> - fprintf fmt "{%a}" - (pp_print_list (fun fmt (s, le) -> fprintf fmt "%s = %a" s pp_lexpr le)) l - | PPwith (le, l) -> - fprintf fmt "{%a with %a}" pp_lexpr le - (pp_print_list (fun fmt (s, le) -> fprintf fmt "%s = %a" s pp_lexpr le)) l - | PPextract (le, i, j) -> - fprintf fmt "Extract (%a, %d, %d)" pp_lexpr le i j - | PPconcat (le1, le2) -> - fprintf fmt "%a^%a" pp_lexpr le1 pp_lexpr le2 - | PPif (cond, bthen, belse) -> - fprintf fmt "if %a then %a else %a" - pp_lexpr cond pp_lexpr bthen pp_lexpr belse - (* Used for an experiment so not complete but will be completed *) - | PPforall (spptl, lebl, lel, le) -> - fprintf fmt "forall %a. [%a] [%a] %a" - pp_str_ppure_type_list spptl pp_lexprl_bool_list lebl - pp_lexpr_list lel pp_lexpr le - | PPexists (_spptl, _lebl, _lel, _le) -> fprintf fmt "exists" - | PPforall_named (sspptl, lebl, lel, le) -> - fprintf fmt "foralln %a. [%a] [%a] %a" - pp_str_str_ppure_type_list sspptl pp_lexprl_bool_list lebl - pp_lexpr_list lel pp_lexpr le - | PPexists_named (_spptl, _lebl, _lel, _le) -> fprintf fmt "existsn" - | PPnamed (s, le) -> fprintf fmt "Named: %s %a" s pp_lexpr le - | PPlet (_slel, _le) -> fprintf fmt "let" - | PPcheck le -> fprintf fmt "check %a" pp_lexpr le - | PPcut le -> fprintf fmt "cut %a" pp_lexpr le - | PPcast (le, ppt) -> - fprintf fmt "cast %a -> %a" pp_lexpr le pp_ppure_type ppt - | PPmatch (_le, _plel) -> fprintf fmt "match" - | PPisConstr (le, s) -> fprintf fmt "isConstr: %a %s" pp_lexpr le s - | PPproject (le, s) -> fprintf fmt "project: %a %s" pp_lexpr le s - -and pp_lexpr_list fmt tl = - Format.fprintf fmt "@[%a@]" - (Format.pp_print_list ~pp_sep:pp_sep_comma (fun fmt e -> - Format.fprintf fmt "%a" pp_lexpr e)) tl - -and pp_lexprl_bool_list fmt tl = - Format.fprintf fmt "@[%a@]" - (Format.pp_print_list ~pp_sep:pp_sep_comma (fun fmt (lel, b) -> - Format.fprintf fmt "(%a, %b)" pp_lexpr_list lel b)) tl - -(* Declarations. *) - -type plogic_type = - | PPredicate of ppure_type list - | PFunction of ppure_type list * ppure_type - -type body_type_decl = - | Record of string * (string * ppure_type) list (* lbl : t *) - | Enum of string list - | Algebraic of (string * (string * ppure_type) list) list - | Abstract - -type type_decl = Loc.t * string list * string * body_type_decl - -type decl = - | Theory of Loc.t * string * string * decl list - | Axiom of Loc.t * string * Util.axiom_kind * lexpr - | Rewriting of Loc.t * string * lexpr list - | Goal of Loc.t * string * lexpr - | Check_sat of Loc.t * string * lexpr - | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type - | Predicate_def of - Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * lexpr - | Function_def of - Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * ppure_type * lexpr - | MutRecDefs of - (Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list - | TypeDecl of type_decl list - | Push of Loc.t * int - | Pop of Loc.t * int - | Reset of Loc.t - | Exit of Loc.t - | Optimize of Loc.t * lexpr * bool - -type file = decl list diff --git a/src/lib/structures/parsed.mli b/src/lib/structures/parsed.mli deleted file mode 100644 index 5c7e177de..000000000 --- a/src/lib/structures/parsed.mli +++ /dev/null @@ -1,141 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -type constant = - | ConstBitv of string - | ConstInt of string - | ConstReal of Numbers.Q.t - | ConstTrue - | ConstFalse - | ConstVoid - -type pp_infix = - | PPand | PPor | PPxor | PPimplies | PPiff - | PPlt | PPle | PPgt | PPge | PPeq | PPneq - | PPadd | PPsub | PPmul | PPdiv | PPmod - | PPpow_int | PPpow_real - -type pp_prefix = - | PPneg | PPnot - -type ppure_type = - | PPTint - | PPTbool - | PPTreal - | PPTunit - | PPTbitv of int - | PPTvarid of string * Loc.t - | PPTexternal of ppure_type list * string * Loc.t - -val pp_ppure_type : Format.formatter -> ppure_type -> unit -val pp_ppure_type_list : Format.formatter -> ppure_type list -> unit - -type pattern = - { pat_loc : Loc.t; pat_desc : string * string list } - -type lexpr = - { pp_loc : Loc.t; pp_desc : pp_desc } - -and pp_desc = - | PPvar of string - | PPapp of string * lexpr list - | PPmapsTo of string * lexpr - | PPinInterval of lexpr * bool * lexpr * lexpr * bool - (* bool = true <-> interval is_open *) - - | PPdistinct of lexpr list - | PPconst of constant - | PPinfix of lexpr * pp_infix * lexpr - | PPprefix of pp_prefix * lexpr - | PPget of lexpr * lexpr - | PPset of lexpr * lexpr * lexpr - | PPdot of lexpr * string - | PPrecord of (string * lexpr) list - | PPwith of lexpr * (string * lexpr) list - | PPextract of lexpr * int * int - | PPconcat of lexpr * lexpr - | PPif of lexpr * lexpr * lexpr - | PPforall of - (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr - | PPexists of - (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr - | PPforall_named of - (string * string * ppure_type) list * (lexpr list * bool) list * - lexpr list * lexpr - | PPexists_named of - (string * string * ppure_type) list * (lexpr list * bool) list * - lexpr list * lexpr - | PPnamed of string * lexpr - | PPlet of (string * lexpr) list * lexpr - | PPcheck of lexpr - | PPcut of lexpr - | PPcast of lexpr * ppure_type - | PPmatch of lexpr * (pattern * lexpr) list - | PPisConstr of lexpr * string - | PPproject of lexpr * string - -val pp_lexpr : Format.formatter -> lexpr -> unit -val pp_lexpr_list : Format.formatter -> lexpr list -> unit - -(* Declarations. *) - -type plogic_type = - | PPredicate of ppure_type list - | PFunction of ppure_type list * ppure_type - -type body_type_decl = - | Record of string * (string * ppure_type) list (* lbl : t *) - | Enum of string list - | Algebraic of (string * (string * ppure_type) list) list - | Abstract - -type type_decl = Loc.t * string list * string * body_type_decl - -type decl = - | Theory of Loc.t * string * string * decl list - | Axiom of Loc.t * string * Util.axiom_kind * lexpr - | Rewriting of Loc.t * string * lexpr list - | Goal of Loc.t * string * lexpr - | Check_sat of Loc.t * string * lexpr - | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type - | Predicate_def of - Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * lexpr - | Function_def of - Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * ppure_type * lexpr - | MutRecDefs of - (Loc.t * (string * string) * - (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list - | TypeDecl of type_decl list - | Push of Loc.t * int - | Pop of Loc.t * int - | Reset of Loc.t - | Exit of Loc.t - | Optimize of Loc.t * lexpr * bool - -type file = decl list