PT.Appl (mk_ident name :: List.map convert_term args)
;;
-let rec atom_of_formula = function
- | A.Disjunction (a,b) ->
- atom_of_formula a @ atom_of_formula b
- | A.NegAtom a -> [a] (* removes the negation *)
- | A.Atom a -> [a]
+let rec atom_of_formula neg pos = function
+ | A.Disjunction (a,b) ->
+ let neg, pos = atom_of_formula neg pos a in
+ atom_of_formula neg pos b
+ | A.NegAtom a -> a::neg, pos
+ | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
+ | A.Atom a -> neg, a::pos
+;;
+
+let atom_of_formula f =
+ let neg, pos = atom_of_formula [] [] f in
+ neg @ pos
;;
let rec mk_arrow component tail = function
else [])@
[GA.Executable(floc,GA.Tactic(floc, Some (
if ueq_case then
- GA.Auto (floc,["paramodulation","";
- "timeout",string_of_int !paramod_timeout])
+ GA.AutoBatch (floc,([],["paramodulation","";
+ "timeout",string_of_int !paramod_timeout]))
else
- GA.Auto (floc,["depth",string_of_int !depth])
+ GA.AutoBatch (floc,([],[
+ "depth",string_of_int 5;
+ "width",string_of_int 5;
+ "size",string_of_int 20;
+ "timeout",string_of_int 10;
+ ]))
),
- GA.Dot(floc)));
+ GA.Semicolon(floc)));
GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
GA.Assumption floc)), GA.Dot(floc)))
]@
let pres_term = TermContentPres.pp_ast content_term in
let dummy_tbl = Hashtbl.create 1 in
let markup = CicNotationPres.render dummy_tbl pres_term in
- let s = BoxPp.render_to_string List.hd width markup in
+ let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
Pcre.substitute
~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
in
CicNotationPp.set_pp_term term_pp;
let lazy_term_pp = fun x -> assert false in
let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
- GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+ GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t
in
let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
let extra_statements_start = [
match raw_preamble with
| None ->
pp (GA.Executable(floc,
- GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
+ GA.Command(floc,GA.Include(floc,false,"logic/equality.ma"))))
| Some s -> s buri
in
let extra_statements_end = [] in