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
GA.AutoBatch (floc,([],["paramodulation","";
"timeout",string_of_int !paramod_timeout]))
else
- GA.AutoBatch (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.Semicolon(floc)));
GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
let width = max_int in
let term_pp content_term =
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 lookup_uri = fun _ -> None in
+ let markup = CicNotationPres.render ~lookup_uri pres_term 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
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