]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicReductionMachine.ml
added generation of LaTeX documentation
[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.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 CicReductionInternalError;;
27 exception WrongUriToInductiveDefinition;;
28
29 let fdebug = ref 1;;
30 let debug t env s =
31  let rec debug_aux t i =
32   let module C = Cic in
33   let module U = UriManager in
34    CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
35  in
36   if !fdebug = 0 then
37    begin
38     print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
39     flush stdout
40    end
41 ;;
42
43 exception Impossible of int;;
44 exception ReferenceToDefinition;;
45 exception ReferenceToAxiom;;
46 exception ReferenceToVariable;;
47 exception ReferenceToCurrentProof;;
48 exception ReferenceToInductiveDefinition;;
49
50 type env = Cic.term list;;
51 type stack = Cic.term list;;
52 type config = int * env * Cic.term * stack;;
53
54 (* k is the length of the environment e *)
55 (* m is the current depth inside the term *)
56 let unwind' m k e t = 
57     let module C = Cic in
58     let module S = CicSubstitution in
59     if e = [] & k = 0 then t else 
60     let rec unwind_aux m = function
61       C.Rel n as t -> if n <= m then t else
62                    let d = try Some (List.nth e (n-m-1))
63                               with _ -> None
64                    in (match d with 
65                    Some t' -> if m = 0 then t'
66                               else S.lift m t'
67                   | None -> C.Rel (n-k))
68     | C.Var _ as t  -> t
69     | C.Meta (i,l) as t -> t
70     | C.Sort _ as t -> t
71     | C.Implicit as t -> t
72     | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *)
73     | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
74     | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
75     | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
76     | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
77     | C.Const _ as t -> t
78     | C.MutInd _ as t -> t
79     | C.MutConstruct _ as t -> t
80     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
81        C.MutCase (sp,cookingsno,i,unwind_aux m outt, unwind_aux m t,
82         List.map (unwind_aux m) pl)
83     | C.Fix (i,fl) ->
84        let len = List.length fl in
85        let substitutedfl =
86         List.map
87          (fun (name,i,ty,bo) -> (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
88           fl
89        in
90         C.Fix (i, substitutedfl)
91     | C.CoFix (i,fl) ->
92        let len = List.length fl in
93        let substitutedfl =
94         List.map
95          (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
96           fl
97        in
98         C.CoFix (i, substitutedfl)
99  in
100   unwind_aux m t          
101     ;;
102
103 let unwind =
104  unwind' 0 
105 ;;
106
107 let rec reduce : config -> Cic.term = 
108     let module C = Cic in
109     let module S = CicSubstitution in 
110     function
111       (k, e, (C.Rel n as t), s) -> let d =
112 (* prerr_string ("Rel " ^ string_of_int n) ; flush stderr ; *)
113                                    try Some (List.nth e (n-1))
114                                    with _ -> None
115                                  in (match d with 
116                                    Some t' -> reduce (0, [],t',s)
117                                  | None -> if s = [] then C.Rel (n-k)
118                                            else C.Appl (C.Rel (n-k)::s))
119     | (k, e, (C.Var uri as t), s) -> 
120         (match CicEnvironment.get_cooked_obj uri 0 with
121             C.Definition _ -> raise ReferenceToDefinition
122           | C.Axiom _ -> raise ReferenceToAxiom
123           | C.CurrentProof _ -> raise ReferenceToCurrentProof
124           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
125           | C.Variable (_,None,_) -> if s = [] then t else C.Appl (t::s)
126           | C.Variable (_,Some body,_) -> reduce (0, [], body, s)
127          )
128     | (k, e, (C.Meta _ as t), s) -> if s = [] then t 
129                                  else C.Appl (t::s)
130     | (k, e, (C.Sort _ as t), s) -> t (* s should be empty *)
131     | (k, e, (C.Implicit as t), s) -> t (* s should be empty *)
132     | (k, e, (C.Cast (te,ty) as t), s) -> reduce (k, e,te,s) (* s should be empty *)
133     | (k, e, (C.Prod _ as t), s) -> unwind k e t (* s should be empty *)
134     | (k, e, (C.Lambda (_,_,t) as t'), []) -> unwind k e t' 
135     | (k, e, C.Lambda (_,_,t), p::s) ->
136 (* prerr_string ("Lambda body: " ^ CicPp.ppterm t) ; flush stderr ; *)
137         reduce (k+1, p::e,t,s) 
138     | (k, e, (C.LetIn (_,m,t) as t'), s) -> let m' = reduce (k,e,m,[]) in
139                                          reduce (k+1, m'::e,t,s)
140     | (k, e, C.Appl [], s) -> raise (Impossible 1)
141     (* this is lazy 
142     | (k, e, C.Appl (he::tl), s) ->  let tl' = List.map (unwind k e) tl
143                                  in reduce (k, e, he, (List.append tl' s)) *)
144     (* this is strict *)
145     | (k, e, C.Appl (he::tl), s) ->
146                                   (* constants are NOT unfolded *)
147                                   let red = function
148                                       C.Const _ as t -> t    
149                                     | t -> reduce (k, e,t,[]) in
150                                   let tl' = List.map red tl in
151                                    reduce (k, e, he , List.append tl' s) 
152 (* 
153     | (k, e, C.Appl ((C.Lambda _ as he)::tl), s) 
154     | (k, e, C.Appl ((C.Const _ as he)::tl), s)  
155     | (k, e, C.Appl ((C.MutCase _ as he)::tl), s) 
156     | (k, e, C.Appl ((C.Fix _ as he)::tl), s) ->
157 (* strict evaluation, but constants are NOT
158                                     unfolded *)
159                                   let red = function
160                                       C.Const _ as t -> t    
161                                     | t -> reduce (k, e,t,[]) in
162                                   let tl' = List.map red tl in
163                                    reduce (k, e, he , List.append tl' s)
164     | (k, e, C.Appl l, s) -> C.Appl (List.append (List.map (unwind k e) l) s) *)
165     | (k, e, (C.Const (uri,cookingsno) as t), s) ->
166        (match CicEnvironment.get_cooked_obj uri cookingsno with
167            C.Definition (_,body,_,_) -> reduce (0, [], body, s) 
168                                         (* constants are closed *)
169          | C.Axiom _ -> if s = [] then t else C.Appl (t::s)
170          | C.Variable _ -> raise ReferenceToVariable
171          | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s)
172          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
173        )
174     | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in 
175                                          if s = [] then t' else C.Appl (t'::s)
176     | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) -> 
177                                           let t' = unwind k e t in
178                                           if s = [] then t' else C.Appl (t'::s)
179     | (k, e, (C.MutCase (mutind,cookingsno,i,_,term,pl) as t),s) ->
180         let decofix =
181         function
182            C.CoFix (i,fl) as t ->
183             let (_,_,body) = List.nth fl i in
184              let body' =
185               let counter = ref (List.length fl) in
186                List.fold_right
187                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
188                 fl
189                 body
190              in
191               reduce (0,[],body',[])
192          | C.Appl (C.CoFix (i,fl) :: tl) ->
193             let (_,_,body) = List.nth fl i in
194              let body' =
195               let counter = ref (List.length fl) in
196                List.fold_right
197                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
198                 fl
199                 body
200              in
201               reduce (0,[], body', tl)
202          | t -> t
203        in
204         (match decofix (reduce (k, e,term,[])) with
205             C.MutConstruct (_,_,_,j) -> reduce (k, e, (List.nth pl (j-1)), s)
206           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
207              let (arity, r, num_ingredients) =
208               match CicEnvironment.get_obj mutind with
209                  C.InductiveDefinition (tl,ingredients,r) ->
210                    let (_,_,arity,_) = List.nth tl i
211                    and num_ingredients =
212                     List.fold_right
213                      (fun (k,l) i ->
214                        if k < cookingsno then i + List.length l else i
215                      ) ingredients 0
216                    in
217                     (arity,r,num_ingredients)
218                | _ -> raise WrongUriToInductiveDefinition
219              in
220               let ts =
221                let num_to_eat = r + num_ingredients in
222                 let rec eat_first =
223                  function
224                     (0,l) -> l
225                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
226                   | _ -> raise (Impossible 5)
227                 in
228                  eat_first (num_to_eat,tl)
229               in
230                reduce (k, e, (List.nth pl (j-1)),(ts@s)) 
231           | C.Cast _ | C.Implicit ->
232             raise (Impossible 2) (* we don't trust our whd ;-) *)
233          | _ -> let t' = unwind k e t in
234                 if s = [] then t' else C.Appl (t'::s)
235        )
236     | (k, e, (C.Fix (i,fl) as t), s) ->
237        let (_,recindex,_,body) = List.nth fl i in
238         let recparam =
239          try
240           Some (List.nth s recindex)
241          with
242           _ -> None
243         in
244          (match recparam with
245              Some recparam ->
246               (match reduce (0,[],recparam,[]) with
247                   (* match recparam with *) 
248                   C.MutConstruct _
249                 | C.Appl ((C.MutConstruct _)::_) ->
250                    (* OLD 
251                    let body' =
252                     let counter = ref (List.length fl) in
253                      List.fold_right
254                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
255                       fl
256                       body
257                    in 
258                     reduce (k, e, body', s) *)
259                    (* NEW *)
260                    let leng = List.length fl in
261                    let fl' = 
262                        let unwind_fl (name,recindex,typ,body) = 
263                            (name,recindex,unwind' leng k e typ, unwind' leng k e body)  in
264                        List.map unwind_fl fl in 
265                    let new_env =
266                      let counter = ref leng in
267                      let rec build_env e =
268                          if !counter = 0 then e else (decr counter; 
269                                     build_env ((C.Fix (!counter,fl'))::e)) in
270                      build_env e in
271                    reduce (k+leng, new_env, body,s)  
272                | _ -> let t' = unwind k e t in 
273                       if s = [] then t' else C.Appl (t'::s)
274              )
275           | None -> let t' = unwind k e t in 
276                     if s = [] then t' else C.Appl (t'::s)
277          )
278     | (k, e,(C.CoFix (i,fl) as t),s) -> let t' = unwind k e t in 
279        if s = [] then t' else C.Appl (t'::s);;
280
281 let rec whd = let module C = Cic in
282     function
283       C.Rel _ as t -> t
284     | C.Var _ as t -> reduce (0, [], t, [])
285     | C.Meta _ as t -> t
286     | C.Sort _ as t -> t
287     | C.Implicit as t -> t
288     | C.Cast (te,ty) -> whd te
289     | C.Prod _ as t -> t
290     | C.Lambda _ as t -> t
291     | C.LetIn (n,s,t) -> reduce (1, [s], t, [])
292     | C.Appl [] -> raise (Impossible 1)
293     | C.Appl (he::tl) -> reduce (0, [], he, tl)
294     | C.Const _ as t -> reduce (0, [], t, [])
295     | C.MutInd _ as t -> t
296     | C.MutConstruct _ as t -> t
297     | C.MutCase _ as t -> reduce (0, [], t, [])
298     | C.Fix _ as t -> reduce (0, [], t, [])
299     | C.CoFix _ as t -> reduce (0, [], t, [])
300     ;;
301
302 (* let whd t = reduce (0, [],t,[]);; 
303  let res = reduce (0, [],t,[]) in
304  let rescsc = CicReductionNaif.whd t in
305   if not (CicReductionNaif.are_convertible res rescsc) then
306    begin
307     prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
308     flush stderr ;
309     prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
310     flush stderr ;
311     prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
312     flush stderr ;
313     assert false ;
314    end
315   else 
316    res ;; *)
317
318
319 (* t1, t2 must be well-typed *)
320 let are_convertible = 
321  let rec aux t1 t2 = 
322  if t1 = t2 then true
323  else
324   let aux2 t1 t2 =
325    let module U = UriManager in
326    let module C = Cic in 
327       match (t1,t2) with
328          (C.Rel n1, C.Rel n2) -> n1 = n2
329        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
330        | (C.Meta n1, C.Meta n2) -> n1 = n2
331        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
332        | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
333           aux s1 s2 && aux t1 t2
334        | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
335           aux s1 s2 && aux t1 t2
336        | (C.Appl l1, C.Appl l2) ->
337           (try
338             List.fold_right2 (fun  x y b -> aux x y && b) l1 l2 true 
339            with
340             Invalid_argument _ -> false
341           )
342        | (C.Const (uri1,_), C.Const (uri2,_)) ->
343            U.eq uri1 uri2 
344        | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
345            U.eq uri1 uri2 && i1 = i2
346        | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
347            U.eq uri1 uri2 && i1 = i2 && j1 = j2
348        | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
349           C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> 
350            (* aux outtype1 outtype2 should be true if aux pl1 pl2 *)
351            U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 &&
352             aux term1 term2 &&
353             List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true
354        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
355           i1 = i2 &&
356            List.fold_right2
357             (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
358               b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2)
359             fl1 fl2 true
360        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
361           i1 = i2 &&
362            List.fold_right2
363             (fun (_,ty1,bo1) (_,ty2,bo2) b ->
364               b && aux ty1 ty2 && aux bo1 bo2)
365             fl1 fl2 true
366        | (_,_) -> false
367   in
368    if aux2 t1 t2 then true
369    else aux2 (whd t1) (whd t2)
370 in
371  aux 
372 ;; 
373
374
375
376
377
378
379
380
381
382
383