1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 module MI = CicMkImplicit
27 module TC = CicTypeChecker
28 module PET = ProofEngineTypes
29 module PEH = ProofEngineHelpers
31 module S = CicSubstitution
32 module PT = PrimitiveTactics
34 module FNG = FreshNamesGenerator
36 let fail_msg1 = "no applicable simplification"
38 let error msg = raise (PET.Fail msg)
40 (* lapply *******************************************************************)
42 let strip_dependent_prods metasenv context t =
43 let irl = MI.identity_relocation_list_for_metavariable context in
44 let mk_meta metasenv t =
45 let index = MI.new_meta metasenv [] in
46 let metasenv = [index, context, t] @ metasenv in
47 metasenv, Cic.Meta (index, irl)
49 let rec aux metasenv metas = function
50 | Cic.Prod (Cic.Name _ as name, t1, t2) ->
51 let metasenv, meta = mk_meta metasenv t1 in
52 aux metasenv (meta :: metas) (S.subst meta t2)
53 | Cic.Prod (Cic.Anonymous, t1, _) ->
54 let metasenv, meta = mk_meta metasenv t1 in
55 metasenv, metas, Some meta
56 | t -> metasenv, metas, None
60 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
61 (* ?(substs = []) *) ?to_what what =
62 let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
63 let lapply_tac (proof, goal) =
64 let xuri, metasenv, u, t = proof in
65 let _, context, _ = CicUtil.lookup_meta goal metasenv in
66 let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
67 let lemma = FNG.clean_dummy_dependent_types lemma in
68 match strip_dependent_prods metasenv context lemma with
69 | metasenv, metas, Some meta ->
70 let pippo = Cic.Appl (what :: List.rev (meta :: metas)) in
71 Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr;
72 let outer_tac = letin_tac pippo in
73 let status = (xuri, metasenv, u, t), goal in
74 PET.apply_tactic outer_tac status
75 | metasenv, metas, None ->
76 failwith "lapply_tac: not implemented"
78 PET.mk_tactic lapply_tac
86 if p <= 0 then conts else aux (T.id_tac :: conts) (pred p)
90 let get_conclusion context t =
91 let rec aux p context = function
92 | Cic.Prod (name, t1, t2) ->
93 aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
94 | Cic.LetIn (name, u1, t2) ->
95 aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
96 | Cic.Cast (t2, t1) -> aux p context t2
100 let get_conclusion_dependences context t =
101 let p, context, conclusion = get_conclusion context t in
103 if q <= 0 then l else
104 let b = TC.does_not_occur context (pred q) q conclusion in
105 aux (b :: l) (pred q)
109 let solve_independents ?with_what deps =
110 let rec aux p conts = function
113 let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
114 aux (succ p) (cont :: conts) tl
115 | false :: tl -> aux (succ p) conts tl
117 let p, conts = aux 0 [] deps in
120 | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
122 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
123 (* ?(substs = []) *) ?to_what what =
124 let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
125 let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
126 let solve_conclusion_tac ?with_what p deps =
127 T.then_ ~start:(intros_tac ())
129 T.thens ~start:(PT.apply_tac what)
130 ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ]
131 (* skip_metas p @ solve_independents ?with_what deps *)
135 let lapply_tac (proof, goal) =
136 let xuri, metasenv, u, t = proof in
137 let _, context, _ = CicUtil.lookup_meta goal metasenv in
138 let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
139 let lemma = FNG.clean_dummy_dependent_types lemma in
140 match strip_dependent_prods metasenv context lemma with
141 | metasenv, p, Some premise, conclusion ->
142 let deps = get_conclusion_dependences context conclusion in
143 let inner_tac = match to_what with
145 T.thens ~start:(cut_tac premise)
147 solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
151 solve_conclusion_tac ~with_what p deps
154 T.thens ~start:(cut_tac conclusion)
155 ~continuations:[T.id_tac; T.id_tac (* inner_tac *)]
158 (* fwd **********************************************************************)
160 let fwd_simpl_tac ~what ~dbd =
161 let fwd_simpl_tac status =
162 let (proof, goal) = status in
163 let _, metasenv, _, _ = proof in
164 let _, context, ty = CicUtil.lookup_meta goal metasenv in
165 let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
166 match MetadataQuery.fwd_simpl ~dbd major with
167 | [] -> error fail_msg1
168 | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
170 PET.mk_tactic fwd_simpl_tac