Skip to content

Commit

Permalink
Merge pull request #155 from glondu/cmdliner-translate
Browse files Browse the repository at this point in the history 
Use cmdliner in translate
  • Loading branch information
@kape1395
kape1395 authored Sep 18, 2024
2 parents d8ade9a + c46c2e6 commit ffb8846
Show file tree
Hide file tree
Showing 4 changed files with 116 additions and 121 deletions.
20 changes: 0 additions & 20 deletions .merlin
View file

This file was deleted.

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
71 changes: 35 additions & 36 deletions translate/fofunctions.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -618,9 +618,8 @@ let rename proposition formula =
(* DSNF TRANSFORMATIONS *)
(******************************************************************)

(* this reference controls how fo formulas are processed: if false,
then by de Morgan laws, by renaming else*)
let useFOrenaming = ref false;;
(* the useFOrenaming argument controls how fo formulas are processed:
if false, then by de Morgan laws, by renaming else*)

(*
(* Transformation to CNF by renaming *)
Expand Down Expand Up @@ -675,13 +674,13 @@ let fodsnfselect form =
(* iP uP sP eP *)
(* *)
(* ASSUME that formula is in NNF *)
let rec dsnfWrap form =
let rec dsnfWrap ~useFOrenaming form =
debug ("dsnfWrap input: " ^ (string_of_formula form));
match form with
| f when (isTemporalFree f) -> (f, [], [], [])
| And(x,y) ->
let (iP1, uP1,sP1,eP1) = dsnfWrap x
and (iP2, uP2,sP2,eP2) = dsnfWrap y
let (iP1, uP1,sP1,eP1) = dsnfWrap ~useFOrenaming x
and (iP2, uP2,sP2,eP2) = dsnfWrap ~useFOrenaming y
in (And(iP1, iP2), union uP1 uP2, union sP1 sP2, union eP1 eP2)
| Always (f) when (isTemporalFree f) ->
(True, [f], [], [])
Expand All @@ -695,9 +694,9 @@ let rec dsnfWrap form =
(True, [], [Always(Or(lhs,rhs))], [])

(* else use the standard transformations *)
| _ -> dsnf form
| _ -> dsnf ~useFOrenaming form

and dsnf form =
and dsnf ~useFOrenaming form =
debug ("dsnf input: " ^ (string_of_formula form));
(* if isTemporalFree form *)
(* then fodsnfselect form *)
Expand All @@ -712,26 +711,26 @@ and dsnf form =
match form with
(* booleans go first *)
| Not x ->
let (iP,uP,sP,eP) = dsnf x
let (iP,uP,sP,eP) = dsnf ~useFOrenaming x
in (Not(iP), uP,sP,eP)
| And(x,y) ->
let (iP1, uP1,sP1,eP1) = dsnf x
and (iP2, uP2,sP2,eP2) = dsnf y
let (iP1, uP1,sP1,eP1) = dsnf ~useFOrenaming x
and (iP2, uP2,sP2,eP2) = dsnf ~useFOrenaming y
in (And(iP1, iP2), union uP1 uP2, union sP1 sP2, union eP1 eP2)
(* | Or(x,y) ->
let (iP1, uP1,sP1,eP1) = dsnf x
and (iP2, uP2,sP2,eP2) = dsnf y
let (iP1, uP1,sP1,eP1) = dsnf ~useFOrenaming x
and (iP2, uP2,sP2,eP2) = dsnf ~useFOrenaming y
in (Or(iP1, iP2), union uP1 uP2, union sP1 sP2, union eP1 eP2)*)
| Or(f, g) when ((not !useFOrenaming) || (isLiteral f) || (isLiteral g)) ->
let (iP1, uP1, sP1, eP1) = dsnf f
and (iP2, uP2, sP2, eP2) = dsnf g
| Or(f, g) when ((not useFOrenaming) || (isLiteral f) || (isLiteral g)) ->
let (iP1, uP1, sP1, eP1) = dsnf ~useFOrenaming f
and (iP2, uP2, sP2, eP2) = dsnf ~useFOrenaming g
in
(Or(iP1, iP2), (union uP1 uP2), (union sP1 sP2), (union eP1 eP2))
| Or(f, g) when (!useFOrenaming) (* both are non-litarls & useFOrenaming *) ->
| Or(f, g) when (useFOrenaming) (* both are non-litarls & useFOrenaming *) ->
let newP = newLiteral (freeVars f)
and (iP1, uP1, sP1, eP1) = dsnf f
and (iP1, uP1, sP1, eP1) = dsnf ~useFOrenaming f
in setSeen iP1 newP ;
let (iP2, uP2, sP2, eP2) = dsnf g
let (iP2, uP2, sP2, eP2) = dsnf ~useFOrenaming g
in
(Or(newP, iP2),
(rename newP iP1)::(union uP1 uP2), (union sP1 sP2), (union eP1 eP2))
Expand All @@ -742,15 +741,15 @@ and dsnf form =
in (Implies(iP1, iP2), union uP1 uP2, union sP1 sP2, union eP1 eP2)*)
(* Quantifiers *)
| Forall(v,y) ->
let (iP,uP,sP,eP) = dsnf y
let (iP,uP,sP,eP) = dsnf ~useFOrenaming y
in (Forall(v, iP), uP,sP,eP)
| Exists(v,y) ->
let (iP,uP,sP,eP) = dsnf y
let (iP,uP,sP,eP) = dsnf ~useFOrenaming y
in (Exists(v, iP), uP,sP,eP)
(* Temporal operators *)
| Always(f) ->
let newP = newLiteral (freeVars f)
and (iP,uP,sP,eP) = dsnf f
and (iP,uP,sP,eP) = dsnf ~useFOrenaming f
in setSeen (Always(f)) newP ;
(newP,
(rename newP iP)::uP,
Expand All @@ -764,7 +763,7 @@ and dsnf form =
if (isLiteral f) then f
else (newLiteral (freeVars f))
)
and (iP,uP,sP,eP) = dsnf f
and (iP,uP,sP,eP) = dsnf ~useFOrenaming f
in setSeen (Next (f)) newP ;
(newP,
(if (isLiteral f) then uP else
Expand All @@ -775,7 +774,7 @@ and dsnf form =
| Sometime(f) ->
let newP = newLiteral (freeVars f)
and newQ = newLiteral (freeVars f)
and (iP,uP,sP,eP) = dsnf f
and (iP,uP,sP,eP) = dsnf ~useFOrenaming f
in setSeen (Sometime(f)) newP ;
(newP,
(rename newQ iP)::uP,
Expand All @@ -786,24 +785,24 @@ and dsnf form =
if not (isLiteral f)
then
let newP = newLiteral (freeVars (Until(f,g)))
in let (iP,uP,sP,eP) = dsnf (Until(newP, g))
and (iP2,uP2,sP2,eP2) = dsnf (f)
in let (iP,uP,sP,eP) = dsnf ~useFOrenaming (Until(newP, g))
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming (f)
in (iP,
(rename newP iP2)::(uP@uP2),
sP@sP2, eP@eP2)
else if not (isLiteral g)
then
let newQ = newLiteral (freeVars (Until(f,g)))
in let (iP,uP,sP,eP) = dsnf (Until(f, newQ))
and (iP2,uP2,sP2,eP2) = dsnf (g)
in let (iP,uP,sP,eP) = dsnf ~useFOrenaming (Until(f, newQ))
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming (g)
in (iP,
(rename newQ iP2)::(uP@uP2),
sP@sP2, eP@eP2)
else (* Both f and g are atoms *)
let newP = newLiteral (freeVars (Until(f,g)))
and newQ = newLiteral (freeVars (Until(f,g)))
and (iP1,uP1,sP1,eP1) = dsnf f
and (iP2,uP2,sP2,eP2) = dsnf g
and (iP1,uP1,sP1,eP1) = dsnf ~useFOrenaming f
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming g
in setSeen (Until(f,g)) newP ;
(newP,
(
Expand All @@ -820,24 +819,24 @@ and dsnf form =
if not (isLiteral f)
then
let newP = newLiteral (freeVars (Unless(f,g)))
in let (iP,uP,sP,eP) = dsnf (Unless(newP, g))
and (iP2,uP2,sP2,eP2) = dsnf (f)
in let (iP,uP,sP,eP) = dsnf ~useFOrenaming (Unless(newP, g))
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming (f)
in (iP,
(rename newP iP2)::(uP@uP2),
sP@sP2,eP@eP2)
else if not (isLiteral g)
then
let newQ = newLiteral (freeVars (Unless(f,g)))
in let (iP,uP,sP,eP) = dsnf (Unless(f, newQ))
and (iP2,uP2,sP2,eP2) = dsnf (g)
in let (iP,uP,sP,eP) = dsnf ~useFOrenaming (Unless(f, newQ))
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming (g)
in (iP,
(rename newQ iP2)::(uP@uP2),
sP@sP2,eP@eP2)
else (* Both f and g are atoms *)
let newP = newLiteral (freeVars (Unless(f,g)))
and newQ = newLiteral (freeVars (Unless(f,g)))
and (iP1,uP1,sP1,eP1) = dsnf f
and (iP2,uP2,sP2,eP2) = dsnf g
and (iP1,uP1,sP1,eP1) = dsnf ~useFOrenaming f
and (iP2,uP2,sP2,eP2) = dsnf ~useFOrenaming g
in setSeen (Unless(f,g)) newP ;
(newP,
(
Expand Down
145 changes: 80 additions & 65 deletions translate/main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,94 +5,75 @@ open Fotypes;;
open Fofunctions;;


let verbose = ref false;;
let useSimplification = ref false;;
let filename = ref "";;
let inx = ref stdin;;
let outx = ref stdout;;
let fo = ref false;;
let atoms = 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) );*)
if ( (String.sub ( Filename.basename Sys.argv.(0)) 0 2 ) = "fo") then fo:=true;
Arg.parse args_spec anonfun usage_spec ;
let lexbuf = Lexing.from_channel !inx in
let fo = String.starts_with ~prefix:"fo" (Filename.basename Sys.argv.(0)) 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 (iP,uP,sP,eP) = dsnfWrap 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
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
end;
(* Skolemization *)
let skolemisedIP = eliminateQ iP
and skolemisedUP = eliminateQl uP
and skolemisedSP = eliminateQl sP
and skolemisedEP = if !fo then (eliminateQl (flood eP constList)) else (eliminateQl eP)
and skolemisedEP = if fo then (eliminateQl (flood eP constList)) else (eliminateQl eP)
in
(* FO transformations *)
let processedIP = if !fo then (processFOconstants skolemisedIP) else skolemisedIP
and processedUP = if !fo then (processFOconstantsl skolemisedUP) else skolemisedUP
and processedSP = if !fo then (foStepClauses skolemisedSP) else skolemisedSP
and processedEP = if !fo then (processFOconstantsl skolemisedEP) else skolemisedEP
let processedIP = if fo then (processFOconstants skolemisedIP) else skolemisedIP
and processedUP = if fo then (processFOconstantsl skolemisedUP) else skolemisedUP
and processedSP = if fo then (foStepClauses skolemisedSP) else skolemisedSP
and processedEP = if fo then (processFOconstantsl skolemisedEP) else skolemisedEP
in
(**)
let cnfedIP = cnf processedIP
Expand Down Expand Up @@ -126,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 ffb8846

Please sign in to comment.