Columbo aufrufen.mlg zum Wurzelverzeichnis wechselnHaskell {Haskell[106] Coq[108] Abap[248]}Datei anzeigen
DECLARE PLUGIN "tuto1_plugin"
{
(* If we forget this line and include our own tactic definition using
TACTIC EXTEND, as below, then we get the strange error message
no implementation available for Tacentries, only when compiling
theories/Loader.v
*)
open Ltac_plugin
open Attributes
open Pp
(* This module defines the types of arguments to be used in the
EXTEND directives below, for example the string one. *)
open Stdarg
}
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "Hello" string(s) ] ->
{ Feedback.msg_notice (strbrk "Hello " ++ str s) }
END
(* reference is allowed as a syntactic entry, but so are all the entries
found the signature of module Prim in file coq/parsing/pcoq.mli *)
VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
| [ "HelloAgain" reference(r)] ->
(* The function Ppconstr.pr_qualid was found by searching all mli files
for a function of type qualid -> Pp.t *)
{ Feedback.msg_notice
(strbrk "Hello again " ++ Ppconstr.pr_qualid r)}
END
(* According to parsing/pcoq.mli, e has type constr_expr *)
(* this type is defined in pretyping/constrexpr.ml *)
(* Question for the developers: why is the file constrexpr.ml and not
constrexpr.mli --> Easier for packing the software in components. *)
VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
| [ "Cmd1" constr(e) ] ->
{ let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") }
END
(* The next step is to make something of parsed expression.
Interesting information in interp/constrintern.mli *)
(* There are several phases of transforming a parsed expression into
the final internal data-type (constr). There exists a collection of
functions that combine all the phases *)
VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
| [ "Cmd2" constr(e) ] ->
{ let _ = Constrintern.interp_constr
(Global.env())
(* Make sure you don't use Evd.empty here, as this does not
check consistency with existing universe constraints. *)
(Evd.from_env (Global.env())) e in
Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") }
END
(* This is to show what happens when typing in an empty environment
with an empty evd.
Question for the developers: why does "Cmd3 (fun x : nat => x)."
raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
| [ "Cmd3" constr(e) ] ->
{ let _ = Constrintern.interp_constr Environ.empty_env
Evd.empty e in
Feedback.msg_notice
(strbrk "Cmd3 accepted something in the empty context")}
END
(* When adding a definition, we have to be careful that just
the operation of constructing a well-typed term may already change
the environment, at the level of universe constraints (which
are recorded in the evd component). The function
Constrintern.interp_constr ignores this side-effect, so it should
not be used here. *)
(* Looking at the interface file interp/constrintern.ml4, I lost
some time because I did not see that the "constr" type appearing
there was "EConstr.constr" and not "Constr.constr". *)
VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] ->
{ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
Simple_declare.packed_declare_definition ~poly i v }
END
VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
| [ "Cmd5" constr(e) ] ->
{ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
let (_, ctx) = v in
let sigma = Evd.from_ctx ctx in
Feedback.msg_notice
(Printer.pr_econstr_env (Global.env()) sigma
(Simple_check.simple_check1 v)) }
END
VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
| [ "Cmd6" constr(e) ] ->
{ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
let sigma, ty = Simple_check.simple_check2 v in
Feedback.msg_notice
(Printer.pr_econstr_env (Global.env()) sigma ty) }
END
VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
| [ "Cmd7" constr(e) ] ->
{ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
let (a, ctx) = v in
let sigma = Evd.from_ctx ctx in
Feedback.msg_notice
(Printer.pr_econstr_env (Global.env()) sigma
(Simple_check.simple_check3 v)) }
END
(* This command takes a name and return its value. It does less
than Print, because it fails on constructors, axioms, and inductive types.
This should be improved, because the error message is an anomaly.
Anomalies should never appear even when using a command outside of its
intended use. *)
VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
| [ "Cmd8" reference(r) ] ->
{ let env = Global.env() in
let sigma = Evd.from_env env in
Feedback.msg_notice
(Printer.pr_econstr_env env sigma
(EConstr.of_constr
(Simple_print.simple_body_access (Nametab.global r)))) }
END
TACTIC EXTEND my_intro
| [ "my_intro" ident(i) ] ->
{ Tactics.introduction i }
END
(* if one write this:
VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
it gives an error message that is basically impossible to understand. *)
VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
| ![ proof ] [ "Cmd9" ] ->
{ fun ~pstate ->
Option.iter (fun (pstate : Proof_global.t) ->
let sigma, env = Pfedit.get_current_context pstate in
let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
Feedback.msg_notice
(Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate;
pstate }
END
[ Original von:0.287Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
]
