Source file g_waterproof.ml

let _ = Mltop.add_known_module "coq-waterproof.plugin"

# 21 "src/g_waterproof.mlg"
 

module Tac2ffi = Ltac2_plugin.Tac2ffi
module Tac2env = Ltac2_plugin.Tac2env
module Tac2expr = Ltac2_plugin.Tac2expr

open Proofview
open Proofview.Notations
open Tac2expr
open Tac2ffi

open Exceptions
open Hint_dataset_declarations
open Waterprove



let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.plugin" ~command:"AutomationShieldEnableSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof", 
                                     Vernacextend.TyTerminal ("Enable", 
                                     Vernacextend.TyTerminal ("Automation", 
                                     Vernacextend.TyTerminal ("Shield", 
                                     Vernacextend.TyNil)))), (let coqpp_body () = 
                                                             Vernacextend.vtdefault (fun () -> 
                                                             
# 40 "src/g_waterproof.mlg"
     
      automation_shield := true
    
                                                             ) in fun ?loc ~atts ()
                                                             -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.plugin" ~command:"AutomationShieldDisableSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof", 
                                     Vernacextend.TyTerminal ("Disable", 
                                     Vernacextend.TyTerminal ("Automation", 
                                     Vernacextend.TyTerminal ("Shield", 
                                     Vernacextend.TyNil)))), (let coqpp_body () = 
                                                             Vernacextend.vtdefault (fun () -> 
                                                             
# 47 "src/g_waterproof.mlg"
     
      automation_shield := false
    
                                                             ) in fun ?loc ~atts ()
                                                             -> coqpp_body (Attributes.unsupported_attributes atts)), None))]


# 52 "src/g_waterproof.mlg"
 

(** Creates a name used to define the function interface *)
let pname (s: string): ml_tactic_name = { mltac_plugin = "coq-core.plugins.coq-waterproof"; mltac_tactic = s }

(** Wrapper around {! Tac2env.define_primitive} to make easier the primitive definition *)
let define_primitive (name: string) (arity: 'a arity) (f: 'a): unit =
  Tac2env.define_primitive (pname name) (mk_closure arity f)

(** 
  Defines a function of arity 0 (that only take a [unit] as an argument)

  This function will be callable in Ltac2 with [Ltac2 @ external <ltac2_name>: unit := "coq-waterproof" "<name>".]
*)
let define0 (name: string) (f: valexpr tactic): unit = define_primitive name arity_one (fun _ -> f)

(** 
  Defines a function of arity 1 (that only take one argument)

  This function will be callable in Ltac2 with [Ltac2 @ external <ltac2_name>: <type> -> unit := "coq-waterproof" "<name>".]
*)
let define1 (name: string) (r0: 'a repr) (f: 'a -> valexpr tactic): unit =
  define_primitive name arity_one @@ fun x -> f (repr_to r0 x)

(** 
  Defines a function of arity 2 of the same way than {! define1}
*)
let define2 (name: string) (r0: 'a repr) (r1: 'b repr) (f: 'a -> 'b -> valexpr tactic): unit =
  define_primitive name (arity_suc arity_one) @@ fun x y -> f (repr_to r0 x) (repr_to r1 y)

(** 
  Defines a function of arity 3 of the same way than {! define1}
*)
let define3 (name: string) (r0: 'a repr) (r1: 'b repr) (r2: 'c repr) (f: 'a -> 'b -> 'c -> valexpr tactic): unit =
  define_primitive name (arity_suc (arity_suc arity_one)) @@ fun x y z -> f (repr_to r0 x) (repr_to r1 y) (repr_to r2 z)

(** 
  Defines a function of arity 4 of the same way than {! define1}
*)
let define4 (name: string) (r0: 'a repr) (r1: 'b repr) (r2: 'c repr) (r3: 'd repr) (f: 'a -> 'b -> 'c -> 'd -> valexpr tactic): unit =
  define_primitive name (arity_suc (arity_suc (arity_suc arity_one))) @@
  fun x0 x1 x2 x3 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2) (repr_to r3 x3)

(** 
  Defines a function of arity 5 of the same way than {! define1}
*)
let define5 (name: string) (r0: 'a repr) (r1: 'b repr) (r2: 'c repr) (r3: 'd repr) (r4: 'e repr) (f: 'a -> 'b -> 'c -> 'd -> 'e -> valexpr tactic): unit =
  define_primitive name (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) @@
  fun x0 x1 x2 x3 x4 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2) (repr_to r3 x3) (repr_to r4 x4)

(** 
  Defines a function of arity 6 of the same way than {! define1}
*)
let define6 (name: string) (r0: 'a repr) (r1: 'b repr) (r2: 'c repr) (r3: 'd repr) (r4: 'e repr) (r5: 'f repr) (f: 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> valexpr tactic): unit =
  define_primitive name (arity_suc (arity_suc (arity_suc (arity_suc (arity_suc arity_one))))) @@
  fun x0 x1 x2 x3 x4 x5 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2) (repr_to r3 x3) (repr_to r4 x4) (repr_to r5 x5)

(** 
  Defines a function of arity 7 of the same way than {! define1}
*)
let define7 (name: string) (r0: 'a repr) (r1: 'b repr) (r2: 'c repr) (r3: 'd repr) (r4: 'e repr) (r5: 'f repr) (r6: 'g repr) (f: 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> valexpr tactic): unit =
  define_primitive name (arity_suc (arity_suc (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))))) @@
  fun x0 x1 x2 x3 x4 x5 x6 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2) (repr_to r3 x3) (repr_to r4 x4) (repr_to r5 x5) (repr_to r6 x6)

(** Comes from [coq/plugins/ltac2/tac2tactics.ml] *)
let thaw (r: 'a repr) (f: (unit, 'a) fun1): 'a tactic = app_fun1 f unit r ()

(** Comes from [coq/plugins/ltac2/tac2tactics.ml] *)
let delayed_of_tactic (tac: 'a tactic) (env: Environ.env) (sigma: Evd.evar_map): (Evd.evar_map * 'a) =
  let _, pv = Proofview.init sigma [] in
  let name, poly = Names.Id.of_string "ltac2_delayed", false in
  let c, pv, _, _ = Proofview.apply ~name ~poly env tac pv in
  let _, sigma = Proofview.proofview pv in
  (sigma, c)


(**
  Utilitary function to cast OCaml types into Ltac2-compatibles types  
  
  Comes from [coq/plugins/ltac2/tac2tactics.ml]
*)
let delayed_of_thunk (r: 'a repr) (tac: (unit, 'a) fun1) (env: Environ.env) (sigma: Evd.evar_map): (Evd.evar_map * 'a) =
  delayed_of_tactic (thaw r tac) env sigma

(** Converts a ['a repr] into a [(unit -> 'a) repr] *)
let thunk (r: 'a repr): (unit, 'a) fun1 repr = fun1 unit r

let _ = define0
let _ = define1
let _ = define2
let _ = define3
let _ = define5
let _ = define7

(** Converts a {! Hint_dataset_declarations.database_type} into a [valexpr] *)
let database_type_to_valexp (database_type: database_type): valexpr = match database_type with
  | Main -> ValInt 0
  | Decidability -> ValInt 1
  | Shorten -> ValInt 2
  
(** Converts a [valexpr] into a {! Hint_dataset_declarations.database_type} *)
let database_type_from_valexp (value: valexpr): database_type = match value with
  | ValInt n ->
    let database_type = match n with
      | 0 -> Main
      | 1 -> Decidability
      | 2 -> Shorten
      | _ -> throw (CastError "cannot cast something an [int] greater than 3 into a [database_type]")
    in database_type
  | _ -> throw (CastError "cannot cast something different than an [int] into a [database_type]")

(* Exports {! Hint_dataset_declarations.database_type} to Ltac2 *)
let () =
  define0 "database_type_main" @@ tclUNIT @@ database_type_to_valexp Main;
  define0 "database_type_decidability" @@ tclUNIT @@ database_type_to_valexp Decidability;
  define0 "database_type_shorten" @@ tclUNIT @@ database_type_to_valexp Shorten

(* Exports {! Waterprove.waterprove} to Ltac2 *)
let () =
  define4 "waterprove" int bool (list (thunk constr)) (make_repr database_type_to_valexp database_type_from_valexp) @@
    fun depth shield lems database_type ->
      begin
        waterprove
          depth
          ~shield
          (List.map (fun lem -> delayed_of_thunk constr lem) lems)
          database_type
      end >>= fun () -> tclUNIT @@ of_unit ()

(* Exports {! Waterprove.rwaterprove} to Ltac2 *)
let () =
  define6 "rwaterprove" int bool (list (thunk constr)) (make_repr database_type_to_valexp database_type_from_valexp) (list constr) (list constr) @@
    fun depth shield lems database_type must_use forbidden ->
      begin
        rwaterprove
          depth
          ~shield
          (List.map (fun lem -> delayed_of_thunk constr lem) lems)
          database_type
          must_use
          forbidden
      end >>= fun () -> tclUNIT @@ of_unit ()