]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_kernel/nCicUntrusted.ml
- weakening leq, we proved cpr_bind_dx
[helm.git] / matita / components / ng_kernel / nCicUntrusted.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 module C = NCic
15 module Ref = NReference
16
17 let map_term_fold_a status g k f a = function
18  | C.Meta _ -> assert false
19  | C.Implicit _
20  | C.Sort _
21  | C.Const _
22  | C.Rel _ as t -> a,t
23  | C.Appl [] | C.Appl [_] -> assert false
24  | C.Appl l as orig ->
25     let fire_beta, upto = 
26       match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 
27     in
28     let a,l1 = HExtlib.sharing_map_acc (f k) a l in
29     a, if l1 == l then orig else 
30        let t =
31         match l1 with
32          | C.Appl l :: tl -> C.Appl (l@tl)
33          | _ -> C.Appl l1
34        in
35         if fire_beta then NCicReduction.head_beta_reduce status ~upto t
36         else t
37  | C.Prod (n,s,t) as orig ->
38      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
39      a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
40  | C.Lambda (n,s,t) as orig -> 
41      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
42      a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
43  | C.LetIn (n,ty,t,b) as orig -> 
44      let a,ty1 = f k a ty in let a,t1 = f k a t in
45      let a,b1 = f (g (n,C.Def (t,ty)) k) a b in
46      a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
47  | C.Match (r,oty,t,pl) as orig -> 
48      let a,oty1 = f k a oty in let a,t1 = f k a t in 
49      let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in
50      a, if oty1 == oty && t1 == t && pl1 == pl then orig 
51         else C.Match(r,oty1,t1,pl1)
52 ;;
53
54 let metas_of_term status subst context term =
55   let rec aux ctx acc = function
56     | NCic.Rel i -> 
57          (match HExtlib.list_skip (i-1) ctx with
58          | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo
59          | _ -> acc)
60     | NCic.Meta(i,l) -> 
61          (try
62            let _,_,bo,_ = NCicUtils.lookup_subst i subst in
63            let bo = NCicSubstitution.subst_meta status l bo in
64            aux ctx acc bo
65          with NCicUtils.Subst_not_found _ -> 
66             let shift, lc = l in
67             let lc = NCicUtils.expand_local_context lc in
68             let l = List.map (NCicSubstitution.lift status shift) lc in
69             List.fold_left (aux ctx) (i::acc) l)
70     | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
71   in
72     HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
73 ;;
74
75 module NCicHash =
76  Hashtbl.Make
77   (struct
78     type t = C.term
79     let equal = (==)
80     let hash = Hashtbl.hash_param 100 1000 
81    end)
82 ;;
83
84 let mk_appl he args = 
85   if args = [] then he else
86   match he with
87   | NCic.Appl l -> NCic.Appl (l@args)
88   | _ -> NCic.Appl (he::args)
89 ;;
90
91 let map_obj_kind ?(skip_body=false) f =
92  let do_bo f x = if skip_body then x else f x in
93  function
94     NCic.Constant (relev,name,bo,ty,attrs) ->
95      NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
96   | NCic.Fixpoint (ind,fl,attrs) ->
97      let fl =
98       List.map
99        (function (relevance,name,recno,ty,bo) -> 
100           relevance,name,recno,f ty,do_bo f bo)
101        fl
102      in
103       NCic.Fixpoint (ind,fl,attrs)
104   | NCic.Inductive (is_ind,lno,itl,attrs) ->
105       let itl = 
106         List.map
107          (fun (relevance,name,ty,cl) ->
108            let cl = 
109              List.map (fun (relevance, name, ty) ->
110                 relevance, name, f ty)
111              cl
112            in
113            relevance, name, f ty, cl)
114          itl
115       in
116       NCic.Inductive (is_ind,lno,itl,attrs)
117 ;;
118
119 exception Occurr;;
120
121 let clean_or_fix_dependent_abstrations status ctx t =
122   let occurrs_1 t =
123     let rec aux n _ = function
124       | NCic.Meta _ -> ()
125       | NCic.Rel i when i = n + 1 -> raise Occurr
126       | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
127     in
128     try aux 0 () t; false
129     with Occurr -> true
130   in
131   let fresh ctx name = 
132     if not (List.mem name ctx) then name 
133     else
134      let rec aux i =
135        let attempt = name ^ string_of_int i in
136        if List.mem attempt ctx then aux (i+1) 
137        else attempt
138      in 
139       aux 0
140   in
141   let rec aux ctx = function
142   | NCic.Meta _ as t -> t
143   | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
144       let name = fresh ctx (String.sub name 1 (String.length name-1)) in
145       NCic.Prod (name,aux ctx s, aux (name::ctx) t)
146   | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
147       NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
148   | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
149   | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
150       let name = fresh ctx ("_"^name) in
151       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
152   | NCic.Prod (name,s,t) when List.mem name ctx ->
153       let name = fresh ctx name in
154       NCic.Prod (name, aux ctx s, aux (name::ctx) t)
155   | NCic.Lambda (name,s,t) when List.mem name ctx ->
156       let name = fresh ctx name in
157       NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
158   | t -> NCicUtils.map status (fun (e,_) ctx -> e::ctx) ctx aux t
159   in
160     aux (List.map fst ctx) t
161 ;;
162
163 let rec fire_projection_redex status on_args = function
164   | C.Meta _ as t -> t
165   | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
166       let l= if on_args then List.map (fire_projection_redex status true) ol else ol in
167       let t = if l == ol then ot else C.Appl l in
168       let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
169       let conclude () =
170         if on_args then 
171           let l' = HExtlib.sharing_map (fire_projection_redex status true) l in
172           if l == l' then t else C.Appl l'
173         else
174           t (* ot is the same *) 
175       in
176       if pragma <> `Projection || List.length args <= rno then conclude ()
177       else
178         (match List.nth l (rno+1) with
179         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
180             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
181             let t = C.Appl (fbody::List.tl l) in
182             (match NCicReduction.head_beta_reduce status ~delta:max_int t with
183              | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
184                 ::kargs),[pat])->
185                   let _,kargs = HExtlib.split_nth leftno kargs in
186                    fire_projection_redex status false 
187                     (NCicReduction.head_beta_reduce status
188                       ~delta:max_int (C.Appl (pat :: kargs)))
189             | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
190                ::kargs),[pat]) :: args) ->
191                   let _,kargs = HExtlib.split_nth leftno kargs in
192                    fire_projection_redex status false 
193                     (NCicReduction.head_beta_reduce status 
194                       ~delta:max_int (C.Appl (pat :: kargs @ args)))
195             | _ -> conclude ()) 
196         | _ -> conclude ())
197   | t when on_args ->
198      NCicUtils.map status (fun _ x -> x) true (fire_projection_redex status) t
199   | t -> t
200 ;;
201
202 let apply_subst status ?(fix_projections=false) subst context t = 
203  let rec apply_subst subst () =
204  function
205     NCic.Meta (i,lc) ->
206      (try
207        let _,_,t,_ = NCicUtils.lookup_subst i subst in
208        let t = NCicSubstitution.subst_meta status lc t in
209         apply_subst subst () t
210       with
211        NCicUtils.Subst_not_found j when j = i ->
212         match lc with
213            _,NCic.Irl _ -> NCic.Meta (i,lc)
214          | n,NCic.Ctx l ->
215             NCic.Meta
216              (i,(0,NCic.Ctx
217                  (List.map (fun t ->
218                    apply_subst subst () (NCicSubstitution.lift status n t)) l))))
219   | t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
220  in
221  (if fix_projections then fire_projection_redex status true else fun x -> x)
222     (clean_or_fix_dependent_abstrations status context (apply_subst subst () t))
223 ;;
224
225 let apply_subst_context status ~fix_projections subst context =
226   let apply_subst = apply_subst status ~fix_projections in
227   let rec aux c = function 
228     | [] -> []
229     | (name,NCic.Decl t as e) :: tl -> 
230         (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
231     | (name,NCic.Def (t1,t2) as e) :: tl -> 
232         (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) :: 
233           aux (e::c) tl
234   in
235     List.rev (aux [] (List.rev context))
236 ;;
237
238 let rec apply_subst_metasenv status subst = function
239   | [] -> []
240   | (i,_) :: _ when List.mem_assoc i subst -> assert false
241   | (i,(name,ctx,ty)) :: tl ->
242       (i,(name,apply_subst_context status ~fix_projections:true subst ctx,
243                apply_subst status ~fix_projections:true subst ctx ty)) ::
244          apply_subst_metasenv status subst tl
245 ;;
246
247 (* hide optional arg *)
248 let apply_subst status s c t = apply_subst status s c t;;
249
250
251 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
252
253 let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
254
255 let kind_of_meta l =
256   try 
257     (match List.find is_kind l with
258     | `IsSort | `IsType | `IsTerm as x -> x
259     | _ -> assert false)
260   with 
261    Not_found -> assert false
262 ;;
263
264 let rec replace_in_metasenv i f = function
265   | [] -> assert false
266   | (j,e)::tl when j=i -> (i,f e) :: tl
267   | x::tl -> x :: replace_in_metasenv i f tl
268 ;;
269           
270 let rec replace_in_subst i f = function
271   | [] -> assert false
272   | (j,e)::tl when j=i -> (i,f e) :: tl
273   | x::tl -> x :: replace_in_subst i f tl
274 ;;
275           
276 let set_kind newkind attrs = 
277   newkind :: List.filter (fun x -> not (is_kind x)) attrs 
278 ;;
279
280 let max_kind k1 k2 = 
281   match k1, k2 with
282   | `IsSort, _ | _, `IsSort -> `IsSort
283   | `IsType, _ | _, `IsType -> `IsType
284   | _ -> `IsTerm
285 ;;
286
287 module OT = 
288   struct 
289     type t = int * NCic.conjecture
290     let compare (i,_) (j,_) = Pervasives.compare i j
291   end
292
293 module MS = HTopoSort.Make(OT)
294 let relations_of_menv status subst m c =
295   let i, (_, ctx, ty) = c in
296   let m = List.filter (fun (j,_) -> j <> i) m in
297   let m_ty = metas_of_term status subst ctx ty in
298   let m_ctx =
299    snd 
300     (List.fold_right
301      (fun i (ctx,res) ->
302       (i::ctx),
303       (match i with
304        | _,NCic.Decl ty -> metas_of_term status subst ctx ty
305        | _,NCic.Def (t,ty) -> 
306          metas_of_term status subst ctx ty @ metas_of_term status subst ctx t) @ res)
307     ctx ([],[]))
308   in
309   let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
310   List.filter (fun (i,_) -> List.exists ((=) i) metas) m
311 ;;
312
313 let sort_metasenv status subst (m : NCic.metasenv) =
314   (MS.topological_sort m (relations_of_menv status subst m) : NCic.metasenv)
315 ;;
316
317 let count_occurrences status ~subst n t = 
318   let occurrences = ref 0 in
319   let rec aux k _ = function
320     | C.Rel m when m = n+k -> incr occurrences
321     | C.Rel _m -> ()
322     | C.Implicit _ -> ()
323     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
324     | C.Meta (mno,(s,l)) ->
325          (try
326             (* possible optimization here: try does_not_occur on l and
327                perform substitution only if DoesOccur is raised *)
328             let _,_,term,_ = NCicUtils.lookup_subst mno subst in
329             aux (k-s) () (NCicSubstitution.subst_meta status (0,l) term)
330           with NCicUtils.Subst_not_found _ -> () (*match l with
331           | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
332           | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
333     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
334   in
335    aux 0 () t;
336    !occurrences
337 ;;
338
339 exception Found_variable
340
341 let looks_closed t = 
342   let rec aux k _ = function
343     | C.Rel m when k < m -> raise Found_variable
344     | C.Rel _m -> ()
345     | C.Implicit _ -> ()
346     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
347     | C.Meta _ -> raise Found_variable
348     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
349   in
350   try aux 0 () t; true with Found_variable -> false
351 ;;