From c25e86e6b4e8bb694d3c8e50f04a92cc33ad807d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 24 Jul 2017 17:41:01 +0200 Subject: Turning the ltac2 subfolder into a standalone plugin. --- theories/Array.v | 14 ++++++++++++++ theories/Constr.v | 43 +++++++++++++++++++++++++++++++++++++++++ theories/Control.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++ theories/Init.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ theories/Int.v | 18 ++++++++++++++++++ theories/Ltac2.v | 16 ++++++++++++++++ theories/Message.v | 20 +++++++++++++++++++ theories/String.v | 14 ++++++++++++++ 8 files changed, 230 insertions(+) create mode 100644 theories/Array.v create mode 100644 theories/Constr.v create mode 100644 theories/Control.v create mode 100644 theories/Init.v create mode 100644 theories/Int.v create mode 100644 theories/Ltac2.v create mode 100644 theories/Message.v create mode 100644 theories/String.v (limited to 'theories') diff --git a/theories/Array.v b/theories/Array.v new file mode 100644 index 0000000000..11b64e3515 --- /dev/null +++ b/theories/Array.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a -> 'a array := "ltac2" "array_make". +Ltac2 @external length : 'a array -> int := "ltac2" "array_length". +Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get". +Ltac2 @external set : 'a array -> int -> 'a -> unit := "ltac2" "array_set". diff --git a/theories/Constr.v b/theories/Constr.v new file mode 100644 index 0000000000..c340e3aa87 --- /dev/null +++ b/theories/Constr.v @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr := "ltac2" "constr_type". +(** Return the type of a term *) + +Ltac2 @ external equal : constr -> constr -> bool := "ltac2" "constr_equal". +(** Strict syntactic equality: only up to α-conversion and evar expansion *) + +Module Unsafe. + +(** Low-level access to kernel term. Use with care! *) + +Ltac2 Type kind := [ +| Rel (int) +| Var (ident) +| Meta (meta) +| Evar (evar, constr list) +| Sort (sort) +| Cast (constr, cast, constr) +| Prod (ident option, constr, constr) +| Lambda (ident option, constr, constr) +| LetIn (ident option, constr, constr, constr) +| App (constr, constr list) +| Constant (constant, instance) +| Ind (inductive, instance) +| Constructor (inductive, instance) +(* + | Case of case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) pfixpoint + | CoFix of ('constr, 'types) pcofixpoint +*) +| Proj (projection, constr) +]. + +End Unsafe. diff --git a/theories/Control.v b/theories/Control.v new file mode 100644 index 0000000000..3bc572547c --- /dev/null +++ b/theories/Control.v @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a := "ltac2" "throw". +(** Fatal exception throwing. This does not induce backtracking. *) + +(** Generic backtracking control *) + +Ltac2 @ external zero : exn -> 'a := "ltac2" "zero". +Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "ltac2" "plus". +Ltac2 @ external once : (unit -> 'a) -> 'a := "ltac2" "once". +Ltac2 @ external dispatch : (unit -> unit) list -> unit := "ltac2" "dispatch". +Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit := "ltac2" "extend". +Ltac2 @ external enter : (unit -> unit) -> unit := "ltac2" "enter". + +(** Proof state manipulation *) + +Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "ltac2" "focus". +Ltac2 @ external shelve : unit -> unit := "ltac2" "shelve". +Ltac2 @ external shelve_unifiable : unit -> unit := "ltac2" "shelve_unifiable". + +Ltac2 @ external new_goal : evar -> unit := "ltac2" "new_goal". +(** Adds the given evar to the list of goals as the last one. If it is + already defined in the current state, don't do anything. Panics if the + evar is not in the current state. *) + +(** Goal inspection *) + +Ltac2 @ external goal : unit -> constr := "ltac2" "goal". +(** Panics if there is not exactly one goal under focus. Otherwise returns + the conclusion of this goal. *) + +Ltac2 @ external hyp : ident -> constr := "ltac2" "hyp". +(** Panics if there is more than one goal under focus. If there is no + goal under focus, looks for the section variable with the given name. + If there is one, looks for the hypothesis with the given name. *) + +(** Refinement *) + +Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine". diff --git a/theories/Init.v b/theories/Init.v new file mode 100644 index 0000000000..1d2d40f5c0 --- /dev/null +++ b/theories/Init.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* int -> bool := "ltac2" "int_equal". +Ltac2 @ external compare : int -> int -> int := "ltac2" "int_compare". +Ltac2 @ external add : int -> int -> int := "ltac2" "int_add". +Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub". +Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul". +Ltac2 @ external neg : int -> int := "ltac2" "int_neg". diff --git a/theories/Ltac2.v b/theories/Ltac2.v new file mode 100644 index 0000000000..221f7be424 --- /dev/null +++ b/theories/Ltac2.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit := "ltac2" "print". + +Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string". + +Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int". + +Ltac2 @ external of_constr : constr -> message := "ltac2" "message_of_constr". +(** Panics if there is more than one goal under focus. *) + +Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat". diff --git a/theories/String.v b/theories/String.v new file mode 100644 index 0000000000..99e1dab76b --- /dev/null +++ b/theories/String.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* char -> string := "ltac2" "string_make". +Ltac2 @external length : string -> int := "ltac2" "string_length". +Ltac2 @external get : string -> int -> char := "ltac2" "string_get". +Ltac2 @external set : string -> int -> char -> unit := "ltac2" "string_set". -- cgit v1.2.3