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.
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_______________________________________________________________ *)
15 module Ref = NReference
17 let map_term_fold_a g k f a = function
18 | C.Meta _ -> assert false
23 | C.Appl [] | C.Appl [_] -> assert false
26 match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
31 (fun t (a,l) -> let a,t = f k a t in a, t :: l)
34 a, if l1 == l then orig else
37 | C.Appl l :: tl -> C.Appl (l@tl)
40 if fire_beta then NCicReduction.head_beta_reduce ~upto t
42 | C.Prod (n,s,t) as orig ->
43 let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
44 a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
45 | C.Lambda (n,s,t) as orig ->
46 let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
47 a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
48 | C.LetIn (n,ty,t,b) as orig ->
49 let a,ty1 = f k a ty in let a,t1 = f k a t in
50 let a,b1 = f (g (n,C.Def (t,ty)) k) a b in
51 a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
52 | C.Match (r,oty,t,pl) as orig ->
53 let a,oty1 = f k a oty in let a,t1 = f k a t in
56 List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[])
58 a, if oty1 == oty && t1 == t && pl1 == pl then orig
59 else C.Match(r,oty1,t1,pl1)
62 let metas_of_term subst context term =
63 let rec aux ctx acc = function
65 (match HExtlib.list_skip (i-1) ctx with
66 | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo
70 let _,_,bo,_ = NCicUtils.lookup_subst i subst in
71 let bo = NCicSubstitution.subst_meta l bo in
73 with NCicUtils.Subst_not_found _ ->
75 let lc = NCicUtils.expand_local_context lc in
76 let l = List.map (NCicSubstitution.lift shift) lc in
77 List.fold_left (aux ctx) (i::acc) l)
78 | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
80 HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
88 let hash = Hashtbl.hash_param 100 1000
93 if args = [] then he else
95 | NCic.Appl l -> NCic.Appl (l@args)
96 | _ -> NCic.Appl (he::args)
99 let map_obj_kind ?(skip_body=false) f =
100 let do_bo f x = if skip_body then x else f x in
102 NCic.Constant (relev,name,bo,ty,attrs) ->
103 NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
104 | NCic.Fixpoint (ind,fl,attrs) ->
107 (function (relevance,name,recno,ty,bo) ->
108 relevance,name,recno,f ty,do_bo f bo)
111 NCic.Fixpoint (ind,fl,attrs)
112 | NCic.Inductive (is_ind,lno,itl,attrs) ->
115 (fun (relevance,name,ty,cl) ->
117 List.map (fun (relevance, name, ty) ->
118 relevance, name, f ty)
121 relevance, name, f ty, cl)
124 NCic.Inductive (is_ind,lno,itl,attrs)
129 let clean_or_fix_dependent_abstrations ctx t =
131 let rec aux n _ = function
133 | NCic.Rel i when i = n + 1 -> raise Occurr
134 | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
136 try aux 0 () t; false
140 if not (List.mem name ctx) then name
143 let attempt = name ^ string_of_int i in
144 if List.mem attempt ctx then aux (i+1)
149 let rec aux ctx = function
150 | NCic.Meta _ as t -> t
151 | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
152 let name = fresh ctx (String.sub name 1 (String.length name-1)) in
153 NCic.Prod (name,aux ctx s, aux (name::ctx) t)
154 | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
155 NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
156 | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
157 | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
158 let name = fresh ctx ("_"^name) in
159 NCic.Prod (name, aux ctx s, aux (name::ctx) t)
160 | NCic.Prod (name,s,t) when List.mem name ctx ->
161 let name = fresh ctx name in
162 NCic.Prod (name, aux ctx s, aux (name::ctx) t)
163 | NCic.Lambda (name,s,t) when List.mem name ctx ->
164 let name = fresh ctx name in
165 NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
166 | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t
168 aux (List.map fst ctx) t
171 let rec fire_projection_redex on_args = function
173 | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
174 let l= if on_args then List.map (fire_projection_redex true) ol else ol in
175 let t = if l == ol then ot else C.Appl l in
176 let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
179 let l' = HExtlib.sharing_map (fire_projection_redex true) l in
180 if l == l' then t else C.Appl l'
182 t (* ot is the same *)
184 if pragma <> `Projection || List.length args <= rno then conclude ()
186 (match List.nth args rno with
187 | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
188 let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
189 let t = C.Appl (fbody::args) in
190 (match NCicReduction.head_beta_reduce ~delta:max_int t with
191 | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
192 let _,kargs = HExtlib.split_nth leftno kargs in
193 fire_projection_redex false
194 (NCicReduction.head_beta_reduce
195 ~delta:max_int (C.Appl (pat :: kargs)))
196 | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
197 let _,kargs = HExtlib.split_nth leftno kargs in
198 fire_projection_redex false
199 (NCicReduction.head_beta_reduce
200 ~delta:max_int (C.Appl (pat :: kargs @ args)))
203 | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
207 let apply_subst ?(fix_projections=false) subst context t =
208 let rec apply_subst subst () =
212 let _,_,t,_ = NCicUtils.lookup_subst i subst in
213 let t = NCicSubstitution.subst_meta lc t in
214 apply_subst subst () t
216 NCicUtils.Subst_not_found j when j = i ->
218 _,NCic.Irl _ -> NCic.Meta (i,lc)
223 apply_subst subst () (NCicSubstitution.lift n t)) l))))
224 | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
226 (if fix_projections then fire_projection_redex true else fun x -> x)
227 (clean_or_fix_dependent_abstrations context (apply_subst subst () t))
230 let apply_subst_context ~fix_projections subst context =
231 let apply_subst = apply_subst ~fix_projections in
232 let rec aux c = function
234 | (name,NCic.Decl t as e) :: tl ->
235 (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
236 | (name,NCic.Def (t1,t2) as e) :: tl ->
237 (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) ::
240 List.rev (aux [] (List.rev context))
243 let rec apply_subst_metasenv subst = function
245 | (i,_) :: _ when List.mem_assoc i subst -> assert false
246 | (i,(name,ctx,ty)) :: tl ->
247 (i,(name,apply_subst_context ~fix_projections:true subst ctx,
248 apply_subst ~fix_projections:true subst ctx ty)) ::
249 apply_subst_metasenv subst tl
252 (* hide optional arg *)
253 let apply_subst s c t = apply_subst s c t;;