helm/ocaml/cic_proof_checking/cicReductionNaif.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    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
  38 ;;
  39
  40 exception Impossible of int;;
  41 exception ReferenceToConstant;;
  42 exception ReferenceToVariable;;
  43 exception ReferenceToCurrentProof;;
  44 exception ReferenceToInductiveDefinition;;
  45 exception RelToHiddenHypothesis;;
  46
  47 (* takes a well-typed term *)
  48 let whd context =
  49  let rec whdaux l =
  50   let module C = Cic in
  51   let module S = CicSubstitution in
  52    function
  53       C.Rel n as t ->
  54        (match List.nth context (n-1) with
  55            Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
  56          | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
  57           | None -> raise RelToHiddenHypothesis
  58        )
  59     | C.Var (uri,exp_named_subst) as t ->
  60         let o,_ =
  61           CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
  62         in
  63        (match o with
  64            C.Constant _ -> raise ReferenceToConstant
  65          | C.CurrentProof _ -> raise ReferenceToCurrentProof
  66          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
  67          | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
  68          | C.Variable (_,Some body,_,_,_) ->
  69             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
  70        )
  71     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
  72     | C.Sort _ as t -> t (* l should be empty *)
  73     | C.Implicit _ as t -> t
  74     | C.Cast (te,ty) -> whdaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
  75     | C.Prod _ as t -> t (* l should be empty *)
  76     | C.Lambda (name,s,t) as t' ->
  77        (match l with
  78            [] -> t'
  79          | he::tl -> whdaux tl (S.subst he t)
  80            (* when name is Anonimous the substitution should be superfluous *)
  81        )
  82     | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
  83     | C.Appl (he::tl) -> whdaux (tl@l) he
  84     | C.Appl [] -> raise (Impossible 1)
  85     | C.Const (uri,exp_named_subst) as t ->
  86         let o,_ =
  87           CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
  88         in
  89        (match o with
  90            C.Constant (_,Some body,_,_,_) ->
  91             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
  92          | C.Constant _ -> if l = [] then t else C.Appl (t::l)
  93          | C.Variable _ -> raise ReferenceToVariable
  94          | C.CurrentProof (_,_,body,_,_,_) ->
  95             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
  96          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
  97        )
  98     | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l)
  99     | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l)
 100     | C.MutCase (mutind,i,_,term,pl) as t->
 101        let decofix =
 102         function
 103            C.CoFix (i,fl) as t ->
 104             let (_,_,body) = List.nth fl i in
 105              let body' =
 106               let counter = ref (List.length fl) in
 107                List.fold_right
 108                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 109                 fl
 110                 body
 111              in
 112               whdaux [] body'
 113          | C.Appl (C.CoFix (i,fl) :: tl) ->
 114             let (_,_,body) = List.nth fl i in
 115              let body' =
 116               let counter = ref (List.length fl) in
 117                List.fold_right
 118                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 119                 fl
 120                 body
 121              in
 122               whdaux tl body'
 123          | t -> t
 124        in
 125         (match decofix (whdaux [] term) with
 126             C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1))
 127           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 128              let (arity, r) =
 129                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 130               match o with
 131                  C.InductiveDefinition (tl,ingredients,r,_) ->
 132                    let (_,_,arity,_) = List.nth tl i in
 133                     (arity,r)
 134                | _ -> raise WrongUriToInductiveDefinition
 135              in
 136               let ts =
 137                let rec eat_first =
 138                 function
 139                    (0,l) -> l
 140                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 141                  | _ -> raise (Impossible 5)
 142                in
 143                 eat_first (r,tl)
 144               in
 145                whdaux (ts@l) (List.nth pl (j-1))
 146           | C.Cast _ | C.Implicit _ ->
 147              raise (Impossible 2) (* we don't trust our whd ;-) *)
 148           | _ -> if l = [] then t else C.Appl (t::l)
 149        )
 150     | C.Fix (i,fl) as t ->
 151        let (_,recindex,_,body) = List.nth fl i in
 152         let recparam =
 153          try
 154           Some (List.nth l recindex)
 155          with
 156           _ -> None
 157         in
 158          (match recparam with
 159              Some recparam ->
 160               (match whdaux [] recparam with
 161                   C.MutConstruct _
 162                 | C.Appl ((C.MutConstruct _)::_) ->
 163                    let body' =
 164                     let counter = ref (List.length fl) in
 165                      List.fold_right
 166                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 167                       fl
 168                       body
 169                    in
 170                     (* Possible optimization: substituting whd recparam in l *)
 171                     whdaux l body'
 172                | _ -> if l = [] then t else C.Appl (t::l)
 173              )
 174           | None -> if l = [] then t else C.Appl (t::l)
 175          )
 176     | C.CoFix (i,fl) as t ->
 177        if l = [] then t else C.Appl (t::l)
 178  in
 179 (*CSC
 180 function t ->
 181 prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ;
 182 List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline "<PRIMA WHD" ; flush stderr ;
 183 let res =
 184 *)
 185   whdaux []
 186 (*CSC
 187 t in prerr_endline "DOPO WHD" ; flush stderr ; res
 188 *)
 189 ;;
 190
 191 (* t1, t2 must be well-typed *)
 192 let are_convertible c t1 t2 ugraph =
 193  let module U = UriManager in
 194  let rec aux test_equality_only context t1 t2 ugraph =
 195   let aux2 test_equality_only t1 t2 ugraph =
 196    (* this trivial euristic cuts down the total time of about five times ;-) *)
 197    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 198    if t1 = t2 then
 199     true,ugraph
 200    else
 201     begin
 202      let module C = Cic in
 203        match (t1,t2) with
 204           (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
 205         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 206             let b = U.eq uri1 uri2 in
 207             if b then
 208              (try
 209                List.fold_right2
 210                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 211                   (* FIXME: lazy! *)
 212                   let b',ugraph' = aux test_equality_only context x y ugraph in
 213                   (U.eq uri1 uri2 && b' && b),ugraph'
 214                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 215               with
 216                Invalid_argument _ -> false,ugraph
 217              )
 218             else
 219               false,ugraph
 220         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 221             let b = n1 = n2 in
 222             if b then
 223              List.fold_left2
 224               (fun (b,ugraph) t1 t2 ->
 225                 if b then
 226                   match t1,t2 with
 227                     None,_
 228                   | _,None  -> true,ugraph
 229                   | Some t1',Some t2' ->
 230                       aux test_equality_only context t1' t2' ugraph
 231                 else
 232                   false,ugraph
 233               ) (true,ugraph) l1 l2
 234             else
 235               false,ugraph
 236           (* TASSI: CONSTRAINTS *)
 237         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 238             true,(CicUniv.add_eq t2 t1 ugraph)
 239           (* TASSI: CONSTRAINTS *)
 240         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 241             true,(CicUniv.add_ge t2 t1 ugraph)
 242           (* TASSI: CONSTRAINTS *)
 243         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
 244           (* TASSI: CONSTRAINTS *)
 245         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
 246         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 247             let b',ugraph' = aux true context s1 s2 ugraph in
 248             if b' then
 249               aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 250                 t1 t2 ugraph'
 251             else
 252               false,ugraph
 253         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 254            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 255            if b' then
 256              aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 257                t1 t2 ugraph'
 258            else
 259              false,ugraph
 260         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 261            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 262            if b' then
 263             aux test_equality_only
 264              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
 265            else
 266              false,ugraph
 267         | (C.Appl l1, C.Appl l2) ->
 268            (try
 269              List.fold_right2
 270                (fun  x y (b,ugraph) ->
 271                  if b then
 272                    aux test_equality_only context x y ugraph
 273                  else
 274                    false,ugraph) l1 l2 (true,ugraph)
 275             with
 276              Invalid_argument _ -> false,ugraph
 277            )
 278         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 279             let b' = U.eq uri1 uri2 in
 280             if b' then
 281              (try
 282                List.fold_right2
 283                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 284                   if b && U.eq uri1 uri2 then
 285                     aux test_equality_only context x y ugraph
 286                   else
 287                     false,ugraph
 288                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 289               with
 290                Invalid_argument _ -> false,ugraph
 291              )
 292             else
 293               false,ugraph
 294         | (C.MutInd (uri1,i1,exp_named_subst1),
 295            C.MutInd (uri2,i2,exp_named_subst2)
 296           ) ->
 297             let b' = U.eq uri1 uri2 && i1 = i2 in
 298             if b' then
 299              (try
 300                List.fold_right2
 301                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 302                   if b && U.eq uri1 uri2 then
 303                     aux test_equality_only context x y ugraph
 304                   else
 305                    false,ugraph
 306                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 307               with
 308                Invalid_argument _ -> false,ugraph
 309              )
 310             else
 311               false,ugraph
 312         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 313            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 314           ) ->
 315             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
 316             if b' then
 317              (try
 318                List.fold_right2
 319                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 320                   if b && U.eq uri1 uri2 then
 321                     aux test_equality_only context x y ugraph
 322                   else
 323                     false,ugraph
 324                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 325               with
 326                Invalid_argument _ -> false,ugraph
 327              )
 328             else
 329               false,ugraph
 330         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 331            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 332             let b' = U.eq uri1 uri2 && i1 = i2 in
 333             if b' then
 334              let b'',ugraph''=aux test_equality_only context
 335                  outtype1 outtype2 ugraph in
 336              if b'' then
 337                let b''',ugraph'''= aux test_equality_only context
 338                    term1 term2 ugraph'' in
 339                List.fold_right2
 340                  (fun x y (b,ugraph) ->
 341                    if b then
 342                      aux test_equality_only context x y ugraph
 343                    else
 344                      false,ugraph)
 345                  pl1 pl2 (true,ugraph''')
 346              else
 347                false,ugraph
 348             else
 349               false,ugraph
 350         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 351            let tys =
 352             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 353            in
 354             if i1 = i2 then
 355              List.fold_right2
 356               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
 357                 if b && recindex1 = recindex2 then
 358                   let b',ugraph' = aux test_equality_only context ty1 ty2
 359                       ugraph in
 360                   if b' then
 361                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 362                   else
 363                     false,ugraph
 364                 else
 365                   false,ugraph)
 366              fl1 fl2 (true,ugraph)
 367             else
 368               false,ugraph
 369         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 370            let tys =
 371             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 372            in
 373             if i1 = i2 then
 374               List.fold_right2
 375               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
 376                 if b then
 377                   let b',ugraph' = aux test_equality_only context ty1 ty2
 378                       ugraph in
 379                   if b' then
 380                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 381                   else
 382                     false,ugraph
 383                 else
 384                   false,ugraph)
 385              fl1 fl2 (true,ugraph)
 386             else
 387               false,ugraph
 388         | (C.Cast _, _) | (_, C.Cast _)
 389         | (C.Implicit _, _) | (_, C.Implicit _) ->
 390             assert false
 391         | (_,_) -> false,ugraph
 392     end
 393   in
 394    let b,ugraph' = aux2 test_equality_only t1 t2 ugraph in
 395    if b then
 396      b,ugraph'
 397    else
 398     begin
 399      debug t1 [t2] "PREWHD";
 400      let t1' = whd context t1 in
 401      let t2' = whd context t2 in
 402       debug t1' [t2'] "POSTWHD";
 403       aux2 test_equality_only t1' t2' ugraph
 404     end
 405  in
 406   aux false c t1 t2 ugraph
 407 ;;