]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_kernel/nCicUntrusted.ml
update in standard library
[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 () = function
164   | C.Meta _ as t -> t
165   | C.Appl((C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r) as hd)::args) as ot->
166       let args'= HExtlib.sharing_map (fire_projection_redex status ()) args in
167       let t = if args == args' then ot else C.Appl (hd::args') in
168       let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
169       if pragma <> `Projection || List.length args <= rno then t
170       else
171         (match List.nth args' rno with
172         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
173             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
174             let t = C.Appl (fbody::args') in
175             (match NCicReduction.head_beta_reduce status ~delta:max_int t with
176              | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
177                 ::kargs),[pat])->
178                   let _,kargs = HExtlib.split_nth leftno kargs in
179                    NCicReduction.head_beta_reduce status
180                     ~delta:max_int (C.Appl (pat :: kargs))
181             | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
182                ::kargs),[pat]) :: args) ->
183                   let _,kargs = HExtlib.split_nth leftno kargs in
184                    fire_projection_redex status ()
185                     (NCicReduction.head_beta_reduce status 
186                       ~delta:max_int (C.Appl (pat :: kargs @ args)))
187             | _ -> assert false) 
188         | _ -> t)
189   | t ->
190      NCicUtils.map status (fun _ x -> x) () (fire_projection_redex status) t
191 ;;
192
193 let apply_subst status ?(fix_projections=false) subst context t = 
194  let rec apply_subst subst () =
195  function
196     NCic.Meta (i,lc) ->
197      (try
198        let _,_,t,_ = NCicUtils.lookup_subst i subst in
199        let t = NCicSubstitution.subst_meta status lc t in
200         apply_subst subst () t
201       with
202        NCicUtils.Subst_not_found j when j = i ->
203         match lc with
204            _,NCic.Irl _ -> NCic.Meta (i,lc)
205          | n,NCic.Ctx l ->
206             NCic.Meta
207              (i,(0,NCic.Ctx
208                  (List.map (fun t ->
209                    apply_subst subst () (NCicSubstitution.lift status n t)) l))))
210   | t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
211  in
212   let t = apply_subst subst () t in
213   let t = clean_or_fix_dependent_abstrations status context t in
214   if fix_projections then
215    fire_projection_redex status () t
216   else
217    t
218 ;;
219
220 let apply_subst_context status ~fix_projections subst context =
221   let apply_subst = apply_subst status ~fix_projections in
222   let rec aux c = function 
223     | [] -> []
224     | (name,NCic.Decl t as e) :: tl -> 
225         (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
226     | (name,NCic.Def (t1,t2) as e) :: tl -> 
227         (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) :: 
228           aux (e::c) tl
229   in
230     List.rev (aux [] (List.rev context))
231 ;;
232
233 let rec apply_subst_metasenv status subst = function
234   | [] -> []
235   | (i,_) :: _ when List.mem_assoc i subst -> assert false
236   | (i,(name,ctx,ty)) :: tl ->
237       (i,(name,apply_subst_context status ~fix_projections:true subst ctx,
238                apply_subst status ~fix_projections:true subst ctx ty)) ::
239          apply_subst_metasenv status subst tl
240 ;;
241
242 (* hide optional arg *)
243 let apply_subst status s c t = apply_subst status s c t;;
244
245
246 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
247
248 let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
249
250 let kind_of_meta l =
251   try 
252     (match List.find is_kind l with
253     | `IsSort | `IsType | `IsTerm as x -> x
254     | _ -> assert false)
255   with 
256    Not_found -> assert false
257 ;;
258
259 let rec replace_in_metasenv i f = function
260   | [] -> assert false
261   | (j,e)::tl when j=i -> (i,f e) :: tl
262   | x::tl -> x :: replace_in_metasenv i f tl
263 ;;
264           
265 let rec replace_in_subst i f = function
266   | [] -> assert false
267   | (j,e)::tl when j=i -> (i,f e) :: tl
268   | x::tl -> x :: replace_in_subst i f tl
269 ;;
270           
271 let set_kind newkind attrs = 
272   (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs 
273 ;;
274
275 let max_kind k1 k2 = 
276   match k1, k2 with
277   | `IsSort, _ | _, `IsSort -> `IsSort
278   | `IsType, _ | _, `IsType -> `IsType
279   | _ -> `IsTerm
280 ;;
281
282 module OT = 
283   struct 
284     type t = int * NCic.conjecture
285     let compare (i,_) (j,_) = Pervasives.compare i j
286   end
287
288 module MS = HTopoSort.Make(OT)
289 let relations_of_menv status subst m c =
290   let i, (_, ctx, ty) = c in
291   let m = List.filter (fun (j,_) -> j <> i) m in
292   let m_ty = metas_of_term status subst ctx ty in
293   let m_ctx =
294    snd 
295     (List.fold_right
296      (fun i (ctx,res) ->
297       (i::ctx),
298       (match i with
299        | _,NCic.Decl ty -> metas_of_term status subst ctx ty
300        | _,NCic.Def (t,ty) -> 
301          metas_of_term status subst ctx ty @ metas_of_term status subst ctx t) @ res)
302     ctx ([],[]))
303   in
304   let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
305   List.filter (fun (i,_) -> List.exists ((=) i) metas) m
306 ;;
307
308 let sort_metasenv status subst (m : NCic.metasenv) =
309   (MS.topological_sort m (relations_of_menv status subst m) : NCic.metasenv)
310 ;;
311
312 let count_occurrences status ~subst n t = 
313   let occurrences = ref 0 in
314   let rec aux k _ = function
315     | C.Rel m when m = n+k -> incr occurrences
316     | C.Rel _m -> ()
317     | C.Implicit _ -> ()
318     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
319     | C.Meta (mno,(s,l)) ->
320          (try
321             (* possible optimization here: try does_not_occur on l and
322                perform substitution only if DoesOccur is raised *)
323             let _,_,term,_ = NCicUtils.lookup_subst mno subst in
324             aux (k-s) () (NCicSubstitution.subst_meta status (0,l) term)
325           with NCicUtils.Subst_not_found _ -> () (*match l with
326           | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
327           | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
328     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
329   in
330    aux 0 () t;
331    !occurrences
332 ;;
333
334 exception Found_variable
335
336 let looks_closed t = 
337   let rec aux k _ = function
338     | C.Rel m when k < m -> raise Found_variable
339     | C.Rel _m -> ()
340     | C.Implicit _ -> ()
341     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
342     | C.Meta _ -> raise Found_variable
343     | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
344   in
345   try aux 0 () t; true with Found_variable -> false
346 ;;