1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Util
open Names
open Term
open Ltac_plugin
open Tacinterp
open Glob_term
open Tacmach
open Tacticals
open Ssrcommon
(* The table and its display command *)
(* FIXME this looks hackish *)
let viewtab : glob_constr list array = Array.make 3 []
let _ =
let init () = Array.fill viewtab 0 3 [] in
let freeze _ = Array.copy viewtab in
let unfreeze vt = Array.blit vt 0 viewtab 0 3 in
Summary.declare_summary "ssrview"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init }
(* Populating the table *)
let cache_viewhint (_, (i, lvh)) =
let mem_raw h = List.exists (Glob_ops.glob_constr_eq h) in
let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in
viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i)
let subst_viewhint ( subst, (i, lvh as ilvh)) =
let lvh' = List.smartmap (Detyping.subst_glob_constr subst) lvh in
if lvh' == lvh then ilvh else i, lvh'
let classify_viewhint x = Libobject.Substitute x
let in_viewhint =
Libobject.declare_object {(Libobject.default_object "VIEW_HINTS") with
Libobject.open_function = (fun i o -> if i = 1 then cache_viewhint o);
Libobject.cache_function = cache_viewhint;
Libobject.subst_function = subst_viewhint;
Libobject.classify_function = classify_viewhint }
let glob_view_hints lvh =
let env = Global.env () in
List.map (Constrintern.intern_constr env Evd.(from_env env)) lvh
let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
let interp_view ist si env sigma gv rv rid =
match DAst.get rv with
| GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) ->
let loc = rv.CAst.loc in
let rv = DAst.make ?loc @@ GApp (rid, rargs) in
snd (interp_open_constr ist (re_sig si sigma) (rv, None))
| _ ->
let interp rc rargs =
interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in
let rec simple_view rargs n =
if n < 0 then view_error "use" gv else
try interp rv rargs with _ -> simple_view (mkRHole :: rargs) (n - 1) in
let view_nbimps = interp_view_nbimps ist (re_sig si sigma) rv in
let view_args = [mkRApp rv (mkRHoles view_nbimps); rid] in
let rec view_with = function
| [] -> simple_view [rid] (interp_nbargs ist (re_sig si sigma) rv)
| hint :: hints -> try interp hint view_args with _ -> view_with hints in
snd (view_with (if view_nbimps < 0 then [] else viewtab.(0)))
let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr =
let c2r ist x = { ist with lfun =
Id.Map.add top_id (Value.of_constr x) ist.lfun } in
let terminate (sigma, c') =
let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
let c' = Reductionops.nf_evar sigma c' in
let n, c', _, ucst = without_ctx pf_abs_evars gl0 (sigma, c') in
let c' = if not prune then c' else without_ctx pf_abs_cterm gl0 n c' in
let gl0 = pf_merge_uc ucst gl0 in
let gl0, ap =
let gl0, ctx = pull_ctx gl0 in
let gl0, ap = pf_abs_prod name gl0 c' (Termops.prod_applist sigma cl [c]) in
push_ctx ctx gl0, ap in
let gl0 = pf_merge_uc_of sigma gl0 in
ap, c', gl0 in
let rec loop (sigma, c') = function
| [] ->
let ap, c', gl = terminate (sigma, c') in
ap, c', conclude ap c' gl
| f :: view ->
let ist, rid =
match EConstr.kind sigma c' with
| Var id -> ist,mkRVar id
| _ -> c2r ist c',mkRltacVar top_id in
let v = intern_term ist env f in
loop (interp_view ist si env sigma f v rid) view
in loop
let pfa_with_view ist ?(next=ref []) (prune, view) cl c conclude clr gl =
let env, sigma, si =
without_ctx pf_env gl, Refiner.project gl, without_ctx sig_it gl in
with_view
ist ~next si env gl c (constr_name sigma c) cl prune conclude clr (sigma, c) view
let pf_with_view_linear ist gl v cl c =
let x,y,gl =
pfa_with_view ist v cl c (fun _ _ -> tac_ctx tclIDTAC) []
(push_ctx (new_ctx ()) gl) in
let gl, _ = pull_ctxs gl in
assert(List.length (sig_it gl) = 1);
x,y,re_sig (List.hd (sig_it gl)) (Refiner.project gl)
(* vim: set filetype=ocaml foldmethod=marker: *)
|
