summaryrefslogtreecommitdiff
path: root/toplevel/whelp.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/whelp.ml4')
-rw-r--r--toplevel/whelp.ml473
1 files changed, 35 insertions, 38 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 888a4f1a..daedc30f 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -1,31 +1,28 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
open Flags
open Pp
-open Util
-open System
+open Errors
open Names
open Term
-open Environ
open Glob_term
open Libnames
+open Globnames
open Nametab
open Detyping
open Constrintern
open Dischargedhypsmap
-open Command
open Pfedit
-open Refiner
open Tacmach
-open Syntax_def
+open Misctypes
(* Coq interface to the Whelp query engine developed at
the University of Bologna *)
@@ -60,8 +57,8 @@ let make_whelp_request req c =
let b = Buffer.create 16
let url_char c =
- if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or
- '0' <= c & c <= '9' or c ='.'
+ if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' ||
+ '0' <= c && c <= '9' || c ='.'
then Buffer.add_char b c
else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
@@ -72,13 +69,13 @@ let rec url_list_with_sep sep f = function
| [a] -> f a
| a::l -> f a; url_string sep; url_list_with_sep sep f l
-let url_id id = url_string (string_of_id id)
+let url_id id = url_string (Id.to_string id)
let uri_of_dirpath dir =
url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
let error_whelp_unknown_reference ref =
- let qid = Nametab.shortest_qualid_of_global Idset.empty ref in
+ let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
errorlabstrm ""
(strbrk "Definitions of the current session, like " ++ pr_qualid qid ++
strbrk ", are not supported in Whelp.")
@@ -86,7 +83,7 @@ let error_whelp_unknown_reference ref =
let uri_of_repr_kn ref (mp,dir,l) =
match mp with
| MPfile sl ->
- uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl)
+ uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl)
| _ ->
error_whelp_unknown_reference ref
@@ -94,8 +91,8 @@ let url_paren f l = url_char '('; f l; url_char ')'
let url_bracket f l = url_char '['; f l; url_char ']'
let whelp_of_glob_sort = function
- | GProp Null -> "Prop"
- | GProp Pos -> "Set"
+ | GProp -> "Prop"
+ | GSet -> "Set"
| GType _ -> "Type"
let uri_int n = Buffer.add_string b (string_of_int n)
@@ -105,7 +102,7 @@ let uri_of_ind_pointer l =
let uri_of_global ref =
match ref with
- | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".")
+ | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".")
| ConstRef cst ->
uri_of_repr_kn ref (repr_con cst); url_string ".con"
| IndRef (kn,i) ->
@@ -113,7 +110,7 @@ let uri_of_global ref =
| ConstructRef ((kn,i),j) ->
uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j]
-let whelm_special = id_of_string "WHELM_ANON_VAR"
+let whelm_special = Id.of_string "WHELM_ANON_VAR"
let url_of_name = function
| Name id -> url_id id
@@ -129,9 +126,9 @@ let uri_params f = function
let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
let section_parameters = function
- | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+ | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) ->
get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
- | GRef (_,(ConstRef cst as ref)) ->
+ | GRef (_,(ConstRef cst as ref),_) ->
get_discharged_hyp_names (path_of_global ref)
| _ -> []
@@ -144,10 +141,9 @@ let merge vl al =
let rec uri_of_constr c =
match c with
| GVar (_,id) -> url_id id
- | GRef (_,ref) -> uri_of_global ref
+ | GRef (_,ref,_) -> uri_of_global ref
| GHole _ | GEvar _ -> url_string "?"
| GSort (_,s) -> url_string (whelp_of_glob_sort s)
- | _ -> url_paren (fun () -> match c with
| GApp (_,f,args) ->
let inst,rest = merge (section_parameters f) args in
uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
@@ -163,30 +159,30 @@ let rec uri_of_constr c =
| GLetIn (_,na,b,c) ->
url_string "let "; url_of_name na; url_string "\\def ";
uri_of_constr b; url_string " in "; uri_of_constr c
- | GCast (_,c, CastConv (_,t)) ->
+ | GCast (_,c, (CastConv t|CastVM t|CastNative t)) ->
uri_of_constr c; url_string ":"; uri_of_constr t
| GRec _ | GIf _ | GLetTuple _ | GCases _ ->
error "Whelp does not support pattern-matching and (co-)fixpoint."
- | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) ->
- anomaly "Written w/o parenthesis"
+ | GCast (_,_, CastCoerce) ->
+ anomaly (Pp.str "Written w/o parenthesis")
| GPatVar _ ->
- anomaly "Found constructors not supported in constr") ()
+ anomaly (Pp.str "Found constructors not supported in constr")
let make_string f x = Buffer.reset b; f x; Buffer.contents b
let send_whelp req s =
let url = make_whelp_request req s in
- let command = subst_command_placeholder browser_cmd_fmt url in
- let _ = run_command (fun x -> x) print_string command in ()
+ let command = Util.subst_command_placeholder browser_cmd_fmt url in
+ let _ = CUnix.run_command ~hook:print_string command in ()
-let whelp_constr req c =
- let c = detype false [whelm_special] [] c in
+let whelp_constr env sigma req c =
+ let c = detype false [whelm_special] env sigma c in
send_whelp req (make_string uri_of_constr c)
let whelp_constr_expr req c =
let (sigma,env)= Lemmas.get_current_context () in
- let _,c = interp_open_constr sigma env c in
- whelp_constr req c
+ let _,c = interp_open_constr env sigma c in
+ whelp_constr env sigma req c
let whelp_locate s =
send_whelp "locate" s
@@ -195,9 +191,9 @@ let whelp_elim ind =
send_whelp "elim" (make_string uri_of_global (IndRef ind))
let on_goal f =
- let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in
- let gls = { Evd.it=List.hd goals ; sigma = sigma } in
- f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+ let gls = Proof.V82.subgoals (get_pftreestate ()) in
+ let gls = { gls with Evd.it = List.hd gls.Evd.it } in
+ f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
type whelp_request =
| Locate of string
@@ -207,21 +203,22 @@ type whelp_request =
let whelp = function
| Locate s -> whelp_locate s
| Elim ind -> whelp_elim ind
- | Constr (s,c) -> whelp_constr s c
+ | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c
VERNAC ARGUMENT EXTEND whelp_constr_request
| [ "Match" ] -> [ "match" ]
| [ "Instance" ] -> [ "instance" ]
END
-VERNAC COMMAND EXTEND Whelp
+VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY
| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ]
| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ]
| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ]
| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
END
-VERNAC COMMAND EXTEND WhelpHint
+VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY
| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ]
-| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ]
+| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] ->
+ [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 02:23:07 +0000