diff --git a/rsc/extra/subgraphs.dot b/rsc/extra/subgraphs.dot index 769a5f44b..749b42d54 100644 --- a/rsc/extra/subgraphs.dot +++ b/rsc/extra/subgraphs.dot @@ -187,7 +187,6 @@ subgraph cluster_lib { "Expr"; "Xliteral"; "Ty"; - "Typed"; "Commands"; "Errors"; "Fpa_rounding"; diff --git a/src/lib/dune b/src/lib/dune index 30cc3b00b..ae03f59d5 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -57,7 +57,7 @@ ; structures Commands Errors Explanation Fpa_rounding Profiling Satml_types Symbols - Expr Var Ty Typed Xliteral ModelMap Id Objective Literal + Expr Var Ty Xliteral ModelMap Id Objective Literal ; util Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue Options Timers Util Vec Version Steps Printer diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 34f858e65..37690ba0e 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -452,7 +452,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct check_if_over (internal_assume ~loc:d.st_loc (n, f, mf)) env | PredDef (f, name) -> check_if_over (internal_pred_def ~loc:d.st_loc (name, f)) env - | RwtDef _ -> assert false | Query (n, f, sort) -> begin (* If we have reached an unknown state, we can return it right diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 262eff96d..76c6bca09 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -761,55 +761,139 @@ let handle_patt_var id (DE.{ term_descr; _ } as term) = "Expected a variable in a case match but got %a" DE.Term.print term -(** Helper function to translate patterns in a pattern-matching from a Dolmen - Term.t to an Alt-Ergo Expr.t *) -let mk_pattern DE.{ term_descr; _ } = - match term_descr with - | App ( - { term_descr = - Cst ({ builtin = B.Constructor { adt; case; }; _ } as cst); _ - }, _, pargs - ) -> - let vnames = - begin match DT.definition adt with - | Some (Adt { cases; _ }) -> - let { DE.dstrs; _ } = cases.(case) in - Array.fold_right ( - fun v acc -> - match v with - | Some dstr -> dstr :: acc - | _ -> assert false - ) dstrs [] - | _ -> - Fmt.failwith - "Expected a constructor for an algebraic data type but got\ - something else for the definition of: %a" - DE.Ty.Const.print adt - end +module Match = struct + type pat = + | Var of Var.t + | Constr of DE.term_cst * (Var.t * DE.term_cst * Ty.t) list + + (** Helper function to translate patterns in a pattern-matching from a Dolmen + Term.t to an Alt-Ergo Expr.t *) + let mk_pat DE.{ term_descr; _ } = + match term_descr with + | App ( + { term_descr = + Cst ({ builtin = B.Constructor { adt; case; }; _ } as cst); _ + }, _, pargs + ) -> + let vnames = + begin match DT.definition adt with + | Some (Adt { cases; _ }) -> + let { DE.dstrs; _ } = cases.(case) in + Array.fold_right ( + fun v acc -> + match v with + | Some dstr -> dstr :: acc + | _ -> assert false + ) dstrs [] + | _ -> + Fmt.failwith + "Expected a constructor for an algebraic data type but got\ + something else for the definition of: %a" + DE.Ty.Const.print adt + end + in + let rev_args = + List.fold_left2 ( + fun acc rn arg -> + let v, n, ty = handle_patt_var rn arg in + (v, n, ty) :: acc + ) [] vnames pargs + in + Constr (cst, List.rev rev_args) + + | Cst ({ builtin = B.Constructor _; _ } as cst) -> + Constr (cst, []) + + | Var ({ builtin = B.Base; path; _ } as t_v) -> + (* Should the type be passed as an argument + instead of re-evaluating it here? *) + let v = Var.of_string (get_basename path) in + let sy = Sy.var v in + Cache.store_sy t_v sy; + (* Adding the matched variable to the store *) + Var v + + | _ -> assert false + + let rec compile_match mk_destr mk_tester e cases accu = + match cases with + | [] -> accu + + | (Var x, p) :: _ -> + E.apply_subst (Var.Map.singleton x e, Ty.esubst) p + + | (Constr (name, args), p) :: l -> + let _then = + List.fold_left + (fun acc (var, destr, ty) -> + let destr = mk_destr destr in + let d = E.mk_term destr [e] ty in + E.mk_let var d acc + ) p args + in + match l with + [] -> _then + | _ -> + let _else = compile_match mk_destr mk_tester e l accu in + let cond = mk_tester name e in + E.mk_ite cond _then _else + + (* (* TO BE REMOVED *) + let debug_compile_match e cases res = + if Options.get_debug_adt () then begin + Printer.print_dbg ~flushed:false ~module_name:"Expr" + "compilation of: match %a with@ " print e; + let p_list_vars fmt l = + match l with + [] -> () + | [e,_,_] -> Var.print fmt e + | (e,_,_) :: l -> + Format.fprintf fmt "(%a" Var.print e; + List.iter (fun (e,_,_) -> Format.fprintf fmt ", %a" Var.print e) l; + Format.fprintf fmt ")" + in + List.iter + (fun (p, v) -> + match p with + | Typed.Constr {name; args} -> + Printer.print_dbg ~flushed:false ~header:false + "| %a %a -> %a@ " + DE.Term.Const.print name + p_list_vars args + print v; + | Typed.Var x -> + Printer.print_dbg ~flushed:false ~header:false + "| %a -> %a@ " Var.print x print v; + )cases; + Printer.print_dbg ~header:false + "end@ result is: %a" print res; + end *) + + let mk_match e cases = + let ty = E.type_info e in + let mk_destr = + match ty with + | Ty.Tadt _ -> (fun hs -> Sy.destruct hs) + | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) + | _ -> assert false in - let rev_args = - List.fold_left2 ( - fun acc rn arg -> - let v, n, ty = handle_patt_var rn arg in - (v, n, ty) :: acc - ) [] vnames pargs + let mk_tester = + match ty with + | Ty.Tadt _ -> E.mk_tester + | Ty.Trecord _ -> + (* no need to test for records *) + (fun _e _name -> assert false) + | _ -> assert false in - let args = List.rev rev_args in - Typed.Constr {name = cst; args} + let res = compile_match mk_destr mk_tester e cases e in + (* debug_compile_match e cases res; *) + res + [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"] + [@ocaml.ppwarning "TODO: add other elim schemes"] + [@ocaml.ppwarning "TODO: add a match construct in expr"] - | Cst ({ builtin = B.Constructor _; _ } as cst) -> - Typed.Constr {name = cst; args = []} - | Var ({ builtin = B.Base; path; _ } as t_v) -> - (* Should the type be passed as an argument - instead of re-evaluating it here? *) - let v = Var.of_string (get_basename path) in - let sy = Sy.var v in - Cache.store_sy t_v sy; - (* Adding the matched variable to the store *) - Typed.Var v - - | _ -> assert false +end let arith_ty = function | `Int -> Ty.Tint @@ -1367,12 +1451,12 @@ let rec mk_expr let pats = List.rev_map ( fun (p, t) -> - let patt = mk_pattern p in + let patt = Match.mk_pat p in let e = aux_mk_expr t in patt, e ) (List.rev pats) in - E.mk_match e pats + Match.mk_match e pats | Binder ((Let_par ls | Let_seq ls) as let_binder, body) -> let lsbis = diff --git a/src/lib/index.mld b/src/lib/index.mld index 2fb328cb7..a1db3b3d0 100644 --- a/src/lib/index.mld +++ b/src/lib/index.mld @@ -35,7 +35,6 @@ be sent to the SMT solver. {!modules: AltErgoLib.Ty -AltErgoLib.Typed AltErgoLib.Expr AltErgoLib.Commands } diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 47856b2a4..45b8dcaf8 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -34,7 +34,6 @@ type sat_decl_aux = | Decl of Id.typed | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) - | RwtDef of (Expr.t Typed.rwt_rule) list | Optimize of Objective.Function.t | Query of string * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt @@ -57,12 +56,6 @@ let print_aux fmt = function Format.fprintf fmt "assume %s(%b): @[%a@]" name b Expr.print e | PredDef (e, name) -> Format.fprintf fmt "pred-def %s: @[%a@]" name Expr.print e - | RwtDef l -> - Format.fprintf fmt "rwrts: @[%a@]" - (Util.print_list_pp - ~sep:Format.pp_print_space - ~pp:(Typed.print_rwt Expr.print) - ) l | Query (name, e, sort) -> Format.fprintf fmt "query %s(%a): @[%a@]" name Ty.print_goal_sort sort Expr.print e diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index 152f1ca0b..06eb89001 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -31,7 +31,6 @@ type sat_decl_aux = | Decl of Id.typed | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) - | RwtDef of (Expr.t Typed.rwt_rule) list | Optimize of Objective.Function.t | Query of string * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7945afddd..8b9ed1e75 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1300,26 +1300,27 @@ let mk_builtin ~is_pos n l = (** smart constructors for datatypes. *) -let is_constr DE.{ builtin; _ } = - match builtin with - | DStd.Builtin.Constructor _ -> true - | _ -> false - let has_attached_order id = DE.Term.Const.get_tag id Nest.order_tag |> Option.is_some let mk_constr c xs ty = - if not @@ is_constr c then - Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c; - (* This assertion ensures that the API of the [Nest] module have been - correctly used, that is [Nest.attach_orders] have been called on - the nest of [id] if [id] is a constructor of ADT. *) - if not @@ has_attached_order c then - Fmt.invalid_arg "no order on constructor %a" DE.Id.print c; - mk_term (Sy.Op (Constr c)) xs ty - -let mk_tester cons t = - mk_builtin ~is_pos:true (Sy.IsConstr cons) [t] + match c.DE.builtin with + | DStd.Builtin.Constructor _ -> + (* This assertion ensures that the API of the [Nest] module have been + correctly used, that is [Nest.attach_orders] have been called on + the nest of [id] if [id] is a constructor of ADT. *) + if not @@ has_attached_order c then + Fmt.invalid_arg "no order on constructor %a" DE.Id.print c; + mk_term (Sy.Op (Constr c)) xs ty + | _ -> + Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c + +let mk_tester c t = + match c.DE.builtin with + | DStd.Builtin.Constructor _ -> + mk_builtin ~is_pos:true (Sy.IsConstr c) [t] + | _ -> + Fmt.invalid_arg "expected a constructor, got %a" DE.Id.print c let mk_record xs ty = mk_term (Sy.Op Record) xs ty @@ -2617,88 +2618,6 @@ let mk_exists name loc binders trs f ~toplevel ~decl_kind = in mk_forall name loc Var.Map.empty trs tmp ~toplevel ~decl_kind - -let rec compile_match mk_destr mker e cases accu = - match cases with - | [] -> accu - - | (Typed.Var x, p) :: _ -> - apply_subst ((Var.Map.singleton x e), Ty.esubst) p - - | (Typed.Constr {name; args}, p) :: l -> - let _then = - List.fold_left - (fun acc (var, destr, ty) -> - let destr = mk_destr destr in - let d = mk_term destr [e] ty in - mk_let var d acc - )p args - in - match l with - [] -> _then - | _ -> - let _else = compile_match mk_destr mker e l accu in - let cond = mker e name in - mk_ite cond _then _else - -(* TO BE REMOVED *) -let debug_compile_match e cases res = - if Options.get_debug_adt () then begin - Printer.print_dbg ~flushed:false ~module_name:"Expr" - "compilation of: match %a with@ " print e; - let p_list_vars fmt l = - match l with - [] -> () - | [e,_,_] -> Var.print fmt e - | (e,_,_) :: l -> - Format.fprintf fmt "(%a" Var.print e; - List.iter (fun (e,_,_) -> Format.fprintf fmt ", %a" Var.print e) l; - Format.fprintf fmt ")" - in - List.iter - (fun (p, v) -> - match p with - | Typed.Constr {name; args} -> - Printer.print_dbg ~flushed:false ~header:false - "| %a %a -> %a@ " - DE.Term.Const.print name - p_list_vars args - print v; - | Typed.Var x -> - Printer.print_dbg ~flushed:false ~header:false - "| %a -> %a@ " Var.print x print v; - )cases; - Printer.print_dbg ~header:false - "end@ result is: %a" print res; - end - -let mk_match e cases = - let ty = type_info e in - let mk_destr = - match ty with - | Ty.Tadt _ -> (fun hs -> Sy.destruct hs) - | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs)) - | _ -> assert false - in - let mker = - match ty with - | Ty.Tadt _ -> - (fun e name -> - mk_builtin ~is_pos:true (Sy.IsConstr name) [e]) - - | Ty.Trecord _ -> - (fun _e _name -> assert false) (* no need to test for records *) - - | _ -> assert false - in - let res = compile_match mk_destr mker e cases e in - debug_compile_match e cases res; - res - [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"] - [@ocaml.ppwarning "TODO: add other elim schemes"] - [@ocaml.ppwarning "TODO: add a match construct in expr"] - - let is_pure e = e.pure module Purification = struct diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index bdb726682..6dec2b1ab 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -294,6 +294,10 @@ val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t [Nest.attach_orders]. *) val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t +(** [mk_tester c e] produces the tester expression ((_ is c) e). + + @raise Invalid_argument if [c] is not a Dolmen constructor. *) + val mk_record : t list -> Ty.t -> t (** Substitutions *) @@ -396,8 +400,6 @@ val mk_exists : val mk_let : Var.t -> t -> t -> t -val mk_match : t -> (Typed.pattern * t) list -> t - val skolemize : quantified -> t val elim_let : recursive:bool -> letin -> t diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml deleted file mode 100644 index 168e7c8a0..000000000 --- a/src/lib/structures/typed.ml +++ /dev/null @@ -1,368 +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/ *) -(* *) -(**************************************************************************) - -(** Anotations (used by the GUI). *) - -module DE = Dolmen.Std.Expr - -type ('a, 'b) annoted = - { c : 'a; - annot : 'b } - -let new_id = let r = ref 0 in fun () -> r := !r+1; !r - -let mk ?(annot=new_id ()) c = { c; annot; } - - -(** Terms and Formulas *) - -type tconstant = - | Tint of string - | Treal of Numbers.Q.t - | Tbitv of string - | Ttrue - | Tfalse - | Tvoid - -type oplogic = - OPand | OPor | OPxor | OPimp | OPnot | OPiff - | OPif - -(** type of pattern in match construct of ADTs *) -type pattern = - | Constr of { name : DE.term_cst ; args : (Var.t * DE.term_cst * Ty.t) list} - (** A pattern case which is a constructor. [name] is the name of - constructor. [args] contains the variables bound by this pattern - with their correponsing destructors and types *) - - | Var of Var.t - (** a pattern that is a variable (or underscore) *) - -type 'a tterm = - { tt_ty : Ty.t; tt_desc : 'a tt_desc } - -and 'a atterm = ('a tterm, 'a) annoted - -and 'a tt_desc = - | TTconst of tconstant - | TTvar of Symbols.t - | TTinfix of 'a atterm * Symbols.t * 'a atterm - | TTprefix of Symbols.t * 'a atterm - | TTapp of Symbols.t * 'a atterm list - | TTmapsTo of Var.t * 'a atterm - | TTinInterval of 'a atterm * Symbols.bound * Symbols.bound - (* bool = true <-> interval is_open *) - - | TTget of 'a atterm * 'a atterm - | TTset of - 'a atterm * 'a atterm * 'a atterm - | TTextract of - 'a atterm * int * int - | TTconcat of 'a atterm * 'a atterm - | TTdot of 'a atterm * Hstring.t - | TTrecord of (Hstring.t * 'a atterm) list - | TTlet of (Symbols.t * 'a atterm) list * 'a atterm - | TTnamed of Hstring.t * 'a atterm - | TTite of 'a atform * - 'a atterm * 'a atterm - | TTproject of 'a atterm * Hstring.t - | TTmatch of 'a atterm * (pattern * 'a atterm) list - | TTform of 'a atform - -and 'a atatom = ('a tatom, 'a) annoted - -and 'a tatom = - | TAtrue - | TAfalse - | TAeq of 'a atterm list - | TAdistinct of 'a atterm list - | TAneq of 'a atterm list - | TAle of 'a atterm list - | TAlt of 'a atterm list - | TApred of 'a atterm * bool (* true <-> negated *) - | TTisConstr of 'a atterm * Hstring.t - -and 'a quant_form = { - (* quantified variables that appear in the formula *) - qf_bvars : (Symbols.t * Ty.t) list ; - qf_triggers : ('a atterm list * bool) list ; - qf_hyp : 'a atform list; - qf_form : 'a atform -} - -and 'a atform = ('a tform, 'a) annoted - -and 'a tform = - | TFatom of 'a atatom - | TFop of oplogic * ('a atform) list - | TFforall of 'a quant_form - | TFexists of 'a quant_form - | TFlet of (Var.t * 'a tlet_kind) list * 'a atform - | TFnamed of Hstring.t * 'a atform - | TFmatch of 'a atterm * (pattern * 'a atform) list - -and 'a tlet_kind = - | TletTerm of 'a atterm - | TletForm of 'a atform - - -(** Rewrite rules *) - -type 'a rwt_rule = { - rwt_vars : (Symbols.t * Ty.t) list; - rwt_left : 'a; - rwt_right : 'a -} - -let print_rwt pp fmt r = - Format.fprintf fmt "@%a@ --> %a@]" pp r.rwt_left pp r.rwt_right - -(** Logic type *) - -type tlogic_type = - | TPredicate of Ty.t list - | TFunction of Ty.t list * Ty.t - -(** Declarations *) - -type 'a atdecl = ('a tdecl, 'a) annoted - -and 'a tdecl = - (* to simplify impl and extension of GUI, a TTtheory is seen a list - of tdecl, although we only allow axioms in theories - declarations *) - | TTheory of - Loc.t * string * Util.theories_extensions * ('a tdecl, 'a) annoted list - | TAxiom of Loc.t * string * Util.axiom_kind * 'a atform - | TRewriting of Loc.t * string * ('a atterm rwt_rule) list - | TGoal of Loc.t * Ty.goal_sort * string * 'a atform - | TLogic of Loc.t * string list * tlogic_type - | TPredicate_def of - Loc.t * string * - (string * Ty.t) list * 'a atform - | TFunction_def of - Loc.t * string * - (string * Ty.t) list * Ty.t * 'a atform - | TTypeDecl of Loc.t * Ty.t - | TPush of Loc.t * int - | TPop of Loc.t * int - | TReset of Loc.t - | TExit of Loc.t - | TOptimize of Loc.t * 'a atterm * bool - -(*****) - -let string_of_op = function - | OPand -> "and" - | OPor -> "or" - | OPimp -> "->" - | OPiff -> "<->" - | _ -> assert false - -let print_binder fmt (s, t) = - Format.fprintf fmt "%a :%a" Symbols.print s Ty.print t - -let print_binders fmt l = - List.iter (fun c -> Format.fprintf fmt "%a, " print_binder c) l - -let rec print_term = - let open Format in - fun fmt t -> match t.c.tt_desc with - | TTconst Ttrue -> - fprintf fmt "true" - | TTconst Tfalse -> - fprintf fmt "false" - | TTconst Tvoid -> - fprintf fmt "void" - | TTconst (Tint n) -> - fprintf fmt "%s" n - | TTconst (Treal n) -> - fprintf fmt "%s" (Numbers.Q.to_string n) - | TTconst Tbitv s -> - fprintf fmt "%s" s - | TTvar s -> - fprintf fmt "%a" Symbols.print s - | TTapp(s,l) -> - fprintf fmt "%a(%a)" Symbols.print s print_term_list l - | TTinfix(t1,s,t2) -> - fprintf fmt "%a %a %a" print_term t1 Symbols.print s print_term t2 - | TTprefix (s, t') -> - fprintf fmt "%a %a" Symbols.print s print_term t' - | TTget (t1, t2) -> - fprintf fmt "%a[%a]" print_term t1 print_term t2 - | TTset (t1, t2, t3) -> - fprintf fmt "%a[%a<-%a]" print_term t1 print_term t2 print_term t3 - | TTextract (t1, i, j) -> - fprintf fmt "%a^{%d, %d}" print_term t1 i j - | TTconcat (t1, t2) -> - fprintf fmt "%a @@ %a" print_term t1 print_term t2 - | TTdot (t1, s) -> - fprintf fmt "%a.%s" print_term t1 (Hstring.view s) - | TTrecord l -> - fprintf fmt "{ "; - List.iter - (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l; - fprintf fmt " }" - | TTlet (binders, t2) -> - fprintf fmt "let %a in %a" print_term_binders binders print_term t2 - | TTnamed (_, t) -> - fprintf fmt "%a" print_term t - - | TTinInterval(e, i, j) -> - fprintf fmt "%a in %a, %a" - print_term e - Symbols.print_bound i - Symbols.print_bound j - - | TTmapsTo(x,e) -> - fprintf fmt "%a |-> %a" Var.print x print_term e - - | TTite(cond, t1, t2) -> - fprintf fmt "(if %a then %a else %a)" - print_formula cond print_term t1 print_term t2 - | TTproject (t1, s) -> - fprintf fmt "%a#%s" - print_term t1 (Hstring.view s) - - | TTform f -> - fprintf fmt "%a" print_formula f - - | TTmatch (e, cases) -> - let pp_vars fmt l = - match l with - [] -> () - | [e,_,_] -> Var.print fmt e - | (e,_,_) :: l -> - fprintf fmt "(%a" Var.print e; - List.iter (fun (e,_,_) -> fprintf fmt ", %a" Var.print e) l; - fprintf fmt ")" - in - fprintf fmt "match %a with\n" print_term e; - List.iter - (fun (p, v) -> - match p with - | Constr {name = n; args = l} -> - fprintf fmt "| %a %a -> %a\n" DE.Term.Const.print n pp_vars l - print_term v - | Var x -> - fprintf fmt "| %a -> %a\n" Var.print x print_term v; - )cases; - fprintf fmt "end@." - -and print_term_binders fmt l = - match l with - | [] -> assert false - | (sy, t) :: l -> - Format.fprintf fmt "%a = %a" Symbols.print sy print_term t; - List.iter (fun (sy, t) -> - Format.fprintf fmt ", %a = %a" Symbols.print sy print_term t) l - -and print_term_list fmt = Util.print_list ~sep:"," ~pp:print_term fmt - -and print_atom = - let open Format in - fun fmt a -> match a.c with - | TAtrue -> - fprintf fmt "True" - | TAfalse -> - fprintf fmt "True" - | TAeq [t1; t2] -> - fprintf fmt "%a = %a" print_term t1 print_term t2 - | TAneq [t1; t2] -> - fprintf fmt "%a <> %a" print_term t1 print_term t2 - | TAle [t1; t2] -> - fprintf fmt "%a <= %a" print_term t1 print_term t2 - | TAlt [t1; t2] -> - fprintf fmt "%a < %a" print_term t1 print_term t2 - | TApred (t, negated) -> - if negated then fprintf fmt "(not (%a))" print_term t - else print_term fmt t - | TTisConstr (t1, s) -> - fprintf fmt "%a ? %s" print_term t1 (Hstring.view s) - | TAdistinct l -> - fprintf fmt "distinct(%a)" print_term_list l - | _ -> assert false - -and print_triggers fmt l = - List.iter (fun (tr, _) -> Format.fprintf fmt "%a | " print_term_list tr) l - -and print_formula = - let open Format in - fun fmt f -> match f.c with - | TFatom a -> - print_atom fmt a - | TFop(OPnot, [f]) -> - fprintf fmt "not %a" print_formula f - | TFop(OPif, [cond; f1;f2]) -> - fprintf fmt "if %a then %a else %a" - print_formula cond print_formula f1 print_formula f2 - | TFop(op, [f1; f2]) -> - fprintf fmt "(%a %s %a)" print_formula f1 (string_of_op op) - print_formula f2 - | TFforall { qf_bvars = l; qf_triggers = t; qf_form = f; _ } -> - fprintf fmt "forall %a [%a]. %a" - print_binders l print_triggers t print_formula f - - | TFlet (binders, f) -> - List.iter - (fun (sy, let_e) -> - fprintf fmt " let %a = " Var.print sy; - match let_e with - | TletTerm t -> fprintf fmt "%a in@." print_term t - | TletForm f -> fprintf fmt "%a in@." print_formula f - )binders; - fprintf fmt "%a" print_formula f - | _ -> fprintf fmt "(formula pprint not implemented)" - - -let rec print_tdecl fmt = function - | TTheory (_, name, _, l) -> - Format.fprintf fmt "th %s: @[%a@]" name - (Util.print_list_pp ~sep:Format.pp_print_space ~pp:print_atdecl) l - | TAxiom (_, name, _kind, f) -> - Format.fprintf fmt "ax %s: @[%a@]" name print_formula f - | TRewriting (_, name, l) -> - Format.fprintf fmt "rwt %s: @[%a@]" name - (Util.print_list_pp ~sep:Format.pp_print_space - ~pp:(print_rwt print_term)) l - | TGoal (_, _sort, name, f) -> - Format.fprintf fmt "goal %s: @[%a@]" name print_formula f - | TPush (_loc,n) -> - Format.fprintf fmt "push %d" n - | TPop (_loc,n) -> - Format.fprintf fmt "pop %d"n - | TLogic _ -> Format.fprintf fmt "logic" - | TPredicate_def _ -> Format.fprintf fmt "predicate def" - | TFunction_def _ -> Format.fprintf fmt "function def" - | TTypeDecl _ -> Format.fprintf fmt "type decl" - | TReset _ -> Format.fprintf fmt "reset" - | TExit _ -> Format.fprintf fmt "exit" - | TOptimize (_loc, obj, is_max) -> - let s = if is_max then "maximize" else "minimize" in - Format.fprintf fmt "%s %a" s print_term obj - -and print_atdecl fmt a = print_tdecl fmt a.c diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli deleted file mode 100644 index f23992689..000000000 --- a/src/lib/structures/typed.mli +++ /dev/null @@ -1,312 +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/ *) -(* *) -(**************************************************************************) - -(** Typed AST - - This module defines a typed AST, used to represent typed terms - before they are hashconsed. *) - - -(** {2 Annotations} *) - -type ('a, 'b) annoted = { - c : 'a; - annot : 'b; -} -(** An annoted structure. Usually used to annotate terms. *) - -val new_id : unit -> int -(** Generate a new, fresh integer (useful for annotations). *) - -val mk : ?annot:int -> 'a -> ('a, int) annoted -(** Create an annoted value with the given annotation. - If no annotation is given, a fresh annotation is generated - using {!new_id}. *) - - -(** {2 Terms and formulas} *) - - -type tconstant = - (* TODO: make Tint hold an arbitrary precision integer ? *) - | Tint of string (** An integer constant. *) - | Treal of Numbers.Q.t (** Real constant. *) - | Tbitv of string (** Bitvector constant. *) - | Ttrue (** The true boolean (or proposition ?) *) - | Tfalse (** The false boolean *) - | Tvoid (** The only value of type unit *) -(** Typed constants. *) - -type oplogic = - | OPand (** conjunction *) - | OPor (** disjunction *) - | OPxor (** exclusive disjunction *) - | OPimp (** implication *) - | OPnot (** negation *) - | OPiff (** equivalence *) - | OPif (** conditional branching *) -(** Logic operators. *) - -type pattern = - | Constr of { - name : Dolmen.Std.Expr.term_cst ; - args : (Var.t * Dolmen.Std.Expr.term_cst * Ty.t) list - } - | Var of Var.t - - -type 'a tterm = { - tt_ty : Ty.t; (** type of the term *) - tt_desc : 'a tt_desc; (** term descriptor *) -} -(** Typed terms. Polymorphic in the annotation: - an ['a tterm] is a term annoted with values of type ['a]. *) - -and 'a atterm = ('a tterm, 'a) annoted -(** type alias for annoted typed terms. *) - -and 'a tt_desc = - | TTconst of tconstant - (** Term constant *) - | TTvar of Symbols.t - (** Term variables *) - | TTinfix of 'a atterm * Symbols.t * 'a atterm - (** Infix symbol application *) - | TTprefix of Symbols.t * 'a atterm - (** Prefix symbol application *) - | TTapp of Symbols.t * 'a atterm list - (** Arbitrary symbol application *) - | TTmapsTo of Var.t * 'a atterm - (** Used in semantic triggers for floating point arithmetic. - See sources/preludes/fpa-theory-2017-01-04-16h00.ae *) - | TTinInterval of 'a atterm * Symbols.bound * Symbols.bound - (** Represent floating point intervals (used for triggers in Floating - point arithmetic theory). - [TTinInterval (lower, l_strict, t, upper, u_strict)] is a constraint - stating that term [t] is in the interval [lower, upper], - and that the lower (resp. upper) bound is strict iff [l_strict] - (resp. [u_strict]) is true. *) - | TTget of 'a atterm * 'a atterm - (** Get operation on arrays *) - | TTset of 'a atterm * 'a atterm * 'a atterm - (** Set operation on arrays *) - | TTextract of 'a atterm * int * int - (** Extract a sub-bitvector *) - | TTconcat of 'a atterm * 'a atterm - (* Concatenation of bitvectors *) - | TTdot of 'a atterm * Hstring.t - (** Field access on structs/records *) - | TTrecord of (Hstring.t * 'a atterm) list - (** Record creation. *) - | TTlet of (Symbols.t * 'a atterm) list * 'a atterm - (** Let-bindings. Accept a list of mutually recursive le-bindings. *) - (* TODO: check that mutually recursive let-bindings are allowed ? *) - | TTnamed of Hstring.t * 'a atterm - (** Attach a label to a term. *) - | TTite of 'a atform * 'a atterm * 'a atterm - (** Conditional branching, of the form - [TTite (condition, then_branch, else_branch)]. *) - - | TTproject of 'a atterm * Hstring.t - (** Field (conditional) access on ADTs. *) - - | TTmatch of 'a atterm * (pattern * 'a atterm) list - (** pattern matching on ADTs *) - - | TTform of 'a atform - (** formulas inside terms: simple way to add them without making a - lot of changes *) -(** Typed terms descriptors. *) -(* TODO: replace tuples by records (possible inline records to - avoid polluting the namespace ?) with explicit field names. *) - - -and 'a atatom = ('a tatom, 'a) annoted -(** Type alias for annoted typed atoms. *) - -and 'a tatom = - | TAtrue - (** The [true] atom *) - | TAfalse - (** The [false] atom *) - | TAeq of 'a atterm list - (** Equality of a set of typed terms. *) - | TAdistinct of 'a atterm list - (** Disequality. All terms in the set are pairwise distinct. *) - | TAneq of 'a atterm list - (** Equality negation: at least two elements in the list - are not equal. *) - | TAle of 'a atterm list - (** Arithmetic ordering: lesser or equal. Chained on lists of terms. *) - | TAlt of 'a atterm list - (** Strict arithmetic ordering: less than. Chained on lists of terms. *) - | TApred of 'a atterm * bool - (** Term predicate, negated if the boolean is true. - [TApred (t, negated)] is satisfied iff [t <=> not negated] *) - - | TTisConstr of 'a atterm * Hstring.t - (** Test if the given term's head symbol is identitical to the - provided ADT consturctor *) - - -(** Typed atoms. *) - -and 'a quant_form = { - qf_bvars : (Symbols.t * Ty.t) list; - (** Variables that are quantified by this formula. *) - qf_triggers : ('a atterm list * bool) list; - (** Triggers associated wiht the formula. - For each trigger, the boolean specifies whether the trigger - was given in the input file (compared to inferred). *) - qf_hyp : 'a atform list; - (** Hypotheses of axioms with semantic triggers in FPA theory. Typically, - these hypotheses reduce to TRUE after instantiation *) - qf_form : 'a atform; - (** The quantified formula. *) -} -(** Quantified formulas. *) - -and 'a atform = ('a tform, 'a) annoted -(** Type alias for typed annoted formulas. *) - -and 'a tform = - | TFatom of 'a atatom - (** Atomic formula. *) - | TFop of oplogic * 'a atform list - (** Application of logical operators. *) - | TFforall of 'a quant_form - (** Universal quantification. *) - | TFexists of 'a quant_form - (** Existencial quantification. *) - | TFlet of (Var.t * 'a tlet_kind) list * - 'a atform - (** Let binding. *) - | TFnamed of Hstring.t * 'a atform - (** Attach a name to a formula. *) - - | TFmatch of 'a atterm * (pattern * 'a atform) list - (** pattern matching on ADTs *) - -(** Typed formulas. *) - -and 'a tlet_kind = - | TletTerm of 'a atterm (** Term let-binding *) - | TletForm of 'a atform (** Formula let-binding *) -(** The different kinds of let-bindings, - whether they bind terms or formulas. *) - - -(** {2 Declarations} *) - - -type 'a rwt_rule = { - rwt_vars : (Symbols.t * Ty.t) list; (** Variables of the rewrite rule *) - rwt_left : 'a; (** Left side of the rewrite rule (aka pattern). *) - rwt_right : 'a; (** Right side of the rewrite rule. *) -} -(** Rewrite rules. - Polymorphic to allow for different representation of terms. *) - -type tlogic_type = - | TPredicate of Ty.t list (** Predicate type declarations *) - | TFunction of Ty.t list * Ty.t (** Function type declarations *) -(** Type declarations. Specifies the list of argument types, - as well as the return type for functions (predicate implicitly - returns a proposition, so there is no need for an explicit return - type). *) - -type 'a atdecl = ('a tdecl, 'a) annoted -(** Type alias for annoted typed declarations. *) - -and 'a tdecl = - | TTheory of Loc.t * string * Util.theories_extensions * 'a atdecl list - (** Theory declarations. The list of declarations in a Theory may - only contain Axioms. *) - | TAxiom of Loc.t * string * Util.axiom_kind * 'a atform - (** New axiom that can be used in proofs. *) - | TRewriting of Loc.t * string * ('a atterm rwt_rule) list - (** New rewrite rule that can be used. *) - | TGoal of Loc.t * Ty.goal_sort * string * 'a atform - (** New goal to prove. *) - | TLogic of Loc.t * string list * tlogic_type - (** Function (or predicate) type declaration. *) - | TPredicate_def of - Loc.t * string * (string * Ty.t) list * 'a atform - (** Predicate definition. - [TPredicate_def (loc, name, vars, body)] defines a predicate - [fun vars => body]. *) - | TFunction_def of - Loc.t * string * - (string * Ty.t) list * Ty.t * 'a atform - (** Predicate definition. - [TPredicate_def (loc, name, vars, ret, body)] defines a function - [fun vars => body], where body has type [ret]. *) - | TTypeDecl of Loc.t * Ty.t - (** New type declaration. [TTypeDecl (loc, vars, t, body)] - declares a type [t], with parameters [vars], and with - contents [body]. This new type may either be abstract, - a record type, or an enumeration. *) - | TPush of Loc.t * int - (** [push (loc,n)] pushs n new assertions levels onto the assertion stack *) - | TPop of Loc.t * int - (** [pop (loc,n)] pops n assertions levels from the assertion stack *) - | TReset of Loc.t - (** Resets all the context. *) - | TExit of Loc.t - (** Exits the solver. *) - - | TOptimize of Loc.t * 'a atterm * bool - (** Optimization declaration. - [TOptimize (loc, obj, is_max)] declares an objective function [obj]. The - flag [is_max] determines if we try to maximize of minimize [obj]. *) - -(** Typed declarations. *) -(* TODO: wrap this in a record to factorize away - the location and name of the declaration ? *) - - -(** {5 Printing} *) - -val print_term : Format.formatter -> _ atterm -> unit -(** Print annoted typed terms. Ignore the annotations. *) - -val print_formula : Format.formatter -> _ atform -> unit -(**Print annoted typed formulas; Ignores the annotations. *) - -val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unit -(** Print a list of bound typed variables. *) - -val print_triggers : Format.formatter -> ('a atterm list * bool) list -> unit -(** Print a list of triggers. *) - -val print_rwt : - (Format.formatter -> 'a -> unit) -> - Format.formatter -> 'a rwt_rule -> unit -(** Print a rewrite rule *) - -val print_atdecl : Format.formatter -> _ atdecl -> unit -(** Print an annoted term decl. *)