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