Decision procedure for iSL

bin/dune

@@ -1,6 +1,6 @@
 (executables
- (public_names uiml_demo benchmark uiml_cmdline)
- (names uiml_demo benchmark uiml_cmdline)
+ (public_names uiml_demo benchmark uiml_cmdline isl_dec)
+ (names uiml_demo benchmark uiml_cmdline isl_dec)
  (modes js native)
  (preprocess (pps js_of_ocaml-ppx))
  (libraries js_of_ocaml UIML angstrom exenum)

bin/isl_dec.ml

@@ -0,0 +1,27 @@
+open Exenum
+open Printer
+open UIML.Formulas
+open Sys
+open Char
+open UIML.DecisionProcedure
+open UIML.Datatypes
+open Stringconversion
+open Modal_expressions_parser
+
+
+
+let nb_args = Array.length Sys.argv
+
+let form = if nb_args = 2 then (Sys.argv.(1)) else "T"
+
+let usage_string =
+  "isl_dec φ: decides the provability of the modal formula φ in iSL.\n"
+
+let print_decision = function
+  | Coq_inl _ -> "Probable"
+  | _ -> "Not provable"
+
+let () =
+  if nb_args = 2 then form |> eval |> coq_Provable_dec [] |>
+     print_decision |> print_string |> print_newline
+  else print_string usage_string

theories/extraction/UIML_extraction.v

@@ -5,7 +5,7 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.PropQuantifiers.
+Require Import ISL.PropQuantifiers ISL.DecisionProcedure.
 
 Require Import ISL.Simp.
 
@@ -41,5 +41,5 @@ Definition isl_simplified_A v f := A_simplified v f.
 
 Set Extraction Output Directory "extraction".
 
-Separate Extraction gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight isl_simp.
+Separate Extraction Provable_dec gl_UI k_UI isl_E isl_A isl_simplified_E isl_simplified_A Formulas.weight isl_simp.