summaryrefslogtreecommitdiff
path: root/plugins/quote
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/quote')
-rw-r--r--plugins/quote/Quote.v2
-rw-r--r--plugins/quote/g_quote.ml425
-rw-r--r--plugins/quote/quote.ml113
3 files changed, 77 insertions, 63 deletions
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index 92e5c75c..ca1a18e8 100644
--- a/plugins/quote/Quote.v
+++ b/plugins/quote/Quote.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e2c9dbaa..e27fe7f4 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -1,22 +1,31 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
-open Util
+open Names
+open Misctypes
open Tacexpr
+open Geninterp
open Quote
-let make_cont k x =
- let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in
- let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
- let tac = <:tactic<let cont := $k in cont $x>> in
- Tacinterp.interp tac
+DECLARE PLUGIN "quote_plugin"
+
+let loc = Loc.ghost
+let cont = (loc, Id.of_string "cont")
+let x = (loc, Id.of_string "x")
+
+let make_cont (k : glob_tactic_expr) (c : Constr.t) =
+ let c = Tacinterp.Value.of_constr c in
+ let tac = TacCall (loc, ArgVar cont, [Reference (ArgVar x)]) in
+ let tac = TacLetIn (false, [(cont, Tacexp k)], TacArg (loc, tac)) in
+ let ist = { lfun = Id.Map.singleton (snd x) c; extra = TacStore.empty; } in
+ Tacinterp.eval_tactic_ist ist tac
TACTIC EXTEND quote
[ "quote" ident(f) ] -> [ quote f [] ]
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 48c67089..637e0e28 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -101,15 +101,14 @@
(*i*)
-open Pp
+open Errors
open Util
open Names
open Term
open Pattern
-open Matching
+open Patternops
+open Constr_matching
open Tacmach
-open Tactics
-open Tacexpr
(*i*)
(*s First, we need to access some Coq constants
@@ -190,16 +189,16 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
type [typ] *)
let coerce_meta_out id =
- let s = string_of_id id in
+ let s = Id.to_string id in
int_of_string (String.sub s 1 (String.length s - 1))
let coerce_meta_in n =
- id_of_string ("M" ^ string_of_int n)
+ Id.of_string ("M" ^ string_of_int n)
let compute_lhs typ i nargsi =
match kind_of_term typ with
- | Ind(sp,0) ->
+ | Ind((sp,0),u) ->
let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
- mkApp (mkConstruct ((sp,0),i+1), argsi)
+ mkApp (mkConstructU (((sp,0),i+1),u), argsi)
| _ -> i_can't_do_that ()
(*s This function builds the pattern from the RHS. Recursive calls are
@@ -208,29 +207,29 @@ let compute_lhs typ i nargsi =
let compute_rhs bodyi index_of_f =
let rec aux c =
match kind_of_term c with
- | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) ->
- let i = destRel (array_last args) in
+ | App (j, args) when isRel j && Int.equal (destRel j) index_of_f (* recursive call *) ->
+ let i = destRel (Array.last args) in
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
- PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
+ PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
| Cast (c,_,_) -> aux c
- | _ -> snd (pattern_of_constr Evd.empty c)
+ | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
in
aux bodyi
(*s Now the function [compute_ivs] itself *)
-let compute_ivs gl f cs =
- let cst =
- try destConst f
- with e when Errors.noncritical e -> i_can't_do_that ()
- in
- let body = Environ.constant_value (Global.env()) cst in
+let compute_ivs f cs gl =
+ let cst = try destConst f with DestKO -> i_can't_do_that () in
+ let body = Environ.constant_value_in (Global.env()) cst in
match decomp_term body with
| Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
let (args3, body3) = decompose_lam body2 in
let nargs3 = List.length args3 in
- begin match decomp_term body3 with
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let is_conv = Reductionops.is_conv env sigma in
+ begin match decomp_term body3 with
| Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
let n_lhs_rhs = ref []
and v_lhs = ref (None : constr option)
@@ -243,14 +242,13 @@ let compute_ivs gl f cs =
(* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *)
(* REL 1 to REL nargsi are argsi (reverse order) *)
(* First we test if the RHS is the RHS for constants *)
- if isRel bodyi && destRel bodyi = 1 then
+ if isRel bodyi && Int.equal (destRel bodyi) 1 then
c_lhs := Some (compute_lhs (snd (List.hd args3))
i nargsi)
(* Then we test if the RHS is the RHS for variables *)
else begin match decompose_app bodyi with
| vmf, [_; _; a3; a4 ]
- when isRel a3 & isRel a4 &
- pf_conv_x gl vmf
+ when isRel a3 && isRel a4 && is_conv vmf
(Lazy.force coq_varmap_find)->
v_lhs := Some (compute_lhs
(snd (List.hd args3))
@@ -264,7 +262,7 @@ let compute_ivs gl f cs =
end)
lci;
- if !c_lhs = None & !v_lhs = None then i_can't_do_that ();
+ if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that ();
(* The Cases predicate is a lambda; we assume no dependency *)
let p = match kind_of_term p with
@@ -299,10 +297,10 @@ binary search trees (see file \texttt{Quote.v}) *)
and variables (open terms) *)
let rec closed_under cset t =
- (ConstrSet.mem t cset) or
+ (ConstrSet.mem t cset) ||
(match (kind_of_term t) with
| Cast(c,_,_) -> closed_under cset c
- | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l
+ | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l
| _ -> false)
(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
@@ -342,8 +340,8 @@ let path_of_int n =
(* returns the list of digits of n in reverse order with
initial 1 removed *)
let rec digits_of_int n =
- if n=1 then []
- else (n mod 2 = 1)::(digits_of_int (n lsr 1))
+ if Int.equal n 1 then []
+ else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
in
List.fold_right
(fun b c -> mkApp ((if b then Lazy.force coq_Right_idx
@@ -361,9 +359,9 @@ let path_of_int n =
(* This function does not descend under binders (lambda and Cases) *)
let rec subterm gl (t : constr) (t' : constr) =
- (pf_conv_x gl t t') or
+ (pf_conv_x gl t t') ||
(match (kind_of_term t) with
- | App (f,args) -> array_exists (fun t -> subterm gl t t') args
+ | App (f,args) -> Array.exists (fun t -> subterm gl t t') args
| Cast(t,_,_) -> (subterm gl t t')
| _ -> false)
@@ -393,7 +391,7 @@ module Constrhash = Hashtbl.Make
[ivs : inversion_scheme]\\
[lc: constr list]\\
[gl: goal sigma]\\ *)
-let quote_terms ivs lc gl =
+let quote_terms ivs lc =
Coqlib.check_required_library ["Coq";"quote";"Quote"];
let varhash = (Constrhash.create 17 : constr Constrhash.t) in
let varlist = ref ([] : constr list) in (* list of variables *)
@@ -403,7 +401,7 @@ let quote_terms ivs lc gl =
match l with
| (lhs, rhs)::tail ->
begin try
- let s1 = matches rhs c in
+ let s1 = Id.Map.bindings (matches (Global.env ()) Evd.empty rhs c) in
let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
in
Termops.subst_meta s2 lhs
@@ -414,7 +412,7 @@ let quote_terms ivs lc gl =
| None ->
begin match ivs.constant_lhs with
| Some c_lhs -> Termops.subst_meta [1, c] c_lhs
- | None -> anomaly "invalid inversion scheme for quote"
+ | None -> anomaly (Pp.str "invalid inversion scheme for quote")
end
| Some var_lhs ->
begin match ivs.constant_lhs with
@@ -440,36 +438,43 @@ let quote_terms ivs lc gl =
auxl ivs.normal_lhs_rhs
in
let lp = List.map aux lc in
- (lp, (btree_of_array (Array.of_list (List.rev !varlist))
- ivs.return_type ))
+ (lp, (btree_of_array (Array.of_list (List.rev !varlist))
+ ivs.return_type ))
(*s actually we could "quote" a list of terms instead of a single
term. Ring for example needs that, but Ring doesn't use Quote
yet. *)
-let quote f lid gl =
- let f = pf_global gl f in
- let cl = List.map (pf_global gl) lid in
- let ivs = compute_ivs gl f cl in
- let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with
- | [p], vm -> (p,vm)
- | _ -> assert false
- in
- match ivs.variable_lhs with
- | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
- | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
-
-let gen_quote cont c f lid gl =
- let f = pf_global gl f in
- let cl = List.map (pf_global gl) lid in
- let ivs = compute_ivs gl f cl in
- let (p, vm) = match quote_terms ivs [c] gl with
+let quote f lid =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let f = Tacmach.New.pf_global f gl in
+ let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+ let ivs = compute_ivs f cl gl in
+ let concl = Proofview.Goal.concl gl in
+ let quoted_terms = quote_terms ivs [concl] in
+ let (p, vm) = match quoted_terms with
+ | [p], vm -> (p,vm)
+ | _ -> assert false
+ in
+ match ivs.variable_lhs with
+ | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+ | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+ end
+
+let gen_quote cont c f lid =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let f = Tacmach.New.pf_global f gl in
+ let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+ let ivs = compute_ivs f cl gl in
+ let quoted_terms = quote_terms ivs [c] in
+ let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
in
match ivs.variable_lhs with
- | None -> cont (mkApp (f, [| p |])) gl
- | Some _ -> cont (mkApp (f, [| vm; p |])) gl
+ | None -> cont (mkApp (f, [| p |]))
+ | Some _ -> cont (mkApp (f, [| vm; p |]))
+ end
(*i
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 01:47:58 +0000