From 389c597c84c7954c4f9cefe4deb3107adb4f1dad Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Sun, 29 May 2022 17:06:19 +0200 Subject: [PATCH 01/16] =?UTF-8?q?Tactique=20de=20skol=C3=A9misation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/handle/skolem.ml | 105 +++++++++++++++++++++++ src/handle/skolem.mli | 4 + tests/skolem.lp | 53 ++++++++++++ tests/skolem.ml | 190 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 352 insertions(+) create mode 100644 src/handle/skolem.ml create mode 100644 src/handle/skolem.mli create mode 100644 tests/skolem.lp create mode 100644 tests/skolem.ml diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml new file mode 100644 index 000000000..9130bd02f --- /dev/null +++ b/src/handle/skolem.ml @@ -0,0 +1,105 @@ +open Common +open Core open Term + +(** Logging function for the skolem tactic. *) +let log_sklm = Logger.make '!' "sklm" "the skolemization tactic" +let log_sklm = log_sklm.pp + +(** Builtin configuration for propositional logic. *) +type config = + { symb_ex : sym (** Exists(∃) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) + ; symb_P : sym (** Encoding of propositions. *)} + +(** [get_config ss pos] build the configuration using [ss]. *) +let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> + let builtin = Builtin.get ss pos in + { symb_ex = builtin "ex" + ; symb_all = builtin "all" + ; symb_P = builtin "P"} + +(*Context of skolemization allow to record introduced variables and their types when +universal quantifiers occurs.*) +let empty_context = [] +let add_ctxt : ctxt->tvar->term->ctxt = + fun c var typ -> + c @ [(var, typ, None)] + + +(**Skolemization*) + +(*[new_skolem ss ctx cpt ex_typ] is called when existantial quantifier ("∃y") occurs. +[ex_typ] is the type of quantificated variable "y". +In order to eliminate ∃ quantifier, we need to extend signature state [ss] with a skolem term, +represented by a fresh symbol that will later replace the binded variable ("y"). +Such skolem term may either be a skolem function or a skolem constant : +The type of a skolem term depends on registered variables in [ctx] +For example, if a set of variables x1:a1, x2:a2,..., xn:an were previously introduced by an +universal quantifier, A skolem term "skt" will take as arguments x1, ..., xn, and must therefore be +typed as follows : skt (x1, x2, ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. +A skolem term is a constant if skolemized term is not in the scope of any universal quantifier, +namely, [ctx] is empty. +For the sake of clarity, we use a counter [cpt] for naming the generated symbol. +OUT : Updated signature state [upt_sig] is returned, as well as introduced symbol [symb_skt] and updated counter*) + let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = + fun ss ctx ctr ex_typ -> + let skt_name = if (ctx == []) then ("c"^(string_of_int (ctr))) else ("f"^(string_of_int (ctr))) in + let skt, _ = Ctxt.to_prod ctx ex_typ in + let upt_sig, symb_skt = Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] + None + in + if Logger.log_enabled () then + log_sklm "New symbol %a" Print.sym symb_skt; + upt_sig, symb_skt,(ctr + 1) + + + +(*[Subst_app ctx tb s] builds [f_appl], the application of a symbol [symb_skt] +and a list of variables extracted from context [ctx]. Then, the binded +variable in [tb] is substituted by [f_appl]*) +(*Assumes type of [symb_skt] correspond to variables's types as they are +listed in context [ctx] *) +let subst_app : ctxt -> tbinder -> sym -> term = + fun ctx tb symb_skt -> + (*args_list : [tvar list], are context's variables*) + let args_list = List.map (fun (v, _, _) -> mk_Vari v) ctx in + (*[add_args] build the application of [f_term] to the list + of variables [args_list].*) + let f_appl= add_args (mk_Symb symb_skt) args_list in + Bindlib.subst tb f_appl + + +(**Main fonction : +[skolemisation ss pos t] return a skolemized form of term [t]. +(ie existential quantifications in [t] are removed) +To this end, for each existential quantifiers in [t], signature state [ss] is +extended with new symbol [symb_skt] in order to substitute the variable binded +by the said quantifier*) +let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> + (*Gets user-defined symbol identifiers mapped using "builtin" command.*) + let cfg = get_config ss pos in + let rec skolemisation ss ctx ctr t = + match get_args t with + | Symb(s), [_;Abst(y, tb)] when s == cfg.symb_ex -> + (* When existential quantification occurs, quantified variable + is substituted by a fresh symbol*) + let maj_ss, nv_sym, maj_ctr = new_skolem ss ctx ctr y in + let maj_term = subst_app ctx tb nv_sym in + skolemisation maj_ss ctx maj_ctr maj_term + | Symb(s), [a;Abst(x, tb)] when s == cfg.symb_all -> + (* When universal quantification occurs, quantified variable + is added to context*) + let var, f = Bindlib.unbind tb in + let maj_ctx = add_ctxt ctx var a in + let maj_f = skolemisation ss maj_ctx ctr f in + let maj_tb = bind var lift maj_f in + (*Reconstruct a term of form ∀ x : P, t', + with t' skolemized*) + add_args (mk_Symb s) [a ; mk_Abst (x, maj_tb)] + | _ -> t + in + let skl_of_t = skolemisation ss empty_context 0 t in + if Logger.log_enabled () then + log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t ; + skl_of_t + diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli new file mode 100644 index 000000000..3054ff6c7 --- /dev/null +++ b/src/handle/skolem.mli @@ -0,0 +1,4 @@ +open Common +open Core open Term + +val handle : Sig_state.t -> Pos.popt -> term -> term \ No newline at end of file diff --git a/tests/skolem.lp b/tests/skolem.lp new file mode 100644 index 000000000..6b057d462 --- /dev/null +++ b/tests/skolem.lp @@ -0,0 +1,53 @@ +constant symbol Prop : TYPE; +builtin "Prop" ≔ Prop; +injective symbol π : Prop → TYPE; +builtin "P" ≔ π; +constant symbol Set : TYPE; +injective symbol τ : Set → TYPE; +builtin "T" ≔ τ; +inductive ℕ : TYPE ≔ // `dN +| 0 : ℕ +| s : ℕ → ℕ; +constant symbol nat : Set; +rule τ nat ↪ ℕ; + +symbol is0 : ℕ → Prop; +builtin "0" ≔ 0; +builtin "+1" ≔ s; +symbol one ≔ s 0; + +symbol + : ℕ → ℕ → ℕ; +notation + infix right 20; +rule 0 + $y ↪ $y +with s $x + $y ↪ s ($x + $y); + +symbol × : ℕ → ℕ → ℕ; // \times +notation × infix right 30; +rule 0 × _ ↪ 0 +with s $x × $y ↪ $y + $x × $y; + +constant symbol ∃ [a] : (τ a → Prop) → Prop; +notation ∃ quantifier; +builtin "ex" ≔ ∃; + +constant symbol ∀ [a] : (τ a → Prop) → Prop; +builtin "all" ≔ ∀; +constant symbol = [a] : τ a → τ a → Prop; +notation = infix 10; +builtin "eq" ≔ =; +symbol =-refl x : π(x = x); +constant symbol eq_refl [a] (x:τ a) : π (x = x); +constant symbol imp : Prop → Prop → Prop; +builtin "imp" ≔ imp; // écrire regle +rule π (imp $a $b) ↪ π $a → π $b; + +symbol zero_eq_zero : π (∃ (λ y : τ nat, (0 + y = 0))) ≔ +begin + print; + simplify +; + print; + skolem; + + print; + +end; \ No newline at end of file diff --git a/tests/skolem.ml b/tests/skolem.ml new file mode 100644 index 000000000..0b0ce67ef --- /dev/null +++ b/tests/skolem.ml @@ -0,0 +1,190 @@ + open Common + open Core open Term open Print + open Parsing + + (** Builtin configuration for propositional logic. *) + type config = + { symb_ex : sym (** Exists(∃) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) } + + (** [get_config ss pos] build the configuration using [ss]. *) + let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> + let builtin = Builtin.get ss pos in + { symb_ex = builtin "ex" + ; symb_all = builtin "all" } + + (**Pour dev uniquement : Permet de parser des termes en passant par une + commande lambdapi. A remplacer par une extension du parser pour pouvoir + tester sur des fichiers .lp*) + let parse_term s = + (* A hack to parse a term: wrap term [s] into [compute s;]. *) + let c = "compute " ^ s ^ ";" in + let command = (Stream.next (Parser.Lp.parse_string "term" c)) in + match command.elt with + | Syntax.P_query {elt=Syntax.P_query_normalize (t, _); _} -> t + | _ -> assert false + + (*let parse_declaration s = + let declaration = (Stream.next (Parser.Lp.parse_file s)) in + match declaration.elt with + | Syntax.P_command {elt=Syntax.P_symbol (s); _} -> s + | _ -> assert false*) + + (**Pour dev uniquement : A partir des termes parsés (pterm), construit + des Core.term *) + let scope_term ss = Scope.scope_term true ss [] + + (**Pour dev uniquement : Création d'une signature restreinte à laquelle + on ajoutera quelques symboles pour tester le code. A remplacer par une fonction + config*) + let new_sig_state : Sig_state.t = + let sign = Sig_state.create_sign (Sign.ghost_path "skl_test") in + Sig_state.of_sign sign + + let add_sym ss id = + Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Kind [] + None + + let sig_state = new_sig_state + (**Création de la signature. *) + + (*let symb_Set = parse_term "constant symbol Set : TYPE;" |> scope_term sig_state + let symb_El = parse_term "injective symbol El : Set → TYPE;" |> scope_term sig_state + let symb_A = parse_term "injective symbol A : Set;" |> scope_term sig_state + let symb_B = parse_term "injective symbol B : Set → Set;" |> scope_term sig_state*) + + let sig_state, symb_p = add_sym sig_state "P" + let sig_state, symb_x = add_sym sig_state "*" + let sig_state = Sig_state.add_notation sig_state symb_x (Sign.Prefix 1.) + (*Déclaration du symbole existentiel + notation quantifier. *) + (*quantifier Allows to write `f x, t instead of f (λ x, t): *) + let sig_state, symb_ex = add_sym sig_state "∃" + let sig_state = Sig_state.add_notation sig_state symb_ex Sign.Quant + let sig_state, symb_all = add_sym sig_state "∀" + let sig_state = Sig_state.add_notation sig_state symb_all Sign.Quant + let sig_state, symb_not = add_sym sig_state "¬" + + let sig_state, symb_Set = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "Set") Term.mk_Type [] None + (**Définition du type dépendant probablement pas correct *) + let sig_state, symb_El = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "El") (Term.mk_Appl (Term.mk_Symb symb_Set, Term.mk_Type)) [] None + let sig_state, symb_A = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "A") (Term.mk_Symb symb_Set) [] None + let sig_state, symb_B = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "B") (Term.mk_Appl (Term.mk_Symb symb_Set, Term.mk_Symb symb_Set)) [] None + + (*Le contexte de la skolémisation permet de mémoriser les variables + universelles. *) + let empty_context = [] + + let add_ctxt : ctxt->tvar->term->ctxt = + fun c var typ -> + (var, typ, None):: c + + + (*Debug : Pattern matching vérifie si [t_abs] est bien une + abstraction, et affiche ses composantes. *) + let decompose_abst t_abs = (*term list -> unit *) + match t_abs with + | [Abst(t, n)] -> (*(term, tbinder) *) + let a, b = Bindlib.unbind n in + Format.printf "Type abstraction : %a @." term t ; (*: term *) + Format.printf "Variable : %a @." term (mk_Vari a) ; (*: tvar*) + Format.printf "Formule : %a @." term b (*: term*) + | _ -> Format.printf "Erreur décomposition abst" + + (*Debug : Prend en argument un terme et vérifie si il est + constitué d'un symbole existentiel suivit d'une abstraction. + TODO : renvoyer l'adbstraction si c'est ok. Sinon erreur*) + (*Pour l'instant, ça sera une fonction term -> bool *) + let precond_simple t = + let u, ts = get_args t in + decompose_abst ts; + (is_symb symb_ex u) && are_quant_args (ts) + + let get_tbinder : term -> tbinder = + fun t_ex -> + let u, t_abs = get_args t_ex in + match t_abs with + | [Abst(a, n)] -> n (*(tbinder) *) + | _ -> failwith "Unable to get_tbinder : term is not an abs" + + + (**Skolémisation*) + (**Pour skolémiser ∃x, P*) + (** 1. Fonction new_skf génère un nouveau symbole de fonction, appelée + fonction de skolem. Soit [y_1, ..., y_n] l'ens des variables libres qui apparaissent + dans le terme P. La fonction de skolem estun symbole d'arité n.*) + (** 2. Substition dans P de la variable x par un symbole de fonction *) + + let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = + fun ss ctx cpt ex_typ -> + let name = if cpt > 0 then ("f"^(string_of_int (cpt))) else "c" in + let maj_sig, n_sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none name) (fst (Ctxt.to_prod ctx ex_typ)) [] + None + in + maj_sig, n_sym,(cpt + 1) + + + + (**Applique à un symbole de fonction [skf] la liste d'argument constituée + des variables quantifiées universelle mémorisés contexte [c]. + Substitution de la variable quantifiée existentielle par l'application + ainsi crée.*) + let subst_app : ctxt -> tbinder -> sym -> term = + fun c formule skf -> + let args_list = List.map (fun (v, _, _) -> mk_Vari v) c in + let f_term = mk_Symb skf in + let f_appl= add_args f_term args_list in + (*mk_Symb skf construit un terme à partir du symbole skf.*) + Bindlib.subst formule f_appl + + + let skolemisation : Sig_state.t -> term -> term = fun ss t -> + let rec skolemisation ss ctx cpt t = + Format.printf "@. Skolemisation du terme t : %a @." term t; + match get_args t with + | Symb(s), [a;Abst(x, tb)] when s == symb_ex -> (** \exists *) + let maj_ss, nv_sym, maj_cpt = new_skolem ss ctx cpt x in + let maj_term = subst_app ctx tb nv_sym in + Format.printf "@. Ex : substitution de %a par %a @." term t term maj_term; + skolemisation maj_ss ctx maj_cpt maj_term + | Symb(s), [a;Abst(b, tb)] when s == symb_all -> + let var, f = Bindlib.unbind tb in + let maj_ctx = add_ctxt ctx var a in + let maj_f = skolemisation ss maj_ctx cpt f in + let maj_tb = bind var lift maj_f in + add_args (mk_Symb s) [a ; mk_Abst (b, maj_tb)] + | _ -> t + in + skolemisation ss empty_context 0 t + + let rec nnf t = + match get_args t with + | Symb(s), [a;Abst(x, tb)] when s == symb_ex -> + let var, p = Bindlib.unbind tb in + let not_tb = bind var lift (nnf p) in + add_args (mk_Symb symb_all) [a; mk_Abst(x, not_tb)] + | Symb(s), [a; Abst(x, tb)] when s == symb_all -> (**Code redondant, remplacer par un ifdans le match case *) + let var, p = Bindlib.unbind tb in + let not_tb = bind var lift (nnf p) in + add_args (mk_Symb symb_ex) [a; mk_Abst(x, not_tb)] + (**PB de distrib du not *) + | Symb(s), tl when s == symb_not -> mk_Appl(nnf hd, tl) + | (hd, tl) -> (add_args (mk_Appl (symb_not, a) hd tl) + + + let _ = + + (*let t = parse_term "∀ P (λ x1 : P, (∃ P (λ y1 : P, ∀ P (λ x2 : P, (∃ P (λ y2 : P, x1 x2 y1 y2))))))" |> scope_term sig_state in + let t2 = parse_term "(∃ P (λ y2 : P, y2))" |> scope_term sig_state in + let t = parse_term "∃ A (λ x : A, (∀ (B x) (λ y : (B x), P x y)))" |> scope_term sig_state in*) + Format.print_string "@. Ligne 1"; + let t = parse_term "¬(∀ P (λ x:P, ∃ P (λ y : P, ∀ P (λ z : P, x y z))))" |> scope_term sig_state in + let nt = nnf t in + Format.print_string "@. Ligne 2"; + Format.printf "@.Terme entrée : %a @." term t; + Format.printf "@.Terme en nnf : %a @." term nt; + let _, _, l = get_args_len t in + Format.print_string "Nombres d'arguments : "; + Format.print_int l; + Format.print_newline (); + (*let skt = (skolemisation sig_state t) in + Format.printf "@.Terme skolémisé : %a @." term skt;*) \ No newline at end of file From 32ac1cab27e8f32c3eb5f21f4cf243a46b7dbc90 Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Mon, 30 May 2022 10:37:58 +0200 Subject: [PATCH 02/16] =?UTF-8?q?D=C3=A9finition=20de=20P=5Ftac=5Fskolem?= =?UTF-8?q?=20dans=20handle.ml?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/handle/tactic.ml | 34 ++++++++++++++++++++++++++++++---- src/parsing/lpLexer.ml | 2 ++ src/parsing/lpParser.mly | 2 ++ src/parsing/pretty.ml | 2 ++ src/parsing/syntax.ml | 2 ++ 5 files changed, 38 insertions(+), 4 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 4ca77dfbe..0a94dba5f 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -18,8 +18,9 @@ let admitted : int Stdlib.ref = Stdlib.ref (-1) (** [add_axiom ss sym_pos m] adds in signature state [ss] a new axiom symbol of type [!(m.meta_type)] and instantiate [m] with it. WARNING: It does not - check whether the type of [m] contains metavariables. *) -let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t = + check whether the type of [m] contains metavariables. Return updated signature + state [ss] and the new axiom symbol.*) +let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t * sym = fun ss sym_pos m -> let name = let i = Stdlib.(incr admitted; !admitted) in @@ -48,7 +49,7 @@ let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t = let ax = _Appl_Symb sym (Array.to_list vars |> List.map _Vari) in Bindlib.(bind_mvar vars ax |> unbox) in - LibMeta.set (new_problem()) m meta_value; ss + LibMeta.set (new_problem()) m meta_value; (ss, sym) (** [admit_meta ss sym_pos m] adds as many axioms as needed in the signature state [ss] to instantiate the metavariable [m] by a fresh axiom added to @@ -61,7 +62,7 @@ let admit_meta : Sig_state.t -> popt -> meta -> Sig_state.t = (* This assertion should be ensured by the typechecking algorithm. *) assert (not (MetaSet.mem m ms)); LibMeta.iter true (admit (MetaSet.add m ms)) [] !(m.meta_type); - Stdlib.(ss := add_axiom !ss sym_pos m) + Stdlib.(ss := fst (add_axiom !ss sym_pos m)) in admit MetaSet.empty m; Stdlib.(!ss) @@ -335,6 +336,31 @@ let handle : let p = new_problem() in tac_refine pos ps gt gs p (Why3_tactic.handle ss sym_pos cfg gt) | _ -> assert false) + | P_tac_skolem -> + (*Gets user-defined symbol identifiers mapped using "builtin" command : *) + let symb_imp = Builtin.get ss pos "imp" in + let symb_P = Builtin.get ss pos "P" in + (*Extract term [t] to skolemized in a typing goal of form π(t) *) + let t = match get_args gt.goal_type with + | Symb(s), [tl] when s == symb_P -> tl + | _ -> Format.print_string "@.Term not in form P (term)"; gt.goal_type + in + let skl_of_t = Skolem.handle ss sym_pos t in + let c = Env.to_ctxt env in + let p = new_problem() in + (*Equisat represents "π(skl_of_t ⇒ t)"*) + let equisat = mk_Appl (mk_Symb symb_P, add_args (mk_Symb symb_imp) [skl_of_t; t]) in + let t_meta_eqs = LibMeta.make p c equisat in + let meta_eqs = match t_meta_eqs with + | Meta(m, _) -> m + |_ -> assert false + in + (*ax is the axiom of equisatisfiability between a term and its + skolemized form.*) + let _, ax = add_axiom ss sym_pos meta_eqs in + let meta_type = LibMeta.make p c mk_Type in + let meta_x = LibMeta.make p c meta_type in + tac_refine sym_pos ps gt gs p (mk_Appl (mk_Symb ax, meta_x)) (** Representation of a tactic output. *) type tac_output = Sig_state.t * proof_state * Query.result diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index d3424894a..7d8350ba9 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -73,6 +73,7 @@ type token = | RULE | SEQUENTIAL | SIMPLIFY + | SKOLEM | SOLVE | SYMBOL | SYMMETRY @@ -239,6 +240,7 @@ let rec token lb = | "rule" -> RULE | "sequential" -> SEQUENTIAL | "simplify" -> SIMPLIFY + | "skolem" -> SKOLEM | "solve" -> SOLVE | "symbol" -> SYMBOL | "symmetry" -> SYMMETRY diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly index 440996de1..d4a2fce4e 100644 --- a/src/parsing/lpParser.mly +++ b/src/parsing/lpParser.mly @@ -66,6 +66,7 @@ %token RULE %token SEQUENTIAL %token SIMPLIFY +%token SKOLEM %token SOLVE %token SYMBOL %token SYMMETRY @@ -310,6 +311,7 @@ tactic: | REWRITE d=SIDE? p=rw_patt_spec? t=term { let b = match d with Some Pratter.Left -> false | _ -> true in make_pos $sloc (P_tac_rewrite(b,p,t)) } + | SKOLEM { make_pos $loc P_tac_skolem } | SIMPLIFY i=qid_or_nat? { make_pos $sloc (P_tac_simpl i) } | SOLVE { make_pos $sloc P_tac_solve } | SYMMETRY { make_pos $sloc P_tac_sym } diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index eed658828..b5a3f5f34 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -65,6 +65,7 @@ let _ = let open LpLexer in ; "rule", RULE ; "sequential", SEQUENTIAL ; "simplify", SIMPLIFY + ; "skolem", SKOLEM ; "solve", SOLVE ; "symbol", SYMBOL ; "symmetry", SYMMETRY @@ -275,6 +276,7 @@ let tactic : p_tactic pp = fun ppf { elt; _ } -> out ppf "rewrite%a%a %a" dir b (Option.pp pat) p term t | P_tac_simpl None -> out ppf "simplify" | P_tac_simpl (Some qid) -> out ppf "simplify %a" qident qid + | P_tac_skolem -> out ppf "skolem" | P_tac_solve -> out ppf "solve" | P_tac_sym -> out ppf "symmetry" | P_tac_why3 p -> diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index deb23ebda..cd9d80587 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -202,6 +202,7 @@ type p_tactic_aux = | P_tac_rewrite of bool * p_rw_patt option * p_term (* The boolean indicates if the equation is applied from left to right. *) | P_tac_simpl of p_qident option + | P_tac_skolem | P_tac_solve | P_tac_sym | P_tac_why3 of string option @@ -560,6 +561,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = | P_tac_sym | P_tac_why3 _ | P_tac_solve + | P_tac_skolem | P_tac_fail | P_tac_generalize _ | P_tac_induction -> (vs, a) From 0c03448e302a3704a1cb32a90e7c1e215748164a Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Tue, 7 Jun 2022 09:45:50 +0200 Subject: [PATCH 03/16] Correction axiome dans la tactique skolemisation --- src/handle/tactic.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 0a94dba5f..93b92baee 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -338,25 +338,27 @@ let handle : | _ -> assert false) | P_tac_skolem -> (*Gets user-defined symbol identifiers mapped using "builtin" command : *) - let symb_imp = Builtin.get ss pos "imp" in let symb_P = Builtin.get ss pos "P" in - (*Extract term [t] to skolemized in a typing goal of form π(t) *) + (*Extract term [t] in a typing goal of form π(t) *) let t = match get_args gt.goal_type with | Symb(s), [tl] when s == symb_P -> tl | _ -> Format.print_string "@.Term not in form P (term)"; gt.goal_type in - let skl_of_t = Skolem.handle ss sym_pos t in + let skl_t = Skolem.handle ss sym_pos t in let c = Env.to_ctxt env in let p = new_problem() in - (*Equisat represents "π(skl_of_t ⇒ t)"*) - let equisat = mk_Appl (mk_Symb symb_P, add_args (mk_Symb symb_imp) [skl_of_t; t]) in + (*Equisat represents "π (skl_t) → π (t)"*) + let var_cst = new_tvar "cst" in + let proof_t = mk_Appl (mk_Symb symb_P, t) in + let proof_skl_t = mk_Appl (mk_Symb symb_P, skl_t) in + let equisat = mk_Prod (proof_skl_t, bind var_cst lift proof_t) in let t_meta_eqs = LibMeta.make p c equisat in let meta_eqs = match t_meta_eqs with | Meta(m, _) -> m |_ -> assert false in - (*ax is the axiom of equisatisfiability between a term and its - skolemized form.*) + (*ax is the axiom of equisatisfiability between a proof of a term [t] + and a proof of its skolemized form [skl_t].*) let _, ax = add_axiom ss sym_pos meta_eqs in let meta_type = LibMeta.make p c mk_Type in let meta_x = LibMeta.make p c meta_type in From c6450169a5126ed29b9e6dcbac4fb2947ca52b0b Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Tue, 7 Jun 2022 09:50:11 +0200 Subject: [PATCH 04/16] suppression tests/skolem.ml --- tests/skolem.ml | 190 ------------------------------------------------ 1 file changed, 190 deletions(-) delete mode 100644 tests/skolem.ml diff --git a/tests/skolem.ml b/tests/skolem.ml deleted file mode 100644 index 0b0ce67ef..000000000 --- a/tests/skolem.ml +++ /dev/null @@ -1,190 +0,0 @@ - open Common - open Core open Term open Print - open Parsing - - (** Builtin configuration for propositional logic. *) - type config = - { symb_ex : sym (** Exists(∃) symbol. *) - ; symb_all : sym (** Forall(∀) symbol. *) } - - (** [get_config ss pos] build the configuration using [ss]. *) - let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> - let builtin = Builtin.get ss pos in - { symb_ex = builtin "ex" - ; symb_all = builtin "all" } - - (**Pour dev uniquement : Permet de parser des termes en passant par une - commande lambdapi. A remplacer par une extension du parser pour pouvoir - tester sur des fichiers .lp*) - let parse_term s = - (* A hack to parse a term: wrap term [s] into [compute s;]. *) - let c = "compute " ^ s ^ ";" in - let command = (Stream.next (Parser.Lp.parse_string "term" c)) in - match command.elt with - | Syntax.P_query {elt=Syntax.P_query_normalize (t, _); _} -> t - | _ -> assert false - - (*let parse_declaration s = - let declaration = (Stream.next (Parser.Lp.parse_file s)) in - match declaration.elt with - | Syntax.P_command {elt=Syntax.P_symbol (s); _} -> s - | _ -> assert false*) - - (**Pour dev uniquement : A partir des termes parsés (pterm), construit - des Core.term *) - let scope_term ss = Scope.scope_term true ss [] - - (**Pour dev uniquement : Création d'une signature restreinte à laquelle - on ajoutera quelques symboles pour tester le code. A remplacer par une fonction - config*) - let new_sig_state : Sig_state.t = - let sign = Sig_state.create_sign (Sign.ghost_path "skl_test") in - Sig_state.of_sign sign - - let add_sym ss id = - Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Kind [] - None - - let sig_state = new_sig_state - (**Création de la signature. *) - - (*let symb_Set = parse_term "constant symbol Set : TYPE;" |> scope_term sig_state - let symb_El = parse_term "injective symbol El : Set → TYPE;" |> scope_term sig_state - let symb_A = parse_term "injective symbol A : Set;" |> scope_term sig_state - let symb_B = parse_term "injective symbol B : Set → Set;" |> scope_term sig_state*) - - let sig_state, symb_p = add_sym sig_state "P" - let sig_state, symb_x = add_sym sig_state "*" - let sig_state = Sig_state.add_notation sig_state symb_x (Sign.Prefix 1.) - (*Déclaration du symbole existentiel + notation quantifier. *) - (*quantifier Allows to write `f x, t instead of f (λ x, t): *) - let sig_state, symb_ex = add_sym sig_state "∃" - let sig_state = Sig_state.add_notation sig_state symb_ex Sign.Quant - let sig_state, symb_all = add_sym sig_state "∀" - let sig_state = Sig_state.add_notation sig_state symb_all Sign.Quant - let sig_state, symb_not = add_sym sig_state "¬" - - let sig_state, symb_Set = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "Set") Term.mk_Type [] None - (**Définition du type dépendant probablement pas correct *) - let sig_state, symb_El = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "El") (Term.mk_Appl (Term.mk_Symb symb_Set, Term.mk_Type)) [] None - let sig_state, symb_A = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "A") (Term.mk_Symb symb_Set) [] None - let sig_state, symb_B = Sig_state.add_symbol sig_state Public Const Eager true (Pos.none "B") (Term.mk_Appl (Term.mk_Symb symb_Set, Term.mk_Symb symb_Set)) [] None - - (*Le contexte de la skolémisation permet de mémoriser les variables - universelles. *) - let empty_context = [] - - let add_ctxt : ctxt->tvar->term->ctxt = - fun c var typ -> - (var, typ, None):: c - - - (*Debug : Pattern matching vérifie si [t_abs] est bien une - abstraction, et affiche ses composantes. *) - let decompose_abst t_abs = (*term list -> unit *) - match t_abs with - | [Abst(t, n)] -> (*(term, tbinder) *) - let a, b = Bindlib.unbind n in - Format.printf "Type abstraction : %a @." term t ; (*: term *) - Format.printf "Variable : %a @." term (mk_Vari a) ; (*: tvar*) - Format.printf "Formule : %a @." term b (*: term*) - | _ -> Format.printf "Erreur décomposition abst" - - (*Debug : Prend en argument un terme et vérifie si il est - constitué d'un symbole existentiel suivit d'une abstraction. - TODO : renvoyer l'adbstraction si c'est ok. Sinon erreur*) - (*Pour l'instant, ça sera une fonction term -> bool *) - let precond_simple t = - let u, ts = get_args t in - decompose_abst ts; - (is_symb symb_ex u) && are_quant_args (ts) - - let get_tbinder : term -> tbinder = - fun t_ex -> - let u, t_abs = get_args t_ex in - match t_abs with - | [Abst(a, n)] -> n (*(tbinder) *) - | _ -> failwith "Unable to get_tbinder : term is not an abs" - - - (**Skolémisation*) - (**Pour skolémiser ∃x, P*) - (** 1. Fonction new_skf génère un nouveau symbole de fonction, appelée - fonction de skolem. Soit [y_1, ..., y_n] l'ens des variables libres qui apparaissent - dans le terme P. La fonction de skolem estun symbole d'arité n.*) - (** 2. Substition dans P de la variable x par un symbole de fonction *) - - let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = - fun ss ctx cpt ex_typ -> - let name = if cpt > 0 then ("f"^(string_of_int (cpt))) else "c" in - let maj_sig, n_sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none name) (fst (Ctxt.to_prod ctx ex_typ)) [] - None - in - maj_sig, n_sym,(cpt + 1) - - - - (**Applique à un symbole de fonction [skf] la liste d'argument constituée - des variables quantifiées universelle mémorisés contexte [c]. - Substitution de la variable quantifiée existentielle par l'application - ainsi crée.*) - let subst_app : ctxt -> tbinder -> sym -> term = - fun c formule skf -> - let args_list = List.map (fun (v, _, _) -> mk_Vari v) c in - let f_term = mk_Symb skf in - let f_appl= add_args f_term args_list in - (*mk_Symb skf construit un terme à partir du symbole skf.*) - Bindlib.subst formule f_appl - - - let skolemisation : Sig_state.t -> term -> term = fun ss t -> - let rec skolemisation ss ctx cpt t = - Format.printf "@. Skolemisation du terme t : %a @." term t; - match get_args t with - | Symb(s), [a;Abst(x, tb)] when s == symb_ex -> (** \exists *) - let maj_ss, nv_sym, maj_cpt = new_skolem ss ctx cpt x in - let maj_term = subst_app ctx tb nv_sym in - Format.printf "@. Ex : substitution de %a par %a @." term t term maj_term; - skolemisation maj_ss ctx maj_cpt maj_term - | Symb(s), [a;Abst(b, tb)] when s == symb_all -> - let var, f = Bindlib.unbind tb in - let maj_ctx = add_ctxt ctx var a in - let maj_f = skolemisation ss maj_ctx cpt f in - let maj_tb = bind var lift maj_f in - add_args (mk_Symb s) [a ; mk_Abst (b, maj_tb)] - | _ -> t - in - skolemisation ss empty_context 0 t - - let rec nnf t = - match get_args t with - | Symb(s), [a;Abst(x, tb)] when s == symb_ex -> - let var, p = Bindlib.unbind tb in - let not_tb = bind var lift (nnf p) in - add_args (mk_Symb symb_all) [a; mk_Abst(x, not_tb)] - | Symb(s), [a; Abst(x, tb)] when s == symb_all -> (**Code redondant, remplacer par un ifdans le match case *) - let var, p = Bindlib.unbind tb in - let not_tb = bind var lift (nnf p) in - add_args (mk_Symb symb_ex) [a; mk_Abst(x, not_tb)] - (**PB de distrib du not *) - | Symb(s), tl when s == symb_not -> mk_Appl(nnf hd, tl) - | (hd, tl) -> (add_args (mk_Appl (symb_not, a) hd tl) - - - let _ = - - (*let t = parse_term "∀ P (λ x1 : P, (∃ P (λ y1 : P, ∀ P (λ x2 : P, (∃ P (λ y2 : P, x1 x2 y1 y2))))))" |> scope_term sig_state in - let t2 = parse_term "(∃ P (λ y2 : P, y2))" |> scope_term sig_state in - let t = parse_term "∃ A (λ x : A, (∀ (B x) (λ y : (B x), P x y)))" |> scope_term sig_state in*) - Format.print_string "@. Ligne 1"; - let t = parse_term "¬(∀ P (λ x:P, ∃ P (λ y : P, ∀ P (λ z : P, x y z))))" |> scope_term sig_state in - let nt = nnf t in - Format.print_string "@. Ligne 2"; - Format.printf "@.Terme entrée : %a @." term t; - Format.printf "@.Terme en nnf : %a @." term nt; - let _, _, l = get_args_len t in - Format.print_string "Nombres d'arguments : "; - Format.print_int l; - Format.print_newline (); - (*let skt = (skolemisation sig_state t) in - Format.printf "@.Terme skolémisé : %a @." term skt;*) \ No newline at end of file From 0f90c9f47be043a43511ae71a1a5d4651d488f18 Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Mon, 4 Jul 2022 10:47:31 +0200 Subject: [PATCH 05/16] nnf + prenexe --- tests/cnfnnf.ml | 319 ++++++++++++++++++++++++++++++++++++++++++++++++ tests/dune | 2 +- 2 files changed, 320 insertions(+), 1 deletion(-) create mode 100644 tests/cnfnnf.ml diff --git a/tests/cnfnnf.ml b/tests/cnfnnf.ml new file mode 100644 index 000000000..2665745cd --- /dev/null +++ b/tests/cnfnnf.ml @@ -0,0 +1,319 @@ +open Common +open Core open Term open Print open Sig_state +open Pos +open Parsing + +(*** Hack pour le debug ***) +let parse_term s = + (* A hack to parse a term: wrap term [s] into [compute s;]. *) + let c = "compute " ^ s ^ ";" in + let command = (Stream.next (Parser.Lp.parse_string "term" c)) in + match command.elt with + | Syntax.P_query {elt=Syntax.P_query_normalize (t, _); _} -> t + | _ -> assert false + +(*** Hack pour le debug ***) +let scope_term ?(ctx=[]) ss = Scope.scope_term true ss ctx + +(*** Hack pour le debug ***) +let add_sym (ss, slist) id = + let ss, sym = Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Type [] + None + in + (ss, sym::slist) + +(*** Hack pour le debug ***) +let sig_state : Sig_state.t = + let sign = Sig_state.create_sign (Sign.ghost_path "") in + Sig_state.of_sign sign + + +(** Builtin configuration for propositional logic. *) +type config = + { symb_P : sym (** Encoding of propositions. *) + ; symb_T : sym (** Encoding of types. *) + ; symb_or : sym (** Disjunction(∨) symbol. *) + ; symb_and : sym (** Conjunction(∧) symbol. *) + ; symb_imp : sym (** Implication(⇒) symbol. *) + ; symb_bot : sym (** Bot(⊥) symbol. *) + ; symb_top : sym (** Top(⊤) symbol. *) + ; symb_not : sym (** Not(¬) symbol. *) + ; symb_ex : sym (** Exists(∃) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) } + + +(** Hack debug -> a remplacer par la fonction get_config cf why3_tactic.ml**) +let fol_symb_str = ["P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" ] +(** [get_config ss pos] build the configuration using [ss]. *) +let get_config slist = + let get n = List.nth slist n in + { symb_P = get 0 + ; symb_T = get 1 + ; symb_or = get 2 + ; symb_and = get 3 + ; symb_imp = get 4 + ; symb_bot = get 5 + ; symb_top = get 6 + ; symb_not = get 7 + ; symb_ex = get 8 + ; symb_all = get 9} + + + +let mk_env symb_p = + let tv = ["A"; "B"] in + let rec aux e tlist = + let tb_p = _Symb symb_p in + match tlist with + | hd::tl -> aux (Env.add (new_tvar hd) tb_p None e) tl + | [] -> e + in + aux Env.empty tv + +type quant = +{ symb : sym +; dom : term +; var : tvar +; typ : term} + +let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = + fun qlist q d v t -> + {symb = q; dom = d; var = v; typ = t}::qlist + +let mk_quant : term -> quant -> term = + fun f q -> + let tb = bind (q.var) lift f in + add_args (mk_Symb q.symb) [q.dom; mk_Abst(q.typ, tb)] + +let nnf_term : config -> term -> term = fun cfg t -> + Printf.printf "------ Start nnf_term ------" ; + let rec nnf_prop t = + Format.printf "@.-___- Start nnf_prop -___- %a @." term t; + match get_args t with + | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [neg t1; nnf_prop t2] + | Symb(s), [t] when s == cfg.symb_not -> + Format.printf "@.NNF Not t, with t = %a @." term t; + neg t + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] + | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t + | Abst(_, _), _ -> Format.printf "@.Etat ABS: %a @." term t; t + | w, _ -> Format.printf "@.NNF puit: %a @." term w; t + and neg t = + Format.printf "@.**** Start Neg**** : %a @." term t; + match get_args t with + | Symb(s), [] when s == cfg.symb_bot -> + mk_Symb cfg.symb_top + (*add_args (mk_Symb cfg.symb_bot) []*) + | Symb(s), [] when s == cfg.symb_top -> + mk_Symb cfg.symb_bot + (*add_args (mk_Symb cfg.symb_top) []*) + | Symb(s), [t1; t2] when s == cfg.symb_and -> + Format.printf "@.NEG : and -> %a @." term t; + add_args (mk_Symb cfg.symb_or) [neg t1; neg t2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> + Format.printf "@.NEG : or -> %a @." term t; + add_args (mk_Symb cfg.symb_and) [neg t1; neg t2] + | Symb(s), [t1; t2] when s == cfg.symb_imp -> + Format.printf "@.NEG : imp -> %a @." term t; + neg (nnf_prop t) + | Symb(s), [nt] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + nnf_prop nt + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let neg_tb = bind var lift (neg p) in + Format.printf "@.NEG : Forall -> %a @." term t; + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg p) in + Format.printf "@.NEG : exists -> %a @." term t; + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | w, _ -> Format.printf "@. NEG : terme atomique -> %a @." term w; add_args (mk_Symb cfg.symb_not) [t] + in + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) + | _ -> failwith "Cant NNF a term that is not a Prop !" + +let prenex_term cfg t = + let rec prenex t = + match get_args t with + | Symb(s), [t1; t2] when s == cfg.symb_and -> + let qlist1, sub1 = prenex t1 + in + let qlist2, sub2 = prenex t2 + in + let t = add_args (mk_Symb s) [sub1; sub2] + in + let qlist = qlist1@qlist2 in + qlist, t + | Symb(s), [t1; t2] when s == cfg.symb_or -> + let qlist1, sub1 = prenex t1 + in + let qlist2, sub2 = prenex t2 + in + let t = add_args (mk_Symb s) [sub1; sub2] + in + let qlist = qlist1@qlist2 in + qlist, t + | Symb(s), [t1; t2] when s == cfg.symb_imp -> failwith "Prenex : symb_imp occurs but t must be NNF" + | Symb(s), [nt] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + let res = + match nt with + | Vari(x) -> ([], t) + | Symb(s) -> ([], t) + | _ -> failwith "Prenex : symb_not formula must be NNF" + in + res + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + qlist, sf + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + qlist, sf + | w, _ -> [], t + in + let qlist, f = + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; prenex t + | _ -> failwith "Cant PRENEX a term that is not a Prop !" + in + List.fold_left mk_quant f (List.rev qlist) + + (*"P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀"*) + + +let _ = + let sig_state, symlist = + List.fold_left add_sym (sig_state, []) fol_symb_str + in + let symlist = List.rev symlist in + let c = get_config symlist + in + let env = mk_env (List.nth symlist 0) + in + let t = parse_term "P (∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥))))" |> scope_term ~ctx:env sig_state in + Format.printf "@.Terme IN : %a @." term t; + let nnt = (nnf_term c t) in + Format.printf "@.Terme en NNF : %a @." term nnt; + let f = parse_term "P (∨ (∀ P (λ x1, x1)) A)" |> scope_term ~ctx:env sig_state in + let pf = prenex_term c t in + Format.printf "@.Terme en PF : %a @." term pf; + + + (*let add_type ss id = + Sig_state.add_symbol ss Public Const Eager true (Pos.none id) mk_Type [] + None + +let add_quant p id = + let ss, ty = p in + let quant_type = mk_Appl (mk_Appl (mk_Appl (ty, ty), ty), ty) in + let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) quant_type [] + None + in + (add_notation ss sym Quant, sym) + +let add_binop p id = + let ss, ty = p in + let binop_type = mk_Appl (mk_Appl (ty, ty), ty) in + let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) binop_type [] + None + in + (add_notation ss sym (Infix(Right, 5.)), sym) + +let add_const ss ty id ty = + Sig_state.add_symbol ss Public Const Eager true (Pos.none id) ty [] + None + +let add_unop ss ty id = + let unop_type = mk_Appl (ty, ty) in + let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) unop_type [] + None + in + (add_notation ss sym (Prefix(3.)), sym)*) + + (*let nnf_term : config -> term -> term = fun cfg t -> + Printf.printf "------ Start nnf_term ------" ; + let symb_P = cfg.symb_P in + let rec nnf_prop t = + Format.printf "@.-___- Start nnf_prop -___- %a @." term t; + match get_args t with + | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_imp -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in + add_args (mk_Symb cfg.symb_or) [neg_term subt1; nnf_prop t2] + | Symb(s), [t] when s == cfg.symb_not -> + Format.printf "@.NNF : Not : %a @." term t; + let subt = mk_Appl (mk_Symb symb_P, t) in + neg_term subt + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] + | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t + | Abst(_, _), _ -> Format.printf "@.NNF Etat ABS: %a @." term t; t + | w, _ -> Format.printf "@.NNF What: %a @." term w; t + and neg_term t = + let rec neg_prop t = + Format.printf "@.**** Start Neg_prop**** : %a @." term t; + match get_args t with + | Symb(s), [] when s == cfg.symb_bot -> + add_args (mk_Symb cfg.symb_bot) [] + | Symb(s), [] when s == cfg.symb_top -> + add_args (mk_Symb cfg.symb_top) [] + | Symb(s), [t1; t2] when s == cfg.symb_and -> + let subt1 = mk_Appl (mk_Symb symb_P, t1) in + let subt2 = mk_Appl (mk_Symb symb_P, t2) in + add_args (mk_Symb cfg.symb_or) [neg_term subt1; neg_term subt2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> + Format.printf "@.neg : OR : %a @." term t; + let subt1 = mk_Appl (mk_Symb symb_P, t1) in + let subt2 = mk_Appl (mk_Symb symb_P, t2) in + add_args (mk_Symb cfg.symb_and) [neg_term subt1; neg_term subt2] + | Symb(s), [t1; t2] when s == cfg.symb_imp -> neg_prop (nnf_prop t) + | Symb(s), [nt] when s == cfg.symb_not -> + Format.printf "@.neg : NOT : %a @." term nt; + (match nt with + | Symb(_) -> t + | Vari (_) -> t + | _ -> + let subtnt = mk_Appl (mk_Symb symb_P, nt) in + nnf_prop subtnt) + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let neg_tb = bind var lift (neg_prop p) in + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg_prop p) in + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | w, tl -> Format.printf "@.NEG What: %a @." term w; List.map (Format.printf "; %a ;" term) tl; t + in + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.NEG get_args : %a @." term (mk_Symb s); neg_prop t + | _ -> Format.printf "@.NEG fails : %a @." term t; failwith "Cant NEG a term that is not a Prop !" + in + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> nnf_prop t + | _ -> failwith "Cant NNF a term that is not a Prop !" + +let fol_symb_str = [ "P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" ]*) \ No newline at end of file diff --git a/tests/dune b/tests/dune index feeb644e1..746b88494 100644 --- a/tests/dune +++ b/tests/dune @@ -1,5 +1,5 @@ (tests - (names ok_ko rewriting purity kernel) + (names ok_ko rewriting purity kernel cnfnnf) (deps (glob_files OK/*.lp) (glob_files OK/*.dk) From bd69824d919d8182c0721f0a52ab190d20059c3b Mon Sep 17 00:00:00 2001 From: "taissir.marce" Date: Wed, 6 Jul 2022 09:28:59 +0200 Subject: [PATCH 06/16] Tactique de skolemisation : Mise en NNF et forme prenexe avant l'elimination des existentiels --- src/handle/skolem.ml | 172 +++++++++++++++++++++++++++++++++++++++++-- src/handle/tactic.ml | 2 +- 2 files changed, 166 insertions(+), 8 deletions(-) diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index 9130bd02f..95c1bc18a 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -1,22 +1,50 @@ open Common -open Core open Term +open Core open Term open Print (** Logging function for the skolem tactic. *) let log_sklm = Logger.make '!' "sklm" "the skolemization tactic" let log_sklm = log_sklm.pp -(** Builtin configuration for propositional logic. *) -type config = +(** Builtin configuration for propositional logic. +type min_config = { symb_ex : sym (** Exists(∃) symbol. *) ; symb_all : sym (** Forall(∀) symbol. *) ; symb_P : sym (** Encoding of propositions. *)} (** [get_config ss pos] build the configuration using [ss]. *) -let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> +let get_min_config : Sig_state.t -> Pos.popt -> min_config = fun ss pos -> let builtin = Builtin.get ss pos in { symb_ex = builtin "ex" ; symb_all = builtin "all" - ; symb_P = builtin "P"} + ; symb_P = builtin "P"}*) + + +(** Builtin configuration for propositional logic. *) +type fol_config = + { symb_P : sym (** Encoding of propositions. *) + ; symb_T : sym (** Encoding of types. *) + ; symb_or : sym (** Disjunction(∨) symbol. *) + ; symb_and : sym (** Conjunction(∧) symbol. *) + ; symb_imp : sym (** Implication(⇒) symbol. *) + ; symb_bot : sym (** Bot(⊥) symbol. *) + ; symb_top : sym (** Top(⊤) symbol. *) + ; symb_not : sym (** Not(¬) symbol. *) + ; symb_ex : sym (** Exists(∃) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) } + +(** [get_config ss pos] build the configuration using [ss]. *) +let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = fun ss pos -> + let builtin = Builtin.get ss pos in + { symb_P = builtin "P" + ; symb_T = builtin "T" + ; symb_or = builtin "or" + ; symb_and = builtin "and" + ; symb_imp = builtin "imp" + ; symb_bot = builtin "bot" + ; symb_top = builtin "top" + ; symb_not = builtin "not" + ; symb_ex = builtin "ex" + ; symb_all = builtin "all" } (*Context of skolemization allow to record introduced variables and their types when universal quantifiers occurs.*) @@ -69,6 +97,133 @@ let subst_app : ctxt -> tbinder -> sym -> term = Bindlib.subst tb f_appl + +type quant = +{ symb : sym +; dom : term +; var : tvar +; typ : term} + +let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = + fun qlist q d v t -> + {symb = q; dom = d; var = v; typ = t}::qlist + +let mk_quant : term -> quant -> term = + fun f q -> + let tb = bind (q.var) lift f in + add_args (mk_Symb q.symb) [q.dom; mk_Abst(q.typ, tb)] + +let nnf_term : fol_config -> term -> term = fun cfg t -> + Printf.printf "------ Start nnf_term ------" ; + let rec nnf_prop t = + Format.printf "@.-___- Start nnf_prop -___- %a @." term t; + match get_args t with + | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] + | Symb(s), [t1; t2] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [neg t1; nnf_prop t2] + | Symb(s), [t] when s == cfg.symb_not -> + Format.printf "@.NNF Not t, with t = %a @." term t; + neg t + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] + | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t + | Abst(_, _), _ -> Format.printf "@.Etat ABS: %a @." term t; t + | w, _ -> Format.printf "@.NNF puit: %a @." term w; t + and neg t = + Format.printf "@.**** Start Neg**** : %a @." term t; + match get_args t with + | Symb(s), [] when s == cfg.symb_bot -> + mk_Symb cfg.symb_top + (*add_args (mk_Symb cfg.symb_bot) []*) + | Symb(s), [] when s == cfg.symb_top -> + mk_Symb cfg.symb_bot + (*add_args (mk_Symb cfg.symb_top) []*) + | Symb(s), [t1; t2] when s == cfg.symb_and -> + Format.printf "@.NEG : and -> %a @." term t; + add_args (mk_Symb cfg.symb_or) [neg t1; neg t2] + | Symb(s), [t1; t2] when s == cfg.symb_or -> + Format.printf "@.NEG : or -> %a @." term t; + add_args (mk_Symb cfg.symb_and) [neg t1; neg t2] + | Symb(s), [_; _] when s == cfg.symb_imp -> + Format.printf "@.NEG : imp -> %a @." term t; + neg (nnf_prop t) + | Symb(s), [nt] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + nnf_prop nt + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let neg_tb = bind var lift (neg p) in + Format.printf "@.NEG : Forall -> %a @." term t; + add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg p) in + Format.printf "@.NEG : exists -> %a @." term t; + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] + | w, _ -> Format.printf "@. NEG : terme atomique -> %a @." term w; add_args (mk_Symb cfg.symb_not) [t] + in + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) + | _ -> failwith "Cant NNF a term that is not a Prop !" + +let prenex_term cfg t = + let rec prenex t = + match get_args t with + | Symb(s), [t1; t2] when s == cfg.symb_and -> + let qlist1, sub1 = prenex t1 + in + let qlist2, sub2 = prenex t2 + in + let t = add_args (mk_Symb s) [sub1; sub2] + in + let qlist = qlist1@qlist2 in + qlist, t + | Symb(s), [t1; t2] when s == cfg.symb_or -> + let qlist1, sub1 = prenex t1 + in + let qlist2, sub2 = prenex t2 + in + let t = add_args (mk_Symb s) [sub1; sub2] + in + let qlist = qlist1@qlist2 in + qlist, t + | Symb(s), [_; _] when s == cfg.symb_imp -> failwith "Prenex : symb_imp occurs but t must be NNF" + | Symb(s), [nt] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + let res = + match nt with + | Vari(_) -> ([], t) + | Symb(_) -> ([], t) + | _ -> failwith "Prenex : symb_not formula must be NNF" + in + res + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + qlist, sf + | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + qlist, sf + | _, _ -> [], t + in + let qlist, f = + match get_args t with + | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; prenex t + | _ -> failwith "Cant PRENEX a term that is not a Prop !" + in + List.fold_left mk_quant f (List.rev qlist) + + + (**Main fonction : [skolemisation ss pos t] return a skolemized form of term [t]. (ie existential quantifications in [t] are removed) @@ -77,7 +232,10 @@ extended with new symbol [symb_skt] in order to substitute the variable binded by the said quantifier*) let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> (*Gets user-defined symbol identifiers mapped using "builtin" command.*) - let cfg = get_config ss pos in + let cfg = get_fol_config ss pos in + let t = mk_Appl (mk_Symb cfg.symb_P, t) in + let t = nnf_term cfg t in + let t = Format.printf "@.La nnf donne : %a @." term t; prenex_term cfg t in let rec skolemisation ss ctx ctr t = match get_args t with | Symb(s), [_;Abst(y, tb)] when s == cfg.symb_ex -> @@ -98,7 +256,7 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> add_args (mk_Symb s) [a ; mk_Abst (x, maj_tb)] | _ -> t in - let skl_of_t = skolemisation ss empty_context 0 t in + let skl_of_t = Format.printf "@.La fp donne : %a @." term t; skolemisation ss empty_context 0 t in if Logger.log_enabled () then log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t ; skl_of_t diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 93b92baee..c508b9b63 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -342,7 +342,7 @@ let handle : (*Extract term [t] in a typing goal of form π(t) *) let t = match get_args gt.goal_type with | Symb(s), [tl] when s == symb_P -> tl - | _ -> Format.print_string "@.Term not in form P (term)"; gt.goal_type + | _ -> Format.printf "@. Typing goal not in form P (term) %a @." term gt.goal_type; gt.goal_type in let skl_t = Skolem.handle ss sym_pos t in let c = Env.to_ctxt env in From dbdb3a0a84398a11b2cbd0f096ac1550dd9f9e68 Mon Sep 17 00:00:00 2001 From: Taissirbw Date: Wed, 6 Jul 2022 09:49:41 +0200 Subject: [PATCH 07/16] Print pour debug en commentaire --- src/handle/skolem.ml | 63 ++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 37 deletions(-) diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index 95c1bc18a..9c97da22d 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -5,19 +5,6 @@ open Core open Term open Print let log_sklm = Logger.make '!' "sklm" "the skolemization tactic" let log_sklm = log_sklm.pp -(** Builtin configuration for propositional logic. -type min_config = - { symb_ex : sym (** Exists(∃) symbol. *) - ; symb_all : sym (** Forall(∀) symbol. *) - ; symb_P : sym (** Encoding of propositions. *)} - -(** [get_config ss pos] build the configuration using [ss]. *) -let get_min_config : Sig_state.t -> Pos.popt -> min_config = fun ss pos -> - let builtin = Builtin.get ss pos in - { symb_ex = builtin "ex" - ; symb_all = builtin "all" - ; symb_P = builtin "P"}*) - (** Builtin configuration for propositional logic. *) type fol_config = @@ -32,7 +19,7 @@ type fol_config = ; symb_ex : sym (** Exists(∃) symbol. *) ; symb_all : sym (** Forall(∀) symbol. *) } -(** [get_config ss pos] build the configuration using [ss]. *) +(** [get_fol_config ss pos] build the configuration using [ss]. *) let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = fun ss pos -> let builtin = Builtin.get ss pos in { symb_P = builtin "P" @@ -96,33 +83,37 @@ let subst_app : ctxt -> tbinder -> sym -> term = let f_appl= add_args (mk_Symb symb_skt) args_list in Bindlib.subst tb f_appl - - +(* quant is a structure for representating quantifiers in a FOF.*) type quant = { symb : sym ; dom : term ; var : tvar ; typ : term} +(* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation of + the universal quantification of x:type_a on top of the list ql, and return the + list.*) let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = fun qlist q d v t -> {symb = q; dom = d; var = v; typ = t}::qlist +(* mk_quant builds an application of the quantifier q on the proposition f.*) let mk_quant : term -> quant -> term = fun f q -> let tb = bind (q.var) lift f in add_args (mk_Symb q.symb) [q.dom; mk_Abst(q.typ, tb)] +(* nnf_term compute the negation normal form of a FOF*) let nnf_term : fol_config -> term -> term = fun cfg t -> - Printf.printf "------ Start nnf_term ------" ; + (*Printf.printf "------ Start nnf_term ------" ;*) let rec nnf_prop t = - Format.printf "@.-___- Start nnf_prop -___- %a @." term t; + (*Format.printf "@.-___- Start nnf_prop -___- %a @." term t;*) match get_args t with | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [neg t1; nnf_prop t2] | Symb(s), [t] when s == cfg.symb_not -> - Format.printf "@.NNF Not t, with t = %a @." term t; + (*Format.printf "@.NNF Not t, with t = %a @." term t;*) neg t | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in @@ -132,44 +123,42 @@ let nnf_term : fol_config -> term -> term = fun cfg t -> let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (nnf_prop p) in add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] - | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t - | Abst(_, _), _ -> Format.printf "@.Etat ABS: %a @." term t; t - | w, _ -> Format.printf "@.NNF puit: %a @." term w; t + | Symb(s), _ -> (*Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s);*) t + | Abst(_, _), _ -> (*Format.printf "@.Etat ABS: %a @." term t;*) t + | w, _ -> (*Format.printf "@.NNF puit: %a @." term w;*) t and neg t = - Format.printf "@.**** Start Neg**** : %a @." term t; + (*Format.printf "@.**** Start Neg**** : %a @." term t;*) match get_args t with | Symb(s), [] when s == cfg.symb_bot -> mk_Symb cfg.symb_top - (*add_args (mk_Symb cfg.symb_bot) []*) | Symb(s), [] when s == cfg.symb_top -> mk_Symb cfg.symb_bot - (*add_args (mk_Symb cfg.symb_top) []*) | Symb(s), [t1; t2] when s == cfg.symb_and -> - Format.printf "@.NEG : and -> %a @." term t; + (*Format.printf "@.NEG : and -> %a @." term t;*) add_args (mk_Symb cfg.symb_or) [neg t1; neg t2] | Symb(s), [t1; t2] when s == cfg.symb_or -> - Format.printf "@.NEG : or -> %a @." term t; + (*Format.printf "@.NEG : or -> %a @." term t; *) add_args (mk_Symb cfg.symb_and) [neg t1; neg t2] | Symb(s), [_; _] when s == cfg.symb_imp -> - Format.printf "@.NEG : imp -> %a @." term t; + (*Format.printf "@.NEG : imp -> %a @." term t;*) neg (nnf_prop t) | Symb(s), [nt] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; + (*Format.printf "@.NEG : not -> %a @." term nt; *) nnf_prop nt | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in let neg_tb = bind var lift (neg p) in - Format.printf "@.NEG : Forall -> %a @." term t; + (*Format.printf "@.NEG : Forall -> %a @." term t;*) add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (neg p) in - Format.printf "@.NEG : exists -> %a @." term t; + (*Format.printf "@.NEG : exists -> %a @." term t;*) add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | w, _ -> Format.printf "@. NEG : terme atomique -> %a @." term w; add_args (mk_Symb cfg.symb_not) [t] + | w, _ -> (*Format.printf "@. NEG : terme atomique -> %a @." term w;*) add_args (mk_Symb cfg.symb_not) [t] in match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) + | (Symb(s), [t]) when s == cfg.symb_P -> (*Format.printf "@.P of : %a @." term t;*) mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) | _ -> failwith "Cant NNF a term that is not a Prop !" let prenex_term cfg t = @@ -195,12 +184,12 @@ let prenex_term cfg t = qlist, t | Symb(s), [_; _] when s == cfg.symb_imp -> failwith "Prenex : symb_imp occurs but t must be NNF" | Symb(s), [nt] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; + (*Format.printf "@.NEG : not -> %a @." term nt; *) let res = match nt with | Vari(_) -> ([], t) | Symb(_) -> ([], t) - | _ -> failwith "Prenex : symb_not formula must be NNF" + | _ -> failwith "Prenex : symb_not before a formula occurs, t is not in NNF"*) in res | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> @@ -217,7 +206,7 @@ let prenex_term cfg t = in let qlist, f = match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; prenex t + | (Symb(s), [t]) when s == cfg.symb_P -> (*Format.printf "@.P of : %a @." term t;*) prenex t | _ -> failwith "Cant PRENEX a term that is not a Prop !" in List.fold_left mk_quant f (List.rev qlist) @@ -235,7 +224,7 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> let cfg = get_fol_config ss pos in let t = mk_Appl (mk_Symb cfg.symb_P, t) in let t = nnf_term cfg t in - let t = Format.printf "@.La nnf donne : %a @." term t; prenex_term cfg t in + let t = prenex_term cfg t in let rec skolemisation ss ctx ctr t = match get_args t with | Symb(s), [_;Abst(y, tb)] when s == cfg.symb_ex -> From 9052a47d0600e81dafc67adfa1d46b5359d6df36 Mon Sep 17 00:00:00 2001 From: gabrielhdt Date: Wed, 20 Jul 2022 11:37:41 +0200 Subject: [PATCH 08/16] Formatting with ocamlformat The incantation is ocamlformat --disable-conf-files --enable-outside-detected-project \ --parse-docstrings --wrap-comments FILE --- src/handle/skolem.ml | 425 +++++++++++++++++++------------------- src/handle/skolem.mli | 5 +- tests/cnfnnf.ml | 465 ++++++++++++++++++++---------------------- 3 files changed, 432 insertions(+), 463 deletions(-) diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index 9c97da22d..cc69e6899 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -1,252 +1,247 @@ open Common -open Core open Term open Print +open Core +open Term +open Print (** Logging function for the skolem tactic. *) let log_sklm = Logger.make '!' "sklm" "the skolemization tactic" -let log_sklm = log_sklm.pp +let log_sklm = log_sklm.pp +type fol_config = { + symb_P : sym; (** Encoding of propositions. *) + symb_T : sym; (** Encoding of types. *) + symb_or : sym; (** Disjunction(∨) symbol. *) + symb_and : sym; (** Conjunction(∧) symbol. *) + symb_imp : sym; (** Implication(⇒) symbol. *) + symb_bot : sym; (** Bot(⊥) symbol. *) + symb_top : sym; (** Top(⊤) symbol. *) + symb_not : sym; (** Not(¬) symbol. *) + symb_ex : sym; (** Exists(∃) symbol. *) + symb_all : sym; (** Forall(∀) symbol. *) +} (** Builtin configuration for propositional logic. *) -type fol_config = - { symb_P : sym (** Encoding of propositions. *) - ; symb_T : sym (** Encoding of types. *) - ; symb_or : sym (** Disjunction(∨) symbol. *) - ; symb_and : sym (** Conjunction(∧) symbol. *) - ; symb_imp : sym (** Implication(⇒) symbol. *) - ; symb_bot : sym (** Bot(⊥) symbol. *) - ; symb_top : sym (** Top(⊤) symbol. *) - ; symb_not : sym (** Not(¬) symbol. *) - ; symb_ex : sym (** Exists(∃) symbol. *) - ; symb_all : sym (** Forall(∀) symbol. *) } (** [get_fol_config ss pos] build the configuration using [ss]. *) -let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = fun ss pos -> +let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = + fun ss pos -> let builtin = Builtin.get ss pos in - { symb_P = builtin "P" - ; symb_T = builtin "T" - ; symb_or = builtin "or" - ; symb_and = builtin "and" - ; symb_imp = builtin "imp" - ; symb_bot = builtin "bot" - ; symb_top = builtin "top" - ; symb_not = builtin "not" - ; symb_ex = builtin "ex" - ; symb_all = builtin "all" } - -(*Context of skolemization allow to record introduced variables and their types when -universal quantifiers occurs.*) + { + symb_P = builtin "P"; + symb_T = builtin "T"; + symb_or = builtin "or"; + symb_and = builtin "and"; + symb_imp = builtin "imp"; + symb_bot = builtin "bot"; + symb_top = builtin "top"; + symb_not = builtin "not"; + symb_ex = builtin "ex"; + symb_all = builtin "all"; + } + +(*Context of skolemization allow to record introduced variables and their types + when universal quantifiers occurs.*) let empty_context = [] -let add_ctxt : ctxt->tvar->term->ctxt = - fun c var typ -> - c @ [(var, typ, None)] +let add_ctxt : ctxt -> tvar -> term -> ctxt = + fun c var typ -> c @ [ (var, typ, None) ] (**Skolemization*) -(*[new_skolem ss ctx cpt ex_typ] is called when existantial quantifier ("∃y") occurs. -[ex_typ] is the type of quantificated variable "y". -In order to eliminate ∃ quantifier, we need to extend signature state [ss] with a skolem term, -represented by a fresh symbol that will later replace the binded variable ("y"). -Such skolem term may either be a skolem function or a skolem constant : -The type of a skolem term depends on registered variables in [ctx] -For example, if a set of variables x1:a1, x2:a2,..., xn:an were previously introduced by an -universal quantifier, A skolem term "skt" will take as arguments x1, ..., xn, and must therefore be -typed as follows : skt (x1, x2, ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. -A skolem term is a constant if skolemized term is not in the scope of any universal quantifier, -namely, [ctx] is empty. -For the sake of clarity, we use a counter [cpt] for naming the generated symbol. -OUT : Updated signature state [upt_sig] is returned, as well as introduced symbol [symb_skt] and updated counter*) - let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = - fun ss ctx ctr ex_typ -> - let skt_name = if (ctx == []) then ("c"^(string_of_int (ctr))) else ("f"^(string_of_int (ctr))) in - let skt, _ = Ctxt.to_prod ctx ex_typ in - let upt_sig, symb_skt = Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] - None - in - if Logger.log_enabled () then - log_sklm "New symbol %a" Print.sym symb_skt; - upt_sig, symb_skt,(ctr + 1) - - - -(*[Subst_app ctx tb s] builds [f_appl], the application of a symbol [symb_skt] -and a list of variables extracted from context [ctx]. Then, the binded -variable in [tb] is substituted by [f_appl]*) -(*Assumes type of [symb_skt] correspond to variables's types as they are -listed in context [ctx] *) +(*[new_skolem ss ctx cpt ex_typ] is called when existantial quantifier ("∃y") + occurs. [ex_typ] is the type of quantificated variable "y". In order to + eliminate ∃ quantifier, we need to extend signature state [ss] with a skolem + term, represented by a fresh symbol that will later replace the binded + variable ("y"). Such skolem term may either be a skolem function or a skolem + constant : The type of a skolem term depends on registered variables in [ctx] + For example, if a set of variables x1:a1, x2:a2,..., xn:an were previously + introduced by an universal quantifier, A skolem term "skt" will take as + arguments x1, ..., xn, and must therefore be typed as follows : skt (x1, x2, + ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. A skolem term is a constant if + skolemized term is not in the scope of any universal quantifier, namely, [ctx] + is empty. For the sake of clarity, we use a counter [cpt] for naming the + generated symbol. OUT : Updated signature state [upt_sig] is returned, as well + as introduced symbol [symb_skt] and updated counter*) +let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = + fun ss ctx ctr ex_typ -> + let skt_name = + if ctx == [] then "c" ^ string_of_int ctr else "f" ^ string_of_int ctr + in + let skt, _ = Ctxt.to_prod ctx ex_typ in + let upt_sig, symb_skt = + Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] + None + in + if Logger.log_enabled () then log_sklm "New symbol %a" Print.sym symb_skt; + (upt_sig, symb_skt, ctr + 1) + +(*[Subst_app ctx tb s] builds [f_appl], the application of a symbol [symb_skt] + and a list of variables extracted from context [ctx]. Then, the binded + variable in [tb] is substituted by [f_appl]*) +(*Assumes type of [symb_skt] correspond to variables's types as they are listed + in context [ctx] *) let subst_app : ctxt -> tbinder -> sym -> term = - fun ctx tb symb_skt -> - (*args_list : [tvar list], are context's variables*) - let args_list = List.map (fun (v, _, _) -> mk_Vari v) ctx in - (*[add_args] build the application of [f_term] to the list - of variables [args_list].*) - let f_appl= add_args (mk_Symb symb_skt) args_list in - Bindlib.subst tb f_appl + fun ctx tb symb_skt -> + (*args_list : [tvar list], are context's variables*) + let args_list = List.map (fun (v, _, _) -> mk_Vari v) ctx in + (*[add_args] build the application of [f_term] to the list of variables + [args_list].*) + let f_appl = add_args (mk_Symb symb_skt) args_list in + Bindlib.subst tb f_appl (* quant is a structure for representating quantifiers in a FOF.*) -type quant = -{ symb : sym -; dom : term -; var : tvar -; typ : term} +type quant = { symb : sym; dom : term; var : tvar; typ : term } (* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation of - the universal quantification of x:type_a on top of the list ql, and return the - list.*) -let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = - fun qlist q d v t -> - {symb = q; dom = d; var = v; typ = t}::qlist - -(* mk_quant builds an application of the quantifier q on the proposition f.*) -let mk_quant : term -> quant -> term = - fun f q -> - let tb = bind (q.var) lift f in - add_args (mk_Symb q.symb) [q.dom; mk_Abst(q.typ, tb)] - -(* nnf_term compute the negation normal form of a FOF*) -let nnf_term : fol_config -> term -> term = fun cfg t -> + the universal quantification of x:type_a on top of the list ql, and return + the list.*) +let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = + fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist + +(* mk_quant builds an application of the quantifier q on the proposition f.*) +let mk_quant : term -> quant -> term = + fun f q -> + let tb = bind q.var lift f in + add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] + +(* nnf_term compute the negation normal form of a FOF*) +let nnf_term : fol_config -> term -> term = + fun cfg t -> (*Printf.printf "------ Start nnf_term ------" ;*) let rec nnf_prop t = (*Format.printf "@.-___- Start nnf_prop -___- %a @." term t;*) match get_args t with - | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [neg t1; nnf_prop t2] - | Symb(s), [t] when s == cfg.symb_not -> - (*Format.printf "@.NNF Not t, with t = %a @." term t;*) - neg t - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] - | Symb(s), _ -> (*Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s);*) t - | Abst(_, _), _ -> (*Format.printf "@.Etat ABS: %a @." term t;*) t - | w, _ -> (*Format.printf "@.NNF puit: %a @." term w;*) t - and neg t = - (*Format.printf "@.**** Start Neg**** : %a @." term t;*) + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> + add_args (mk_Symb cfg.symb_or) [ neg t1; nnf_prop t2 ] + | Symb s, [ t ] when s == cfg.symb_not -> + (*Format.printf "@.NNF Not t, with t = %a @." term t;*) + neg t + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, nnf_tb) ] + | Symb _, _ + | Abst (_, _), _ -> t + | _, _ -> t + and neg t = match get_args t with - | Symb(s), [] when s == cfg.symb_bot -> - mk_Symb cfg.symb_top - | Symb(s), [] when s == cfg.symb_top -> - mk_Symb cfg.symb_bot - | Symb(s), [t1; t2] when s == cfg.symb_and -> - (*Format.printf "@.NEG : and -> %a @." term t;*) - add_args (mk_Symb cfg.symb_or) [neg t1; neg t2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> - (*Format.printf "@.NEG : or -> %a @." term t; *) - add_args (mk_Symb cfg.symb_and) [neg t1; neg t2] - | Symb(s), [_; _] when s == cfg.symb_imp -> - (*Format.printf "@.NEG : imp -> %a @." term t;*) - neg (nnf_prop t) - | Symb(s), [nt] when s == cfg.symb_not -> - (*Format.printf "@.NEG : not -> %a @." term nt; *) - nnf_prop nt - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + | Symb s, [] when s == cfg.symb_bot -> mk_Symb cfg.symb_top + | Symb s, [] when s == cfg.symb_top -> mk_Symb cfg.symb_bot + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + add_args (mk_Symb cfg.symb_or) [ neg t1; neg t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + add_args (mk_Symb cfg.symb_and) [ neg t1; neg t2 ] + | Symb s, [ _; _ ] when s == cfg.symb_imp -> + neg (nnf_prop t) + | Symb s, [ nt ] when s == cfg.symb_not -> + nnf_prop nt + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in let neg_tb = bind var lift (neg p) in - (*Format.printf "@.NEG : Forall -> %a @." term t;*) - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (neg p) in - (*Format.printf "@.NEG : exists -> %a @." term t;*) - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | w, _ -> (*Format.printf "@. NEG : terme atomique -> %a @." term w;*) add_args (mk_Symb cfg.symb_not) [t] + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, neg_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg p) in + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | _, _ -> + add_args (mk_Symb cfg.symb_not) [ t ] in match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> (*Format.printf "@.P of : %a @." term t;*) mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) - | _ -> failwith "Cant NNF a term that is not a Prop !" + | Symb s, [ t ] when s == cfg.symb_P -> + (*Format.printf "@.P of : %a @." term t;*) + mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) + | _ -> failwith "Cant NNF a term that is not a Prop !" let prenex_term cfg t = let rec prenex t = match get_args t with - | Symb(s), [t1; t2] when s == cfg.symb_and -> - let qlist1, sub1 = prenex t1 - in - let qlist2, sub2 = prenex t2 - in - let t = add_args (mk_Symb s) [sub1; sub2] - in - let qlist = qlist1@qlist2 in - qlist, t - | Symb(s), [t1; t2] when s == cfg.symb_or -> - let qlist1, sub1 = prenex t1 - in - let qlist2, sub2 = prenex t2 - in - let t = add_args (mk_Symb s) [sub1; sub2] - in - let qlist = qlist1@qlist2 in - qlist, t - | Symb(s), [_; _] when s == cfg.symb_imp -> failwith "Prenex : symb_imp occurs but t must be NNF" - | Symb(s), [nt] when s == cfg.symb_not -> - (*Format.printf "@.NEG : not -> %a @." term nt; *) - let res = - match nt with - | Vari(_) -> ([], t) - | Symb(_) -> ([], t) - | _ -> failwith "Prenex : symb_not before a formula occurs, t is not in NNF"*) - in - res - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - qlist, sf - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - qlist, sf - | _, _ -> [], t + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ _; _ ] when s == cfg.symb_imp -> + failwith "Prenex : symb_imp occurs but t must be NNF" + | Symb s, [ nt ] when s == cfg.symb_not -> + let res = + match nt with + | Vari _ -> ([], t) + | Symb _ -> ([], t) + | _ -> + failwith + "Prenex : symb_not before a formula occurs, t is not in NNF" + in + res + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | _, _ -> ([], t) in - let qlist, f = + let qlist, f = match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> (*Format.printf "@.P of : %a @." term t;*) prenex t - | _ -> failwith "Cant PRENEX a term that is not a Prop !" - in + | Symb s, [ t ] when s == cfg.symb_P -> + (*Format.printf "@.P of : %a @." term t;*) prenex t + | _ -> failwith "Cant PRENEX a term that is not a Prop !" + in List.fold_left mk_quant f (List.rev qlist) - - -(**Main fonction : -[skolemisation ss pos t] return a skolemized form of term [t]. -(ie existential quantifications in [t] are removed) -To this end, for each existential quantifiers in [t], signature state [ss] is -extended with new symbol [symb_skt] in order to substitute the variable binded -by the said quantifier*) -let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> - (*Gets user-defined symbol identifiers mapped using "builtin" command.*) - let cfg = get_fol_config ss pos in - let t = mk_Appl (mk_Symb cfg.symb_P, t) in - let t = nnf_term cfg t in - let t = prenex_term cfg t in - let rec skolemisation ss ctx ctr t = - match get_args t with - | Symb(s), [_;Abst(y, tb)] when s == cfg.symb_ex -> - (* When existential quantification occurs, quantified variable - is substituted by a fresh symbol*) - let maj_ss, nv_sym, maj_ctr = new_skolem ss ctx ctr y in - let maj_term = subst_app ctx tb nv_sym in - skolemisation maj_ss ctx maj_ctr maj_term - | Symb(s), [a;Abst(x, tb)] when s == cfg.symb_all -> - (* When universal quantification occurs, quantified variable - is added to context*) - let var, f = Bindlib.unbind tb in - let maj_ctx = add_ctxt ctx var a in - let maj_f = skolemisation ss maj_ctx ctr f in - let maj_tb = bind var lift maj_f in - (*Reconstruct a term of form ∀ x : P, t', - with t' skolemized*) - add_args (mk_Symb s) [a ; mk_Abst (x, maj_tb)] - | _ -> t - in - let skl_of_t = Format.printf "@.La fp donne : %a @." term t; skolemisation ss empty_context 0 t in - if Logger.log_enabled () then - log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t ; - skl_of_t - +(**Main fonction : [skolemisation ss pos t] return a skolemized form of term + [t]. (ie existential quantifications in [t] are removed) To this end, for + each existential quantifiers in [t], signature state [ss] is extended with + new symbol [symb_skt] in order to substitute the variable binded by the said + quantifier*) +let handle : Sig_state.t -> Pos.popt -> term -> term = + fun ss pos t -> + (*Gets user-defined symbol identifiers mapped using "builtin" command.*) + let cfg = get_fol_config ss pos in + let t = mk_Appl (mk_Symb cfg.symb_P, t) in + let t = nnf_term cfg t in + let t = prenex_term cfg t in + let rec skolemisation ss ctx ctr t = + match get_args t with + | Symb s, [ _; Abst (y, tb) ] when s == cfg.symb_ex -> + (* When existential quantification occurs, quantified variable is + substituted by a fresh symbol*) + let maj_ss, nv_sym, maj_ctr = new_skolem ss ctx ctr y in + let maj_term = subst_app ctx tb nv_sym in + skolemisation maj_ss ctx maj_ctr maj_term + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + (* When universal quantification occurs, quantified variable is added to + context*) + let var, f = Bindlib.unbind tb in + let maj_ctx = add_ctxt ctx var a in + let maj_f = skolemisation ss maj_ctx ctr f in + let maj_tb = bind var lift maj_f in + (*Reconstruct a term of form ∀ x : P, t', with t' skolemized*) + add_args (mk_Symb s) [ a; mk_Abst (x, maj_tb) ] + | _ -> t + in + let skl_of_t = + Format.printf "@.La fp donne : %a @." term t; + skolemisation ss empty_context 0 t + in + if Logger.log_enabled () then + log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t; + skl_of_t diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli index 3054ff6c7..e20d9a51e 100644 --- a/src/handle/skolem.mli +++ b/src/handle/skolem.mli @@ -1,4 +1,5 @@ open Common -open Core open Term +open Core +open Term -val handle : Sig_state.t -> Pos.popt -> term -> term \ No newline at end of file +val handle : Sig_state.t -> Pos.popt -> term -> term diff --git a/tests/cnfnnf.ml b/tests/cnfnnf.ml index 2665745cd..2b7037444 100644 --- a/tests/cnfnnf.ml +++ b/tests/cnfnnf.ml @@ -1,5 +1,8 @@ open Common -open Core open Term open Print open Sig_state +open Core +open Term +open Print +open Sig_state open Pos open Parsing @@ -7,313 +10,283 @@ open Parsing let parse_term s = (* A hack to parse a term: wrap term [s] into [compute s;]. *) let c = "compute " ^ s ^ ";" in - let command = (Stream.next (Parser.Lp.parse_string "term" c)) in + let command = Stream.next (Parser.Lp.parse_string "term" c) in match command.elt with - | Syntax.P_query {elt=Syntax.P_query_normalize (t, _); _} -> t + | Syntax.P_query { elt = Syntax.P_query_normalize (t, _); _ } -> t | _ -> assert false (*** Hack pour le debug ***) -let scope_term ?(ctx=[]) ss = Scope.scope_term true ss ctx +let scope_term ?(ctx = []) ss = Scope.scope_term true ss ctx (*** Hack pour le debug ***) let add_sym (ss, slist) id = - let ss, sym = Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Type [] - None + let ss, sym = + Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Type + [] None in - (ss, sym::slist) + (ss, sym :: slist) (*** Hack pour le debug ***) let sig_state : Sig_state.t = let sign = Sig_state.create_sign (Sign.ghost_path "") in Sig_state.of_sign sign - +type config = { + symb_P : sym; (** Encoding of propositions. *) + symb_T : sym; (** Encoding of types. *) + symb_or : sym; (** Disjunction(∨) symbol. *) + symb_and : sym; (** Conjunction(∧) symbol. *) + symb_imp : sym; (** Implication(⇒) symbol. *) + symb_bot : sym; (** Bot(⊥) symbol. *) + symb_top : sym; (** Top(⊤) symbol. *) + symb_not : sym; (** Not(¬) symbol. *) + symb_ex : sym; (** Exists(∃) symbol. *) + symb_all : sym; (** Forall(∀) symbol. *) +} (** Builtin configuration for propositional logic. *) -type config = - { symb_P : sym (** Encoding of propositions. *) - ; symb_T : sym (** Encoding of types. *) - ; symb_or : sym (** Disjunction(∨) symbol. *) - ; symb_and : sym (** Conjunction(∧) symbol. *) - ; symb_imp : sym (** Implication(⇒) symbol. *) - ; symb_bot : sym (** Bot(⊥) symbol. *) - ; symb_top : sym (** Top(⊤) symbol. *) - ; symb_not : sym (** Not(¬) symbol. *) - ; symb_ex : sym (** Exists(∃) symbol. *) - ; symb_all : sym (** Forall(∀) symbol. *) } - (** Hack debug -> a remplacer par la fonction get_config cf why3_tactic.ml**) -let fol_symb_str = ["P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" ] +let fol_symb_str = [ "P"; "t"; "∨"; "∧"; "⇒"; "⊥"; "⊤"; "¬"; "∃"; "∀" ] + (** [get_config ss pos] build the configuration using [ss]. *) let get_config slist = let get n = List.nth slist n in - { symb_P = get 0 - ; symb_T = get 1 - ; symb_or = get 2 - ; symb_and = get 3 - ; symb_imp = get 4 - ; symb_bot = get 5 - ; symb_top = get 6 - ; symb_not = get 7 - ; symb_ex = get 8 - ; symb_all = get 9} - - + { + symb_P = get 0; + symb_T = get 1; + symb_or = get 2; + symb_and = get 3; + symb_imp = get 4; + symb_bot = get 5; + symb_top = get 6; + symb_not = get 7; + symb_ex = get 8; + symb_all = get 9; + } let mk_env symb_p = - let tv = ["A"; "B"] in + let tv = [ "A"; "B" ] in let rec aux e tlist = let tb_p = _Symb symb_p in - match tlist with - | hd::tl -> aux (Env.add (new_tvar hd) tb_p None e) tl + match tlist with + | hd :: tl -> aux (Env.add (new_tvar hd) tb_p None e) tl | [] -> e in aux Env.empty tv -type quant = -{ symb : sym -; dom : term -; var : tvar -; typ : term} +type quant = { symb : sym; dom : term; var : tvar; typ : term } -let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = - fun qlist q d v t -> - {symb = q; dom = d; var = v; typ = t}::qlist +let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = + fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist -let mk_quant : term -> quant -> term = - fun f q -> - let tb = bind (q.var) lift f in - add_args (mk_Symb q.symb) [q.dom; mk_Abst(q.typ, tb)] +let mk_quant : term -> quant -> term = + fun f q -> + let tb = bind q.var lift f in + add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] -let nnf_term : config -> term -> term = fun cfg t -> - Printf.printf "------ Start nnf_term ------" ; +let nnf_term : config -> term -> term = + fun cfg t -> + Printf.printf "------ Start nnf_term ------"; let rec nnf_prop t = Format.printf "@.-___- Start nnf_prop -___- %a @." term t; match get_args t with - | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [neg t1; nnf_prop t2] - | Symb(s), [t] when s == cfg.symb_not -> - Format.printf "@.NNF Not t, with t = %a @." term t; - neg t - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] - | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t - | Abst(_, _), _ -> Format.printf "@.Etat ABS: %a @." term t; t - | w, _ -> Format.printf "@.NNF puit: %a @." term w; t - and neg t = + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> + add_args (mk_Symb cfg.symb_or) [ neg t1; nnf_prop t2 ] + | Symb s, [ t ] when s == cfg.symb_not -> + Format.printf "@.NNF Not t, with t = %a @." term t; + neg t + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, nnf_tb) ] + | Symb s, _ -> + Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); + t + | Abst (_, _), _ -> + Format.printf "@.Etat ABS: %a @." term t; + t + | w, _ -> + Format.printf "@.NNF puit: %a @." term w; + t + and neg t = Format.printf "@.**** Start Neg**** : %a @." term t; match get_args t with - | Symb(s), [] when s == cfg.symb_bot -> - mk_Symb cfg.symb_top - (*add_args (mk_Symb cfg.symb_bot) []*) - | Symb(s), [] when s == cfg.symb_top -> - mk_Symb cfg.symb_bot - (*add_args (mk_Symb cfg.symb_top) []*) - | Symb(s), [t1; t2] when s == cfg.symb_and -> - Format.printf "@.NEG : and -> %a @." term t; - add_args (mk_Symb cfg.symb_or) [neg t1; neg t2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> - Format.printf "@.NEG : or -> %a @." term t; - add_args (mk_Symb cfg.symb_and) [neg t1; neg t2] - | Symb(s), [t1; t2] when s == cfg.symb_imp -> - Format.printf "@.NEG : imp -> %a @." term t; - neg (nnf_prop t) - | Symb(s), [nt] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; - nnf_prop nt - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> + | Symb s, [] when s == cfg.symb_bot -> + mk_Symb cfg.symb_top (*add_args (mk_Symb cfg.symb_bot) []*) + | Symb s, [] when s == cfg.symb_top -> + mk_Symb cfg.symb_bot (*add_args (mk_Symb cfg.symb_top) []*) + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + Format.printf "@.NEG : and -> %a @." term t; + add_args (mk_Symb cfg.symb_or) [ neg t1; neg t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + Format.printf "@.NEG : or -> %a @." term t; + add_args (mk_Symb cfg.symb_and) [ neg t1; neg t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> + Format.printf "@.NEG : imp -> %a @." term t; + neg (nnf_prop t) + | Symb s, [ nt ] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + nnf_prop nt + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in let neg_tb = bind var lift (neg p) in Format.printf "@.NEG : Forall -> %a @." term t; - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (neg p) in - Format.printf "@.NEG : exists -> %a @." term t; - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | w, _ -> Format.printf "@. NEG : terme atomique -> %a @." term w; add_args (mk_Symb cfg.symb_not) [t] + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, neg_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg p) in + Format.printf "@.NEG : exists -> %a @." term t; + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | w, _ -> + Format.printf "@. NEG : terme atomique -> %a @." term w; + add_args (mk_Symb cfg.symb_not) [ t ] in match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) - | _ -> failwith "Cant NNF a term that is not a Prop !" + | Symb s, [ t ] when s == cfg.symb_P -> + Format.printf "@.P of : %a @." term t; + mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) + | _ -> failwith "Cant NNF a term that is not a Prop !" let prenex_term cfg t = let rec prenex t = match get_args t with - | Symb(s), [t1; t2] when s == cfg.symb_and -> - let qlist1, sub1 = prenex t1 - in - let qlist2, sub2 = prenex t2 - in - let t = add_args (mk_Symb s) [sub1; sub2] - in - let qlist = qlist1@qlist2 in - qlist, t - | Symb(s), [t1; t2] when s == cfg.symb_or -> - let qlist1, sub1 = prenex t1 - in - let qlist2, sub2 = prenex t2 - in - let t = add_args (mk_Symb s) [sub1; sub2] - in - let qlist = qlist1@qlist2 in - qlist, t - | Symb(s), [t1; t2] when s == cfg.symb_imp -> failwith "Prenex : symb_imp occurs but t must be NNF" - | Symb(s), [nt] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; - let res = - match nt with - | Vari(x) -> ([], t) - | Symb(s) -> ([], t) - | _ -> failwith "Prenex : symb_not formula must be NNF" - in - res - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - qlist, sf - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - qlist, sf - | w, _ -> [], t + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> + failwith "Prenex : symb_imp occurs but t must be NNF" + | Symb s, [ nt ] when s == cfg.symb_not -> + Format.printf "@.NEG : not -> %a @." term nt; + let res = + match nt with + | Vari x -> ([], t) + | Symb s -> ([], t) + | _ -> failwith "Prenex : symb_not formula must be NNF" + in + res + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | w, _ -> ([], t) in - let qlist, f = + let qlist, f = match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.P of : %a @." term t; prenex t - | _ -> failwith "Cant PRENEX a term that is not a Prop !" - in + | Symb s, [ t ] when s == cfg.symb_P -> + Format.printf "@.P of : %a @." term t; + prenex t + | _ -> failwith "Cant PRENEX a term that is not a Prop !" + in List.fold_left mk_quant f (List.rev qlist) - (*"P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀"*) - +(*"P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀"*) -let _ = - let sig_state, symlist = +let _ = + let sig_state, symlist = List.fold_left add_sym (sig_state, []) fol_symb_str in let symlist = List.rev symlist in - let c = get_config symlist - in - let env = mk_env (List.nth symlist 0) + let c = get_config symlist in + let env = mk_env (List.nth symlist 0) in + let t = + parse_term "P (∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥))))" + |> scope_term ~ctx:env sig_state in - let t = parse_term "P (∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥))))" |> scope_term ~ctx:env sig_state in Format.printf "@.Terme IN : %a @." term t; - let nnt = (nnf_term c t) in + let nnt = nnf_term c t in Format.printf "@.Terme en NNF : %a @." term nnt; - let f = parse_term "P (∨ (∀ P (λ x1, x1)) A)" |> scope_term ~ctx:env sig_state in + let f = + parse_term "P (∨ (∀ P (λ x1, x1)) A)" |> scope_term ~ctx:env sig_state + in let pf = prenex_term c t in - Format.printf "@.Terme en PF : %a @." term pf; + Format.printf "@.Terme en PF : %a @." term pf +(*let add_type ss id = Sig_state.add_symbol ss Public Const Eager true (Pos.none + id) mk_Type [] None - (*let add_type ss id = - Sig_state.add_symbol ss Public Const Eager true (Pos.none id) mk_Type [] - None + let add_quant p id = let ss, ty = p in let quant_type = mk_Appl (mk_Appl + (mk_Appl (ty, ty), ty), ty) in let ss, sym = Sig_state.add_symbol ss Public + Const Eager true (Pos.none id) quant_type [] None in (add_notation ss sym + Quant, sym) -let add_quant p id = - let ss, ty = p in - let quant_type = mk_Appl (mk_Appl (mk_Appl (ty, ty), ty), ty) in - let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) quant_type [] - None - in - (add_notation ss sym Quant, sym) + let add_binop p id = let ss, ty = p in let binop_type = mk_Appl (mk_Appl (ty, + ty), ty) in let ss, sym = Sig_state.add_symbol ss Public Const Eager true + (Pos.none id) binop_type [] None in (add_notation ss sym (Infix(Right, 5.)), + sym) -let add_binop p id = - let ss, ty = p in - let binop_type = mk_Appl (mk_Appl (ty, ty), ty) in - let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) binop_type [] - None - in - (add_notation ss sym (Infix(Right, 5.)), sym) + let add_const ss ty id ty = Sig_state.add_symbol ss Public Const Eager true + (Pos.none id) ty [] None -let add_const ss ty id ty = - Sig_state.add_symbol ss Public Const Eager true (Pos.none id) ty [] - None + let add_unop ss ty id = let unop_type = mk_Appl (ty, ty) in let ss, sym = + Sig_state.add_symbol ss Public Const Eager true (Pos.none id) unop_type [] + None in (add_notation ss sym (Prefix(3.)), sym)*) -let add_unop ss ty id = - let unop_type = mk_Appl (ty, ty) in - let ss, sym = Sig_state.add_symbol ss Public Const Eager true (Pos.none id) unop_type [] - None - in - (add_notation ss sym (Prefix(3.)), sym)*) +(*let nnf_term : config -> term -> term = fun cfg t -> Printf.printf "------ + Start nnf_term ------" ; let symb_P = cfg.symb_P in let rec nnf_prop t = + Format.printf "@.-___- Start nnf_prop -___- %a @." term t; match get_args t + with | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) + [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == cfg.symb_or -> + add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == + cfg.symb_imp -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in add_args (mk_Symb + cfg.symb_or) [neg_term subt1; nnf_prop t2] | Symb(s), [t] when s == + cfg.symb_not -> Format.printf "@.NNF : Not : %a @." term t; let subt = mk_Appl + (mk_Symb symb_P, t) in neg_term subt | Symb(s), [a;Abst(x,tb)] when s == + cfg.symb_all -> let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift + (nnf_prop p) in add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] | + Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> let var, p = Bindlib.unbind + tb in let nnf_tb = bind var lift (nnf_prop p) in add_args (mk_Symb + cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] | Symb(s), _ -> Format.printf "@.NNF Quel + symbole ? : %a @." term (mk_Symb s); t | Abst(_, _), _ -> Format.printf "@.NNF + Etat ABS: %a @." term t; t | w, _ -> Format.printf "@.NNF What: %a @." term w; + t and neg_term t = let rec neg_prop t = Format.printf "@.**** Start + Neg_prop**** : %a @." term t; match get_args t with | Symb(s), [] when s == + cfg.symb_bot -> add_args (mk_Symb cfg.symb_bot) [] | Symb(s), [] when s == + cfg.symb_top -> add_args (mk_Symb cfg.symb_top) [] | Symb(s), [t1; t2] when s + == cfg.symb_and -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in let subt2 = + mk_Appl (mk_Symb symb_P, t2) in add_args (mk_Symb cfg.symb_or) [neg_term + subt1; neg_term subt2] | Symb(s), [t1; t2] when s == cfg.symb_or -> + Format.printf "@.neg : OR : %a @." term t; let subt1 = mk_Appl (mk_Symb + symb_P, t1) in let subt2 = mk_Appl (mk_Symb symb_P, t2) in add_args (mk_Symb + cfg.symb_and) [neg_term subt1; neg_term subt2] | Symb(s), [t1; t2] when s == + cfg.symb_imp -> neg_prop (nnf_prop t) | Symb(s), [nt] when s == cfg.symb_not + -> Format.printf "@.neg : NOT : %a @." term nt; (match nt with | Symb(_) -> t + | Vari (_) -> t | _ -> let subtnt = mk_Appl (mk_Symb symb_P, nt) in nnf_prop + subtnt) | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> let var, p = + Bindlib.unbind tb in let neg_tb = bind var lift (neg_prop p) in add_args + (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] | Symb(s), [a;Abst(x,tb)] when s + == cfg.symb_ex -> - (*let nnf_term : config -> term -> term = fun cfg t -> - Printf.printf "------ Start nnf_term ------" ; - let symb_P = cfg.symb_P in - let rec nnf_prop t = - Format.printf "@.-___- Start nnf_prop -___- %a @." term t; - match get_args t with - | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] - | Symb(s), [t1; t2] when s == cfg.symb_imp -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in - add_args (mk_Symb cfg.symb_or) [neg_term subt1; nnf_prop t2] - | Symb(s), [t] when s == cfg.symb_not -> - Format.printf "@.NNF : Not : %a @." term t; - let subt = mk_Appl (mk_Symb symb_P, t) in - neg_term subt - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] - | Symb(s), _ -> Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); t - | Abst(_, _), _ -> Format.printf "@.NNF Etat ABS: %a @." term t; t - | w, _ -> Format.printf "@.NNF What: %a @." term w; t - and neg_term t = - let rec neg_prop t = - Format.printf "@.**** Start Neg_prop**** : %a @." term t; - match get_args t with - | Symb(s), [] when s == cfg.symb_bot -> - add_args (mk_Symb cfg.symb_bot) [] - | Symb(s), [] when s == cfg.symb_top -> - add_args (mk_Symb cfg.symb_top) [] - | Symb(s), [t1; t2] when s == cfg.symb_and -> - let subt1 = mk_Appl (mk_Symb symb_P, t1) in - let subt2 = mk_Appl (mk_Symb symb_P, t2) in - add_args (mk_Symb cfg.symb_or) [neg_term subt1; neg_term subt2] - | Symb(s), [t1; t2] when s == cfg.symb_or -> - Format.printf "@.neg : OR : %a @." term t; - let subt1 = mk_Appl (mk_Symb symb_P, t1) in - let subt2 = mk_Appl (mk_Symb symb_P, t2) in - add_args (mk_Symb cfg.symb_and) [neg_term subt1; neg_term subt2] - | Symb(s), [t1; t2] when s == cfg.symb_imp -> neg_prop (nnf_prop t) - | Symb(s), [nt] when s == cfg.symb_not -> - Format.printf "@.neg : NOT : %a @." term nt; - (match nt with - | Symb(_) -> t - | Vari (_) -> t - | _ -> - let subtnt = mk_Appl (mk_Symb symb_P, nt) in - nnf_prop subtnt) - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let neg_tb = bind var lift (neg_prop p) in - add_args (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] - | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> - - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (neg_prop p) in - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] - | w, tl -> Format.printf "@.NEG What: %a @." term w; List.map (Format.printf "; %a ;" term) tl; t - in - match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> Format.printf "@.NEG get_args : %a @." term (mk_Symb s); neg_prop t - | _ -> Format.printf "@.NEG fails : %a @." term t; failwith "Cant NEG a term that is not a Prop !" - in - match get_args t with - | (Symb(s), [t]) when s == cfg.symb_P -> nnf_prop t - | _ -> failwith "Cant NNF a term that is not a Prop !" + let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (neg_prop p) in + add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] | w, tl -> + Format.printf "@.NEG What: %a @." term w; List.map (Format.printf "; %a ;" + term) tl; t in match get_args t with | (Symb(s), [t]) when s == cfg.symb_P -> + Format.printf "@.NEG get_args : %a @." term (mk_Symb s); neg_prop t | _ -> + Format.printf "@.NEG fails : %a @." term t; failwith "Cant NEG a term that is + not a Prop !" in match get_args t with | (Symb(s), [t]) when s == cfg.symb_P + -> nnf_prop t | _ -> failwith "Cant NNF a term that is not a Prop !" -let fol_symb_str = [ "P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" ]*) \ No newline at end of file + let fol_symb_str = [ "P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" + ]*) From ac1183a40e8c030176ccb3ac01afeb12c8b70655 Mon Sep 17 00:00:00 2001 From: gabrielhdt Date: Thu, 21 Jul 2022 08:06:44 +0200 Subject: [PATCH 09/16] Expose prenex, nnf, tests --- src/handle/skolem.ml | 91 ++++++------- src/handle/skolem.mli | 32 +++++ tests/cnfnnf.ml | 294 +++++++----------------------------------- 3 files changed, 119 insertions(+), 298 deletions(-) diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index cc69e6899..e324f497e 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -1,10 +1,9 @@ open Common open Core open Term -open Print (** Logging function for the skolem tactic. *) -let log_sklm = Logger.make '!' "sklm" "the skolemization tactic" +let log_sklm = Logger.make 'y' "sklm" "the skolemization tactic" let log_sklm = log_sklm.pp @@ -39,10 +38,6 @@ let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = symb_all = builtin "all"; } -(*Context of skolemization allow to record introduced variables and their types - when universal quantifiers occurs.*) -let empty_context = [] - let add_ctxt : ctxt -> tvar -> term -> ctxt = fun c var typ -> c @ [ (var, typ, None) ] @@ -89,8 +84,15 @@ let subst_app : ctxt -> tbinder -> sym -> term = let f_appl = add_args (mk_Symb symb_skt) args_list in Bindlib.subst tb f_appl -(* quant is a structure for representating quantifiers in a FOF.*) -type quant = { symb : sym; dom : term; var : tvar; typ : term } +type quant = { + symb : sym; (** The symbol that stand for the quantifier. *) + dom : term; (** The domain of the quantification. *) + var : tvar; (** The variable bound by the quantification. *) + typ : term; + (** The type of the quantified variable {b NOTE} It should always be + [T dom] where [T] is the builtin that interprets type codes. *) +} +(** A structure to represent quantifiers in a FOF. *) (* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation of the universal quantification of x:type_a on top of the list ql, and return @@ -98,18 +100,17 @@ type quant = { symb : sym; dom : term; var : tvar; typ : term } let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist -(* mk_quant builds an application of the quantifier q on the proposition f.*) +(* [mk_quant t q] builds an application of the quantifier q on the proposition + f.*) let mk_quant : term -> quant -> term = fun f q -> let tb = bind q.var lift f in add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] -(* nnf_term compute the negation normal form of a FOF*) -let nnf_term : fol_config -> term -> term = +(** [nnf_term cfg t] computes the negation normal form of a first order formula. *) +let nnf_of : fol_config -> term -> term = fun cfg t -> - (*Printf.printf "------ Start nnf_term ------" ;*) let rec nnf_prop t = - (*Format.printf "@.-___- Start nnf_prop -___- %a @." term t;*) match get_args t with | Symb s, [ t1; t2 ] when s == cfg.symb_and -> add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] @@ -117,9 +118,7 @@ let nnf_term : fol_config -> term -> term = add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> add_args (mk_Symb cfg.symb_or) [ neg t1; nnf_prop t2 ] - | Symb s, [ t ] when s == cfg.symb_not -> - (*Format.printf "@.NNF Not t, with t = %a @." term t;*) - neg t + | Symb s, [ t ] when s == cfg.symb_not -> neg t | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (nnf_prop p) in @@ -128,8 +127,7 @@ let nnf_term : fol_config -> term -> term = let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (nnf_prop p) in add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, nnf_tb) ] - | Symb _, _ - | Abst (_, _), _ -> t + | Symb _, _ | Abst (_, _), _ -> t | _, _ -> t and neg t = match get_args t with @@ -139,10 +137,8 @@ let nnf_term : fol_config -> term -> term = add_args (mk_Symb cfg.symb_or) [ neg t1; neg t2 ] | Symb s, [ t1; t2 ] when s == cfg.symb_or -> add_args (mk_Symb cfg.symb_and) [ neg t1; neg t2 ] - | Symb s, [ _; _ ] when s == cfg.symb_imp -> - neg (nnf_prop t) - | Symb s, [ nt ] when s == cfg.symb_not -> - nnf_prop nt + | Symb s, [ _; _ ] when s == cfg.symb_imp -> neg (nnf_prop t) + | Symb s, [ nt ] when s == cfg.symb_not -> nnf_prop nt | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> let var, p = Bindlib.unbind tb in let neg_tb = bind var lift (neg p) in @@ -151,16 +147,13 @@ let nnf_term : fol_config -> term -> term = let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (neg p) in add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] - | _, _ -> - add_args (mk_Symb cfg.symb_not) [ t ] + | _, _ -> add_args (mk_Symb cfg.symb_not) [ t ] in - match get_args t with - | Symb s, [ t ] when s == cfg.symb_P -> - (*Format.printf "@.P of : %a @." term t;*) - mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) - | _ -> failwith "Cant NNF a term that is not a Prop !" + nnf_prop t + +exception PrenexFormulaNotNnf of term -let prenex_term cfg t = +let prenex_of cfg t = let rec prenex t = match get_args t with | Symb s, [ t1; t2 ] when s == cfg.symb_and -> @@ -175,16 +168,13 @@ let prenex_term cfg t = let t = add_args (mk_Symb s) [ sub1; sub2 ] in let qlist = qlist1 @ qlist2 in (qlist, t) - | Symb s, [ _; _ ] when s == cfg.symb_imp -> - failwith "Prenex : symb_imp occurs but t must be NNF" + | Symb s, [ _; _ ] when s == cfg.symb_imp -> raise @@ PrenexFormulaNotNnf t | Symb s, [ nt ] when s == cfg.symb_not -> let res = match nt with | Vari _ -> ([], t) | Symb _ -> ([], t) - | _ -> - failwith - "Prenex : symb_not before a formula occurs, t is not in NNF" + | _ -> raise @@ PrenexFormulaNotNnf t in res | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> @@ -199,26 +189,24 @@ let prenex_term cfg t = (qlist, sf) | _, _ -> ([], t) in - let qlist, f = - match get_args t with - | Symb s, [ t ] when s == cfg.symb_P -> - (*Format.printf "@.P of : %a @." term t;*) prenex t - | _ -> failwith "Cant PRENEX a term that is not a Prop !" - in + let qlist, f = prenex t in List.fold_left mk_quant f (List.rev qlist) -(**Main fonction : [skolemisation ss pos t] return a skolemized form of term - [t]. (ie existential quantifications in [t] are removed) To this end, for - each existential quantifiers in [t], signature state [ss] is extended with - new symbol [symb_skt] in order to substitute the variable binded by the said - quantifier*) +(** [handle ss pos t] returns a skolemized form of term [t] (at position [pos]). + A term is skolemized when it has no existential quantifiers: to this end, + for each existential quantifier in [t], signature state [ss] is extended + with a new symbol in order to substitute the variable bound by the said + quantifier. + @raise NotProp when the argument [t] is not an encoded proposition. *) let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> (*Gets user-defined symbol identifiers mapped using "builtin" command.*) let cfg = get_fol_config ss pos in - let t = mk_Appl (mk_Symb cfg.symb_P, t) in - let t = nnf_term cfg t in - let t = prenex_term cfg t in + let t = nnf_of cfg t in + let t = + try prenex_of cfg t + with PrenexFormulaNotNnf _ -> assert false (* [t] is put into nnf before *) + in let rec skolemisation ss ctx ctr t = match get_args t with | Symb s, [ _; Abst (y, tb) ] when s == cfg.symb_ex -> @@ -238,10 +226,7 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = add_args (mk_Symb s) [ a; mk_Abst (x, maj_tb) ] | _ -> t in - let skl_of_t = - Format.printf "@.La fp donne : %a @." term t; - skolemisation ss empty_context 0 t - in + let skl_of_t = skolemisation ss [] 0 t in if Logger.log_enabled () then log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t; skl_of_t diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli index e20d9a51e..70b37ad6f 100644 --- a/src/handle/skolem.mli +++ b/src/handle/skolem.mli @@ -2,4 +2,36 @@ open Common open Core open Term +type fol_config = { + symb_P : sym; (** Encoding of propositions. *) + symb_T : sym; (** Encoding of types. *) + symb_or : sym; (** Disjunction(∨) symbol. *) + symb_and : sym; (** Conjunction(∧) symbol. *) + symb_imp : sym; (** Implication(⇒) symbol. *) + symb_bot : sym; (** Bot(⊥) symbol. *) + symb_top : sym; (** Top(⊤) symbol. *) + symb_not : sym; (** Not(¬) symbol. *) + symb_ex : sym; (** Exists(∃) symbol. *) + symb_all : sym; (** Forall(∀) symbol. *) +} +(** Builtin configuration for propositional logic. *) + +val nnf_of : fol_config -> term -> term +(** [nnf_of cfg phi] computes the negation normal form of first order formula + [phi]. *) + +exception PrenexFormulaNotNnf of term +(** Raised by [prenex_of] when its formula is not in negation normal form. *) + +val prenex_of : fol_config -> term -> term +(** [prenex_of cfg phi] computes the prenex normal form of first order formula + [phi]. + @raise PrenexFormulaNotNnf when formula [phi] is not in negation normal + form. *) + val handle : Sig_state.t -> Pos.popt -> term -> term +(** [handle ss pos t] returns a skolemized form of term [t] (at position [pos]). + A term is skolemized when it has no existential quantifiers: to this end, + for each existential quantifier in [t], signature state [ss] is extended + with a new symbol in order to substitute the variable bound by the said + quantifier. *) diff --git a/tests/cnfnnf.ml b/tests/cnfnnf.ml index 2b7037444..efe948bfc 100644 --- a/tests/cnfnnf.ml +++ b/tests/cnfnnf.ml @@ -1,12 +1,10 @@ open Common open Core open Term -open Print open Sig_state -open Pos open Parsing -(*** Hack pour le debug ***) +(** Hack to parse easily a single term *) let parse_term s = (* A hack to parse a term: wrap term [s] into [compute s;]. *) let c = "compute " ^ s ^ ";" in @@ -15,10 +13,8 @@ let parse_term s = | Syntax.P_query { elt = Syntax.P_query_normalize (t, _); _ } -> t | _ -> assert false -(*** Hack pour le debug ***) -let scope_term ?(ctx = []) ss = Scope.scope_term true ss ctx +let scope_term ?(env = []) ss = Scope.scope_term true ss env -(*** Hack pour le debug ***) let add_sym (ss, slist) id = let ss, sym = Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Type @@ -26,43 +22,30 @@ let add_sym (ss, slist) id = in (ss, sym :: slist) -(*** Hack pour le debug ***) let sig_state : Sig_state.t = - let sign = Sig_state.create_sign (Sign.ghost_path "") in + let sign = Sig_state.create_sign (Path.ghost "cnfnnf") in Sig_state.of_sign sign -type config = { - symb_P : sym; (** Encoding of propositions. *) - symb_T : sym; (** Encoding of types. *) - symb_or : sym; (** Disjunction(∨) symbol. *) - symb_and : sym; (** Conjunction(∧) symbol. *) - symb_imp : sym; (** Implication(⇒) symbol. *) - symb_bot : sym; (** Bot(⊥) symbol. *) - symb_top : sym; (** Top(⊤) symbol. *) - symb_not : sym; (** Not(¬) symbol. *) - symb_ex : sym; (** Exists(∃) symbol. *) - symb_all : sym; (** Forall(∀) symbol. *) -} (** Builtin configuration for propositional logic. *) -(** Hack debug -> a remplacer par la fonction get_config cf why3_tactic.ml**) let fol_symb_str = [ "P"; "t"; "∨"; "∧"; "⇒"; "⊥"; "⊤"; "¬"; "∃"; "∀" ] (** [get_config ss pos] build the configuration using [ss]. *) let get_config slist = let get n = List.nth slist n in - { - symb_P = get 0; - symb_T = get 1; - symb_or = get 2; - symb_and = get 3; - symb_imp = get 4; - symb_bot = get 5; - symb_top = get 6; - symb_not = get 7; - symb_ex = get 8; - symb_all = get 9; - } + Handle.Skolem. + { + symb_P = get 0; + symb_T = get 1; + symb_or = get 2; + symb_and = get 3; + symb_imp = get 4; + symb_bot = get 5; + symb_top = get 6; + symb_not = get 7; + symb_ex = get 8; + symb_all = get 9; + } let mk_env symb_p = let tv = [ "A"; "B" ] in @@ -74,219 +57,40 @@ let mk_env symb_p = in aux Env.empty tv -type quant = { symb : sym; dom : term; var : tvar; typ : term } - -let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = - fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist - -let mk_quant : term -> quant -> term = - fun f q -> - let tb = bind q.var lift f in - add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] - -let nnf_term : config -> term -> term = - fun cfg t -> - Printf.printf "------ Start nnf_term ------"; - let rec nnf_prop t = - Format.printf "@.-___- Start nnf_prop -___- %a @." term t; - match get_args t with - | Symb s, [ t1; t2 ] when s == cfg.symb_and -> - add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] - | Symb s, [ t1; t2 ] when s == cfg.symb_or -> - add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] - | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> - add_args (mk_Symb cfg.symb_or) [ neg t1; nnf_prop t2 ] - | Symb s, [ t ] when s == cfg.symb_not -> - Format.printf "@.NNF Not t, with t = %a @." term t; - neg t - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (nnf_prop p) in - add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, nnf_tb) ] - | Symb s, _ -> - Format.printf "@.NNF Quel symbole ? : %a @." term (mk_Symb s); - t - | Abst (_, _), _ -> - Format.printf "@.Etat ABS: %a @." term t; - t - | w, _ -> - Format.printf "@.NNF puit: %a @." term w; - t - and neg t = - Format.printf "@.**** Start Neg**** : %a @." term t; - match get_args t with - | Symb s, [] when s == cfg.symb_bot -> - mk_Symb cfg.symb_top (*add_args (mk_Symb cfg.symb_bot) []*) - | Symb s, [] when s == cfg.symb_top -> - mk_Symb cfg.symb_bot (*add_args (mk_Symb cfg.symb_top) []*) - | Symb s, [ t1; t2 ] when s == cfg.symb_and -> - Format.printf "@.NEG : and -> %a @." term t; - add_args (mk_Symb cfg.symb_or) [ neg t1; neg t2 ] - | Symb s, [ t1; t2 ] when s == cfg.symb_or -> - Format.printf "@.NEG : or -> %a @." term t; - add_args (mk_Symb cfg.symb_and) [ neg t1; neg t2 ] - | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> - Format.printf "@.NEG : imp -> %a @." term t; - neg (nnf_prop t) - | Symb s, [ nt ] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; - nnf_prop nt - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> - let var, p = Bindlib.unbind tb in - let neg_tb = bind var lift (neg p) in - Format.printf "@.NEG : Forall -> %a @." term t; - add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, neg_tb) ] - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> - let var, p = Bindlib.unbind tb in - let nnf_tb = bind var lift (neg p) in - Format.printf "@.NEG : exists -> %a @." term t; - add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] - | w, _ -> - Format.printf "@. NEG : terme atomique -> %a @." term w; - add_args (mk_Symb cfg.symb_not) [ t ] - in - match get_args t with - | Symb s, [ t ] when s == cfg.symb_P -> - Format.printf "@.P of : %a @." term t; - mk_Appl (mk_Symb cfg.symb_P, nnf_prop t) - | _ -> failwith "Cant NNF a term that is not a Prop !" - -let prenex_term cfg t = - let rec prenex t = - match get_args t with - | Symb s, [ t1; t2 ] when s == cfg.symb_and -> - let qlist1, sub1 = prenex t1 in - let qlist2, sub2 = prenex t2 in - let t = add_args (mk_Symb s) [ sub1; sub2 ] in - let qlist = qlist1 @ qlist2 in - (qlist, t) - | Symb s, [ t1; t2 ] when s == cfg.symb_or -> - let qlist1, sub1 = prenex t1 in - let qlist2, sub2 = prenex t2 in - let t = add_args (mk_Symb s) [ sub1; sub2 ] in - let qlist = qlist1 @ qlist2 in - (qlist, t) - | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> - failwith "Prenex : symb_imp occurs but t must be NNF" - | Symb s, [ nt ] when s == cfg.symb_not -> - Format.printf "@.NEG : not -> %a @." term nt; - let res = - match nt with - | Vari x -> ([], t) - | Symb s -> ([], t) - | _ -> failwith "Prenex : symb_not formula must be NNF" - in - res - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - (qlist, sf) - | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> - let var, f = Bindlib.unbind tb in - let qlist, sf = prenex f in - let qlist = add_quant qlist s a var x in - (qlist, sf) - | w, _ -> ([], t) +(** Setup a signature state, a first order logic configuration and an + environment to scope properly formulae. *) +let sig_state, cfg = + let ss, symlist = List.fold_left add_sym (sig_state, []) fol_symb_str in + Timed.(Print.sig_state := sig_state); + (ss, get_config (List.rev symlist)) + +(** An environment defining two variables [A] and [B]. *) +let env = + Env.empty |> Env.add (new_tvar "A") _Kind None |> Env.add (new_tvar "B") _Kind None + +let test_nnf () = + let formula = + parse_term "∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥)))" + |> scope_term ~env sig_state in - let qlist, f = - match get_args t with - | Symb s, [ t ] when s == cfg.symb_P -> - Format.printf "@.P of : %a @." term t; - prenex t - | _ -> failwith "Cant PRENEX a term that is not a Prop !" + let witness = "∀ P (λ x1, ∀ B (λ y1, ∧ (∧ (¬ x1) (¬ y1)) ⊤))" in + Alcotest.(check string) + "Negation normal form" witness + (Format.asprintf "%a" Print.term (Handle.Skolem.nnf_of cfg formula)) + +let test_pnf () = + let formula = + parse_term "∨ (∀ P (λ x1, x1)) A" |> scope_term ~env sig_state in - List.fold_left mk_quant f (List.rev qlist) - -(*"P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀"*) + let witness = "∀ P (λ x1, ∨ x1 A)" in + Alcotest.(check string) + "Prenex normal form" witness + (Format.asprintf "%a" Print.term (Handle.Skolem.prenex_of cfg formula)) let _ = - let sig_state, symlist = - List.fold_left add_sym (sig_state, []) fol_symb_str - in - let symlist = List.rev symlist in - let c = get_config symlist in - let env = mk_env (List.nth symlist 0) in - let t = - parse_term "P (∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥))))" - |> scope_term ~ctx:env sig_state - in - Format.printf "@.Terme IN : %a @." term t; - let nnt = nnf_term c t in - Format.printf "@.Terme en NNF : %a @." term nnt; - let f = - parse_term "P (∨ (∀ P (λ x1, x1)) A)" |> scope_term ~ctx:env sig_state - in - let pf = prenex_term c t in - Format.printf "@.Terme en PF : %a @." term pf - -(*let add_type ss id = Sig_state.add_symbol ss Public Const Eager true (Pos.none - id) mk_Type [] None - - let add_quant p id = let ss, ty = p in let quant_type = mk_Appl (mk_Appl - (mk_Appl (ty, ty), ty), ty) in let ss, sym = Sig_state.add_symbol ss Public - Const Eager true (Pos.none id) quant_type [] None in (add_notation ss sym - Quant, sym) - - let add_binop p id = let ss, ty = p in let binop_type = mk_Appl (mk_Appl (ty, - ty), ty) in let ss, sym = Sig_state.add_symbol ss Public Const Eager true - (Pos.none id) binop_type [] None in (add_notation ss sym (Infix(Right, 5.)), - sym) - - let add_const ss ty id ty = Sig_state.add_symbol ss Public Const Eager true - (Pos.none id) ty [] None - - let add_unop ss ty id = let unop_type = mk_Appl (ty, ty) in let ss, sym = - Sig_state.add_symbol ss Public Const Eager true (Pos.none id) unop_type [] - None in (add_notation ss sym (Prefix(3.)), sym)*) - -(*let nnf_term : config -> term -> term = fun cfg t -> Printf.printf "------ - Start nnf_term ------" ; let symb_P = cfg.symb_P in let rec nnf_prop t = - Format.printf "@.-___- Start nnf_prop -___- %a @." term t; match get_args t - with | Symb(s), [t1; t2] when s == cfg.symb_and -> add_args (mk_Symb s) - [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == cfg.symb_or -> - add_args (mk_Symb s) [nnf_prop t1; nnf_prop t2] | Symb(s), [t1; t2] when s == - cfg.symb_imp -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in add_args (mk_Symb - cfg.symb_or) [neg_term subt1; nnf_prop t2] | Symb(s), [t] when s == - cfg.symb_not -> Format.printf "@.NNF : Not : %a @." term t; let subt = mk_Appl - (mk_Symb symb_P, t) in neg_term subt | Symb(s), [a;Abst(x,tb)] when s == - cfg.symb_all -> let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift - (nnf_prop p) in add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] | - Symb(s), [a;Abst(x,tb)] when s == cfg.symb_ex -> let var, p = Bindlib.unbind - tb in let nnf_tb = bind var lift (nnf_prop p) in add_args (mk_Symb - cfg.symb_ex) [a; mk_Abst(x, nnf_tb)] | Symb(s), _ -> Format.printf "@.NNF Quel - symbole ? : %a @." term (mk_Symb s); t | Abst(_, _), _ -> Format.printf "@.NNF - Etat ABS: %a @." term t; t | w, _ -> Format.printf "@.NNF What: %a @." term w; - t and neg_term t = let rec neg_prop t = Format.printf "@.**** Start - Neg_prop**** : %a @." term t; match get_args t with | Symb(s), [] when s == - cfg.symb_bot -> add_args (mk_Symb cfg.symb_bot) [] | Symb(s), [] when s == - cfg.symb_top -> add_args (mk_Symb cfg.symb_top) [] | Symb(s), [t1; t2] when s - == cfg.symb_and -> let subt1 = mk_Appl (mk_Symb symb_P, t1) in let subt2 = - mk_Appl (mk_Symb symb_P, t2) in add_args (mk_Symb cfg.symb_or) [neg_term - subt1; neg_term subt2] | Symb(s), [t1; t2] when s == cfg.symb_or -> - Format.printf "@.neg : OR : %a @." term t; let subt1 = mk_Appl (mk_Symb - symb_P, t1) in let subt2 = mk_Appl (mk_Symb symb_P, t2) in add_args (mk_Symb - cfg.symb_and) [neg_term subt1; neg_term subt2] | Symb(s), [t1; t2] when s == - cfg.symb_imp -> neg_prop (nnf_prop t) | Symb(s), [nt] when s == cfg.symb_not - -> Format.printf "@.neg : NOT : %a @." term nt; (match nt with | Symb(_) -> t - | Vari (_) -> t | _ -> let subtnt = mk_Appl (mk_Symb symb_P, nt) in nnf_prop - subtnt) | Symb(s), [a;Abst(x,tb)] when s == cfg.symb_all -> let var, p = - Bindlib.unbind tb in let neg_tb = bind var lift (neg_prop p) in add_args - (mk_Symb cfg.symb_ex) [a; mk_Abst(x, neg_tb)] | Symb(s), [a;Abst(x,tb)] when s - == cfg.symb_ex -> - - let var, p = Bindlib.unbind tb in let nnf_tb = bind var lift (neg_prop p) in - add_args (mk_Symb cfg.symb_all) [a; mk_Abst(x, nnf_tb)] | w, tl -> - Format.printf "@.NEG What: %a @." term w; List.map (Format.printf "; %a ;" - term) tl; t in match get_args t with | (Symb(s), [t]) when s == cfg.symb_P -> - Format.printf "@.NEG get_args : %a @." term (mk_Symb s); neg_prop t | _ -> - Format.printf "@.NEG fails : %a @." term t; failwith "Cant NEG a term that is - not a Prop !" in match get_args t with | (Symb(s), [t]) when s == cfg.symb_P - -> nnf_prop t | _ -> failwith "Cant NNF a term that is not a Prop !" - - let fol_symb_str = [ "P"; "t" ; "∨" ; "∧" ; "⇒" ; "⊥" ; "⊤" ; "¬" ; "∃"; "∀" - ]*) + let open Alcotest in + run "proposition transformations" + [ + ( "prop", + [ test_case "nnf" `Quick test_nnf; test_case "pnf" `Quick test_pnf ] ); + ] From a87af9200c96aace4be1f749e74dee839918ac44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 28 Dec 2022 17:57:16 +0100 Subject: [PATCH 10/16] fix compil and sanity check --- src/export/coq.ml | 1 + src/handle/skolem.ml | 65 ++++++++++++++++++++++--------------------- src/handle/skolem.mli | 20 ++++++------- src/handle/tactic.ml | 18 ++++++------ 4 files changed, 54 insertions(+), 50 deletions(-) diff --git a/src/export/coq.ml b/src/export/coq.ml index c7b86cdf8..4ec830a74 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -179,6 +179,7 @@ let rw_patt : p_rw_patt pp = fun ppf p -> let tactic : p_tactic pp = fun ppf { elt; _ } -> begin match elt with + | P_tac_skolem -> out ppf "skolem" | P_tac_admit -> out ppf "admit" | P_tac_apply t -> out ppf "apply %a" term t | P_tac_assume ids -> diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index e324f497e..47cb3b997 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -2,10 +2,8 @@ open Common open Core open Term -(** Logging function for the skolem tactic. *) -let log_sklm = Logger.make 'y' "sklm" "the skolemization tactic" - -let log_sklm = log_sklm.pp +let log = Logger.make 'a' "sklm" "skolemization" +let log = log.pp type fol_config = { symb_P : sym; (** Encoding of propositions. *) @@ -48,17 +46,17 @@ let add_ctxt : ctxt -> tvar -> term -> ctxt = eliminate ∃ quantifier, we need to extend signature state [ss] with a skolem term, represented by a fresh symbol that will later replace the binded variable ("y"). Such skolem term may either be a skolem function or a skolem - constant : The type of a skolem term depends on registered variables in [ctx] - For example, if a set of variables x1:a1, x2:a2,..., xn:an were previously - introduced by an universal quantifier, A skolem term "skt" will take as - arguments x1, ..., xn, and must therefore be typed as follows : skt (x1, x2, - ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. A skolem term is a constant if - skolemized term is not in the scope of any universal quantifier, namely, [ctx] - is empty. For the sake of clarity, we use a counter [cpt] for naming the - generated symbol. OUT : Updated signature state [upt_sig] is returned, as well - as introduced symbol [symb_skt] and updated counter*) -let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = - fun ss ctx ctr ex_typ -> + constant : The type of a skolem term depends on registered variables in + [ctx] For example, if a set of variables x1:a1, x2:a2,..., xn:an were + previously introduced by an universal quantifier, A skolem term "skt" will + take as arguments x1, ..., xn, and must therefore be typed as follows : skt + (x1, x2, ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. A skolem term is a + constant if skolemized term is not in the scope of any universal quantifier, + namely, [ctx] is empty. For the sake of clarity, we use a counter [cpt] for + naming the generated symbol. OUT : Updated signature state [upt_sig] is + returned, as well as introduced symbol [symb_skt] and updated counter*) +let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int + = fun ss ctx ctr ex_typ -> let skt_name = if ctx == [] then "c" ^ string_of_int ctr else "f" ^ string_of_int ctr in @@ -67,14 +65,14 @@ let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] None in - if Logger.log_enabled () then log_sklm "New symbol %a" Print.sym symb_skt; + if Logger.log_enabled () then log "New symbol %a" Print.sym symb_skt; (upt_sig, symb_skt, ctr + 1) (*[Subst_app ctx tb s] builds [f_appl], the application of a symbol [symb_skt] and a list of variables extracted from context [ctx]. Then, the binded variable in [tb] is substituted by [f_appl]*) -(*Assumes type of [symb_skt] correspond to variables's types as they are listed - in context [ctx] *) +(*Assumes type of [symb_skt] correspond to variables's types as they are + listed in context [ctx] *) let subst_app : ctxt -> tbinder -> sym -> term = fun ctx tb symb_skt -> (*args_list : [tvar list], are context's variables*) @@ -94,9 +92,9 @@ type quant = { } (** A structure to represent quantifiers in a FOF. *) -(* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation of - the universal quantification of x:type_a on top of the list ql, and return - the list.*) +(* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation + of the universal quantification of x:type_a on top of the list ql, and + return the list.*) let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist @@ -107,7 +105,8 @@ let mk_quant : term -> quant -> term = let tb = bind q.var lift f in add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] -(** [nnf_term cfg t] computes the negation normal form of a first order formula. *) +(** [nnf_term cfg t] computes the negation normal form of a first order + formula. *) let nnf_of : fol_config -> term -> term = fun cfg t -> let rec nnf_prop t = @@ -168,7 +167,8 @@ let prenex_of cfg t = let t = add_args (mk_Symb s) [ sub1; sub2 ] in let qlist = qlist1 @ qlist2 in (qlist, t) - | Symb s, [ _; _ ] when s == cfg.symb_imp -> raise @@ PrenexFormulaNotNnf t + | Symb s, [ _; _ ] when s == cfg.symb_imp -> + raise @@ PrenexFormulaNotNnf t | Symb s, [ nt ] when s == cfg.symb_not -> let res = match nt with @@ -192,11 +192,11 @@ let prenex_of cfg t = let qlist, f = prenex t in List.fold_left mk_quant f (List.rev qlist) -(** [handle ss pos t] returns a skolemized form of term [t] (at position [pos]). - A term is skolemized when it has no existential quantifiers: to this end, - for each existential quantifier in [t], signature state [ss] is extended - with a new symbol in order to substitute the variable bound by the said - quantifier. +(** [handle ss pos t] returns a skolemized form of term [t] (at position + [pos]). A term is skolemized when it has no existential quantifiers: to + this end, for each existential quantifier in [t], signature state [ss] is + extended with a new symbol in order to substitute the variable bound by + the said quantifier. @raise NotProp when the argument [t] is not an encoded proposition. *) let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> @@ -205,7 +205,8 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = let t = nnf_of cfg t in let t = try prenex_of cfg t - with PrenexFormulaNotNnf _ -> assert false (* [t] is put into nnf before *) + with PrenexFormulaNotNnf _ -> + assert false (* [t] is put into nnf before *) in let rec skolemisation ss ctx ctr t = match get_args t with @@ -216,8 +217,8 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = let maj_term = subst_app ctx tb nv_sym in skolemisation maj_ss ctx maj_ctr maj_term | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> - (* When universal quantification occurs, quantified variable is added to - context*) + (* When universal quantification occurs, quantified variable is added + to context*) let var, f = Bindlib.unbind tb in let maj_ctx = add_ctxt ctx var a in let maj_f = skolemisation ss maj_ctx ctr f in @@ -228,5 +229,5 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = in let skl_of_t = skolemisation ss [] 0 t in if Logger.log_enabled () then - log_sklm "Skolemized form of %a is %a" Print.term t Print.term skl_of_t; + log "Skolemized form of %a is %a" Print.term t Print.term skl_of_t; skl_of_t diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli index 70b37ad6f..a75282862 100644 --- a/src/handle/skolem.mli +++ b/src/handle/skolem.mli @@ -2,6 +2,7 @@ open Common open Core open Term +(** Builtin configuration for propositional logic. *) type fol_config = { symb_P : sym; (** Encoding of propositions. *) symb_T : sym; (** Encoding of types. *) @@ -14,24 +15,23 @@ type fol_config = { symb_ex : sym; (** Exists(∃) symbol. *) symb_all : sym; (** Forall(∀) symbol. *) } -(** Builtin configuration for propositional logic. *) -val nnf_of : fol_config -> term -> term (** [nnf_of cfg phi] computes the negation normal form of first order formula [phi]. *) +val nnf_of : fol_config -> term -> term -exception PrenexFormulaNotNnf of term (** Raised by [prenex_of] when its formula is not in negation normal form. *) +exception PrenexFormulaNotNnf of term -val prenex_of : fol_config -> term -> term (** [prenex_of cfg phi] computes the prenex normal form of first order formula [phi]. @raise PrenexFormulaNotNnf when formula [phi] is not in negation normal - form. *) + form. *) +val prenex_of : fol_config -> term -> term +(** [handle ss pos t] returns a skolemized form of term [t] (at position + [pos]). A term is skolemized when it has no existential quantifiers: to + this end, for each existential quantifier in [t], signature state [ss] is + extended with a new symbol in order to substitute the variable bound by + the said quantifier. *) val handle : Sig_state.t -> Pos.popt -> term -> term -(** [handle ss pos t] returns a skolemized form of term [t] (at position [pos]). - A term is skolemized when it has no existential quantifiers: to this end, - for each existential quantifier in [t], signature state [ss] is extended - with a new symbol in order to substitute the variable bound by the said - quantifier. *) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index c508b9b63..247619fc9 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -17,9 +17,9 @@ let log_tact = log_tact.pp let admitted : int Stdlib.ref = Stdlib.ref (-1) (** [add_axiom ss sym_pos m] adds in signature state [ss] a new axiom symbol - of type [!(m.meta_type)] and instantiate [m] with it. WARNING: It does not - check whether the type of [m] contains metavariables. Return updated signature - state [ss] and the new axiom symbol.*) + of type [!(m.meta_type)] and instantiate [m] with it. WARNING: It does not + check whether the type of [m] contains metavariables. Return updated + signature state [ss] and the new axiom symbol.*) let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t * sym = fun ss sym_pos m -> let name = @@ -336,24 +336,26 @@ let handle : let p = new_problem() in tac_refine pos ps gt gs p (Why3_tactic.handle ss sym_pos cfg gt) | _ -> assert false) - | P_tac_skolem -> + | P_tac_skolem -> (*Gets user-defined symbol identifiers mapped using "builtin" command : *) let symb_P = Builtin.get ss pos "P" in (*Extract term [t] in a typing goal of form π(t) *) - let t = match get_args gt.goal_type with + let t = match get_args gt.goal_type with | Symb(s), [tl] when s == symb_P -> tl - | _ -> Format.printf "@. Typing goal not in form P (term) %a @." term gt.goal_type; gt.goal_type + | _ -> + Format.printf "@. Typing goal not in form P (term) %a @." + term gt.goal_type; gt.goal_type in let skl_t = Skolem.handle ss sym_pos t in let c = Env.to_ctxt env in - let p = new_problem() in + let p = new_problem() in (*Equisat represents "π (skl_t) → π (t)"*) let var_cst = new_tvar "cst" in let proof_t = mk_Appl (mk_Symb symb_P, t) in let proof_skl_t = mk_Appl (mk_Symb symb_P, skl_t) in let equisat = mk_Prod (proof_skl_t, bind var_cst lift proof_t) in let t_meta_eqs = LibMeta.make p c equisat in - let meta_eqs = match t_meta_eqs with + let meta_eqs = match t_meta_eqs with | Meta(m, _) -> m |_ -> assert false in From feb5f9c277ad019ee30172d76e0bd62759e468f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 28 Dec 2022 18:17:43 +0100 Subject: [PATCH 11/16] factorize fol config with why3_tactic --- src/handle/fol.ml | 31 +++++++++++++++++++++++++++++++ src/handle/skolem.ml | 36 +++--------------------------------- src/handle/skolem.mli | 19 +++---------------- src/handle/why3_tactic.ml | 28 +--------------------------- 4 files changed, 38 insertions(+), 76 deletions(-) create mode 100644 src/handle/fol.ml diff --git a/src/handle/fol.ml b/src/handle/fol.ml new file mode 100644 index 000000000..78e54c0ef --- /dev/null +++ b/src/handle/fol.ml @@ -0,0 +1,31 @@ +(** Configuration for tactics based on first-order logic. *) + +open Common +open Core open Term + +(** Builtin configuration for propositional logic. *) +type config = + { symb_P : sym (** Encoding of propositions. *) + ; symb_T : sym (** Encoding of types. *) + ; symb_or : sym (** Disjunction(∨) symbol. *) + ; symb_and : sym (** Conjunction(∧) symbol. *) + ; symb_imp : sym (** Implication(⇒) symbol. *) + ; symb_bot : sym (** Bot(⊥) symbol. *) + ; symb_top : sym (** Top(⊤) symbol. *) + ; symb_not : sym (** Not(¬) symbol. *) + ; symb_ex : sym (** Exists(∃) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) } + +(** [get_config ss pos] build the configuration using [ss]. *) +let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> + let builtin = Builtin.get ss pos in + { symb_P = builtin "P" + ; symb_T = builtin "T" + ; symb_or = builtin "or" + ; symb_and = builtin "and" + ; symb_imp = builtin "imp" + ; symb_bot = builtin "bot" + ; symb_top = builtin "top" + ; symb_not = builtin "not" + ; symb_ex = builtin "ex" + ; symb_all = builtin "all" } diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index 47cb3b997..bca0f12ad 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -1,41 +1,11 @@ open Common open Core open Term +open Fol let log = Logger.make 'a' "sklm" "skolemization" let log = log.pp -type fol_config = { - symb_P : sym; (** Encoding of propositions. *) - symb_T : sym; (** Encoding of types. *) - symb_or : sym; (** Disjunction(∨) symbol. *) - symb_and : sym; (** Conjunction(∧) symbol. *) - symb_imp : sym; (** Implication(⇒) symbol. *) - symb_bot : sym; (** Bot(⊥) symbol. *) - symb_top : sym; (** Top(⊤) symbol. *) - symb_not : sym; (** Not(¬) symbol. *) - symb_ex : sym; (** Exists(∃) symbol. *) - symb_all : sym; (** Forall(∀) symbol. *) -} -(** Builtin configuration for propositional logic. *) - -(** [get_fol_config ss pos] build the configuration using [ss]. *) -let get_fol_config : Sig_state.t -> Pos.popt -> fol_config = - fun ss pos -> - let builtin = Builtin.get ss pos in - { - symb_P = builtin "P"; - symb_T = builtin "T"; - symb_or = builtin "or"; - symb_and = builtin "and"; - symb_imp = builtin "imp"; - symb_bot = builtin "bot"; - symb_top = builtin "top"; - symb_not = builtin "not"; - symb_ex = builtin "ex"; - symb_all = builtin "all"; - } - let add_ctxt : ctxt -> tvar -> term -> ctxt = fun c var typ -> c @ [ (var, typ, None) ] @@ -107,7 +77,7 @@ let mk_quant : term -> quant -> term = (** [nnf_term cfg t] computes the negation normal form of a first order formula. *) -let nnf_of : fol_config -> term -> term = +let nnf_of : config -> term -> term = fun cfg t -> let rec nnf_prop t = match get_args t with @@ -201,7 +171,7 @@ let prenex_of cfg t = let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> (*Gets user-defined symbol identifiers mapped using "builtin" command.*) - let cfg = get_fol_config ss pos in + let cfg = get_config ss pos in let t = nnf_of cfg t in let t = try prenex_of cfg t diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli index a75282862..6541bbb5b 100644 --- a/src/handle/skolem.mli +++ b/src/handle/skolem.mli @@ -1,24 +1,11 @@ open Common open Core open Term - -(** Builtin configuration for propositional logic. *) -type fol_config = { - symb_P : sym; (** Encoding of propositions. *) - symb_T : sym; (** Encoding of types. *) - symb_or : sym; (** Disjunction(∨) symbol. *) - symb_and : sym; (** Conjunction(∧) symbol. *) - symb_imp : sym; (** Implication(⇒) symbol. *) - symb_bot : sym; (** Bot(⊥) symbol. *) - symb_top : sym; (** Top(⊤) symbol. *) - symb_not : sym; (** Not(¬) symbol. *) - symb_ex : sym; (** Exists(∃) symbol. *) - symb_all : sym; (** Forall(∀) symbol. *) -} +open Fol (** [nnf_of cfg phi] computes the negation normal form of first order formula [phi]. *) -val nnf_of : fol_config -> term -> term +val nnf_of : config -> term -> term (** Raised by [prenex_of] when its formula is not in negation normal form. *) exception PrenexFormulaNotNnf of term @@ -27,7 +14,7 @@ exception PrenexFormulaNotNnf of term [phi]. @raise PrenexFormulaNotNnf when formula [phi] is not in negation normal form. *) -val prenex_of : fol_config -> term -> term +val prenex_of : config -> term -> term (** [handle ss pos t] returns a skolemized form of term [t] (at position [pos]). A term is skolemized when it has no existential quantifiers: to diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml index b35f916b3..b2cbe3bd1 100644 --- a/src/handle/why3_tactic.ml +++ b/src/handle/why3_tactic.ml @@ -4,6 +4,7 @@ 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" @@ -37,33 +38,6 @@ let why3_datadir : string = Why3.Whyconf.datadir why3_main let why3_env : Why3.Env.env = Why3.Env.create_env (Why3.Whyconf.loadpath why3_main) -(** Builtin configuration for propositional logic. *) -type config = - { symb_P : sym (** Encoding of propositions. *) - ; symb_T : sym (** Encoding of types. *) - ; symb_or : sym (** Disjunction(∨) symbol. *) - ; symb_and : sym (** Conjunction(∧) symbol. *) - ; symb_imp : sym (** Implication(⇒) symbol. *) - ; symb_bot : sym (** Bot(⊥) symbol. *) - ; symb_top : sym (** Top(⊤) symbol. *) - ; symb_not : sym (** Not(¬) symbol. *) - ; symb_ex : sym (** Exists(∃) symbol. *) - ; symb_all : sym (** Forall(∀) symbol. *) } - -(** [get_config ss pos] build the configuration using [ss]. *) -let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> - let builtin = Builtin.get ss pos in - { symb_P = builtin "P" - ; symb_T = builtin "T" - ; symb_or = builtin "or" - ; symb_and = builtin "and" - ; symb_imp = builtin "imp" - ; symb_bot = builtin "bot" - ; symb_top = builtin "top" - ; symb_not = builtin "not" - ; symb_ex = builtin "ex" - ; symb_all = builtin "all" } - (** A map from lambdapi terms to Why3 constants. *) type cnst_table = (term * Why3.Term.lsymbol) list From 9e4c0e62e2fe0a7d4278e741a24bff0aacf55be6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 28 Dec 2022 19:07:47 +0100 Subject: [PATCH 12/16] renamings --- src/handle/skolem.ml | 57 ++++++++++++++++++++----------------------- src/handle/skolem.mli | 25 ++++++++----------- src/handle/tactic.ml | 56 ++++++++++++++++++------------------------ 3 files changed, 60 insertions(+), 78 deletions(-) diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml index bca0f12ad..d8947c080 100644 --- a/src/handle/skolem.ml +++ b/src/handle/skolem.ml @@ -1,35 +1,30 @@ +(** Skolemization tactic. *) + open Common -open Core -open Term +open Core open Term open Fol let log = Logger.make 'a' "sklm" "skolemization" let log = log.pp -let add_ctxt : ctxt -> tvar -> term -> ctxt = +let add_var : ctxt -> tvar -> term -> ctxt = fun c var typ -> c @ [ (var, typ, None) ] -(**Skolemization*) - -(*[new_skolem ss ctx cpt ex_typ] is called when existantial quantifier ("∃y") - occurs. [ex_typ] is the type of quantificated variable "y". In order to - eliminate ∃ quantifier, we need to extend signature state [ss] with a skolem - term, represented by a fresh symbol that will later replace the binded - variable ("y"). Such skolem term may either be a skolem function or a skolem - constant : The type of a skolem term depends on registered variables in - [ctx] For example, if a set of variables x1:a1, x2:a2,..., xn:an were - previously introduced by an universal quantifier, A skolem term "skt" will - take as arguments x1, ..., xn, and must therefore be typed as follows : skt - (x1, x2, ..., xn) : a1 -> a2 -> ... -> an -> ex_typ. A skolem term is a - constant if skolemized term is not in the scope of any universal quantifier, - namely, [ctx] is empty. For the sake of clarity, we use a counter [cpt] for - naming the generated symbol. OUT : Updated signature state [upt_sig] is - returned, as well as introduced symbol [symb_skt] and updated counter*) +(* [new_skolem ss ctx ctr ex_typ] is called when existantial quantifier "∃y" + occurs. [ex_typ] is the type of the quantified variable "y". In order to + eliminate ∃ quantifier, we need to extend signature state [ss] with a + skolem term, represented by a fresh symbol that will later replace the + binded variable "y". Such skolem term may either be a skolem function or a + skolem constant: the type of a skolem term depends on registered variables + in [ctx]. For example, if a set of variables x1:a1, x2:a2,..., xn:an were + previously introduced by an universal quantifier, A skolem term "skt" will + take as arguments x1, ..., xn, and must therefore have type a1 -> a2 -> + ... -> an -> ex_typ. We use a counter [ctr] for naming the generated + symbols. OUT : Updated signature state [upt_sig] is returned, as well as + introduced symbol [symb_skt] and updated counter. *) let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int = fun ss ctx ctr ex_typ -> - let skt_name = - if ctx == [] then "c" ^ string_of_int ctr else "f" ^ string_of_int ctr - in + let skt_name = "f" ^ string_of_int ctr in let skt, _ = Ctxt.to_prod ctx ex_typ in let upt_sig, symb_skt = Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] @@ -77,7 +72,7 @@ let mk_quant : term -> quant -> term = (** [nnf_term cfg t] computes the negation normal form of a first order formula. *) -let nnf_of : config -> term -> term = +let nnf : config -> term -> term = fun cfg t -> let rec nnf_prop t = match get_args t with @@ -120,9 +115,9 @@ let nnf_of : config -> term -> term = in nnf_prop t -exception PrenexFormulaNotNnf of term +exception NotInNnf of term -let prenex_of cfg t = +let pnf cfg t = let rec prenex t = match get_args t with | Symb s, [ t1; t2 ] when s == cfg.symb_and -> @@ -138,13 +133,13 @@ let prenex_of cfg t = let qlist = qlist1 @ qlist2 in (qlist, t) | Symb s, [ _; _ ] when s == cfg.symb_imp -> - raise @@ PrenexFormulaNotNnf t + raise @@ NotInNnf t | Symb s, [ nt ] when s == cfg.symb_not -> let res = match nt with | Vari _ -> ([], t) | Symb _ -> ([], t) - | _ -> raise @@ PrenexFormulaNotNnf t + | _ -> raise @@ NotInNnf t in res | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> @@ -172,10 +167,10 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = fun ss pos t -> (*Gets user-defined symbol identifiers mapped using "builtin" command.*) let cfg = get_config ss pos in - let t = nnf_of cfg t in + let t = nnf cfg t in let t = - try prenex_of cfg t - with PrenexFormulaNotNnf _ -> + try pnf cfg t + with NotInNnf _ -> assert false (* [t] is put into nnf before *) in let rec skolemisation ss ctx ctr t = @@ -190,7 +185,7 @@ let handle : Sig_state.t -> Pos.popt -> term -> term = (* When universal quantification occurs, quantified variable is added to context*) let var, f = Bindlib.unbind tb in - let maj_ctx = add_ctxt ctx var a in + let maj_ctx = add_var ctx var a in let maj_f = skolemisation ss maj_ctx ctr f in let maj_tb = bind var lift maj_f in (*Reconstruct a term of form ∀ x : P, t', with t' skolemized*) diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli index 6541bbb5b..b9f998e56 100644 --- a/src/handle/skolem.mli +++ b/src/handle/skolem.mli @@ -3,22 +3,17 @@ open Core open Term open Fol -(** [nnf_of cfg phi] computes the negation normal form of first order formula - [phi]. *) -val nnf_of : config -> term -> term +(** [nnf cfg phi] returns the negation normal form of [phi], assuming it is + the encoding of a first-order formula using [cfg]. *) +val nnf : config -> term -> term -(** Raised by [prenex_of] when its formula is not in negation normal form. *) -exception PrenexFormulaNotNnf of term +exception NotInNnf of term -(** [prenex_of cfg phi] computes the prenex normal form of first order formula - [phi]. - @raise PrenexFormulaNotNnf when formula [phi] is not in negation normal - form. *) -val prenex_of : config -> term -> term +(** [pnf cfg phi] returns the prenex normal form of [phi]. + @raise NotInNnf when formula [phi] is not in negation normal form. *) +val pnf : config -> term -> term -(** [handle ss pos t] returns a skolemized form of term [t] (at position - [pos]). A term is skolemized when it has no existential quantifiers: to - this end, for each existential quantifier in [t], signature state [ss] is - extended with a new symbol in order to substitute the variable bound by - the said quantifier. *) +(** [skolem ss pos t] returns the skolemized form of [t] ([pos] is used for + error messages). Existential quantifiers are replaced by new symbols that + are added in the signature state [ss]. *) val handle : Sig_state.t -> Pos.popt -> term -> term diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 247619fc9..ca2fceec6 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -311,24 +311,20 @@ let handle : | P_tac_sym -> let cfg = Rewrite.get_eq_config ss pos in let (a,l,r), vs = Rewrite.get_eq_data cfg pos gt.goal_type in - begin match ps.proof_goals with - | Typ gt::gs -> - let a,l,r = - if Array.length vs = 0 then a,l,r - else fst (Rewrite.get_eq_data cfg pos gt.goal_type) - in - let p = new_problem() in - let prf = - let mt = - mk_Appl(mk_Symb cfg.symb_P, - add_args (mk_Symb cfg.symb_eq) [a; r; l]) in - let meta_term = LibMeta.make p (Env.to_ctxt gt.goal_hyps) mt in - (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *) - Rewrite.swap cfg a r l meta_term - in - tac_refine pos ps gt gs p prf - | _ -> assert false - end + let a,l,r = + if Array.length vs = 0 then a,l,r + else fst (Rewrite.get_eq_data cfg pos gt.goal_type) + in + let p = new_problem() in + let prf = + let mt = + mk_Appl(mk_Symb cfg.symb_P, + add_args (mk_Symb cfg.symb_eq) [a; r; l]) in + let meta_term = LibMeta.make p (Env.to_ctxt gt.goal_hyps) mt in + (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *) + Rewrite.swap cfg a r l meta_term + in + tac_refine pos ps gt gs p prf | P_tac_why3 cfg -> let ps = assume (count_products (Env.to_ctxt env) gt.goal_type) in (match ps.proof_goals with @@ -337,34 +333,30 @@ let handle : tac_refine pos ps gt gs p (Why3_tactic.handle ss sym_pos cfg gt) | _ -> assert false) | P_tac_skolem -> - (*Gets user-defined symbol identifiers mapped using "builtin" command : *) - let symb_P = Builtin.get ss pos "P" in - (*Extract term [t] in a typing goal of form π(t) *) - let t = match get_args gt.goal_type with - | Symb(s), [tl] when s == symb_P -> tl - | _ -> - Format.printf "@. Typing goal not in form P (term) %a @." - term gt.goal_type; gt.goal_type + let sym_P = Builtin.get ss pos "P" in + let t = + match get_args gt.goal_type with + | Symb(s), [t] when s == sym_P -> t + | _ -> fatal pos "Goal not of form (%a _)@." sym sym_P in let skl_t = Skolem.handle ss sym_pos t in + (* FIXME. We currently generate an axiom ax: P skl_t → P t in order to + build a proof of P t from a proof of P skl_t. *) let c = Env.to_ctxt env in let p = new_problem() in - (*Equisat represents "π (skl_t) → π (t)"*) let var_cst = new_tvar "cst" in - let proof_t = mk_Appl (mk_Symb symb_P, t) in - let proof_skl_t = mk_Appl (mk_Symb symb_P, skl_t) in + let proof_t = mk_Appl (mk_Symb sym_P, t) in + let proof_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in let equisat = mk_Prod (proof_skl_t, bind var_cst lift proof_t) in let t_meta_eqs = LibMeta.make p c equisat in let meta_eqs = match t_meta_eqs with | Meta(m, _) -> m |_ -> assert false in - (*ax is the axiom of equisatisfiability between a proof of a term [t] - and a proof of its skolemized form [skl_t].*) let _, ax = add_axiom ss sym_pos meta_eqs in let meta_type = LibMeta.make p c mk_Type in let meta_x = LibMeta.make p c meta_type in - tac_refine sym_pos ps gt gs p (mk_Appl (mk_Symb ax, meta_x)) + tac_refine pos ps gt gs p (mk_Appl (mk_Symb ax, meta_x)) (** Representation of a tactic output. *) type tac_output = Sig_state.t * proof_state * Query.result From ac421648f52575827482f4cfd5ffee6c502fc2cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 29 Dec 2022 11:07:25 +0100 Subject: [PATCH 13/16] tactics do not need to generate new sig_state as axioms do not need to be added in scope --- src/common/pos.ml | 2 +- src/handle/command.ml | 31 +++++++-------- src/handle/tactic.ml | 84 +++++++++++++++++++-------------------- src/handle/why3_tactic.ml | 1 + src/pure/pure.ml | 3 +- tests/OK/admit.lp | 2 +- tests/cnfnnf.ml | 11 ++--- 7 files changed, 65 insertions(+), 69 deletions(-) diff --git a/src/common/pos.ml b/src/common/pos.ml index ce7e831d9..9ff3df19a 100644 --- a/src/common/pos.ml +++ b/src/common/pos.ml @@ -69,7 +69,7 @@ let cat : popt -> popt -> popt = fun p1 p2 -> | None, Some p -> Some p | None, None -> None -(** [shift k p] returns a position that is [k] characters before [p]. *) +(** [shift k p] returns a position that is [k] characters after [p]. *) let shift : int -> popt -> popt = fun k p -> match p with | None -> assert false diff --git a/src/handle/command.ml b/src/handle/command.ml index 3a838cb69..25a42f316 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -470,22 +470,19 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = match pe.elt with | P_proof_abort -> wrn pe.pos "Proof aborted."; ss | P_proof_admitted -> - (* If the proof is finished, display a warning. *) - let ss = if finished ps then - ( wrn pe.pos "The proof is finished. Use 'end' instead."; ss ) - else - (* We admit all the remaining typing goals. *) - let admit_goal ss g = - match g with - | Unif _ -> fatal pos "Cannot admit unification goals." - | Typ gt -> - let m = gt.goal_meta in - match !(m.meta_value) with - | None -> Tactic.admit_meta ss p_sym_nam.pos m - | Some _ -> ss - in List.fold_left admit_goal ss ps.proof_goals + fatal pe.pos "The proof is finished. Use 'end' instead."; + (* Admit all the remaining typing goals. *) + let admit_goal g = + match g with + | Unif _ -> fatal pos "Cannot admit unification goals." + | Typ gt -> + let m = gt.goal_meta in + match !(m.meta_value) with + | None -> Tactic.admit_meta ss p_sym_nam.pos m + | Some _ -> () in + List.iter admit_goal ps.proof_goals; (* Add the symbol in the signature with a warning. *) Console.out 2 (Color.red "symbol %a : %a") uid id term a; wrn pe.pos "Proof admitted."; @@ -564,7 +561,7 @@ let handle : compiler -> Sig_state.t -> Syntax.p_command -> Sig_state.t = match p with | None -> ss | Some d -> - let ss, ps, _ = - fold_proof (Tactic.handle d.pdata_sym_pos d.pdata_prv) - (ss, d.pdata_state, None) d.pdata_proof + let ps, _ = + fold_proof (Tactic.handle ss d.pdata_sym_pos d.pdata_prv) + (d.pdata_state, None) d.pdata_proof in d.pdata_finalize ss ps diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index ca2fceec6..b6219c30e 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -20,14 +20,14 @@ let admitted : int Stdlib.ref = Stdlib.ref (-1) of type [!(m.meta_type)] and instantiate [m] with it. WARNING: It does not check whether the type of [m] contains metavariables. Return updated signature state [ss] and the new axiom symbol.*) -let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t * sym = +let add_axiom : Sig_state.t -> popt -> meta -> sym = fun ss sym_pos m -> let name = let i = Stdlib.(incr admitted; !admitted) in Printf.sprintf "_ax%i" i in (* Create a symbol with the same type as the metavariable *) - let ss, sym = + let sym = Console.out 1 (Color.red "axiom %a: %a") uid name term !(m.meta_type); (* Temporary hack for axioms to have a declaration position in the order @@ -38,7 +38,10 @@ let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t * sym = else shift (n - 100) sym_pos in let id = Pos.make pos name in - Sig_state.add_symbol ss Public Defin Eager true id !(m.meta_type) [] None + (* We ignore the new ss returned by Sig_state.add_symbol: axioms do not + need to be in scope. *) + snd (Sig_state.add_symbol ss + Public Defin Eager true id !(m.meta_type) [] None) in (* Create the value which will be substituted for the metavariable. This value is [sym x0 ... xn] where [xi] are variables that will be @@ -49,29 +52,26 @@ let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t * sym = let ax = _Appl_Symb sym (Array.to_list vars |> List.map _Vari) in Bindlib.(bind_mvar vars ax |> unbox) in - LibMeta.set (new_problem()) m meta_value; (ss, sym) + LibMeta.set (new_problem()) m meta_value; sym (** [admit_meta ss sym_pos m] adds as many axioms as needed in the signature state [ss] to instantiate the metavariable [m] by a fresh axiom added to the signature [ss]. *) -let admit_meta : Sig_state.t -> popt -> meta -> Sig_state.t = +let admit_meta : Sig_state.t -> popt -> meta -> unit = fun ss sym_pos m -> - let ss = Stdlib.ref ss in (* [ms] records the metas that we are instantiating. *) let rec admit ms m = (* This assertion should be ensured by the typechecking algorithm. *) assert (not (MetaSet.mem m ms)); LibMeta.iter true (admit (MetaSet.add m ms)) [] !(m.meta_type); - Stdlib.(ss := fst (add_axiom !ss sym_pos m)) + ignore (add_axiom ss sym_pos m) in - admit MetaSet.empty m; Stdlib.(!ss) + admit MetaSet.empty m (** [tac_admit ss pos ps gt] admits typing goal [gt]. *) -let tac_admit : - Sig_state.t -> popt -> proof_state -> goal_typ -> Sig_state.t * proof_state - = fun ss sym_pos ps gt -> - let ss = admit_meta ss sym_pos gt.goal_meta in - ss, remove_solved_goals ps +let tac_admit: Sig_state.t -> popt -> proof_state -> goal_typ -> proof_state = + fun ss sym_pos ps gt -> + admit_meta ss sym_pos gt.goal_meta; remove_solved_goals ps (** [tac_solve pos ps] tries to simplify the unification goals of the proof state [ps] and fails if constraints are unsolvable. *) @@ -182,6 +182,7 @@ let handle : match elt with | P_tac_fail | P_tac_query _ -> assert false (* done before *) + (* Tactics that apply to both unification and typing goals: *) | P_tac_simpl None -> {ps with proof_goals = Goal.simpl (Eval.snf []) g :: gs} | P_tac_simpl (Some qid) -> @@ -189,6 +190,7 @@ let handle : {ps with proof_goals = Goal.simpl (Eval.unfold_sym s) g :: gs} | P_tac_solve -> tac_solve pos ps | _ -> + (* Tactics that apply to typing goals only: *) match g with | Unif _ -> fatal pos "Not a typing goal." | Typ ({goal_hyps=env;_} as gt) -> @@ -214,11 +216,11 @@ let handle : tac_refine pos ps gt gs p (scope t) in match elt with - | P_tac_admit | P_tac_fail | P_tac_query _ | P_tac_simpl _ | P_tac_solve -> assert false (* done before *) + | P_tac_admit -> tac_admit ss sym_pos ps gt | P_tac_apply pt -> let t = scope pt in (* Compute the product arity of the type of [t]. *) @@ -285,8 +287,7 @@ let handle : tac_refine pos ps gt gs p u end | P_tac_induction -> tac_induction pos ps gt gs - | P_tac_refine t -> - let p = new_problem() in tac_refine pos ps gt gs p (scope t) + | P_tac_refine t -> tac_refine pos ps gt gs (new_problem()) (scope t) | P_tac_refl -> let cfg = Rewrite.get_eq_config ss pos in let (a,l,_), vs = Rewrite.get_eq_data cfg pos gt.goal_type in @@ -300,7 +301,7 @@ let handle : else let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in a,l in let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in - let p = new_problem() in tac_refine pos ps gt gs p prf + tac_refine pos ps gt gs (new_problem()) prf | _ -> assert false end | P_tac_rewrite(l2r,pat,eq) -> @@ -328,9 +329,10 @@ let handle : | P_tac_why3 cfg -> let ps = assume (count_products (Env.to_ctxt env) gt.goal_type) in (match ps.proof_goals with - | Typ gt::gs -> - let p = new_problem() in - tac_refine pos ps gt gs p (Why3_tactic.handle ss sym_pos cfg gt) + | Typ gt::gs -> + (*FIXME: Why3_tactic.handle should return an updated ss.*) + let t = Why3_tactic.handle ss pos cfg gt in + tac_refine pos ps gt gs (new_problem()) t | _ -> assert false) | P_tac_skolem -> let sym_P = Builtin.get ss pos "P" in @@ -340,26 +342,23 @@ let handle : | _ -> fatal pos "Goal not of form (%a _)@." sym sym_P in let skl_t = Skolem.handle ss sym_pos t in - (* FIXME. We currently generate an axiom ax: P skl_t → P t in order to - build a proof of P t from a proof of P skl_t. *) + (* FIXME. We generate an axiom ax: P skl_t → P t in order to build a proof + of P t from a proof of P skl_t. *) + let p_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in let c = Env.to_ctxt env in + let ax_typ = mk_Prod (p_skl_t, bind (new_tvar "_") lift gt.goal_type) in + let ax_typ, arity = Ctxt.to_prod c ax_typ in + let m = LibMeta.fresh (new_problem()) ax_typ arity in + (*FIXME: check that ax_typ has no meta.*) + let ax = add_axiom ss sym_pos m in + (*let gt = match Goal.of_meta m with Typ gt -> gt | _ -> assert false in + let _, ps = tac_admit ss sym_pos ps gt in*) let p = new_problem() in - let var_cst = new_tvar "cst" in - let proof_t = mk_Appl (mk_Symb sym_P, t) in - let proof_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in - let equisat = mk_Prod (proof_skl_t, bind var_cst lift proof_t) in - let t_meta_eqs = LibMeta.make p c equisat in - let meta_eqs = match t_meta_eqs with - | Meta(m, _) -> m - |_ -> assert false - in - let _, ax = add_axiom ss sym_pos meta_eqs in - let meta_type = LibMeta.make p c mk_Type in - let meta_x = LibMeta.make p c meta_type in - tac_refine pos ps gt gs p (mk_Appl (mk_Symb ax, meta_x)) + let new_goal = LibMeta.make p c p_skl_t in + tac_refine pos ps gt gs p (mk_Appl (mk_Symb ax, new_goal)) (** Representation of a tactic output. *) -type tac_output = Sig_state.t * proof_state * Query.result +type tac_output = proof_state * Query.result (** [handle ss sym_pos prv ps tac] applies tactic [tac] in the proof state [ps] and returns the new proof state. *) @@ -370,23 +369,22 @@ let handle : | P_tac_fail -> fatal pos "Call to tactic \"fail\"" | P_tac_query(q) -> if Logger.log_enabled () then log_tact "%a@." Pretty.tactic tac; - ss, ps, Query.handle ss (Some ps) q + ps, Query.handle ss (Some ps) q | _ -> match ps.proof_goals with | [] -> fatal pos "No remaining goals." - | Typ gt::_ when elt = P_tac_admit -> - let ss, ps = tac_admit ss sym_pos ps gt in ss, ps, None | g::_ -> if Logger.log_enabled () then log_tact ("%a@\n" ^^ Color.red "%a") Proof.Goal.pp g Pretty.tactic tac; - ss, handle ss sym_pos prv ps tac, None + handle ss sym_pos prv ps tac, None (** [handle sym_pos prv r tac n] applies the tactic [tac] from the previous tactic output [r] and checks that the number of goals of the new proof state is compatible with the number [n] of subproofs. *) -let handle : popt -> bool -> tac_output -> p_tactic -> int -> tac_output = - fun sym_pos prv (ss, ps, _) t nb_subproofs -> - let (_, ps', _) as a = handle ss sym_pos prv ps t in +let handle : + Sig_state.t -> popt -> bool -> tac_output -> p_tactic -> int -> tac_output = + fun ss sym_pos prv (ps, _) t nb_subproofs -> + let (ps', _) as a = handle ss sym_pos prv ps t in let nb_goals_before = List.length ps.proof_goals in let nb_goals_after = List.length ps'.proof_goals in let nb_newgoals = nb_goals_after - nb_goals_before in diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml index b2cbe3bd1..d481bc163 100644 --- a/src/handle/why3_tactic.ml +++ b/src/handle/why3_tactic.ml @@ -259,6 +259,7 @@ let handle : fatal pos "\"%s\" did not find a proof" prover_name; (* Create a new axiom name that represents the proved goal. *) let axiom_name = new_axiom_name () in + (*FIXME: we should check that there is no meta in the type of m. *) (* Add the axiom to the current signature. *) let a = Sign.add_symbol ss.signature Public Defin Eager true diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 8668f4be7..a781671cb 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -166,8 +166,7 @@ let handle_command : state -> Command.t -> command_result = let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result = fun (_, ss, ps, finalize, prv, sym_pos) tac n -> try - let ss, ps, qres = - Handle.Tactic.handle sym_pos prv (ss, ps, None) tac n in + let ps, qres = Handle.Tactic.handle ss sym_pos prv (ps, None) tac n in let qres = Option.map (fun f -> f ()) qres in Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres) with Fatal(p,m) -> Tac_Error(p,m) diff --git a/tests/OK/admit.lp b/tests/OK/admit.lp index ac22e28ad..b374c8002 100644 --- a/tests/OK/admit.lp +++ b/tests/OK/admit.lp @@ -18,7 +18,7 @@ symbol π_f: Prf (f _) begin admit // Adds an axiom [ax_?] -admitted; +end; // Two metas, one depending on the other symbol prop2: Prf prop1 → Prop; diff --git a/tests/cnfnnf.ml b/tests/cnfnnf.ml index efe948bfc..51a3d6c4a 100644 --- a/tests/cnfnnf.ml +++ b/tests/cnfnnf.ml @@ -33,7 +33,7 @@ let fol_symb_str = [ "P"; "t"; "∨"; "∧"; "⇒"; "⊥"; "⊤"; "¬"; "∃"; " (** [get_config ss pos] build the configuration using [ss]. *) let get_config slist = let get n = List.nth slist n in - Handle.Skolem. + Handle.Fol. { symb_P = get 0; symb_T = get 1; @@ -65,8 +65,9 @@ let sig_state, cfg = (ss, get_config (List.rev symlist)) (** An environment defining two variables [A] and [B]. *) -let env = - Env.empty |> Env.add (new_tvar "A") _Kind None |> Env.add (new_tvar "B") _Kind None +let env = Env.empty + |> Env.add (new_tvar "A") _Kind None + |> Env.add (new_tvar "B") _Kind None let test_nnf () = let formula = @@ -76,7 +77,7 @@ let test_nnf () = let witness = "∀ P (λ x1, ∀ B (λ y1, ∧ (∧ (¬ x1) (¬ y1)) ⊤))" in Alcotest.(check string) "Negation normal form" witness - (Format.asprintf "%a" Print.term (Handle.Skolem.nnf_of cfg formula)) + (Format.asprintf "%a" Print.term (Handle.Skolem.nnf cfg formula)) let test_pnf () = let formula = @@ -85,7 +86,7 @@ let test_pnf () = let witness = "∀ P (λ x1, ∨ x1 A)" in Alcotest.(check string) "Prenex normal form" witness - (Format.asprintf "%a" Print.term (Handle.Skolem.prenex_of cfg formula)) + (Format.asprintf "%a" Print.term (Handle.Skolem.pnf cfg formula)) let _ = let open Alcotest in From 14e775fb3cd22f21d6c6b47756ad9aca7c15eba8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 29 Dec 2022 12:31:09 +0100 Subject: [PATCH 14/16] why3 tactic: let tac_admit generate the axiom --- src/handle/tactic.ml | 10 ++++------ src/handle/why3_tactic.ml | 33 ++++++--------------------------- src/handle/why3_tactic.mli | 11 +++++------ 3 files changed, 15 insertions(+), 39 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index b6219c30e..934dfbf27 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -329,11 +329,9 @@ let handle : | P_tac_why3 cfg -> let ps = assume (count_products (Env.to_ctxt env) gt.goal_type) in (match ps.proof_goals with - | Typ gt::gs -> - (*FIXME: Why3_tactic.handle should return an updated ss.*) - let t = Why3_tactic.handle ss pos cfg gt in - tac_refine pos ps gt gs (new_problem()) t - | _ -> assert false) + | Typ gt::_ -> + Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt + | _ -> assert false) | P_tac_skolem -> let sym_P = Builtin.get ss pos "P" in let t = @@ -344,7 +342,7 @@ let handle : let skl_t = Skolem.handle ss sym_pos t in (* FIXME. We generate an axiom ax: P skl_t → P t in order to build a proof of P t from a proof of P skl_t. *) - let p_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in + let p_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in let c = Env.to_ctxt env in let ax_typ = mk_Prod (p_skl_t, bind (new_tvar "_") lift gt.goal_type) in let ax_typ, arity = Ctxt.to_prod c ax_typ in diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml index d481bc163..d2bb40f7f 100644 --- a/src/handle/why3_tactic.ml +++ b/src/handle/why3_tactic.ml @@ -98,11 +98,6 @@ end = struct List.fold_left f acc tbl end -(** [new_axiom_name ()] generates a fresh axiom name. *) -let new_axiom_name : unit -> string = - let counter = ref 0 in - fun _ -> incr counter; "Why3axiom_" ^ (string_of_int !counter) - (** [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]. *) @@ -240,14 +235,12 @@ let run_task : Why3.Task.task -> Pos.popt -> string -> bool = ~limit driver tsk in Why3.Call_provers.((wait_on_call call).pr_answer = Valid) -(** [handle ss pos prover_name g] runs the Why3 prover corresponding - to the name [prover_name] (if given or a default one otherwise) - on the goal [g]. - If the prover succeeded to prove the goal, then this is reflected by a new - axiom that is added to signature [ss]. *) +(** [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 -> term = - fun ss pos prover_name {goal_meta = m; goal_hyps = hyps; goal_type = trm} -> + 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 @@ -256,18 +249,4 @@ let handle : 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; - (* Create a new axiom name that represents the proved goal. *) - let axiom_name = new_axiom_name () in - (*FIXME: we should check that there is no meta in the type of m. *) - (* Add the axiom to the current signature. *) - let a = - Sign.add_symbol ss.signature Public Defin Eager true - (Pos.make pos axiom_name) !(m.meta_type) [] - in - if Logger.log_enabled () then - log_why3 "axiom %a created" uid axiom_name; - (* Return the variable terms of each item in the context. *) - let terms = List.rev_map (fun (_, (x, _, _)) -> mk_Vari x) hyps in - (* Apply the instance of the axiom with context. *) - add_args (mk_Symb a) terms + fatal pos "\"%s\" did not find a proof" prover_name diff --git a/src/handle/why3_tactic.mli b/src/handle/why3_tactic.mli index 60e1d31c1..393a508f7 100644 --- a/src/handle/why3_tactic.mli +++ b/src/handle/why3_tactic.mli @@ -1,7 +1,7 @@ (** Calling a prover using Why3. *) open Common -open Core open Term +open Core open Timed (** [default_prover] contains the name of the current prover. Note that it can @@ -12,8 +12,7 @@ val default_prover : string ref a proof. It can be changed with "set prover ". *) val timeout : int ref -(** [handle ss pos ps prover_name g] runs the Why3 prover corresponding to the - name [prover_name] (if given or a default one otherwise) on the goal [g]. - If the prover succeeded to prove the goal, then this is reflected by a new - axiom that is added to signature [ss]. *) -val handle: Sig_state.t -> Pos.popt -> string option -> Proof.goal_typ -> term +(** [handle ss pos ps 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. *) +val handle: Sig_state.t -> Pos.popt -> string option -> Proof.goal_typ -> unit From cecef1565e3ee4f4fa9d4e9944f87dd3cbbb4739 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 29 Dec 2022 12:43:37 +0100 Subject: [PATCH 15/16] detail --- src/handle/tactic.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 934dfbf27..d6cf4813f 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -349,8 +349,6 @@ let handle : let m = LibMeta.fresh (new_problem()) ax_typ arity in (*FIXME: check that ax_typ has no meta.*) let ax = add_axiom ss sym_pos m in - (*let gt = match Goal.of_meta m with Typ gt -> gt | _ -> assert false in - let _, ps = tac_admit ss sym_pos ps gt in*) let p = new_problem() in let new_goal = LibMeta.make p c p_skl_t in tac_refine pos ps gt gs p (mk_Appl (mk_Symb ax, new_goal)) From f4a3ec78e4d6fe3c51d33b816e560ec05a9e5883 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 3 Jan 2023 12:48:33 +0100 Subject: [PATCH 16/16] update bnf grammar --- doc/lambdapi.bnf | 157 ----------------------------------------------- 1 file changed, 157 deletions(-) diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index 7b9c40d13..02ef7dbd0 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -12,160 +12,3 @@ QID ::= [UID "."]+ UID ::= "assert" | "assertnot" - ::= "require" "open" * ";" - | "require" * ";" - | "require" "as" ";" - | "open" * ";" - | * "symbol" * ":" - [] ";" - | * "symbol" * [":" ] - "≔" ";" - | * * "inductive" ("with" - )* ";" - | "rule" ("with" )* ";" - | "builtin" "≔" ";" - | "coerce_rule" ";" - | "unif_rule" ";" - | "notation" ";" - | ";" - - - ::= * "⊢" ":" - | * "⊢" "≡" - | "compute" - | "print" [] - | "proofterm" - | "debug" ("+"|"-") - | "flag" - | "prover" - | "prover_timeout" - | "verbose" - | "type" - - ::= UID - | QID - - ::= [] "associative" - | "commutative" - | "constant" - | "injective" - | "opaque" - | "private" - | "protected" - | "sequential" - - ::= UID - - ::= - | - - ::= - | - - ::= - | "(" + ":" ")" - | "[" + [":" ] "]" - - ::= - | - | "_" - - ::= - | - | - | "→" - - ::= "`" - | "Π" - | "λ" - | "let" * [":" ] "≔" "in" - - ::= + - - ::= - | "_" - | "TYPE" - | "?" UID [] - | "$" UID [] - | "(" ")" - | "[" "]" - | - - ::= "." "[" [ (";" )*] "]" - - ::= - | - - ::= UID - | QID - - ::= "@" UID - | "@" QID - - ::= + "," - | ":" "," - - ::= - | - | - - ::= "begin" + - | "begin" [] - - ::= "{" [] "}" - - ::= - | ";" - | ";" - - ::= * - - ::= "abort" - | "admitted" - | "end" - - ::= - | "admit" - | "apply" - | "assume" + - | "fail" - | "generalize" - | "have" ":" - | "induction" - | "refine" - | "reflexivity" - | "rewrite" [] [] - | "simplify" [] - | "solve" - | "symmetry" - | "why3" [] - - ::= - | "in" - | "in" "in" - | "in" ["in" ] - | "as" "in" - - ::= "." "[" "]" - - ::= * ":" "≔" ["|"] [ - ("|" )*] - - ::= * ":" - - ::= "↪" - - ::= "↪" "[" (";" - )* "]" - - ::= "≡" - - ::= "infix" [] - | "postfix" - | "prefix" - | "quantifier" - - ::= - | - -