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