From 9eaaa02d2368fc86348ce61376f39e1aaea27d9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= <feree@irif.fr>
Date: Fri, 28 Jun 2024 17:19:06 +0200
Subject: [PATCH] Add cmdline tool back

---
 bin/dune                              |  9 ++--
 bin/printer.ml                        | 30 ++++++++++++
 bin/uiml_cmdline.ml                   | 69 +++++++++++++++++++++++++++
 bin/uiml_demo.ml                      | 24 +---------
 dune-project                          |  2 +-
 theories/extraction/UIML_extraction.v |  3 +-
 6 files changed, 109 insertions(+), 28 deletions(-)
 create mode 100644 bin/printer.ml
 create mode 100644 bin/uiml_cmdline.ml

diff --git a/bin/dune b/bin/dune
index 157f8cd..4952ca8 100644
--- a/bin/dune
+++ b/bin/dune
@@ -1,6 +1,9 @@
 (executables
- (public_names uiml_demo benchmark)
- (names uiml_demo benchmark)
+ (public_names uiml_demo benchmark uiml_cmdline)
+ (names uiml_demo benchmark uiml_cmdline)
  (modes js native)
  (preprocess (pps js_of_ocaml-ppx))
- (libraries js_of_ocaml UIML angstrom))
+ (libraries js_of_ocaml UIML angstrom exenum)
+)
+
+
diff --git a/bin/printer.ml b/bin/printer.ml
new file mode 100644
index 0000000..bdfd66c
--- /dev/null
+++ b/bin/printer.ml
@@ -0,0 +1,30 @@
+open UIML.Formulas
+open Stringconversion
+open UIML.Datatypes
+
+let rec int_of_nat = function
+| O -> 0
+| S n -> 1 + int_of_nat n
+
+
+let string_of_formula ?(classical = false) =
+  let rec string_of_formula =
+  function
+| Var v -> camlstring_of_coqstring v
+| Bot -> "⊥"
+| Implies(Bot, Bot) -> "⊤"
+(* diamond *)
+| Implies(Box(Implies(f, Bot)),Bot) when classical -> "⋄ " ^ bracket f
+(* double negation *)
+| Implies(Implies(f, Bot), Bot) when classical -> string_of_formula f
+| Box f -> "□ " ^ bracket f
+| And (f, g) -> bracket f ^ " ∧ " ^ bracket g
+| Or (f, g) -> bracket f ^ " ∨ " ^ bracket g
+| Implies (f, Bot) -> "¬ " ^ bracket f (* pretty print ¬ *)
+| Implies (f, g) -> bracket f ^ " → " ^ bracket g
+and bracket e = match e with
+| Implies(Implies(f, Bot), Bot) when classical -> bracket f
+| Implies(Box(Implies(f, Bot)),Bot) when classical -> "⋄ " ^ bracket f
+| Var _ | Bot | Implies(_, Bot) | Box _ -> string_of_formula e
+| e -> "(" ^ string_of_formula e ^ ")"
+  in string_of_formula
\ No newline at end of file
diff --git a/bin/uiml_cmdline.ml b/bin/uiml_cmdline.ml
new file mode 100644
index 0000000..c65ab88
--- /dev/null
+++ b/bin/uiml_cmdline.ml
@@ -0,0 +1,69 @@
+open ExEnum
+open Printer
+open UIML.Formulas
+open Sys
+open Char
+open UIML.UIML_extraction
+open Stringconversion
+
+
+
+(* n first variables *)
+let rec n_vars n = if n <= 1 then [['p']] else [Char.chr ((Char.code 'p') + n)] :: n_vars (n - 1)
+
+let e_vars = from_list ~name:"variables" (n_vars 4)
+
+(* Type term is recursive, hence we need a lazy enumeration first. *)
+let rec l_e_formulas = lazy
+    begin
+      let r_formulas = pay l_e_formulas in
+      union
+	[ single Bot ;
+    map e_vars (fun x -> Var x) ;
+	  map (pair r_formulas r_formulas) (fun (t1, t2) -> And (t1, t2)) ;
+    map (pair r_formulas r_formulas) (fun (t1, t2) -> Or (t1, t2)) ;
+    map (pair r_formulas r_formulas) (fun (t1, t2) -> Implies (t1, t2)) ;
+    map r_formulas (fun x -> Box x);
+	]
+    end
+
+
+(* Enumeration for formulas. *)
+let e_formulas = Lazy.force l_e_formulas
+
+(* The code below prints _num_ formulas and their existential interpolant *)
+
+let nb_args = Array.length Sys.argv
+
+let start = if nb_args < 2 then 0 else int_of_string Sys.argv.(1)
+let num = if nb_args < 3 then 1 else int_of_string Sys.argv.(2)
+
+let usage_string =
+"Usage: propquant s n shows n example formulas φ(0), ... φ(n-1),
+        and computes E x0 φ(i) and A x0 φ(i) for each 0 ≤ i < n.
+        The formulas are chosen from an enumeration of all formulas in variables p, q, r, s, t.
+        The argument s determines where to start in this enumeration.
+
+        For example, try: propquant.exe 0 10, propquant.exe 5893 100.\n"
+
+let v : variable = coqstring_of_camlstring "p"
+
+let show_test (f: form) : string =
+    ("φ        : " ^ string_of_formula f ^ "\n" ^
+                 "Weight: " ^ string_of_int (int_of_nat (weight f)) ^ "\n") ^
+    let t_start = Sys.time() in
+    let e_result = isl_E v f in
+    let run_time = Sys.time() -. t_start in
+    ("Time: " ^ string_of_float run_time ^ "s\n") ^
+    ("Eₚ(φ): " ^
+                  string_of_formula e_result ^ "\n" ^
+                 "Weight: " ^ string_of_int (int_of_nat (weight e_result)) ^ "\n") ^
+    let a_result = isl_A v f in
+    ("Aₚ(φ): " ^
+                 string_of_formula a_result ^ "\n" ^
+                "Weight: " ^ string_of_int (int_of_nat (weight a_result)) ^ "\n-------------------\n")
+
+let () = 
+  if nb_args < 2 then (print_string usage_string)
+  else
+    show e_formulas show_test start num;
diff --git a/bin/uiml_demo.ml b/bin/uiml_demo.ml
index 119ab38..b43c020 100644
--- a/bin/uiml_demo.ml
+++ b/bin/uiml_demo.ml
@@ -1,31 +1,9 @@
 open UIML.UIML_extraction
-open UIML.Datatypes
 open UIML.Formulas
 open Js_of_ocaml
 open Modal_expressions_parser
 open Stringconversion
-
-let string_of_formula ?(classical = false) =
-  let rec string_of_formula =
-  function
-| Var v -> camlstring_of_coqstring v
-| Bot -> "⊥"
-| Implies(Bot, Bot) -> "⊤"
-(* diamond *)
-| Implies(Box(Implies(f, Bot)),Bot) when classical -> "⋄ " ^ bracket f
-(* double negation *)
-| Implies(Implies(f, Bot), Bot) when classical -> string_of_formula f
-| Box f -> "□ " ^ bracket f
-| And (f, g) -> bracket f ^ " ∧ " ^ bracket g
-| Or (f, g) -> bracket f ^ " ∨ " ^ bracket g
-| Implies (f, Bot) -> "¬ " ^ bracket f (* pretty print ¬ *)
-| Implies (f, g) -> bracket f ^ " → " ^ bracket g
-and bracket e = match e with
-| Implies(Implies(f, Bot), Bot) when classical -> bracket f
-| Implies(Box(Implies(f, Bot)),Bot) when classical -> "⋄ " ^ bracket f
-| Var _ | Bot | Implies(_, Bot) | Box _ -> string_of_formula e
-| e -> "(" ^ string_of_formula e ^ ")"
-  in string_of_formula
+open Printer
 
 let catch_e f = try f() with
   ParseError -> "Parse Error"
diff --git a/dune-project b/dune-project
index 938c2ab..08cab06 100644
--- a/dune-project
+++ b/dune-project
@@ -26,7 +26,7 @@
  (synopsis "Propositional quantifiers for modal logics formalised")
  (description "")
  (allow_empty)
- (depends ocaml dune coq-stdpp js_of_ocaml angstrom)
+ (depends ocaml dune coq-stdpp js_of_ocaml angstrom exenum)
  (tags
   (coq "intuitionistic logic" "proof theory" "propositional quantifiers" "extraction")))
 
diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
index e44ec5d..31144f7 100644
--- a/theories/extraction/UIML_extraction.v
+++ b/theories/extraction/UIML_extraction.v
@@ -41,6 +41,7 @@ Definition isl_A v f := Af v f.
 Definition isl_simplified_E v f := E_simplified v f.
 Definition isl_simplified_A v f := A_simplified v f.
 
-Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A.
+Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight.
+
 
 Cd "..".