package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/src/lambdapi.handle/why3_tactic.ml.html
Source file why3_tactic.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
(** Implementation of the why3 tactic. *) open Lplib open Extra open Timed open Common open Error open Core open Term open Print open Fol (** Logging function for external prover calling with Why3. *) let log_why3 = Logger.make 'y' "why3" "why3 provers" let log_why3 = log_why3.pp (** [default_prover] contains the name of the current prover. Note that it can be changed by using the "set prover <string>" command. *) let default_prover : string ref = ref "Alt-Ergo" (** [timeout] is the current time limit (in seconds) for a Why3 prover to find a proof. It can be changed with "set prover <int>". *) let timeout : int ref = ref 2 (** [why3_config] is the Why3 configuration read from the configuration file (["~/.why3.conf"] usually). For more information, visit the Why3 documentation at http://why3.lri.fr/api/Whyconf.html. *) let why3_config : Why3.Whyconf.config = let cfg = Why3.Whyconf.init_config None in let provers = Why3.Whyconf.get_provers cfg in Console.out 2 "provers available for why3:"; let prover p _ = Console.out 2 "%a" Why3.Whyconf.print_prover p in Why3.Whyconf.Mprover.iter prover provers; cfg (** [why3_main] is the main section of the Why3 configuration. *) let why3_main : Why3.Whyconf.main = Why3.Whyconf.get_main why3_config (** [why3_env] is the initialized Why3 environment. *) let why3_env : Why3.Env.env = Why3.Env.create_env (Why3.Whyconf.loadpath why3_main) (** A map from lambdapi terms to Why3 constants. *) type cnst_table = (term * Why3.Term.lsymbol) list (** Table of declared types, these types may be variables or constants. *) module TyTable : sig type t val empty : t val ty_of_term : t -> term -> t * Why3.Ty.ty (** [ty_of_term tbl te] fetches the type associated to term [te] in table [tbl] if it exists, or it creates such a type and return the created type and the new table. *) (** {b FIXME} the translation of types {!ty_of_term} is correct on non empty types only. *) val fold_left : do_var:('a -> term -> Why3.Ty.tvsymbol -> 'a) -> do_sym:('a -> term -> Why3.Ty.tysymbol -> 'a) -> 'a -> t -> 'a (** [fold_left ~do_var ~do_sym init tbl] folds over the table [tbl] with initial value [init] using [do_var] to operate on type variables and [do_sym] to operate on type symbols. *) end = struct (* The module is created to hide the type [sym_or_var] *) type sym_or_var = TySym of Why3.Ty.tysymbol | TyVar of Why3.Ty.tvsymbol type t = (term * sym_or_var) list let empty = [] let ty_of_term tbl te = match List.assoc_eq (Eval.eq_modulo []) te tbl with | TySym s -> (tbl, Why3.Ty.ty_app s []) | TyVar v -> (tbl, Why3.Ty.ty_var v) | exception Not_found -> ( (* FIXME generate a new goal to ensure that types translated as fresh constants are inhabited. *) match get_args te with | Symb s, [] -> let id = Why3.Ident.id_fresh s.sym_name in let sym = Why3.(Ty.create_tysymbol id [] Ty.NoDef) in ((te,TySym sym)::tbl, Why3.Ty.ty_app sym []) | Vari x, [] -> let sym = Why3.Ty.tv_of_string (Bindlib.name_of x) in ((te,TyVar sym)::tbl, Why3.Ty.ty_var sym) | _ -> let id = Why3.Ident.id_fresh "ty" in let sym = Why3.(Ty.create_tysymbol id [] Ty.NoDef) in ((te,TySym sym)::tbl, Why3.Ty.ty_app sym [])) let fold_left ~do_var ~do_sym acc tbl = let f acc (t,s_or_v) = match s_or_v with | TySym s -> do_sym acc t s | TyVar v -> do_var acc t v in List.fold_left f acc tbl end (** [translate_term cfg tbl t] translates the given lambdapi term [t] into the correspondig Why3 term, using the configuration [cfg] and constants in the association list [tbl]. *) let translate_term : config -> cnst_table -> TyTable.t -> term -> (cnst_table * TyTable.t * Why3.Term.term) option = fun cfg tbl ty_tbl t -> let rec translate_prop tbl ty_tbl t = match get_args t with | Symb(s), [t1; t2] when s == cfg.symb_and -> let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in (tbl, ty_tbl, Why3.Term.t_and t1 t2) | Symb(s), [t1; t2] when s == cfg.symb_or -> let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in (tbl, ty_tbl, Why3.Term.t_or t1 t2) | Symb(s), [t1; t2] when s == cfg.symb_imp -> let (tbl, ty_tbl, t1) = translate_prop tbl ty_tbl t1 in let (tbl, ty_tbl, t2) = translate_prop tbl ty_tbl t2 in (tbl, ty_tbl, Why3.Term.t_implies t1 t2) | Symb(s), [t] when s == cfg.symb_not -> let (tbl, ty_tbl, t) = translate_prop tbl ty_tbl t in (tbl, ty_tbl, Why3.Term.t_not t) | Symb(s), [] when s == cfg.symb_bot -> (tbl, ty_tbl, Why3.Term.t_false) | Symb(s), [] when s == cfg.symb_top -> (tbl, ty_tbl, Why3.Term.t_true) | Symb(s), [a;Abst(_,t)] when s == cfg.symb_ex || s == cfg.symb_all -> let (ty_tbl, ty) = TyTable.ty_of_term ty_tbl a in let x, t = Bindlib.unbind t in let (tbl, ty_tbl ,t) = translate_prop tbl ty_tbl t in let tquant = let id = Why3.Ident.id_fresh (Bindlib.name_of x) in let vid = Why3.(Term.create_vsymbol id) ty in let close = if s == cfg.symb_ex then Why3.Term.t_exists_close else Why3.Term.t_forall_close (* Other cases excluded by pattern matching *) in close [vid] [] t in (tbl, ty_tbl, tquant) | _ -> (* If the term [p] is mapped in [tbl] then use it. *) try let sym = List.assoc_eq (Eval.eq_modulo []) t tbl in (tbl, ty_tbl, Why3.Term.ps_app sym []) with Not_found -> (* Otherwise generate a new constant in why3. *) let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "P") [] in ((t, sym)::tbl, ty_tbl, Why3.Term.ps_app sym []) in match get_args t with | (Symb(s), [t]) when s == cfg.symb_P -> Some (translate_prop tbl ty_tbl t) | _ -> None (** [encode ss pos hs g] translates the hypotheses [hs] and the goal [g] into Why3 terms, to construct a Why3 task. *) let encode : Sig_state.t -> Pos.popt -> Env.env -> term -> Why3.Task.task = fun ss pos hs g -> let cfg = get_config ss pos in let (constants, types, hypothesis) = let translate_hyp (tbl,ty_tbl, map) (name, (_, hyp, _)) = match translate_term cfg tbl ty_tbl (Bindlib.unbox hyp) with | Some(tbl, ty_tbl, why3_hyp) -> (tbl, ty_tbl, StrMap.add name why3_hyp map) | None -> (tbl, ty_tbl , map) in List.fold_left translate_hyp ([], TyTable.empty, StrMap.empty) hs in (* Translate the goal term. *) let (tbl, ty_tbl, why3_term) = match translate_term cfg constants types g with | Some(tbl, ty_tbl, why3_term) -> (tbl, ty_tbl, why3_term) | None -> fatal pos "The goal [%a] is not of the form [P _]" term g in (* Add the declaration of every constant in a task. *) let fn tsk (_,t) = Why3.Task.add_param_decl tsk t in let tsk = List.fold_left fn None tbl in (* Same for types. *) let tsk = let do_sym tsk _ tys = Why3.Task.add_ty_decl tsk tys in let do_var tsk _ _ = tsk in TyTable.fold_left ~do_var ~do_sym tsk ty_tbl in (* Add the declaration of every hypothesis in the task. *) let fn name t tsk = let axiom = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh name) in Why3.Task.add_prop_decl tsk Why3.Decl.Paxiom axiom t in let tsk = StrMap.fold fn hypothesis tsk in (* Add the goal itself. *) let goal = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "main_goal") in (* Return the task that contains the encoded lambdapi formula in Why3. *) Why3.Task.add_prop_decl tsk Why3.Decl.Pgoal goal why3_term (** [run_task tsk pos prover_name] Run the task [tsk] with the specified prover named [prover_name] and return the answer of the prover. *) let run_task : Why3.Task.task -> Pos.popt -> string -> bool = fun tsk pos prover_name -> (* Filter the set of why3 provers. *) let filter = Why3.Whyconf.parse_filter_prover prover_name in let provers = Why3.Whyconf.filter_provers why3_config filter in (* Fail if we did not find a matching prover. *) if Why3.Whyconf.Mprover.is_empty provers then begin fatal_msg "prover \"%s\" not found.@." prover_name; let provers = Why3.Whyconf.get_provers why3_config in let _ = if Why3.Whyconf.Mprover.is_empty provers then fatal_msg "There are no available Why3 provers.@." else let fn p _ = fatal_msg " - %a@." Why3.Whyconf.print_prover p in fatal_msg "The available Why3 provers are:@."; Why3.Whyconf.Mprover.iter fn provers in fatal_msg "Why3 configuration read from \"%s\".@." (Why3.Whyconf.get_conf_file why3_config); fatal_msg "Your prover might not be installed or detected, "; fatal pos "remember to run [why3 config detect]." end; (* Return the prover configuration and load the driver. *) let prover = snd (Why3.Whyconf.Mprover.max_binding provers) in let driver = try Why3.Driver.(load_driver_for_prover why3_main why3_env prover) with e -> fatal pos "Failed to load driver for \"%s\": %a" prover.prover.prover_name Why3.Exn_printer.exn_printer e in (* Actually run the prover. *) let command = prover.Why3.Whyconf.command and limit = {Why3.Call_provers.empty_limit with limit_time = float_of_int!timeout} in let call = Why3.Driver.prove_task ~command ~config:why3_main ~limit driver tsk in Why3.Call_provers.((wait_on_call call).pr_answer = Valid) (** [handle ss pos prover_name gt] runs the Why3 prover corresponding to [prover_name] (if given or a default one otherwise) on the goal type [gt], and fails if no proof is found. *) let handle : Sig_state.t -> Pos.popt -> string option -> Proof.goal_typ -> unit = fun ss pos prover_name {goal_meta = _; goal_hyps = hyps; goal_type = trm} -> (* Get the name of the prover. *) let prover_name = Option.get !default_prover prover_name in if Logger.log_enabled () then log_why3 "running with prover \"%s\"" prover_name; (* Encode the goal in Why3. *) let tsk = encode ss pos hyps trm in (* Run the task with the prover named [prover_name]. *) if not (run_task tsk pos prover_name) then fatal pos "\"%s\" did not find a proof" prover_name
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>