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.1.0+9.0"

(* 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 (Procq.Symbol.nterm Procq.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 (Procq.Symbol.nterm Procq.Constr.lconstr, act)
  )
(* End of hack *)



# 74 "src/g_waterproof.mlg"
 
let () = Mltop.add_init_function "coq-waterproof.plugin" @@ fun () ->
    Procq.set_keyword_state
      (List.fold_left CLexer.add_keyword (Procq.get_keyword_state())
      ["and"; "as"; "hold"; "holds"; "it"; "or"; "we"; "that"])


let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 82 "src/g_waterproof.mlg"
     
      automation_shield := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 89 "src/g_waterproof.mlg"
     
      automation_shield := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 96 "src/g_waterproof.mlg"
     
      filter_errors := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 103 "src/g_waterproof.mlg"
     
      filter_errors := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 110 "src/g_waterproof.mlg"
     
      automation_debug := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 117 "src/g_waterproof.mlg"
     
      automation_debug := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 124 "src/g_waterproof.mlg"
     
      print_rewrite_hints := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 131 "src/g_waterproof.mlg"
     
      print_rewrite_hints := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 138 "src/g_waterproof.mlg"
     
      print_hypothesis_help := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 145 "src/g_waterproof.mlg"
     
      print_hypothesis_help := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 152 "src/g_waterproof.mlg"
     
      Feedback.msg_notice (Pp.str waterproof_version)
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 159 "src/g_waterproof.mlg"
     
      redirect_feedback := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 166 "src/g_waterproof.mlg"
     
      redirect_feedback := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 174 "src/g_waterproof.mlg"
     
      redirect_errors := true
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 181 "src/g_waterproof.mlg"
     
      redirect_errors := false
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]

let () = Vernacextend.static_vernac_extend ~plugin:(Some "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 () = Vernactypes.vtdefault (fun () -> 
# 188 "src/g_waterproof.mlg"
     
      add_wp_feedback_logger ()
    
                               ) in
            fun ?loc ~atts () ->
            coqpp_body (Attributes.unsupported_attributes atts)),
          None))]


# 193 "src/g_waterproof.mlg"
 
  open Ltac2_plugin.Tac2entries
  open Unfold_framework
  open Stdarg
  open Procq.Constr

  type pre_unfold_entry =
    | PreUnfold
    | PreApply of Constrexpr.constr_expr
    | PreRewrite of Constrexpr.constr_expr

  let pr_pre_unfold_entry env sigma ent =
    let open Pp in
    match ent with
    | PreUnfold -> str "unfold"
    | PreApply e -> str "apply" ++ str " with term " ++ Ppconstr.pr_constr_expr env sigma e
    | PreRewrite e -> str "rewrite" ++ str " with term " ++ Ppconstr.pr_constr_expr env sigma e


let (wit_unfold_action_entry, unfold_action_entry) =
  Vernacextend.vernac_argument_extend ~plugin:"coq-waterproof.plugin" ~name:"unfold_action_entry" 
  {
    Vernacextend.arg_parsing =
    Vernacextend.Arg_rules
    ([(Procq.Production.make
       (Procq.Rule.next
        (Procq.Rule.next
         (Procq.Rule.next
          (Procq.Rule.next (Procq.Rule.stop)
           ((Procq.Symbol.token (Procq.terminal ";"))))
          ((Procq.Symbol.token (Procq.terminal "by"))))
         ((Procq.Symbol.token (Procq.terminal "rewrite"))))
        ((Procq.Symbol.nterm constr)))
       (fun e _ _ _ loc -> 
# 216 "src/g_waterproof.mlg"
                                        PreRewrite e 
                           ));
     (Procq.Production.make
      (Procq.Rule.next
       (Procq.Rule.next
        (Procq.Rule.next
         (Procq.Rule.next (Procq.Rule.stop)
          ((Procq.Symbol.token (Procq.terminal ";"))))
         ((Procq.Symbol.token (Procq.terminal "by"))))
        ((Procq.Symbol.token (Procq.terminal "apply"))))
       ((Procq.Symbol.nterm constr)))
      (fun e _ _ _ loc -> 
# 215 "src/g_waterproof.mlg"
                                      PreApply e 
                          ));
     (Procq.Production.make
      (Procq.Rule.next
       (Procq.Rule.next
        (Procq.Rule.next (Procq.Rule.stop)
         ((Procq.Symbol.token (Procq.terminal ";"))))
        ((Procq.Symbol.token (Procq.terminal "by"))))
       ((Procq.Symbol.token (Procq.terminal "unfold"))))
      (fun _ _ _ loc -> 
# 214 "src/g_waterproof.mlg"
                             PreUnfold 
                        ))]);
    Vernacextend.arg_printer = fun env sigma -> 
# 213 "src/g_waterproof.mlg"
             pr_pre_unfold_entry env sigma 
    ;
    }
let _ = (wit_unfold_action_entry, unfold_action_entry)

let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-waterproof.plugin") ~command:"RegisterUnfold" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Waterproof",
           Vernacextend.TyTerminal
           ("Register",
            Vernacextend.TyTerminal
            ("Expand",
             Vernacextend.TyNonTerminal (Extend.TUlist1 (Extend.TUentry (Genarg.get_arg_tag wit_string)),
             Vernacextend.TyTerminal
             (";",
              Vernacextend.TyTerminal
              ("for",
               Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ref),
               Vernacextend.TyTerminal
               (";",
                Vernacextend.TyTerminal
                ("as",
                 Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_string),
                 Vernacextend.TyNonTerminal (Extend.TUopt (Extend.TUentry (Genarg.get_arg_tag wit_unfold_action_entry)),
                 Vernacextend.TyNil))))))))))),
          (let coqpp_body s id name opt_unfold_action () =
            (let notation_data_pair = 
# 225 "src/g_waterproof.mlg"
     
      register_unfold s id
    
             in Vernactypes.vtdefault (fun () -> 
# 228 "src/g_waterproof.mlg"
     
      let (notation_data, old_notation_data) = notation_data_pair in
      let located_id = Nametab.locate id in
      add_to_unfold_map s located_id;
      register_notation_interpretation notation_data;
      register_notation_interpretation old_notation_data;
      let ua =
        begin
          match opt_unfold_action with
          | None -> Unfold_entry name
          | Some PreUnfold -> Unfold_entry name
          | Some (PreApply e) -> Apply_entry (name, e)
          | Some (PreRewrite e) -> Rewrite_entry (name, e)
        end in
      register_unfold_entry located_id ua
    
            )) in fun s id name opt_unfold_action ?loc ~atts () ->
            coqpp_body s id name opt_unfold_action
              (Attributes.unsupported_attributes atts)),
          Some (fun s id name opt_unfold_action -> 
# 223 "src/g_waterproof.mlg"
                                                        Vernacextend.(VtSideff ([], VtNow)) 
               )))]