summaryrefslogtreecommitdiff
path: root/contrib/dp/dp_gappa.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp/dp_gappa.ml')
-rw-r--r--contrib/dp/dp_gappa.ml445
1 files changed, 445 insertions, 0 deletions
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
new file mode 100644
index 00000000..70439a97
--- /dev/null
+++ b/contrib/dp/dp_gappa.ml
@@ -0,0 +1,445 @@
+
+open Format
+open Util
+open Pp
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Names
+open Nameops
+open Termops
+open Coqlib
+open Hipattern
+open Libnames
+open Declarations
+open Evarutil
+
+let debug = ref false
+
+(* 1. gappa syntax trees and output *)
+
+module Constant = struct
+
+ open Bigint
+
+ type t = { mantissa : bigint; base : int; exp : bigint }
+
+ let create (b, m, e) =
+ { mantissa = m; base = b; exp = e }
+
+ let of_int x =
+ { mantissa = x; base = 1; exp = zero }
+
+ let print fmt x = match x.base with
+ | 1 -> fprintf fmt "%s" (to_string x.mantissa)
+ | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp)
+ | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp)
+ | _ -> assert false
+
+end
+
+type binop = Bminus | Bplus | Bmult | Bdiv
+
+type unop = Usqrt | Uabs | Uopp
+
+type rounding_mode = string
+
+type term =
+ | Tconst of Constant.t
+ | Tvar of string
+ | Tbinop of binop * term * term
+ | Tunop of unop * term
+ | Tround of rounding_mode * term
+
+type pred =
+ | Pin of term * Constant.t * Constant.t
+
+let rec print_term fmt = function
+ | Tconst c -> Constant.print fmt c
+ | Tvar s -> pp_print_string fmt s
+ | Tbinop (op, t1, t2) ->
+ let op = match op with
+ | Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/"
+ in
+ fprintf fmt "(%a %s %a)" print_term t1 op print_term t2
+ | Tunop (Uabs, t) ->
+ fprintf fmt "|%a|" print_term t
+ | Tunop (Uopp | Usqrt as op, t) ->
+ let s = match op with
+ | Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false
+ in
+ fprintf fmt "(%s(%a))" s print_term t
+ | Tround (m, t) ->
+ fprintf fmt "(%s(%a))" m print_term t
+
+let print_pred fmt = function
+ | Pin (t, c1, c2) ->
+ fprintf fmt "%a in [%a, %a]"
+ print_term t Constant.print c1 Constant.print c2
+
+let temp_file f = if !debug then f else Filename.temp_file f ".v"
+let remove_file f = if not !debug then try Sys.remove f with _ -> ()
+
+let read_gappa_proof f =
+ let buf = Buffer.create 1024 in
+ Buffer.add_char buf '(';
+ let cin = open_in f in
+ let rec skip_space () =
+ let c = input_char cin in if c = ' ' then skip_space () else c
+ in
+ while input_char cin <> '=' do () done;
+ try
+ while true do
+ let c = skip_space () in
+ if c = ':' then raise Exit;
+ Buffer.add_char buf c;
+ let s = input_line cin in
+ Buffer.add_string buf s;
+ Buffer.add_char buf '\n';
+ done;
+ assert false
+ with Exit ->
+ close_in cin;
+ remove_file f;
+ Buffer.add_char buf ')';
+ Buffer.contents buf
+
+exception GappaFailed
+exception GappaProofFailed
+
+let patch_gappa_proof fin fout =
+ let cin = open_in fin in
+ let cout = open_out fout in
+ let fmt = formatter_of_out_channel cout in
+ let last = ref "" in
+ let defs = ref "" in
+ try
+ while true do
+ let s = input_line cin in
+ if s = "Qed." then
+ fprintf fmt "Defined.@\n"
+ else begin
+ begin
+ try Scanf.sscanf s "Lemma %s "
+ (fun n -> defs := n ^ " " ^ !defs; last := n)
+ with Scanf.Scan_failure _ ->
+ try Scanf.sscanf s "Definition %s "
+ (fun n -> defs := n ^ " " ^ !defs)
+ with Scanf.Scan_failure _ ->
+ ()
+ end;
+ fprintf fmt "%s@\n" s
+ end
+ done
+ with End_of_file ->
+ close_in cin;
+ fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last;
+ close_out cout
+
+let call_gappa hl p =
+ let gappa_in = temp_file "gappa_input" in
+ let c = open_out gappa_in in
+ let fmt = formatter_of_out_channel c in
+ fprintf fmt "@[{ ";
+ List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl;
+ fprintf fmt "%a }@]@." print_pred p;
+ close_out c;
+ let gappa_out = temp_file "gappa_output" in
+ let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaFailed;
+ remove_file gappa_in;
+ let gappa_out2 = temp_file "gappa2" in
+ patch_gappa_proof gappa_out gappa_out2;
+ remove_file gappa_out;
+ let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaProofFailed;
+ let gappa_out3 = temp_file "gappa3" in
+ let c = open_out gappa_out3 in
+ let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
+ Printf.fprintf c
+ "Require \"%s\". Set Printing Depth 9999999. Print %s.proof."
+ (Filename.chop_suffix gappa_out2 ".v") gappa2;
+ close_out c;
+ let lambda = temp_file "gappa_lambda" in
+ let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in
+ let out = Sys.command cmd in
+ if out <> 0 then raise GappaProofFailed;
+ remove_file gappa_out2; remove_file gappa_out3;
+ remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o");
+ read_gappa_proof lambda
+
+(* 2. coq -> gappa translation *)
+
+exception NotGappa
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+ init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+ @ [["Coq"; "ZArith"; "BinInt"];
+ ["Coq"; "Reals"; "Rdefinitions"];
+ ["Coq"; "Reals"; "Raxioms";];
+ ["Coq"; "Reals"; "Rbasic_fun";];
+ ["Coq"; "Reals"; "R_sqrt";];
+ ["Coq"; "Reals"; "Rfunctions";];
+ ["Gappa"; "Gappa_tactic";];
+ ["Gappa"; "Gappa_fixed";];
+ ["Gappa"; "Gappa_float";];
+ ["Gappa"; "Gappa_round_def";];
+ ["Gappa"; "Gappa_pred_bnd";];
+ ["Gappa"; "Gappa_definitions";];
+ ]
+
+let constant = gen_constant_in_modules "gappa" coq_modules
+
+let coq_refl_equal = lazy (constant "refl_equal")
+let coq_Rle = lazy (constant "Rle")
+let coq_R = lazy (constant "R")
+(*
+let coq_Rplus = lazy (constant "Rplus")
+let coq_Rminus = lazy (constant "Rminus")
+let coq_Rmult = lazy (constant "Rmult")
+let coq_Rdiv = lazy (constant "Rdiv")
+let coq_powerRZ = lazy (constant "powerRZ")
+let coq_R1 = lazy (constant "R1")
+let coq_Ropp = lazy (constant "Ropp")
+let coq_Rabs = lazy (constant "Rabs")
+let coq_sqrt = lazy (constant "sqrt")
+*)
+
+let coq_convert = lazy (constant "convert")
+let coq_reUnknown = lazy (constant "reUnknown")
+let coq_reFloat2 = lazy (constant "reFloat2")
+let coq_reFloat10 = lazy (constant "reFloat10")
+let coq_reInteger = lazy (constant "reInteger")
+let coq_reBinary = lazy (constant "reBinary")
+let coq_reUnary = lazy (constant "reUnary")
+let coq_reRound = lazy (constant "reRound")
+let coq_roundDN = lazy (constant "roundDN")
+let coq_roundUP = lazy (constant "roundUP")
+let coq_roundNE = lazy (constant "roundNE")
+let coq_roundZR = lazy (constant "roundZR")
+let coq_rounding_fixed = lazy (constant "rounding_fixed")
+let coq_rounding_float = lazy (constant "rounding_float")
+let coq_boAdd = lazy (constant "boAdd")
+let coq_boSub = lazy (constant "boSub")
+let coq_boMul = lazy (constant "boMul")
+let coq_boDiv = lazy (constant "boDiv")
+let coq_uoAbs = lazy (constant "uoAbs")
+let coq_uoNeg = lazy (constant "uoNeg")
+let coq_uoSqrt = lazy (constant "uoSqrt")
+let coq_subset = lazy (constant "subset")
+let coq_makepairF = lazy (constant "makepairF")
+
+let coq_true = lazy (constant "true")
+let coq_false = lazy (constant "false")
+
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+let coq_xH = lazy (constant "xH")
+let coq_xI = lazy (constant "xI")
+let coq_xO = lazy (constant "xO")
+let coq_IZR = lazy (constant "IZR")
+
+(* translates a closed Coq term p:positive into a FOL term of type int *)
+let rec tr_positive p = match kind_of_term p with
+ | Term.Construct _ when p = Lazy.force coq_xH ->
+ 1
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+ 2 * (tr_positive a) + 1
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+ 2 * (tr_positive a)
+ | Term.Cast (p, _, _) ->
+ tr_positive p
+ | _ ->
+ raise NotGappa
+
+(* translates a closed Coq term t:Z into a term of type int *)
+let rec tr_arith_constant t = match kind_of_term t with
+ | Term.Construct _ when t = Lazy.force coq_Z0 -> 0
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a)
+ | Term.Cast (t, _, _) -> tr_arith_constant t
+ | _ -> raise NotGappa
+
+(* translates a closed Coq term p:positive into a FOL term of type bigint *)
+let rec tr_bigpositive p = match kind_of_term p with
+ | Term.Construct _ when p = Lazy.force coq_xH ->
+ Bigint.one
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+ Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a))
+ | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+ (Bigint.mult_2 (tr_bigpositive a))
+ | Term.Cast (p, _, _) ->
+ tr_bigpositive p
+ | _ ->
+ raise NotGappa
+
+(* translates a closed Coq term t:Z into a term of type bigint *)
+let rec tr_arith_bigconstant t = match kind_of_term t with
+ | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a
+ | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
+ Bigint.neg (tr_bigpositive a)
+ | Term.Cast (t, _, _) -> tr_arith_bigconstant t
+ | _ -> raise NotGappa
+
+let decomp c =
+ let c, args = decompose_app c in
+ kind_of_term c, args
+
+let tr_bool c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_true -> true
+ | c, [] when c = Lazy.force coq_false -> false
+ | _ -> raise NotGappa
+
+let tr_float b m e =
+ (b, tr_arith_bigconstant m, tr_arith_bigconstant e)
+
+let tr_binop c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_boAdd -> Bplus
+ | c, [] when c = Lazy.force coq_boSub -> Bminus
+ | c, [] when c = Lazy.force coq_boMul -> Bmult
+ | c, [] when c = Lazy.force coq_boDiv -> Bdiv
+ | _ -> assert false
+
+let tr_unop c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_uoNeg -> Uopp
+ | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt
+ | c, [] when c = Lazy.force coq_uoAbs -> Uabs
+ | _ -> raise NotGappa
+
+let tr_var c = match decomp c with
+ | Var x, [] -> string_of_id x
+ | _ -> assert false
+
+let tr_mode c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_roundDN -> "dn"
+ | c, [] when c = Lazy.force coq_roundNE -> "ne"
+ | c, [] when c = Lazy.force coq_roundUP -> "up"
+ | c, [] when c = Lazy.force coq_roundZR -> "zr"
+ | _ -> raise NotGappa
+
+let tr_rounding_mode c = match decompose_app c with
+ | c, [a;b] when c = Lazy.force coq_rounding_fixed ->
+ let a = tr_mode a in
+ let b = tr_arith_constant b in
+ sprintf "fixed<%d,%s>" b a
+ | c, [a;p;e] when c = Lazy.force coq_rounding_float ->
+ let a = tr_mode a in
+ let p = tr_positive p in
+ let e = tr_arith_constant e in
+ sprintf "float<%d,%d,%s>" p (-e) a
+ | _ ->
+ raise NotGappa
+
+(* REexpr -> term *)
+let rec tr_term c0 =
+ let c, args = decompose_app c0 in
+ match kind_of_term c, args with
+ | _, [a] when c = Lazy.force coq_reUnknown ->
+ Tvar (tr_var a)
+ | _, [a; b] when c = Lazy.force coq_reFloat2 ->
+ Tconst (Constant.create (tr_float 2 a b))
+ | _, [a; b] when c = Lazy.force coq_reFloat10 ->
+ Tconst (Constant.create (tr_float 10 a b))
+ | _, [a] when c = Lazy.force coq_reInteger ->
+ Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero))
+ | _, [op;a;b] when c = Lazy.force coq_reBinary ->
+ Tbinop (tr_binop op, tr_term a, tr_term b)
+ | _, [op;a] when c = Lazy.force coq_reUnary ->
+ Tunop (tr_unop op, tr_term a)
+ | _, [op;a] when c = Lazy.force coq_reRound ->
+ Tround (tr_rounding_mode op, tr_term a)
+ | _ ->
+ msgnl (str "tr_term: " ++ Printer.pr_constr c0);
+ assert false
+
+let tr_rle c =
+ let c, args = decompose_app c in
+ match kind_of_term c, args with
+ | _, [a;b] when c = Lazy.force coq_Rle ->
+ begin match decompose_app a, decompose_app b with
+ | (ac, [at]), (bc, [bt])
+ when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert ->
+ at, bt
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+
+let tr_pred c =
+ let c, args = decompose_app c in
+ match kind_of_term c, args with
+ | _, [a;b] when c = build_coq_and () ->
+ begin match tr_rle a, tr_rle b with
+ | (c1, t1), (t2, c2) when t1 = t2 ->
+ begin match tr_term c1, tr_term c2 with
+ | Tconst c1, Tconst c2 ->
+ Pin (tr_term t1, c1, c2)
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+ end
+ | _ ->
+ raise NotGappa
+
+let is_R c = match decompose_app c with
+ | c, [] when c = Lazy.force coq_R -> true
+ | _ -> false
+
+let tr_hyps =
+ List.fold_left
+ (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) []
+
+let constr_of_string gl s =
+ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
+ Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
+
+let var_name = function
+ | Name id ->
+ let s = string_of_id id in
+ let s = String.sub s 1 (String.length s - 1) in
+ mkVar (id_of_string s)
+ | Anonymous ->
+ assert false
+
+let build_proof_term c0 =
+ let bl,c = decompose_lam c0 in
+ List.fold_right
+ (fun (x,t) pf ->
+ mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
+ bl c0
+
+let gappa_internal gl =
+ try
+ let c = tr_pred (pf_concl gl) in
+ let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in
+ let pf = constr_of_string gl s in
+ let pf = build_proof_term pf in
+ Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl
+ with
+ | NotGappa -> error "not a gappa goal"
+ | GappaFailed -> error "gappa failed"
+ | GappaProofFailed -> error "incorrect gappa proof term"
+
+let gappa_prepare =
+ let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
+ lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
+
+let gappa gl =
+ Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
+ Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl
+
+(*
+Local Variables:
+compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt"
+End:
+*)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 20:58:02 +0000