summaryrefslogtreecommitdiff
path: root/contrib/dp/dp_simplify.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp/dp_simplify.ml')
-rw-r--r--contrib/dp/dp_simplify.ml117
1 files changed, 0 insertions, 117 deletions
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
deleted file mode 100644
index d5376b8d..00000000
--- a/contrib/dp/dp_simplify.ml
+++ /dev/null
@@ -1,117 +0,0 @@
-
-open Format
-open Fol
-
-let is_simplify_ident s =
- let is_simplify_char = function
- | 'a'..'z' | 'A'..'Z' | '0'..'9' -> true
- | _ -> false
- in
- try
- String.iter (fun c -> if not (is_simplify_char c) then raise Exit) s; true
- with Exit ->
- false
-
-let ident fmt s =
- if is_simplify_ident s then fprintf fmt "%s" s else fprintf fmt "|%s|" s
-
-let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-let comma fmt () = fprintf fmt ",@ "
-
-let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(+@ %a@ %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(-@ %a@ %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(*@ %a@ %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "%a" ident id
- | App (id, tl) ->
- fprintf fmt "@[(%a@ %a)@]" ident id print_terms tl
-
-and print_terms fmt tl =
- print_list space print_term fmt tl
-
-let rec print_predicate fmt p =
- let pp = print_predicate in
- match p with
- | True ->
- fprintf fmt "TRUE"
- | False ->
- fprintf fmt "FALSE"
- | Fatom (Eq (a, b)) ->
- fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b
- | Fatom (Le (a, b)) ->
- fprintf fmt "@[(<= %a@ %a)@]" print_term a print_term b
- | Fatom (Lt (a, b))->
- fprintf fmt "@[(< %a@ %a)@]" print_term a print_term b
- | Fatom (Ge (a, b)) ->
- fprintf fmt "@[(>= %a@ %a)@]" print_term a print_term b
- | Fatom (Gt (a, b)) ->
- fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
- | Fatom (Pred (id, tl)) ->
- fprintf fmt "@[(EQ (%a@ %a) |@@true|)@]" ident id print_terms tl
- | Imp (a, b) ->
- fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b
- | And (a, b) ->
- fprintf fmt "@[(AND@ %a@ %a)@]" pp a pp b
- | Or (a, b) ->
- fprintf fmt "@[(OR@ %a@ %a)@]" pp a pp b
- | Not a ->
- fprintf fmt "@[(NOT@ %a)@]" pp a
- | Forall (id, _, p) ->
- fprintf fmt "@[(FORALL (%a)@ %a)@]" ident id pp p
- | Exists (id, _, p) ->
- fprintf fmt "@[(EXISTS (%a)@ %a)@]" ident id pp p
-
-(**
-let rec string_list l = match l with
- [] -> ""
- | [e] -> e
- | e::l' -> e ^ " " ^ (string_list l')
-**)
-
-let print_query fmt (decls,concl) =
- let print_decl = function
- | DeclVar (id, [], t) ->
- fprintf fmt "@[;; %s : %s@]@\n" id t
- | DeclVar (id, l, t) ->
- fprintf fmt "@[;; %s : %a -> %s@]@\n"
- id (print_list comma pp_print_string) l t
- | DeclPred (id, []) ->
- fprintf fmt "@[;; %s : BOOLEAN @]@\n" id
- | DeclPred (id, l) ->
- fprintf fmt "@[;; %s : %a -> BOOLEAN@]@\n"
- id (print_list comma pp_print_string) l
- | DeclType id ->
- fprintf fmt "@[;; %s : TYPE@]@\n" id
- | Assert (id, f) ->
- fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
- in
- List.iter print_decl decls;
- fprintf fmt "%a@." print_predicate concl
-
-let call q =
- let f = Filename.temp_file "coq_dp" ".sx" in
- let c = open_out f in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[%a@]@." print_query q;
- close_out c;
- ignore (Sys.command (sprintf "cat %s" f));
- let cmd =
- sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" f
- in
- prerr_endline cmd; flush stderr;
- let out = Sys.command cmd in
- if out = 0 then Valid else if out = 1 then Invalid else Timeout
- (* TODO: effacer le fichier f et le fichier out *)