Skip to content

Commit

Permalink
Use cmdliner in translate
Browse files Browse the repository at this point in the history 
Signed-off-by: Stephane Glondu <[email protected]>
  • Loading branch information
Stephane Glondu committed Sep 17, 2024
1 parent 87917c0 commit c46c2e6
Show file tree
Hide file tree
Showing 2 changed files with 74 additions and 59 deletions.
1 change: 1 addition & 0 deletions translate/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
(executable
(name main)
(public_name translate)
(libraries cmdliner)
(modules_without_implementation fotypes))

(install ; It has to be installed under 2 names for some reason.
Expand Down
132 changes: 73 additions & 59 deletions translate/main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,83 +5,63 @@ open Fotypes;;
open Fofunctions;;


let verbose = ref false;;
let useSimplification = ref false;;
let filename = ref "";;
let inx = ref stdin;;
let outx = ref stdout;;
let atoms = ref false;;
let useFOrenaming = ref false;;

(*let resetVerbose = verbose := false;;*)

let setInFilename name = inx := open_in name;;
let setOutFilename name = outx := open_out name;;

let args_spec = ("-v", Arg.Set verbose, "Be verbose (print intermediate transformations).")::
("-s", Arg.Set useSimplification, "Use simplifications.")::
("-r", Arg.Set useFOrenaming, "Transform to CNF by renaming")::
(*("-fo", Arg.Set fo, "Perform transformation for FO (expanding domains).")::*)
("-al", Arg.Set atoms, "Include the 'order' statement with the list of all atoms in the input formula (experimental feature).")::
("-i", Arg.String setInFilename,
"Specify the input file. If not given, stdin is used.")::
("-o", Arg.String setOutFilename,
"Specify the output file. If not given, stdout is used.")::
[];;

let usage_spec = "Usage: translate [-v] [-s] [-i infile] [-o outfile]";;

let anonfun astring = Arg.usage args_spec usage_spec; exit 0;;

(* main function *)
let _ =
let main verbose useSimplification useFOrenaming atoms inFilename outFilename =
try
(*print_string ( Filename.basename Sys.argv.(0) );*)
let fo = String.starts_with ~prefix:"fo" (Filename.basename Sys.argv.(0)) in
Arg.parse args_spec anonfun usage_spec ;
let lexbuf = Lexing.from_channel !inx in
let inx =
match inFilename with
| None -> stdin
| Some name -> open_in name
in
let outx =
match outFilename with
| None -> stdout
| Some name -> open_out name
in
let lexbuf = Lexing.from_channel inx in
let result = Foyacc.start Folex.lexer lexbuf in
let constList = constsOf result in
if !atoms=true then begin
if atoms then begin
let atomList = getAtoms result in
output_string !outx ("order(" ^ (string_of_clause atomList) ^ ").\n");
output_string outx ("order(" ^ (string_of_clause atomList) ^ ").\n");
end;
if !verbose=true then begin
output_string !outx ("Input: " ^ string_of_formula result^"\n");
flush !outx
if verbose then begin
output_string outx ("Input: " ^ string_of_formula result^"\n");
flush outx
end;
let inNNF = nnf result in
if !verbose then begin
output_string !outx "In NNF: ";
output_string !outx (string_of_formula inNNF^"\n");
if verbose then begin
output_string outx "In NNF: ";
output_string outx (string_of_formula inNNF^"\n");
debug("DONE");
flush !outx;
flush outx;
debug("DONE");
end;
debug("done ");
let simplified =
if !useSimplification then
simplify inNNF !outx !verbose
if useSimplification then
simplify inNNF outx verbose
else inNNF
in
if !verbose then begin
output_string !outx "After all simplifications:\n";
output_string !outx (string_of_formula simplified^"\n");
flush !outx
if verbose then begin
output_string outx "After all simplifications:\n";
output_string outx (string_of_formula simplified^"\n");
flush outx
end;
let useFOrenaming = !useFOrenaming in
let (iP,uP,sP,eP) = dsnfWrap ~useFOrenaming simplified in
if !verbose then begin
output_string !outx "After transformations, the DSNF is\n";
output_string !outx "iP = {\n";
output_string !outx ((string_of_formula iP)^"\n}\n");
output_string !outx "uP = {\n";
output_string !outx ((string_of_formulas uP)^"\n}\n");
output_string !outx "sP = {\n";
output_string !outx ((string_of_formulas sP)^"\n}\n");
output_string !outx "eP = {\n";
output_string !outx ((string_of_formulas eP)^"\n}\n");
flush !outx
if verbose then begin
output_string outx "After transformations, the DSNF is\n";
output_string outx "iP = {\n";
output_string outx ((string_of_formula iP)^"\n}\n");
output_string outx "uP = {\n";
output_string outx ((string_of_formulas uP)^"\n}\n");
output_string outx "sP = {\n";
output_string outx ((string_of_formulas sP)^"\n}\n");
output_string outx "eP = {\n";
output_string outx ((string_of_formulas eP)^"\n}\n");
flush outx
end;
(* Skolemization *)
let skolemisedIP = eliminateQ iP
Expand Down Expand Up @@ -127,8 +107,42 @@ let _ =
(* Collect strings *)
let resultStr = preamble^icstring^ucstring^scstring^ecstring^ending^"\n" in
(*print_string (string_of_clause (!newNamesList));*)
output_string !outx (resultStr); if !outx != stdout then close_out !outx
output_string outx (resultStr); if outx != stdout then close_out outx
with Parsing.Parse_error -> print_endline ("Parse error line " ^
string_of_int (!Folex.currentLine) ^ " characters " ^
string_of_int (!Folex.posmin) ^ "-" ^ string_of_int (!Folex.posmax))
| Sys_error astring -> print_endline (astring);;

open Cmdliner

let verbose =
let doc = "Be verbose (print intermediate transformations)." in
Arg.(value & flag & info ["v"] ~doc)

let useSimplification =
let doc = "Use simplifications." in
Arg.(value & flag & info ["s"] ~doc)

let useFOrenaming =
let doc = "Transform to CNF by renaming." in
Arg.(value & flag & info ["r"] ~doc)

let atoms =
let doc = "Include the 'order' statement with the list of all atoms in the input formula (experimental feature)." in
Arg.(value & flag & info ["al"] ~doc)

let inFilename =
let doc = "Specify the input file. If not given, stdin is used." in
Arg.(value & opt (some file) None & info ["i"] ~doc)

let outFilename =
let doc = "Specify the output file. If not given, stdout is used." in
Arg.(value & opt (some string) None & info ["o"] ~doc)

let main_t = Term.(const main $ verbose $ useSimplification $ useFOrenaming $ atoms $ inFilename $ outFilename)

let cmd =
let info = Cmd.info "translate" in
Cmd.v info main_t

let () = exit (Cmd.eval cmd)

0 comments on commit c46c2e6

Please sign in to comment.