diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/g_ltac2.ml4 | 16 | ||||
| -rw-r--r-- | src/tac2core.ml | 56 | ||||
| -rw-r--r-- | src/tac2entries.ml | 44 | ||||
| -rw-r--r-- | src/tac2entries.mli | 42 | ||||
| -rw-r--r-- | src/tac2intern.ml | 16 | ||||
| -rw-r--r-- | src/tac2print.ml | 2 | ||||
| -rw-r--r-- | theories/Constr.v | 7 | ||||
| -rw-r--r-- | theories/Env.v | 22 | ||||
| -rw-r--r-- | theories/Ltac2.v | 1 |
10 files changed, 147 insertions, 60 deletions
diff --git a/_CoqProject b/_CoqProject index 5af42197ea..15e02a6484 100644 --- a/_CoqProject +++ b/_CoqProject @@ -44,5 +44,6 @@ theories/Constr.v theories/Pattern.v theories/Fresh.v theories/Std.v +theories/Env.v theories/Notations.v theories/Ltac2.v diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 16e7278235..82ab53298e 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -81,14 +81,14 @@ let test_dollar_ident = end let tac2expr = Tac2entries.Pltac.tac2expr -let tac2type = Gram.entry_create "tactic:tac2type" -let tac2def_val = Gram.entry_create "tactic:tac2def_val" -let tac2def_typ = Gram.entry_create "tactic:tac2def_typ" -let tac2def_ext = Gram.entry_create "tactic:tac2def_ext" -let tac2def_syn = Gram.entry_create "tactic:tac2def_syn" -let tac2def_mut = Gram.entry_create "tactic:tac2def_mut" -let tac2def_run = Gram.entry_create "tactic:tac2def_run" -let tac2mode = Gram.entry_create "vernac:ltac2_command" +let tac2type = Entry.create "tactic:tac2type" +let tac2def_val = Entry.create "tactic:tac2def_val" +let tac2def_typ = Entry.create "tactic:tac2def_typ" +let tac2def_ext = Entry.create "tactic:tac2def_ext" +let tac2def_syn = Entry.create "tactic:tac2def_syn" +let tac2def_mut = Entry.create "tactic:tac2def_mut" +let tac2def_run = Entry.create "tactic:tac2def_run" +let tac2mode = Entry.create "vernac:ltac2_command" let ltac1_expr = Pltac.tactic_expr diff --git a/src/tac2core.ml b/src/tac2core.ml index d745d52c82..6ff353ce30 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -494,6 +494,26 @@ let () = define3 "constr_closenl" (list ident) int constr begin fun ids k c -> return (Value.of_constr ans) end +let () = define1 "constr_case" (repr_ext val_inductive) begin fun ind -> + Proofview.tclENV >>= fun env -> + try + let ans = Inductiveops.make_case_info env ind Constr.RegularStyle in + return (Value.of_ext Value.val_case ans) + with e when CErrors.noncritical e -> + throw err_notfound +end + +let () = define2 "constr_constructor" (repr_ext val_inductive) int begin fun (ind, i) k -> + Proofview.tclENV >>= fun env -> + try + let open Declarations in + let ans = Environ.lookup_mind ind env in + let _ = ans.mind_packets.(i).mind_consnames.(k) in + return (Value.of_ext val_constructor ((ind, i), (k + 1))) + with e when CErrors.noncritical e -> + throw err_notfound +end + let () = define3 "constr_in_context" ident constr closure begin fun id t c -> Proofview.Goal.goals >>= function | [gl] -> @@ -801,6 +821,42 @@ let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun avoid id -> return (Value.of_ident nid) end +(** Env *) + +let () = define1 "env_get" (list ident) begin fun ids -> + let r = match ids with + | [] -> None + | _ :: _ as ids -> + let (id, path) = List.sep_last ids in + let path = DirPath.make (List.rev path) in + let fp = Libnames.make_path path id in + try Some (Nametab.global_of_path fp) with Not_found -> None + in + return (Value.of_option Value.of_reference r) +end + +let () = define1 "env_expand" (list ident) begin fun ids -> + let r = match ids with + | [] -> [] + | _ :: _ as ids -> + let (id, path) = List.sep_last ids in + let path = DirPath.make (List.rev path) in + let qid = Libnames.make_qualid path id in + Nametab.locate_all qid + in + return (Value.of_list Value.of_reference r) +end + +let () = define1 "env_path" reference begin fun r -> + match Nametab.path_of_global r with + | fp -> + let (path, id) = Libnames.repr_path fp in + let path = DirPath.repr path in + return (Value.of_list Value.of_ident (List.rev_append path [id])) + | exception Not_found -> + throw err_notfound +end + (** ML types *) let constr_flags () = diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 8ebfeec948..c26fbdc478 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -22,28 +22,28 @@ open Tac2intern module Pltac = struct -let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr" - -let q_ident = Pcoq.Gram.entry_create "tactic:q_ident" -let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings" -let q_with_bindings = Pcoq.Gram.entry_create "tactic:q_with_bindings" -let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern" -let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns" -let q_destruction_arg = Pcoq.Gram.entry_create "tactic:q_destruction_arg" -let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause" -let q_conversion = Pcoq.Gram.entry_create "tactic:q_conversion" -let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting" -let q_clause = Pcoq.Gram.entry_create "tactic:q_clause" -let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch" -let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences" -let q_reference = Pcoq.Gram.entry_create "tactic:q_reference" -let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag" -let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching" -let q_goal_matching = Pcoq.Gram.entry_create "tactic:q_goal_matching" -let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb" -let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location" -let q_pose = Pcoq.Gram.entry_create "tactic:q_pose" -let q_assert = Pcoq.Gram.entry_create "tactic:q_assert" +let tac2expr = Pcoq.Entry.create "tactic:tac2expr" + +let q_ident = Pcoq.Entry.create "tactic:q_ident" +let q_bindings = Pcoq.Entry.create "tactic:q_bindings" +let q_with_bindings = Pcoq.Entry.create "tactic:q_with_bindings" +let q_intropattern = Pcoq.Entry.create "tactic:q_intropattern" +let q_intropatterns = Pcoq.Entry.create "tactic:q_intropatterns" +let q_destruction_arg = Pcoq.Entry.create "tactic:q_destruction_arg" +let q_induction_clause = Pcoq.Entry.create "tactic:q_induction_clause" +let q_conversion = Pcoq.Entry.create "tactic:q_conversion" +let q_rewriting = Pcoq.Entry.create "tactic:q_rewriting" +let q_clause = Pcoq.Entry.create "tactic:q_clause" +let q_dispatch = Pcoq.Entry.create "tactic:q_dispatch" +let q_occurrences = Pcoq.Entry.create "tactic:q_occurrences" +let q_reference = Pcoq.Entry.create "tactic:q_reference" +let q_strategy_flag = Pcoq.Entry.create "tactic:q_strategy_flag" +let q_constr_matching = Pcoq.Entry.create "tactic:q_constr_matching" +let q_goal_matching = Pcoq.Entry.create "tactic:q_goal_matching" +let q_hintdb = Pcoq.Entry.create "tactic:q_hintdb" +let q_move_location = Pcoq.Entry.create "tactic:q_move_location" +let q_pose = Pcoq.Entry.create "tactic:q_pose" +let q_assert = Pcoq.Entry.create "tactic:q_assert" end (** Tactic definition *) diff --git a/src/tac2entries.mli b/src/tac2entries.mli index 37944981d7..f97e35fec0 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -56,32 +56,32 @@ val backtrace : backtrace Exninfo.t module Pltac : sig -val tac2expr : raw_tacexpr Pcoq.Gram.entry +val tac2expr : raw_tacexpr Pcoq.Entry.t (** Quoted entries. To be used for complex notations. *) open Tac2qexpr -val q_ident : Id.t CAst.t or_anti Pcoq.Gram.entry -val q_bindings : bindings Pcoq.Gram.entry -val q_with_bindings : bindings Pcoq.Gram.entry -val q_intropattern : intro_pattern Pcoq.Gram.entry -val q_intropatterns : intro_pattern list CAst.t Pcoq.Gram.entry -val q_destruction_arg : destruction_arg Pcoq.Gram.entry -val q_induction_clause : induction_clause Pcoq.Gram.entry -val q_conversion : conversion Pcoq.Gram.entry -val q_rewriting : rewriting Pcoq.Gram.entry -val q_clause : clause Pcoq.Gram.entry -val q_dispatch : dispatch Pcoq.Gram.entry -val q_occurrences : occurrences Pcoq.Gram.entry -val q_reference : reference or_anti Pcoq.Gram.entry -val q_strategy_flag : strategy_flag Pcoq.Gram.entry -val q_constr_matching : constr_matching Pcoq.Gram.entry -val q_goal_matching : goal_matching Pcoq.Gram.entry -val q_hintdb : hintdb Pcoq.Gram.entry -val q_move_location : move_location Pcoq.Gram.entry -val q_pose : pose Pcoq.Gram.entry -val q_assert : assertion Pcoq.Gram.entry +val q_ident : Id.t CAst.t or_anti Pcoq.Entry.t +val q_bindings : bindings Pcoq.Entry.t +val q_with_bindings : bindings Pcoq.Entry.t +val q_intropattern : intro_pattern Pcoq.Entry.t +val q_intropatterns : intro_pattern list CAst.t Pcoq.Entry.t +val q_destruction_arg : destruction_arg Pcoq.Entry.t +val q_induction_clause : induction_clause Pcoq.Entry.t +val q_conversion : conversion Pcoq.Entry.t +val q_rewriting : rewriting Pcoq.Entry.t +val q_clause : clause Pcoq.Entry.t +val q_dispatch : dispatch Pcoq.Entry.t +val q_occurrences : occurrences Pcoq.Entry.t +val q_reference : reference or_anti Pcoq.Entry.t +val q_strategy_flag : strategy_flag Pcoq.Entry.t +val q_constr_matching : constr_matching Pcoq.Entry.t +val q_goal_matching : goal_matching Pcoq.Entry.t +val q_hintdb : hintdb Pcoq.Entry.t +val q_move_location : move_location Pcoq.Entry.t +val q_pose : pose Pcoq.Entry.t +val q_assert : assertion Pcoq.Entry.t end (** {5 Hooks} *) diff --git a/src/tac2intern.ml b/src/tac2intern.ml index f3b222df21..ff8fb4c0f4 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -356,8 +356,8 @@ let rec unify0 env t1 t2 = match kind env t1, kind env t2 with let unify ?loc env t1 t2 = try unify0 env t1 t2 with CannotUnify (u1, u2) -> - user_err ?loc (str "This expression has type " ++ pr_glbtype env t1 ++ - str " but an expression was expected of type " ++ pr_glbtype env t2) + user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++ + spc () ++ str "but an expression was expected of type" ++ spc () ++ pr_glbtype env t2) let unify_arrow ?loc env ft args = let ft0 = ft in @@ -372,11 +372,11 @@ let unify_arrow ?loc env ft args = iter ft args true | GTypRef _, _ :: _ -> if is_fun then - user_err ?loc (str "This function has type " ++ pr_glbtype env ft0 ++ - str " and is applied to too many arguments") + user_err ?loc (str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++ + spc () ++ str "and is applied to too many arguments") else - user_err ?loc (str "This expression has type " ++ pr_glbtype env ft0 ++ - str " and is not a function") + user_err ?loc (str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++ + spc () ++ str "and is not a function") in iter ft args false @@ -475,13 +475,13 @@ let check_elt_empty loc env t = match kind env t with | GTypVar _ -> user_err ?loc (str "Cannot infer an empty type for this expression") | GTypArrow _ | GTypRef (Tuple _, _) -> - user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type") + user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type") | GTypRef (Other kn, _) -> let def = Tac2env.interp_type kn in match def with | _, GTydAlg { galg_constructors = [] } -> kn | _ -> - user_err ?loc (str "Type " ++ pr_glbtype env t ++ str " is not an empty type") + user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type") let check_unit ?loc t = let env = empty_env () in diff --git a/src/tac2print.ml b/src/tac2print.ml index cab1530d15..9c530dfc51 100644 --- a/src/tac2print.ml +++ b/src/tac2print.ml @@ -49,7 +49,7 @@ let pr_glbtype_gen pr lvl c = | T5_r | T5_l | T2 | T1 -> fun x -> x | T0 -> paren in - paren (pr_glbtype lvl t ++ spc () ++ pr_typref kn) + paren (pr_glbtype T1 t ++ spc () ++ pr_typref kn) | GTypRef (Other kn, tl) -> let paren = match lvl with | T5_r | T5_l | T2 | T1 -> fun x -> x diff --git a/theories/Constr.v b/theories/Constr.v index 072c613920..d8d222730e 100644 --- a/theories/Constr.v +++ b/theories/Constr.v @@ -57,6 +57,13 @@ Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "con (** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *) +Ltac2 @ external case : inductive -> case := "ltac2" "constr_case". +(** Generate the case information for a given inductive type. *) + +Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "constr_constructor". +(** Generate the i-th constructor for a given inductive type. Indexing starts + at 0. Panics if there is no such constructor. *) + End Unsafe. Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context". diff --git a/theories/Env.v b/theories/Env.v new file mode 100644 index 0000000000..7e36aa7990 --- /dev/null +++ b/theories/Env.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* 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. +Require Import Std. + +Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get". +(** Returns the global reference corresponding to the absolute name given as + argument if it exists. *) + +Ltac2 @ external expand : ident list -> Std.reference list := "ltac2" "env_expand". +(** Returns the list of all global references whose absolute name contains + the argument list as a prefix. *) + +Ltac2 @ external path : Std.reference -> ident list := "ltac2" "env_path". +(** Returns the absolute name of the given reference. Panics if the reference + does not exist. *) diff --git a/theories/Ltac2.v b/theories/Ltac2.v index 7b2f592ac6..3fe71f4c65 100644 --- a/theories/Ltac2.v +++ b/theories/Ltac2.v @@ -18,4 +18,5 @@ Require Ltac2.Control. Require Ltac2.Fresh. Require Ltac2.Pattern. Require Ltac2.Std. +Require Ltac2.Env. Require Export Ltac2.Notations. |