From: denes Date: Fri, 5 Jun 2009 15:33:35 +0000 (+0000) Subject: First tests for paramodulation (pretty printer, unification) X-Git-Tag: make_still_working~3914 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b97a7976503b2d2e5cbc9199f848135a324775a8;p=helm.git First tests for paramodulation (pretty printer, unification) --- diff --git a/helm/software/components/METAS/meta.helm-ng_tactics.src b/helm/software/components/METAS/meta.helm-ng_tactics.src index 9b5db1359..73770ac9b 100644 --- a/helm/software/components/METAS/meta.helm-ng_tactics.src +++ b/helm/software/components/METAS/meta.helm-ng_tactics.src @@ -1,4 +1,4 @@ -requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics" +requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics helm-ng_paramodulation" version="0.0.1" archive(byte)="ng_tactics.cma" archive(native)="ng_tactics.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 3303e7a59..51b2f4bbf 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -38,6 +38,7 @@ MODULES = \ ng_refiner \ ng_disambiguation \ grafite_parser \ + ng_paramodulation \ ng_tactics \ grafite_engine \ tptp_grafite \ diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index dcfaf6c05..169873bf0 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -62,6 +62,7 @@ type ntactic = | NLetIn of loc * npattern * CicNotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern | NRewrite of loc * direction * CicNotationPt.term * npattern + | NAuto of loc * CicNotationPt.term auto_params type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) @@ -171,7 +172,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 21 +let magic = 22 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index e335c1b63..a9a15568f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -101,7 +101,7 @@ let pp_ntactic ~map_unicode_to_tex = function | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false - | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false + | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ | NAuto _ -> assert false ;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d4738a551..a9e5a56b5 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -604,6 +604,9 @@ let eval_ng_tac (text, prefix_len, tac) = ) hyps, (text,prefix_len,concl)) ) seqs) + | GrafiteAst.NAuto (_loc, params) -> + NTactics.auto_tac + ~params | GrafiteAst.NCases (_loc, what, where) -> NTactics.cases_tac ~what:(text,prefix_len,what) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index ce7f5c6ca..222e85f09 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -220,6 +220,7 @@ EXTEND SYMBOL <:unicode>; concl = tactic_term -> (List.rev hyps,concl) ] -> G.NAssert (loc, seqs) + | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params) | IDENT "ncases"; what = tactic_term ; where = pattern_spec -> G.NCases (loc, what, where) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 16b4a0b16..9cb1b46ee 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,24 +1,25 @@ -terms.cmi: pp.cmi: terms.cmi founif.cmi: terms.cmi index.cmi: terms.cmi orderings.cmi: terms.cmi -subst.cmi: terms.cmi +fosubst.cmi: terms.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi pp.cmx: terms.cmx pp.cmi -founif.cmo: terms.cmi subst.cmi founif.cmi -founif.cmx: terms.cmx subst.cmx founif.cmi +founif.cmo: terms.cmi fosubst.cmi founif.cmi +founif.cmx: terms.cmx fosubst.cmx founif.cmi index.cmo: terms.cmi index.cmi index.cmx: terms.cmx index.cmi orderings.cmo: terms.cmi orderings.cmi orderings.cmx: terms.cmx orderings.cmi -subst.cmo: terms.cmi subst.cmi -subst.cmx: terms.cmx subst.cmi +fosubst.cmo: terms.cmi fosubst.cmi +fosubst.cmx: terms.cmx fosubst.cmi nCicBlob.cmo: terms.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi cicBlob.cmx: terms.cmx cicBlob.cmi +paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi +paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile index 7eee8d511..152c74a1b 100644 --- a/helm/software/components/ng_paramodulation/Makefile +++ b/helm/software/components/ng_paramodulation/Makefile @@ -1,8 +1,8 @@ PACKAGE = ng_paramodulation INTERFACE_FILES = \ - terms.mli pp.mli founif.mli index.mli orderings.mli subst.mli \ - nCicBlob.mli cicBlob.mli + terms.mli pp.mli fosubst.mli founif.mli index.mli orderings.mli \ + nCicBlob.mli cicBlob.mli paramod.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml index f0caf2591..195f53df7 100644 --- a/helm/software/components/ng_paramodulation/cicBlob.ml +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -31,5 +31,7 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct let names = List.map (function Some (x,_) -> Some x | _ -> None) C.context;; let pp t = CicPp.pp t names;; + + let embed t = assert false;; end diff --git a/helm/software/components/ng_paramodulation/fosubst.ml b/helm/software/components/ng_paramodulation/fosubst.ml new file mode 100644 index 000000000..1b9f2624c --- /dev/null +++ b/helm/software/components/ng_paramodulation/fosubst.ml @@ -0,0 +1,39 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module Subst (B : Terms.Blob) = struct + + let id_subst = [];; + + let build_subst n t tail = (n,t) :: tail ;; + + let rec lookup_subst var subst = + match var with + | Terms.Var i -> + (try + lookup_subst (List.assoc i subst) subst + with + Not_found -> var) + | _ -> var + ;; + let lookup_subst i subst = lookup_subst (Terms.Var i) subst;; + + let is_in_subst i subst = List.mem_assoc i subst;; + + (* filter out from metasenv the variables in substs *) + let filter subst varlist = + List.filter + (fun m -> + not (is_in_subst m subst)) + varlist + ;; + +end diff --git a/helm/software/components/ng_paramodulation/fosubst.mli b/helm/software/components/ng_paramodulation/fosubst.mli new file mode 100644 index 000000000..dd7e0c2ec --- /dev/null +++ b/helm/software/components/ng_paramodulation/fosubst.mli @@ -0,0 +1,23 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +module Subst (B : Terms.Blob) : + sig + val id_subst : B.t Terms.substitution + val build_subst : + int -> B.t Terms.foterm -> B.t Terms.substitution -> + B.t Terms.substitution + val lookup_subst : + int -> B.t Terms.substitution -> B.t Terms.foterm + val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist + end diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml index 048d082c5..bcea59ad5 100644 --- a/helm/software/components/ng_paramodulation/founif.ml +++ b/helm/software/components/ng_paramodulation/founif.ml @@ -14,7 +14,7 @@ exception UnificationFailure of string Lazy.t;; module Founif (B : Terms.Blob) = struct - module Subst = Subst.Subst(B) + module Subst = Fosubst.Subst(B) module U = Terms.Utils(B) let unification vars locked_vars t1 t2 = diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index d07fba8a4..9ec7fa4cb 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -43,9 +43,11 @@ module Index(B : Terms.Blob) = struct let rec aux arity = function | Terms.Leaf a -> [Constant (a, arity)] | Terms.Var i -> assert (arity = 0); [Variable] - | Terms.Node (Terms.Var _::_) -> assert false + | Terms.Node (Terms.Var _::_) -> + (* FIXME : should this be allowed or not ? *) + assert false | Terms.Node ([] | [ _ ] ) -> assert false - | Terms.Node (Terms.Node _::_) -> assert false + | Terms.Node (Terms.Node _::_) -> assert false | Terms.Node (hd::tl) -> aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) in diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 87d081dea..e01edfae3 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -11,7 +11,7 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) -module type NCicContext = +module type NCicContext = sig val metasenv : NCic.metasenv val subst : NCic.substitution @@ -35,4 +35,17 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; + let rec embed = function + | NCic.Meta (i,_) -> Terms.Var i, [i] + | NCic.Appl l -> + let rec aux acc l = function + |[] -> acc@l + |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl + in + let res,vars = List.fold_left + (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l + in (Terms.Node (List.rev res)), vars + | t -> Terms.Leaf t, [] +;; + end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml new file mode 100644 index 000000000..3206ff7d2 --- /dev/null +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -0,0 +1,25 @@ +let nparamod metasenv subst context t = + let module C = struct + let metasenv = metasenv + let subst = subst + let context = context + end + in + let module B = NCicBlob.NCicBlob(C) in + let module Pp = Pp.Pp (B) in + let res,vars = B.embed t in + let module FU = Founif.Founif(B) in + let test_unification vars = function + | Terms.Node [_; _; lhs; rhs] -> + prerr_endline "Unification test :"; + prerr_endline (Pp.pp_foterm lhs); + prerr_endline (Pp.pp_foterm rhs); + FU.unification vars [] lhs rhs + | _ -> assert false + in + let subst,vars = test_unification vars res in + prerr_endline "Result :"; + prerr_endline (Pp.pp_foterm res); + prerr_endline "Substitution :"; + prerr_endline (Pp.pp_substitution subst) +;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli new file mode 100644 index 000000000..db112450d --- /dev/null +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -0,0 +1 @@ +val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> unit diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml deleted file mode 100644 index 1b9f2624c..000000000 --- a/helm/software/components/ng_paramodulation/subst.ml +++ /dev/null @@ -1,39 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module Subst (B : Terms.Blob) = struct - - let id_subst = [];; - - let build_subst n t tail = (n,t) :: tail ;; - - let rec lookup_subst var subst = - match var with - | Terms.Var i -> - (try - lookup_subst (List.assoc i subst) subst - with - Not_found -> var) - | _ -> var - ;; - let lookup_subst i subst = lookup_subst (Terms.Var i) subst;; - - let is_in_subst i subst = List.mem_assoc i subst;; - - (* filter out from metasenv the variables in substs *) - let filter subst varlist = - List.filter - (fun m -> - not (is_in_subst m subst)) - varlist - ;; - -end diff --git a/helm/software/components/ng_paramodulation/subst.mli b/helm/software/components/ng_paramodulation/subst.mli deleted file mode 100644 index dd7e0c2ec..000000000 --- a/helm/software/components/ng_paramodulation/subst.mli +++ /dev/null @@ -1,23 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -module Subst (B : Terms.Blob) : - sig - val id_subst : B.t Terms.substitution - val build_subst : - int -> B.t Terms.foterm -> B.t Terms.substitution -> - B.t Terms.substitution - val lookup_subst : - int -> B.t Terms.substitution -> B.t Terms.foterm - val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist - end diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 72e32987a..38e1723c2 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -64,6 +64,7 @@ module type Blob = val eq : t -> t -> bool val compare : t -> t -> int val pp : t -> string + val embed : t -> t foterm * int list end module Utils (B : Blob) = struct diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 02e3a8b66..47c2c6e40 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -62,7 +62,9 @@ module type Blob = (* TODO: consider taking in input an imperative buffer for Format * val pp : Format.formatter -> t -> unit * *) - val pp : t -> string + val pp : t -> string + + val embed : t -> t foterm * int list end module Utils (B : Blob) : diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index a0d8eba48..f9916befc 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -553,3 +553,15 @@ let assert_tac seqs status = [merge_tac]) ) status ;; + +let auto ~params status goal = + let gty = get_goalty status goal in + let n,h,metasenv,subst,o = status.pstatus in + let status,t = term_of_cic_term status gty (ctx_of gty) in + Paramod.nparamod metasenv subst (ctx_of gty) t; + status +;; + +let auto_tac ~params status = + distribute_tac (auto ~params) status +;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 3e13035eb..142300cc0 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -51,3 +51,6 @@ val letin_tac: val assert_tac: ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list -> NTacStatus.tactic + +val auto_tac: + params:'a -> NTacStatus.tactic diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends index 0a676a77c..ccbafd0cd 100644 --- a/helm/software/matita/tests/depends +++ b/helm/software/matita/tests/depends @@ -1,8 +1,8 @@ TPTP/Veloci/GRP595-1.p.ma logic/equality.ma TPTP/Veloci/GRP570-1.p.ma logic/equality.ma dependent_guarded_bove_capretta.ma nat/nat.ma -TPTP/Veloci/SYN083-1.p.ma logic/equality.ma interactive/test5.ma +TPTP/Veloci/SYN083-1.p.ma logic/equality.ma TPTP/Veloci/COL008-1.p.ma logic/equality.ma TPTP/Veloci/GRP604-1.p.ma logic/equality.ma record.ma @@ -12,8 +12,8 @@ TPTP/Veloci/COL016-1.p.ma logic/equality.ma TPTP/Veloci/GRP612-1.p.ma logic/equality.ma TPTP/Veloci/COL024-1.p.ma logic/equality.ma TPTP/Veloci/GRP139-1.p.ma logic/equality.ma -TPTP/Veloci/ROB010-1.p.ma logic/equality.ma TPTP/Veloci/BOO006-2.p.ma logic/equality.ma +TPTP/Veloci/ROB010-1.p.ma logic/equality.ma TPTP/Veloci/LCL157-1.p.ma logic/equality.ma TPTP/Veloci/LCL132-1.p.ma logic/equality.ma constructor.ma coq.ma @@ -35,8 +35,8 @@ TPTP/Veloci/COL063-3.p.ma logic/equality.ma TPTP/Veloci/LCL112-2.p.ma logic/equality.ma formal_topology.ma logic/connectives.ma TPTP/Veloci/RNG023-7.p.ma logic/equality.ma -replace.ma coq.ma test2.ma coq.ma +replace.ma coq.ma TPTP/Veloci/COL064-7.p.ma logic/equality.ma TPTP/Veloci/BOO009-2.p.ma logic/equality.ma TPTP/Veloci/GRP510-1.p.ma logic/equality.ma @@ -59,19 +59,19 @@ paramodulation/boolean_algebra.ma coq.ma TPTP/Veloci/GRP496-1.p.ma logic/equality.ma TPTP/Veloci/COL084-1.p.ma logic/equality.ma TPTP/Veloci/GRP174-1.p.ma logic/equality.ma -TPTP/Veloci/RNG011-5.p.ma logic/equality.ma TPTP/Veloci/GRP614-1.p.ma logic/equality.ma +TPTP/Veloci/RNG011-5.p.ma logic/equality.ma inversion.ma coq.ma TPTP/Veloci/GRP592-1.p.ma logic/equality.ma -TPTP/Veloci/GRP182-1.p.ma logic/equality.ma bad_tests/baseuri.ma +TPTP/Veloci/GRP182-1.p.ma logic/equality.ma TPTP/Veloci/GRP116-1.p.ma logic/equality.ma coercions.ma nat/compare.ma nat/times.ma TPTP/Veloci/GRP011-4.p.ma logic/equality.ma TPTP/Veloci/GRP149-1.p.ma logic/equality.ma TPTP/Veloci/COL013-1.p.ma logic/equality.ma -TPTP/Veloci/GRP567-1.p.ma logic/equality.ma TPTP/Veloci/COL064-2.p.ma logic/equality.ma +TPTP/Veloci/GRP567-1.p.ma logic/equality.ma comments.ma coq.ma TPTP/Veloci/COL021-1.p.ma logic/equality.ma TPTP/Veloci/BOO006-4.p.ma logic/equality.ma @@ -96,8 +96,8 @@ ng_pts.ma TPTP/Veloci/GRP545-1.p.ma logic/equality.ma TPTP/Veloci/GRP520-1.p.ma logic/equality.ma TPTP/Veloci/GRP457-1.p.ma logic/equality.ma -TPTP/Veloci/BOO009-4.p.ma logic/equality.ma TPTP/Veloci/COL064-9.p.ma logic/equality.ma +TPTP/Veloci/BOO009-4.p.ma logic/equality.ma TPTP/Veloci/LAT040-1.p.ma logic/equality.ma TPTP/Veloci/GRP578-1.p.ma logic/equality.ma change.ma coq.ma @@ -134,8 +134,8 @@ TPTP/Veloci/BOO003-4.p.ma logic/equality.ma ng_elim.ma ng_pts.ma TPTP/Veloci/GRP597-1.p.ma logic/equality.ma TPTP/Veloci/GRP572-1.p.ma logic/equality.ma -TPTP/Veloci/GRP162-1.p.ma logic/equality.ma TPTP/Veloci/GRP484-1.p.ma logic/equality.ma +TPTP/Veloci/GRP162-1.p.ma logic/equality.ma fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma TPTP/Veloci/BOO011-4.p.ma logic/equality.ma TPTP/Veloci/GRP580-1.p.ma logic/equality.ma @@ -151,27 +151,28 @@ clearbody.ma coq.ma TPTP/Veloci/LCL134-1.p.ma logic/equality.ma TPTP/Veloci/COL060-2.p.ma logic/equality.ma TPTP/Veloci/BOO016-2.p.ma logic/equality.ma -TPTP/Veloci/LAT039-2.p.ma logic/equality.ma TPTP/Veloci/GRP542-1.p.ma logic/equality.ma +TPTP/Veloci/LAT039-2.p.ma logic/equality.ma +TPTP/Veloci/GRP157-1.p.ma logic/equality.ma TPTP/Veloci/GRP186-4.p.ma logic/equality.ma TPTP/Veloci/GRP454-1.p.ma logic/equality.ma -TPTP/Veloci/GRP157-1.p.ma logic/equality.ma TPTP/Veloci/GRP509-1.p.ma logic/equality.ma TPTP/Veloci/GRP550-1.p.ma logic/equality.ma ng_commands.ma nat/nat.ma ng_pts.ma TPTP/Veloci/GRP487-1.p.ma logic/equality.ma +paratest.ma nat/plus.ma paramodulation/BOO075-1.ma TPTP/Veloci/GRP605-1.p.ma logic/equality.ma fguidi.ma logic/connectives.ma nat/nat.ma TPTP/Veloci/GRP583-1.p.ma logic/equality.ma TPTP/Veloci/GRP517-1.p.ma logic/equality.ma -TPTP/Veloci/GRP495-1.p.ma logic/equality.ma TPTP/Veloci/COL083-1.p.ma logic/equality.ma +TPTP/Veloci/GRP495-1.p.ma logic/equality.ma TPTP/Veloci/GRP173-1.p.ma logic/equality.ma coercions_propagation.ma logic/connectives.ma nat/orders.ma TPTP/Veloci/LAT045-1.p.ma logic/equality.ma -TPTP/Veloci/GRP010-4.p.ma logic/equality.ma TPTP/Veloci/GRP558-1.p.ma logic/equality.ma +TPTP/Veloci/GRP010-4.p.ma logic/equality.ma interactive/test_instance.ma TPTP/Veloci/COL012-1.p.ma logic/equality.ma TPTP/Veloci/COL063-2.p.ma logic/equality.ma @@ -183,8 +184,8 @@ bad_induction.ma logic/equality.ma nat/nat.ma TPTP/Veloci/RNG023-6.p.ma logic/equality.ma color.ma logic/equality.ma nat/nat.ma TPTP/Veloci/COL064-6.p.ma logic/equality.ma -apply2.ma nat/nat.ma metasenv_ordering.ma coq.ma +apply2.ma nat/nat.ma TPTP/Veloci/GRP608-1.p.ma logic/equality.ma TPTP/Veloci/BOO010-2.p.ma logic/equality.ma TPTP/Veloci/LCL153-1.p.ma logic/equality.ma @@ -211,8 +212,8 @@ TPTP/Veloci/GRP577-1.p.ma logic/equality.ma TPTP/Veloci/GRP552-1.p.ma logic/equality.ma TPTP/Veloci/BOO013-2.p.ma logic/equality.ma rewrite.ma coq.ma -TPTP/Veloci/GRP497-1.p.ma logic/equality.ma bad_tests/auto.ma coq.ma +TPTP/Veloci/GRP497-1.p.ma logic/equality.ma diabolic_fix.ma nat/nat.ma TPTP/Veloci/GRP001-2.p.ma logic/equality.ma test4.ma coq.ma @@ -221,10 +222,10 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma TPTP/Veloci/GRP514-1.p.ma logic/equality.ma TPTP/Veloci/LCL139-1.p.ma logic/equality.ma TPTP/Veloci/GRP547-1.p.ma logic/equality.ma +TPTP/Veloci/COL004-3.p.ma logic/equality.ma TPTP/Veloci/GRP459-1.p.ma logic/equality.ma TPTP/Veloci/BOO069-1.p.ma logic/equality.ma TPTP/Veloci/GRP137-1.p.ma logic/equality.ma -TPTP/Veloci/COL004-3.p.ma logic/equality.ma TPTP/Veloci/GRP188-2.p.ma logic/equality.ma apply.ma coq.ma TPTP/Veloci/GRP467-1.p.ma logic/equality.ma @@ -232,7 +233,6 @@ TPTP/Veloci/GRP145-1.p.ma logic/equality.ma TPTP/Veloci/COL063-4.p.ma logic/equality.ma TPTP/Veloci/LCL155-1.p.ma logic/equality.ma TPTP/Veloci/GRP588-1.p.ma logic/equality.ma -lara.ma nat/nat.ma TPTP/Veloci/GRP153-1.p.ma logic/equality.ma paramodulation.ma coq.ma TPTP/Veloci/GRP596-1.p.ma logic/equality.ma @@ -240,8 +240,8 @@ coercions_nonuniform.ma TPTP/Veloci/GRP161-1.p.ma logic/equality.ma TPTP/Veloci/COL064-8.p.ma logic/equality.ma TPTP/Veloci/LDA001-1.p.ma logic/equality.ma -TPTP/Veloci/COL050-1.p.ma logic/equality.ma TPTP/Veloci/BOO010-4.p.ma logic/equality.ma +TPTP/Veloci/COL050-1.p.ma logic/equality.ma TPTP/Veloci/LCL110-2.p.ma logic/equality.ma TPTP/Veloci/GRP491-1.p.ma logic/equality.ma TPTP/Veloci/COL061-3.p.ma logic/equality.ma @@ -250,9 +250,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma compose.ma logic/equality.ma TPTP/Veloci/COL025-1.p.ma logic/equality.ma TPTP/Veloci/GRP115-1.p.ma logic/equality.ma -hard_refine.ma coq.ma letrecand.ma nat/nat.ma unifhint.ma list/list.ma nat/nat.ma nat/plus.ma +hard_refine.ma coq.ma paramodulation/group.ma coq.ma TPTP/Veloci/LCL158-1.p.ma logic/equality.ma TPTP/Veloci/LCL133-1.p.ma logic/equality.ma @@ -263,11 +263,11 @@ TPTP/Veloci/GRP156-1.p.ma logic/equality.ma mysql_escaping.ma TPTP/Veloci/LCL141-1.p.ma logic/equality.ma TPTP/Veloci/GRP182-2.p.ma logic/equality.ma -TPTP/Veloci/LDA007-3.p.ma logic/equality.ma interactive/drop.ma interactive/test6.ma TPTP/Veloci/GRP599-1.p.ma logic/equality.ma TPTP/Veloci/GRP574-1.p.ma logic/equality.ma +TPTP/Veloci/LDA007-3.p.ma logic/equality.ma unfold.ma coq.ma TPTP/Veloci/GRP486-1.p.ma logic/equality.ma TPTP/Veloci/GRP189-1.p.ma logic/equality.ma @@ -292,8 +292,8 @@ TPTP/Veloci/COL062-2.p.ma logic/equality.ma match_inference.ma simpl.ma coq.ma unifhint_simple.ma logic/equality.ma -TPTP/Veloci/GRP142-1.p.ma logic/equality.ma TPTP/Veloci/COL063-6.p.ma logic/equality.ma +TPTP/Veloci/GRP142-1.p.ma logic/equality.ma third.ma first.ma second.ma TPTP/Veloci/GRP560-1.p.ma logic/equality.ma TPTP/Veloci/GRP150-1.p.ma logic/equality.ma @@ -307,8 +307,8 @@ coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma li TPTP/Veloci/GRP117-1.p.ma logic/equality.ma multiple_inheritance.ma logic/equality.ma test3.ma coq.ma -TPTP/Veloci/GRP168-2.p.ma logic/equality.ma TPTP/Veloci/ROB013-1.p.ma logic/equality.ma +TPTP/Veloci/GRP168-2.p.ma logic/equality.ma TPTP/Veloci/GRP012-4.p.ma logic/equality.ma naiveparamod.ma logic/equality.ma TPTP/Veloci/GRP176-2.p.ma logic/equality.ma @@ -336,7 +336,7 @@ TPTP/Veloci/GRP136-1.p.ma logic/equality.ma TPTP/Veloci/GRP458-1.p.ma logic/equality.ma coercions_open.ma logic/equality.ma nat/nat.ma paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma -ng_uris_and_notation.ma nat/nat.ma +ng_uris_and_notation.ma nat/nat.ma ng_pts.ma TPTP/Veloci/GRP144-1.p.ma logic/equality.ma TPTP/Veloci/BOO018-4.p.ma logic/equality.ma TPTP/Veloci/LAT008-1.p.ma logic/equality.ma diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma new file mode 100644 index 000000000..4e8747297 --- /dev/null +++ b/helm/software/matita/tests/paratest.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "nat/plus.ma". + +ntheorem foo: \forall x, y. ((λz. x + x = z + z) ?). +##[ #x; #y; nnormalize; nauto. \ No newline at end of file