X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftptp2grafite%2Fmain.ml;h=4a57812432a6c4ead7ee46c66fe5aaf5eb96f989;hb=63349b091357ba4cf3b9924bd1ffecd543f37252;hp=315bfc1006b94175f94a94f0af3e8ac85dd8d9f4;hpb=5d8d504eb46d181d7a915b2be154022ea83da4df;p=helm.git diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml index 315bfc100..4a5781243 100644 --- a/components/binaries/tptp2grafite/main.ml +++ b/components/binaries/tptp2grafite/main.ml @@ -12,12 +12,11 @@ let mk_ident s = PT.Ident ((try List.assoc s kw with Not_found -> s),None) ;; - let rec collect_arities_from_term = function | A.Constant name -> [name,0] | A.Variable name -> [] | A.Function (name,l) -> - (name,List.length l) :: List.flatten (List.map collect_arities_from_term l) + (name,List.length l)::List.flatten (List.map collect_arities_from_term l) ;; let rec collect_fv_from_term = function @@ -79,19 +78,20 @@ let rec mk_arrow component = function mk_arrow component (n-1)) ;; -let build_ctx_for_arities arities t = +let build_ctx_for_arities univesally arities t = + let binder = if univesally then `Forall else `Exists in let rec aux = function | [] -> t | (name,nargs)::tl -> PT.Binder - (`Forall, + (binder, (mk_ident name,Some (mk_arrow "A" nargs)), aux tl) in aux arities ;; -let convert_atom a = +let convert_atom universally a = let aux = function | A.Proposition _ -> assert false | A.Predicate (name,params) -> @@ -99,11 +99,12 @@ let convert_atom a = assert false | A.True -> mk_ident "True" | A.False -> mk_ident "False" - | A.Eq (l,r) + | A.Eq (l,r) | A.NotEq (l,r) -> (* removes the negation *) PT.Appl [mk_ident "eq";mk_ident "A";convert_term l;convert_term r] in - build_ctx_for_arities (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a) + build_ctx_for_arities universally + (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a) ;; let collect_arities atom ctx = @@ -112,20 +113,40 @@ let collect_arities atom ctx = (List.flatten (List.map collect_arities_from_atom atoms))) ;; -let rec convert_formula no_arities context f = +let assert_formulae_is_1eq_negated f = + let atom = atom_of_formula f in + match atom with + | A.Eq (l,r) -> failwith "Negated formula is not negated" + | A.NotEq (l,r) -> () + | _ -> failwith "Not a unit equality formula" +;; + +let rec convert_formula fv no_arities context f = let atom = atom_of_formula f in - let t = convert_atom atom in + let t = convert_atom (fv = []) atom in let rec build_ctx n = function | [] -> t | hp::tl -> PT.Binder (`Forall, (mk_ident ("H" ^ string_of_int n), - Some (convert_formula true [] hp)), + Some (convert_formula [] true [] hp)), build_ctx (n+1) tl) in let arities = if no_arities then [] else collect_arities atom context in - build_ctx_for_arities arities (build_ctx 0 context) + build_ctx_for_arities true arities (build_ctx 0 context) +;; + +let check_if_atom_is_negative = function + | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false + | A.Eq _ -> false + | A.NotEq _ -> true +;; + +let check_if_formula_is_negative = function + | A.Disjunction _ -> assert false + | A.NegAtom a -> not (check_if_atom_is_negative a) + | A.Atom a -> check_if_atom_is_negative a ;; let convert_ast statements context = function @@ -149,23 +170,47 @@ let convert_ast statements context = function | A.Axiom | A.Hypothesis -> statements, f::context + | A.Negated_conjecture when not (check_if_formula_is_negative f) -> + statements, f::context | A.Negated_conjecture -> - if collect_fv_from_formulae f <> [] then - (*prerr_endline "CONTIENE FV";*)(); + assert_formulae_is_1eq_negated f; + let fv = collect_fv_from_formulae f in + if fv <> [] then + prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv); let f = PT.Binder (`Forall, (mk_ident "A",Some (PT.Sort `Set)), - convert_formula false context f) + convert_formula fv false context f) in let o = PT.Theorem (`Theorem,name,f,None) in statements @ [ GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o))); GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Intros (floc,None,[])),Some (GA.Dot(floc)))); - GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, + GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @ + (if fv <> [] then + (List.flatten + (List.map + (fun _ -> + [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, + GA.Exists floc),Some (GA.Branch floc))); + GA.Executable(floc,GA.Tactical(floc, GA.Pos (floc,2),None))]) + fv)) + else [])@ + [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, GA.Auto (floc,None,None,Some "paramodulation",None)), - Some (GA.Dot(floc)))); + Some (GA.Dot(floc))))]@ + (if fv <> [] then + (List.flatten + (List.map + (fun _ -> + [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None)); + GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some + (GA.Merge floc)))]) + fv)) + else [])@ + [GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, + GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))); GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))], context | A.Definition