aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Array.v14
-rw-r--r--theories/Constr.v43
-rw-r--r--theories/Control.v49
-rw-r--r--theories/Init.v56
-rw-r--r--theories/Int.v18
-rw-r--r--theories/Ltac2.v16
-rw-r--r--theories/Message.v20
-rw-r--r--theories/String.v14
8 files changed, 230 insertions, 0 deletions
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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 @external make : int -> '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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 @ external type : constr -> 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+(** Panic *)
+
+Ltac2 @ external throw : exn -> '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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Declare ML Module "ltac2_plugin".
+
+Global Set Default Proof Mode "Ltac2".
+
+(** Primitive types *)
+
+Ltac2 Type int.
+Ltac2 Type string.
+Ltac2 Type char.
+Ltac2 Type ident.
+
+(** Constr-specific built-in types *)
+Ltac2 Type meta.
+Ltac2 Type evar.
+Ltac2 Type sort.
+Ltac2 Type cast.
+Ltac2 Type instance.
+Ltac2 Type constant.
+Ltac2 Type inductive.
+Ltac2 Type constructor.
+Ltac2 Type projection.
+Ltac2 Type constr.
+
+Ltac2 Type message.
+Ltac2 Type exn := [ .. ].
+Ltac2 Type 'a array.
+
+(** Pervasive types *)
+
+Ltac2 Type 'a option := [ None | Some ('a) ].
+
+Ltac2 Type 'a ref := { mutable contents : 'a }.
+
+Ltac2 Type bool := [ true | false ].
+
+(** Pervasive exceptions *)
+
+Ltac2 Type exn ::= [ Out_of_bounds ].
+(** Used for bound checking, e.g. with String and Array. *)
+
+Ltac2 Type exn ::= [ Not_focussed ].
+(** In Ltac2, the notion of "current environment" only makes sense when there is
+ at most one goal under focus. Contrarily to Ltac1, instead of dynamically
+ focussing when we need it, we raise this non-backtracking error when it does
+ not make sense. *)
+
+Ltac2 Type exn ::= [ Not_found ].
+(** Used when something is missing. *)
diff --git a/theories/Int.v b/theories/Int.v
new file mode 100644
index 0000000000..0a90d757b6
--- /dev/null
+++ b/theories/Int.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 Type exn ::= [ Division_by_zero ].
+
+Ltac2 @ external equal : int -> 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Export Ltac2.Init.
+
+Require Ltac2.Int.
+Require Ltac2.String.
+Require Ltac2.Array.
+Require Ltac2.Message.
+Require Ltac2.Constr.
+Require Ltac2.Control.
diff --git a/theories/Message.v b/theories/Message.v
new file mode 100644
index 0000000000..b2159612cb
--- /dev/null
+++ b/theories/Message.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 @ external print : message -> 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 @external make : int -> 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".
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:07:36 +0000