]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicSubstitution.ml
added generation of LaTeX documentation
[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml
1 (* Copyright (C) 2000, 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 exception CannotSubstInMeta;;
27 exception RelToHiddenHypothesis;;
28
29 let lift n =
30  let rec liftaux k =
31   let module C = Cic in
32    function
33       C.Rel m ->
34        if m < k then
35         C.Rel m
36        else
37         C.Rel (m + n)
38     | C.Var _  as t -> t
39     | C.Meta (i,l) ->
40        let l' =
41         List.map
42          (function
43              None -> None
44            | Some t -> Some (liftaux k t)
45          ) l
46        in
47         C.Meta(i,l')
48     | C.Sort _ as t -> t
49     | C.Implicit as t -> t
50     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
51     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
52     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
53     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
54     | C.Appl l -> C.Appl (List.map (liftaux k) l)
55     | C.Const _ as t -> t
56     | C.MutInd _ as t -> t
57     | C.MutConstruct _ as t -> t
58     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
59        C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
60         List.map (liftaux k) pl)
61     | C.Fix (i, fl) ->
62        let len = List.length fl in
63        let liftedfl =
64         List.map
65          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
66           fl
67        in
68         C.Fix (i, liftedfl)
69     | C.CoFix (i, fl) ->
70        let len = List.length fl in
71        let liftedfl =
72         List.map
73          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
74           fl
75        in
76         C.CoFix (i, liftedfl)
77  in
78   if n = 0 then
79    (function t -> t)
80   else
81    liftaux 1
82 ;;
83
84 let subst arg =
85  let rec substaux k =
86   let module C = Cic in
87    function
88       C.Rel n as t ->
89        (match n with
90            n when n = k -> lift (k - 1) arg
91          | n when n < k -> t
92          | _            -> C.Rel (n - 1)
93        )
94     | C.Var _ as t  -> t
95     | C.Meta (i, l) as t -> 
96        let l' =
97         List.map
98          (function
99              None -> None
100            | Some t -> Some (substaux k t)
101          ) l
102        in
103         C.Meta(i,l')
104     | C.Sort _ as t -> t
105     | C.Implicit as t -> t
106     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
107     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
108     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
109     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
110     | C.Appl (he::tl) ->
111        (* Invariant: no Appl applied to another Appl *)
112        let tl' = List.map (substaux k) tl in
113         begin
114          match substaux k he with
115             C.Appl l -> C.Appl (l@tl')
116           | _ as he' -> C.Appl (he'::tl')
117         end
118     | C.Appl _ -> assert false
119     | C.Const _ as t -> t
120     | C.MutInd _ as t -> t
121     | C.MutConstruct _ as t -> t
122     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
123        C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
124         List.map (substaux k) pl)
125     | C.Fix (i,fl) ->
126        let len = List.length fl in
127        let substitutedfl =
128         List.map
129          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
130           fl
131        in
132         C.Fix (i, substitutedfl)
133     | C.CoFix (i,fl) ->
134        let len = List.length fl in
135        let substitutedfl =
136         List.map
137          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
138           fl
139        in
140         C.CoFix (i, substitutedfl)
141  in
142   substaux 1
143 ;;
144
145 let undebrujin_inductive_def uri =
146  function
147     Cic.InductiveDefinition (dl,params,n_ind_params) ->
148      let dl' =
149       List.map
150        (fun (name,inductive,arity,constructors) ->
151          let constructors' =
152           List.map
153            (fun (name,ty,r) ->
154              let ty' =
155               let counter = ref (List.length dl) in
156                List.fold_right
157                 (fun _ ->
158                   decr counter ;
159                   subst (Cic.MutInd (uri,0,!counter))
160                 ) dl ty
161              in
162               (name,ty',r)
163            ) constructors
164          in
165           (name,inductive,arity,constructors')
166        ) dl
167       in
168        Cic.InductiveDefinition (dl', params, n_ind_params)
169   | obj -> obj
170 ;;
171
172 (* l is the relocation list *)
173
174 let lift_meta l t = 
175     let module C = Cic in
176     if l = [] then t else 
177     let rec aux k = function
178       C.Rel n as t -> 
179         if n <= k then t else 
180          (try
181            match List.nth l (n-k-1) with
182               None -> raise RelToHiddenHypothesis
183             | Some t -> lift k t
184           with
185            (Failure _) -> assert false
186          )
187     | C.Var _ as t  -> t
188     | C.Meta (i,l) ->
189        let l' =
190         List.map
191          (function
192              None -> None
193            | Some t ->
194               try
195                Some (aux k t)
196               with
197                RelToHiddenHypothesis -> None
198          ) l
199        in
200         C.Meta(i,l')
201     | C.Sort _ as t -> t
202     | C.Implicit as t -> t
203     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
204     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
205     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
206     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
207     | C.Appl l -> C.Appl (List.map (aux k) l)
208     | C.Const _ as t -> t
209     | C.MutInd _ as t -> t
210     | C.MutConstruct _ as t -> t
211     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
212        C.MutCase (sp,cookingsno,i,aux k outt, aux k t,
213         List.map (aux k) pl)
214     | C.Fix (i,fl) ->
215        let len = List.length fl in
216        let substitutedfl =
217         List.map
218          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
219           fl
220        in
221         C.Fix (i, substitutedfl)
222     | C.CoFix (i,fl) ->
223        let len = List.length fl in
224        let substitutedfl =
225         List.map
226          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
227           fl
228        in
229         C.CoFix (i, substitutedfl)
230  in
231   aux 0 t          
232 ;;