From 8f4e84c24ac202914110b34bb241f16ce9fe9d0a Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 20 May 2005 15:43:46 +0000 Subject: Interface vers outil de recherche Whelp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7049 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 6 +- toplevel/whelp.ml4 | 191 +++++++++++++++++++++++++++++++++++++++++++++++++++++ toplevel/whelp.mli | 24 +++++++ 3 files changed, 218 insertions(+), 3 deletions(-) create mode 100644 toplevel/whelp.ml4 create mode 100644 toplevel/whelp.mli diff --git a/Makefile b/Makefile index dd7c67c889..1deb32175c 100644 --- a/Makefile +++ b/Makefile @@ -176,7 +176,7 @@ PARSING=\ parsing/pcoq.cmo parsing/egrammar.cmo parsing/g_xml.cmo \ parsing/ppconstr.cmo translate/ppconstrnew.cmo parsing/printer.cmo \ parsing/pptactic.cmo translate/pptacticnew.cmo parsing/tactic_printer.cmo \ - parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo + parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo HIGHPARSING=\ parsing/g_prim.cmo parsing/g_proofs.cmo parsing/g_basevernac.cmo \ @@ -209,7 +209,7 @@ TOPLEVEL=\ toplevel/command.cmo toplevel/record.cmo \ translate/ppvernacnew.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ - toplevel/vernacentries.cmo toplevel/vernac.cmo \ + toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ toplevel/toplevel.cmo toplevel/usage.cmo \ toplevel/coqinit.cmo toplevel/coqtop.cmo @@ -221,7 +221,7 @@ HIGHTACTICS=\ SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 USERTAC = $(SPECTAC) ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ - tactics/eauto.ml4 + tactics/eauto.ml4 toplevel/whelp.ml4 USERTACCMO=$(USERTAC:.ml4=.cmo) USERTACCMX=$(USERTAC:.ml4=.cmx) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 new file mode 100644 index 0000000000..b27a74c2f9 --- /dev/null +++ b/toplevel/whelp.ml4 @@ -0,0 +1,191 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl) + | _ -> + error_whelp_unknown_reference ref + +let url_encode_product = "%5Cforall+" (* \forall *) +let url_encode_imply = "%5Cto+" (* \to *) +let url_encode_lambda = "%5Clambda+" (* \lambda *) +let url_encode_let = "let+" (* let *) +let url_encode_def = "%5Cdef+" (* \def *) +let url_encode_in = "+in+" (* in *) +let url_encode_colon = "%3A" (* : *) +let url_encode_dot = "." (* . *) +let url_encode_semicolon = "%3B" (* ; *) +let uri_encode_question_mark = "%3F" (* ? *) +let url_encode_lpar = "%28" (* ( *) +let url_encode_rpar = "%29" (* ) *) +let url_encode_slash = "%2F" (* / *) +let url_encode_subst = "%5Csubst" (* \subst *) +let url_encode_assign = "%5CAssign" (* \Assign *) +let url_encode_ind_pointer = ".ind%23xpointer" (* .ind#xpointer *) +let url_paren s = url_encode_lpar ^ s ^ url_encode_rpar +let url_bracket s = "%5B" ^ s ^ "%5D" + +let uri_of_sort = function + | RProp Null -> "Prop" + | RProp Pos -> "Set" + | RType _ -> "Type" + +let uri_of_global ref = + match ref with + | VarRef id -> error "Unknown Whelp reference: "^(string_of_id id) + | ConstRef cst -> + uri_of_repr_kn ref (repr_con cst) + ^".con" + | IndRef (kn,i) -> + uri_of_repr_kn ref (repr_kn kn) ^ url_encode_ind_pointer ^ + url_paren ("1" ^ url_encode_slash ^ string_of_int (i+1)) + | ConstructRef ((kn,i),j) -> + uri_of_repr_kn ref (repr_kn kn) ^ url_encode_ind_pointer ^ + url_paren ("1" ^ url_encode_slash ^ string_of_int (i+1) + ^ url_encode_slash ^ string_of_int j) + +let whelm_special = id_of_string "WHELM_ANON_VAR" + +let url_of_name = function + | Name id -> string_of_id id + | Anonymous -> string_of_id whelm_special (* No anon id in Whelp *) + +let uri_of_binding (id,c) = string_of_id id ^ url_encode_assign ^ c + +let uri_params = function + | [] -> "" + | l -> url_encode_subst ^ url_bracket + (String.concat url_encode_semicolon (List.map uri_of_binding l)) + +let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) + +let section_parameters = function + | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) -> + get_discharged_hyp_names (sp_of_global (IndRef(induri,0))) + | RRef (_,(ConstRef cst as ref)) -> + get_discharged_hyp_names (sp_of_global ref) + | _ -> [] + +let merge vl al = + let rec aux acc = function + | ([],l) | (_,([] as l)) -> List.rev acc, l + | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) + in aux [] (vl,al) + +let rec uri_of_constr = function + | RVar (_,id) -> string_of_id id + | RRef (_,ref) -> (uri_of_global ref) + | RApp (_,f,args) -> + let args = List.map uri_of_constr args in + let inst,rest = merge (section_parameters f) args in + url_paren (uri_of_constr f ^ "+" ^ uri_params inst ^ + String.concat "+" rest) + | RLambda (_,na,ty,c) -> + url_paren (url_encode_lambda ^ url_of_name na ^ url_encode_colon + ^ uri_of_constr ty ^ url_encode_dot ^ uri_of_constr c) + | RProd (_,Anonymous,ty,c) -> + url_paren (uri_of_constr ty ^ url_encode_imply ^ uri_of_constr c) + | RProd (_,Name id,ty,c) -> + url_paren (url_encode_product ^ string_of_id id ^ url_encode_colon + ^ uri_of_constr ty ^ url_encode_dot ^ uri_of_constr c) + | RLetIn (_,na,b,c) -> + url_paren (url_encode_let ^ url_of_name na ^ url_encode_def ^ + uri_of_constr b ^ url_encode_in ^ uri_of_constr c) + | RCast (_,c,t) -> + url_paren (uri_of_constr c ^ url_encode_colon ^ uri_of_constr t) + | RHole _ | REvar _ -> uri_encode_question_mark + | RSort (_,s) -> uri_of_sort s + | RRec _ | RIf _ | RLetTuple _ | ROrderedCase _ | RCases _ -> + error "Whelp does not support pattern-matching and (co-)fixpoint" + | RPatVar _ | RDynamic _ -> + anomaly "Found constructors not supported in constr" + +let send_whelp req s = + let url = make_whelp_request req s in + let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in + let _ = run_command (fun x -> x) print_string command in () + +let whelp_constr env req c = + let c = detype (false,env) [whelm_special] [] c in + send_whelp req (uri_of_constr c) + +let whelp_constr_expr req c = + let (sigma,env)= get_current_context () in + let _,c = interp_openconstr_gen sigma env ([],[]) c None in + whelp_constr env req c + +let whelp_locate s = + send_whelp "locate" s + +let whelp_elim ind = + send_whelp "elim" +(* (uri_of_global (IndRef ind))*) + (string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef ind))) + +let locate_inductive r = + let (loc,qid) = qualid_of_reference r in + try match Syntax_def.locate_global qid with + | IndRef ind -> ind + | _ -> user_err_loc (loc,"",str "Inductive type expected") + with Not_found -> error_global_not_found_loc loc qid + +type whelp_request = + | Locate of string + | Elim of inductive + | Constr of string * env * constr + +let whelp = function + | Locate s -> whelp_locate s + | Elim ind -> whelp_elim ind + | Constr (s,env,c) -> whelp_constr env s c + +VERNAC ARGUMENT EXTEND whelp_constr_request +| [ "Match" ] -> [ "match" ] +| [ "Hint" ] -> [ "hint" ] +| [ "Instance" ] -> [ "instance" ] +END + +VERNAC COMMAND EXTEND Whelp +| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] +| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] +END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli new file mode 100644 index 0000000000..1871f39064 --- /dev/null +++ b/toplevel/whelp.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit -- cgit v1.2.3