]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/proofEngineHelpers.ml
dependencies between statuses simplified
[helm.git] / helm / software / components / tactics / proofEngineHelpers.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 exception Bad_pattern of string Lazy.t
29
30 let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
31   CicMkImplicit.new_meta metasenv subst
32
33 let subst_meta_in_proof proof meta term newmetasenv =
34  let uri,metasenv,initial_subst,bo,ty, attrs = proof in
35    (* empty context is ok for term since it wont be used by apply_subst *)
36    (* hack: since we do not know the context and the type of term, we
37       create a substitution with cc =[] and type = Implicit; they will be
38       in  any case dropped by apply_subst, but it would be better to rewrite
39       the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
40   let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
41    let metasenv' =
42     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
43    in
44     let metasenv'' =
45      List.map
46       (function i,canonical_context,ty ->
47         let canonical_context' =
48          List.map
49           (function
50               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
51             | None -> None
52             | Some (n,Cic.Def (bo,ty)) ->
53                Some (n,Cic.Def (subst_in bo,subst_in ty))
54           ) canonical_context
55         in
56          i,canonical_context',(subst_in ty)
57       ) metasenv'
58     in
59      let bo' = lazy (subst_in (Lazy.force bo)) in
60      (* Metavariables can appear also in the *statement* of the theorem
61       * since the parser does not reject as statements terms with
62       * metavariable therein *)
63      let ty' = subst_in ty in
64       let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
65        (newproof, metasenv'')
66
67 (*CSC: commento vecchio *)
68 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
69 (* This (heavy) function must be called when a tactic can instantiate old *)
70 (* metavariables (i.e. existential variables). It substitues the metasenv *)
71 (* of the proof with the result of removing [meta] from the domain of     *)
72 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
73 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
74 (*  current proof.                                                        *)
75 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
76 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
77 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
78 (*CSC: [newmetasenv].                                             *)
79 let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
80  let (uri,_,initial_subst,bo,ty, attrs) = proof in
81   let subst_in = CicMetaSubst.apply_subst subst in
82   let bo' = lazy (subst_in (Lazy.force bo)) in
83   (* Metavariables can appear also in the *statement* of the theorem
84    * since the parser does not reject as statements terms with
85    * metavariable therein *)
86   let ty' = subst_in ty in
87   let metasenv' =
88    List.fold_right
89     (fun metasenv_entry i ->
90       match metasenv_entry with
91          (m,canonical_context,ty) when m <> meta ->
92            let canonical_context' =
93             List.map
94              (function
95                  None -> None
96                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
97                | Some (i,Cic.Def (bo,ty)) ->
98                   Some (i,Cic.Def (subst_in bo,subst_in ty))
99              ) canonical_context
100            in
101             (m,canonical_context',subst_in ty)::i
102        | _ -> i
103     ) newmetasenv []
104   in
105   (* qui da capire se per la fase transitoria si fa initial_subst @ subst
106    * oppure subst *)
107    let newproof = uri,metasenv',subst,bo',ty', attrs in
108     (newproof, metasenv')
109
110 let compare_metasenvs ~oldmetasenv ~newmetasenv =
111  List.map (function (i,_,_) -> i)
112   (List.filter
113    (function (i,_,_) ->
114      not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
115 ;;
116
117 (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
118 let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
119   let rec find subst metasenv ugraph context w t =
120    try
121     let subst,metasenv,ugraph =
122      CicUnification.fo_unif_subst subst context metasenv w t ugraph
123     in
124       subst,metasenv,ugraph,[context,t]
125    with
126      CicUnification.UnificationFailure _
127    | CicUnification.Uncertain _ ->
128       match t with
129       | Cic.Sort _ 
130       | Cic.Rel _ -> subst,metasenv,ugraph,[]
131       | Cic.Meta (_, ctx) -> 
132           List.fold_left (
133             fun (subst,metasenv,ugraph,acc) e -> 
134               match e with 
135               | None -> subst,metasenv,ugraph,acc 
136               | Some t ->
137                  let subst,metasenv,ugraph,res =
138                   find subst metasenv ugraph context w t
139                  in
140                   subst,metasenv,ugraph, res @ acc
141           ) (subst,metasenv,ugraph,[]) ctx
142       | Cic.Lambda (name, t1, t2) 
143       | Cic.Prod (name, t1, t2) ->
144          let subst,metasenv,ugraph,rest1 =
145           find subst metasenv ugraph context w t1 in
146          let subst,metasenv,ugraph,rest2 =
147           find subst metasenv ugraph (Some (name, Cic.Decl t1)::context)
148            (CicSubstitution.lift 1 w) t2
149          in
150           subst,metasenv,ugraph,rest1 @ rest2
151       | Cic.LetIn (name, t1, t2, t3) -> 
152          let subst,metasenv,ugraph,rest1 =
153           find subst metasenv ugraph context w t1 in
154          let subst,metasenv,ugraph,rest2 =
155           find subst metasenv ugraph context w t2 in
156          let subst,metasenv,ugraph,rest3 =
157           find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context)
158            (CicSubstitution.lift 1 w) t3
159          in
160           subst,metasenv,ugraph,rest1 @ rest2 @ rest3
161       | Cic.Appl l -> 
162           List.fold_left
163            (fun (subst,metasenv,ugraph,acc) t ->
164              let subst,metasenv,ugraph,res =
165               find subst metasenv ugraph context w t
166              in
167               subst,metasenv,ugraph,res @ acc)
168            (subst,metasenv,ugraph,[]) l
169       | Cic.Cast (t, ty) ->
170          let subst,metasenv,ugraph,rest =
171           find subst metasenv ugraph context w t in
172          let subst,metasenv,ugraph,resty =
173           find subst metasenv ugraph context w ty
174          in
175           subst,metasenv,ugraph,rest @ resty
176       | Cic.Implicit _ -> assert false
177       | Cic.Const (_, esubst)
178       | Cic.Var (_, esubst) 
179       | Cic.MutInd (_, _, esubst) 
180       | Cic.MutConstruct (_, _, _, esubst) -> 
181           List.fold_left
182            (fun (subst,metasenv,ugraph,acc) (_, t) ->
183              let subst,metasenv,ugraph,res =
184               find subst metasenv ugraph context w t
185              in
186               subst,metasenv,ugraph,res @ acc)
187            (subst,metasenv,ugraph,[]) esubst
188       | Cic.MutCase (_, _, outty, indterm, patterns) -> 
189          let subst,metasenv,ugraph,resoutty =
190           find subst metasenv ugraph context w outty in
191          let subst,metasenv,ugraph,resindterm =
192           find subst metasenv ugraph context w indterm in
193          let subst,metasenv,ugraph,respatterns =
194           List.fold_left
195            (fun (subst,metasenv,ugraph,acc) p ->
196              let subst,metaseng,ugraph,res =
197               find subst metasenv ugraph context w p
198              in
199               subst,metasenv,ugraph,res @ acc
200            ) (subst,metasenv,ugraph,[]) patterns
201          in
202           subst,metasenv,ugraph,resoutty @ resindterm @ respatterns
203       | Cic.Fix (_, funl) -> 
204          let tys =
205           List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
206          in
207           List.fold_left (
208             fun (subst,metasenv,ugraph,acc) (_, _, ty, bo) ->
209              let subst,metasenv,ugraph,resty =
210               find subst metasenv ugraph context w ty in
211              let subst,metasenv,ugraph,resbo =
212               find subst metasenv ugraph (tys @ context) w bo
213              in
214               subst,metasenv,ugraph, resty @ resbo @ acc
215           ) (subst,metasenv,ugraph,[]) funl
216       | Cic.CoFix (_, funl) ->
217          let tys =
218           List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
219          in
220           List.fold_left (
221             fun (subst,metasenv,ugraph,acc) (_, ty, bo) ->
222              let subst,metasenv,ugraph,resty =
223               find subst metasenv ugraph context w ty in
224              let subst,metasenv,ugraph,resbo =
225               find subst metasenv ugraph (tys @ context) w bo
226              in
227               subst,metasenv,ugraph, resty @ resbo @ acc
228           ) (subst,metasenv,ugraph,[]) funl
229   in
230   find subst metasenv ugraph context wanted t
231   
232 let select_in_term 
233   ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where) 
234 =
235   let add_ctx context name entry = (Some (name, entry)) :: context in
236   let map2 error_msg f l1 l2 = 
237     try 
238       List.map2 f l1 l2 
239     with
240     | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg))
241   in
242   let rec aux context where term =
243     match (where, term) with
244     | Cic.Implicit (Some `Hole), t -> [context,t]
245     | Cic.Implicit (Some `Type), t -> []
246     | Cic.Implicit None,_ -> []
247     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
248         List.concat
249           (map2 "wrong number of argument in explicit substitution"
250             (fun t1 t2 ->
251               (match (t1, t2) with
252                   Some t1, Some t2 -> aux context t1 t2
253                 | _ -> []))
254             ctxt1 ctxt2)
255     | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) ->
256        aux context te1 te2 @ aux context ty1 ty2
257     | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
258     | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
259         aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
260     | Cic.Prod (Cic.Name n1, s1, t1), 
261       Cic.Prod ((Cic.Name n2) as name , s2, t2)
262     | Cic.Lambda (Cic.Name n1, s1, t1), 
263       Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
264         aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
265     | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
266     | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
267     | Cic.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) -> 
268         aux context s1 s2 @
269         aux context ty1 ty2 @
270         aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
271     | Cic.LetIn (Cic.Name n1, s1, ty1, t1), 
272       Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2-> 
273         aux context s1 s2 @
274         aux context ty1 ty2 @
275         aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
276     | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> []
277     | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2
278     | Cic.Var (_, subst1), Cic.Var (_, subst2)
279     | Cic.Const (_, subst1), Cic.Const (_, subst2)
280     | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2)
281     | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) ->
282         auxs context (List.map snd subst1) (List.map snd subst2)
283     | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
284         aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
285     | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
286        let tys =
287         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
288        in
289         List.concat
290           (map2 "wrong number of mutually recursive functions"
291             (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
292               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
293             funs1 funs2)
294     | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
295        let tys =
296         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
297        in
298         List.concat
299           (map2 "wrong number of mutually co-recursive functions"
300             (fun (_, ty1, bo1) (_, ty2, bo2) ->
301               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
302             funs1 funs2)
303     | x,y -> 
304         raise (Bad_pattern 
305                 (lazy (Printf.sprintf "Pattern %s versus term %s" 
306                   (CicPp.ppterm x)
307                   (CicPp.ppterm y))))
308   and auxs context terms1 terms2 =  (* as aux for list of terms *)
309     List.concat (map2 "wrong number of arguments in application"
310       (fun t1 t2 -> aux context t1 t2) terms1 terms2)
311   in
312    let roots =
313      match where with
314      | None -> []
315      | Some where -> aux context where term
316    in
317     match wanted with
318        None -> subst,metasenv,ugraph,roots
319      | Some wanted ->
320         let rec find_in_roots subst =
321          function
322             [] -> subst,metasenv,ugraph,[]
323           | (context',where)::tl ->
324              let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
325              let subst,metasenv,ugraph,found =
326               let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
327                find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
328                 where
329              in
330               subst,metasenv,ugraph,found @ tl'
331         in
332          find_in_roots subst roots
333 ;;
334
335 (** create a pattern from a term and a list of subterms.
336 * the pattern is granted to have a ? for every subterm that has no selected
337 * subterms
338 * @param equality equality function used while walking the term. Defaults to
339 * physical equality (==) *)
340 let pattern_of ?(equality=(==)) ~term terms =
341   let (===) x y = equality x y in
342   let not_found = false, Cic.Implicit None in
343   let rec aux t =
344     match t with
345     | t when List.exists (fun t' -> t === t') terms ->
346        true,Cic.Implicit (Some `Hole)
347     | Cic.Var (uri, subst) ->
348        let b,subst = aux_subst subst in
349         if b then
350          true,Cic.Var (uri, subst)
351         else
352          not_found
353     | Cic.Meta (i, ctxt) ->
354         let b,ctxt =
355           List.fold_right
356            (fun e (b,ctxt) ->
357              match e with
358                 None -> b,None::ctxt
359               | Some t -> let bt,t = aux t in b||bt ,Some t::ctxt
360            ) ctxt (false,[])
361         in
362          if b then
363           true,Cic.Meta (i, ctxt)
364          else
365           not_found
366     | Cic.Cast (te, ty) ->
367        let b1,te = aux te in
368        let b2,ty = aux ty in
369         if b1||b2 then true,Cic.Cast (te, ty)
370         else
371          not_found
372     | Cic.Prod (_, s, t) ->
373        let b1,s = aux s in
374        let b2,t = aux t in
375         if b1||b2 then
376          true, Cic.Prod (Cic.Anonymous, s, t)
377         else
378          not_found
379     | Cic.Lambda (_, s, t) ->
380        let b1,s = aux s in
381        let b2,t = aux t in
382         if b1||b2 then
383          true, Cic.Lambda (Cic.Anonymous, s, t)
384         else
385          not_found
386     | Cic.LetIn (_, s, ty, t) ->
387        let b1,s = aux s in
388        let b2,ty = aux ty in
389        let b3,t = aux t in
390         if b1||b2||b3 then
391          true, Cic.LetIn (Cic.Anonymous, s, ty, t)
392         else
393          not_found
394     | Cic.Appl terms ->
395        let b,terms =
396         List.fold_right
397          (fun t (b,terms) ->
398            let bt,t = aux t in
399             b||bt,t::terms
400          ) terms (false,[])
401        in
402         if b then
403          true,Cic.Appl terms
404         else
405          not_found
406     | Cic.Const (uri, subst) ->
407        let b,subst = aux_subst subst in
408         if b then
409          true, Cic.Const (uri, subst)
410         else
411          not_found
412     | Cic.MutInd (uri, tyno, subst) ->
413        let b,subst = aux_subst subst in
414         if b then
415          true, Cic.MutInd (uri, tyno, subst)
416         else
417          not_found
418     | Cic.MutConstruct (uri, tyno, consno, subst) ->
419        let b,subst = aux_subst subst in
420         if b then
421          true, Cic.MutConstruct (uri, tyno, consno, subst)
422         else
423          not_found
424     | Cic.MutCase (uri, tyno, outty, t, pat) ->
425        let b1,outty = aux outty in
426        let b2,t = aux t in
427        let b3,pat =
428         List.fold_right
429          (fun t (b,pat) ->
430            let bt,t = aux t in
431             bt||b,t::pat
432          ) pat (false,[])
433        in
434         if b1 || b2 || b3 then
435          true, Cic.MutCase (uri, tyno, outty, t, pat)
436         else
437          not_found
438     | Cic.Fix (funno, funs) ->
439         let b,funs =
440           List.fold_right
441            (fun (name, i, ty, bo) (b,funs) ->
442              let b1,ty = aux ty in
443              let b2,bo = aux bo in
444               b||b1||b2, (name, i, ty, bo)::funs) funs (false,[])
445         in
446          if b then
447           true, Cic.Fix (funno, funs)
448          else
449           not_found
450     | Cic.CoFix (funno, funs) ->
451         let b,funs =
452           List.fold_right
453            (fun (name, ty, bo) (b,funs) ->
454              let b1,ty = aux ty in
455              let b2,bo = aux bo in
456               b||b1||b2, (name, ty, bo)::funs) funs (false,[])
457         in
458          if b then
459           true, Cic.CoFix (funno, funs)
460          else
461           not_found
462     | Cic.Rel _
463     | Cic.Sort _
464     | Cic.Implicit _ -> not_found
465   and aux_subst subst =
466     List.fold_right
467      (fun (uri, t) (b,subst) ->
468        let b1,t = aux t in
469         b||b1,(uri, t)::subst) subst (false,[])
470   in
471    snd (aux term)
472
473 exception Fail of string Lazy.t
474
475   (** select metasenv conjecture pattern
476   * select all subterms of [conjecture] matching [pattern].
477   * It returns the set of matched terms (that can be compared using physical
478   * equality to the subterms of [conjecture]) together with their contexts.
479   * The representation of the set mimics the ProofEngineTypes.pattern type:
480   * a list of hypothesis (names of) together with the list of its matched
481   * subterms (and their contexts) + the list of matched subterms of the
482   * with their context conclusion. Note: in the result the list of hypothesis
483   * has an entry for each entry in the context and in the same order.
484   * Of course the list of terms (with their context) associated to the
485   * hypothesis name may be empty. 
486   *
487   * @raise Bad_pattern
488   * *)
489   let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty)
490        ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
491   =
492    let what, hyp_patterns, goal_pattern = pattern in
493    let find_pattern_for name =
494      try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
495      with Not_found -> None in
496    (* Multiple hypotheses with the same name can be in the context.
497       In this case we need to pick the last one, but we will perform
498       a fold_right on the context. Thus we pre-process hyp_patterns. *)
499    let full_hyp_pattern =
500     let rec aux blacklist =
501      function
502         [] -> []
503       | None::tl -> None::aux blacklist tl
504       | Some (name,_)::tl ->
505          if List.mem name blacklist then
506           None::aux blacklist tl
507          else
508           find_pattern_for name::aux (name::blacklist) tl
509     in
510      aux [] context
511    in
512    let subst,metasenv,ugraph,ty_terms =
513     select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty
514      ~pattern:(what,goal_pattern) 
515    in
516    let subst,metasenv,ugraph,context_terms =
517     let subst,metasenv,ugraph,res,_ =
518      (List.fold_right
519       (fun (pattern,entry) (subst,metasenv,ugraph,res,context) ->
520         match entry with
521           None -> subst,metasenv,ugraph,None::res,None::context
522         | Some (name,Cic.Decl term) ->
523             (match pattern with
524             | None ->
525                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
526             | Some pat ->
527                 let subst,metasenv,ugraph,terms =
528                  select_in_term ~subst ~metasenv ~context ~ugraph ~term
529                   ~pattern:(what, Some pat)
530                 in
531                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
532                   (entry::context))
533         | Some (name,Cic.Def (bo, ty)) ->
534             (match pattern with
535             | None ->
536                let selected_ty = [] in
537                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
538                  (entry::context)
539             | Some pat -> 
540                 let subst,metasenv,ugraph,terms_bo =
541                  select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo
542                   ~pattern:(what, Some pat) in
543                 let subst,metasenv,ugraph,terms_ty =
544                  let subst,metasenv,ugraph,res =
545                   select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty
546                    ~pattern:(what, Some pat)
547                  in
548                   subst,metasenv,ugraph,res
549                 in
550                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
551                   (entry::context))
552       ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[]))
553     in
554      subst,metasenv,ugraph,res
555    in
556     subst,metasenv,ugraph,context_terms, ty_terms
557 ;;
558
559 (** locate_in_term equality what where context
560 * [what] must match a subterm of [where] according to [equality]
561 * It returns the matched terms together with their contexts in [where]
562 * [equality] defaults to physical equality
563 * [context] must be the context of [where]
564 *)
565 let locate_in_term ?(equality=(fun _ -> (==))) what ~where context =
566   let add_ctx context name entry =
567       (Some (name, entry)) :: context in
568   let rec aux context where =
569    if equality context what where then [context,where]
570    else
571     match where with
572     | Cic.Implicit _
573     | Cic.Meta _
574     | Cic.Rel _
575     | Cic.Sort _
576     | Cic.Var _
577     | Cic.Const _
578     | Cic.MutInd _
579     | Cic.MutConstruct _ -> []
580     | Cic.Cast (te, ty) -> aux context te @ aux context ty
581     | Cic.Prod (name, s, t)
582     | Cic.Lambda (name, s, t) ->
583         aux context s @ aux (add_ctx context name (Cic.Decl s)) t
584     | Cic.LetIn (name, s, ty, t) -> 
585         aux context s @
586         aux context ty @
587         aux (add_ctx context name (Cic.Def (s,ty))) t
588     | Cic.Appl tl -> auxs context tl
589     | Cic.MutCase (_, _, out, t, pat) ->
590         aux context out @ aux context t @ auxs context pat
591     | Cic.Fix (_, funs) ->
592        let tys =
593         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
594        in
595         List.concat
596           (List.map
597             (fun (_, _, ty, bo) -> 
598               aux context ty @ aux (tys @ context) bo)
599             funs)
600     | Cic.CoFix (_, funs) ->
601        let tys =
602         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
603        in
604         List.concat
605           (List.map
606             (fun (_, ty, bo) ->
607               aux context ty @ aux (tys @ context) bo)
608             funs)
609   and auxs context tl =  (* as aux for list of terms *)
610     List.concat (List.map (fun t -> aux context t) tl)
611   in
612    aux context where
613
614 (** locate_in_conjecture equality what where context
615 * [what] must match a subterm of [where] according to [equality]
616 * It returns the matched terms together with their contexts in [where]
617 * [equality] defaults to physical equality
618 * [context] must be the context of [where]
619 *)
620 let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
621  let context,res =
622   List.fold_right
623    (fun entry (context,res) ->
624      match entry with
625         None -> entry::context, res
626       | Some (_, Cic.Decl ty) ->
627          let res = res @ locate_in_term what ~where:ty context in
628          let context' = entry::context in
629           context',res
630       | Some (_, Cic.Def (bo,ty)) ->
631          let res = res @ locate_in_term what ~where:bo context in
632          let res = res @ locate_in_term what ~where:ty context in
633          let context' = entry::context in
634           context',res
635    ) context ([],[])
636  in
637   res @ locate_in_term what ~where:ty context
638
639 let lookup_type metasenv context hyp =
640    let rec aux p = function
641       | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
642       | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t
643       | _ :: tail -> aux (succ p) tail
644       | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
645    in
646    aux 1 context
647
648 let find_hyp name =
649  let rec find_hyp n =
650   function
651      [] -> assert false
652    | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
653       Cic.Rel n, CicSubstitution.lift n ty
654    | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
655    | _::tl -> find_hyp (n+1) tl
656  in
657   find_hyp 1
658 ;;
659
660 (* sort pattern hypotheses from the smallest to the highest Rel *)
661 let sort_pattern_hyps context (t,hpatterns,cpattern) =
662  let hpatterns =
663   List.sort
664    (fun (id1,_) (id2,_) ->
665      let t1,_ = find_hyp id1 context in
666      let t2,_ = find_hyp id2 context in
667      match t1,t2 with
668         Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
669       | _,_ -> assert false) hpatterns
670  in
671   t,hpatterns,cpattern
672 ;;
673
674 (* FG: **********************************************************************)
675
676 let get_name context index =
677    try match List.nth context (pred index) with
678       | Some (Cic.Name name, _)     -> Some name
679       | _                           -> None
680    with Invalid_argument "List.nth" -> None
681
682 let get_rel context name =
683    let rec aux i = function
684       | []                                      -> None
685       | Some (Cic.Name s, _) :: _ when s = name -> Some (Cic.Rel i)
686       | _ :: tl                                 -> aux (succ i) tl
687    in
688    aux 1 context
689
690 let split_with_whd (c, t) =
691    let add s v c = Some (s, Cic.Decl v) :: c in
692    let rec aux whd a n c = function
693       | Cic.Prod (s, v, t)  -> aux false ((c, v) :: a) (succ n) (add s v c) t
694       | v when whd          -> (c, v) :: a, n
695       | v                   -> aux true a n c (CicReduction.whd c v)
696     in
697     aux false [] 0 c t
698
699 let split_with_normalize (c, t) =
700    let add s v c = Some (s, Cic.Decl v) :: c in
701    let rec aux a n c = function
702       | Cic.Prod (s, v, t)  -> aux ((c, v) :: a) (succ n) (add s v c) t
703       | v                   -> (c, v) :: a, n
704     in
705     aux [] 0 c (CicReduction.normalize c t)
706
707   (* menv sorting *)
708 module OT = 
709   struct 
710     type t = Cic.conjecture
711     let compare (i,_,_) (j,_,_) = Pervasives.compare i j
712   end
713 module MS = HTopoSort.Make(OT)
714 let relations_of_menv m c =
715   let i, ctx, ty = c in
716   let m = List.filter (fun (j,_,_) -> j <> i) m in
717   let m_ty = List.map fst (CicUtil.metas_of_term ty) in
718   let m_ctx = 
719     List.flatten
720       (List.map 
721         (function 
722          | None -> []
723          | Some (_,Cic.Decl t) ->
724              List.map fst (CicUtil.metas_of_term ty)
725          | Some (_,Cic.Def (t,ty)) -> 
726              List.map fst (CicUtil.metas_of_term ty) @
727              List.map fst (CicUtil.metas_of_term t))
728         ctx)
729   in
730   let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
731   List.filter (fun (i,_,_) -> List.exists ((=) i) metas) m
732 ;;
733 let sort_metasenv (m : Cic.metasenv) =
734   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
735 ;;