Source file g_waterproof.ml

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

# 21 "src/g_waterproof.mlg"
 
open Exceptions
open Waterprove

let waterproof_version : string = "3.0.0+8.17"

(* The code below is a hack to patch in (open_)lconstr into Ltac2 *)
(* It should be removed when merged to coq-master (open_)lconstr should be in release 9.1 *)
let add_scope s f =
  Ltac2_plugin.Tac2entries.register_scope (Names.Id.of_string s) f

let rec pr_scope =
  let open Ltac2_plugin.Tac2expr in
  let open CAst in function
    | SexprStr {v=s; _} -> Pp.qstring s
    | SexprInt {v=n; _} -> Pp.int n
    | SexprRec (_, {v=na; _}, args) ->
      let na = match na with
        | None -> Pp.str "_"
        | Some id -> Names.Id.print id
      in
      Pp.(na ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")")

let scope_fail s args =
  let open Pp in
  let args = str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")" in
  CErrors.user_err (str "Invalid arguments " ++ args ++ str " in scope " ++ str s)

let () = add_scope "lconstr" (fun arg ->
  let delimiters = List.map (function
      | Ltac2_plugin.Tac2expr.SexprRec (_, { v = Some s; _ }, []) -> s
      | _ -> scope_fail "lconstr" arg)
      arg
  in
  let act e = Ltac2_plugin.Tac2quote.of_constr ~delimiters e in
  Ltac2_plugin.Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.lconstr, act)
  )

let () = add_scope "open_lconstr" (fun arg ->
  let delimiters = List.map (function
      | Ltac2_plugin.Tac2expr.SexprRec (_, { v = Some s; _ }, []) -> s
      | _ -> scope_fail "open_.constr" arg)
      arg
  in
  let act e = Ltac2_plugin.Tac2quote.of_open_constr ~delimiters e in
  Ltac2_plugin.Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.lconstr, act)
  )
(* End of hack *)


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 () -> 
                                                             
# 73 "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 () -> 
                                                             
# 80 "src/g_waterproof.mlg"
     
      automation_shield := false
    
                                                             ) in fun ?loc ~atts ()
                                                             -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

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

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

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

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

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

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

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

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

let () = Vernacextend.vernac_extend ~plugin:"coq-waterproof.plugin" ~command:"PrintVersionSideEff" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Waterproof", 
                                     Vernacextend.TyTerminal ("Print", 
                                     Vernacextend.TyTerminal ("Version", 
                                     Vernacextend.TyNil))), (let coqpp_body () = 
                                                            Vernacextend.vtdefault (fun () -> 
                                                            
# 143 "src/g_waterproof.mlg"
     
      Feedback.msg_notice (Pp.str waterproof_version)
    
                                                            ) in fun ?loc ~atts ()
                                                            -> coqpp_body (Attributes.unsupported_attributes atts)), None))]

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

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

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

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

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