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_______________________________________________________________ *)
12 (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *)
14 let expand_local_context = function
16 let rec aux acc = function
18 | n -> aux (NCic.Rel n::acc) (n-1)
21 | NCic.Ctx lctx -> lctx
24 exception Subst_not_found of int
26 let lookup_subst n subst =
29 with Not_found -> raise (Subst_not_found n)
31 let fold f g acc = function
37 | NCic.Appl l -> List.fold_left f acc l
39 | NCic.Lambda (_,s,t) -> f (g (f acc s)) t
40 | NCic.LetIn (_,ty,t,bo) -> f (g (f (f acc ty) t)) bo
41 | NCic.Match (_,oty,t,pl) -> List.fold_left f (f (f acc oty) t) pl
45 let unchanged = ref true in
46 let rec aux b = function
47 | [] as t -> unchanged := b; t
50 he1 :: aux (b && he1 == he) tl
52 let l1 = aux true l in
53 if !unchanged then l else l1
56 let map f g k = function
61 | NCic.Rel _ as t -> t
62 | NCic.Appl l -> NCic.Appl (sharing_map (f k) l)
63 | NCic.Prod (n,s,t) as orig ->
64 let s1 = f k s in let t1 = f (g k) t in
65 if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
66 | NCic.Lambda (n,s,t) as orig ->
67 let s1 = f k s in let t1 = f (g k) t in
68 if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
69 | NCic.LetIn (n,ty,t,b) as orig ->
70 let ty1 = f k ty in let t1 = f k t in let b1 = f (g k) b in
71 if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1)
72 | NCic.Match (r,oty,t,pl) as orig ->
73 let oty1 = f k oty in let t1 = f k t in let pl1 = sharing_map (f k) pl in
74 if oty1 == oty && t1 == t && pl1 == pl then orig
75 else NCic.Match(r,oty1,t1,pl1)