diff options
Diffstat (limited to 'plugins/quote')
-rw-r--r-- | plugins/quote/Quote.v | 2 | ||||
-rw-r--r-- | plugins/quote/g_quote.ml4 | 25 | ||||
-rw-r--r-- | plugins/quote/quote.ml | 113 |
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 |