helm/ocaml/cic_proof_checking/cicElim.ml

   1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 exception Elim_failure of string
  29 exception Can_t_eliminate
  30
  31 (*
  32 let debug_print = fun _ -> () *)
  33 let debug_print = prerr_endline
  34
  35 let counter = ref ~-1 ;;
  36
  37 let fresh_binder () =  Cic.Name "matita_dummy"
  38 (*
  39  incr counter;
  40  Cic.Name ("e" ^ string_of_int !counter) *)
  41
  42   (** verifies if a given inductive type occurs in a term in target position *)
  43 let rec recursive uri typeno = function
  44   | Cic.Prod (_, _, target) -> recursive uri typeno target
  45   | Cic.MutInd (uri', typeno', [])
  46   | Cic.Appl (Cic.MutInd  (uri', typeno', []) :: _) ->
  47       UriManager.eq uri uri' && typeno = typeno'
  48   | _ -> false
  49
  50   (** given a list of constructor types, return true if at least one of them is
  51   * recursive, false otherwise *)
  52 let recursive_type uri typeno constructors =
  53   let rec aux = function
  54     | Cic.Prod (_, src, tgt) -> recursive uri typeno src || aux tgt
  55     | _ -> false
  56   in
  57   List.exists (fun (_, ty) -> aux ty) constructors
  58
  59 let unfold_appl = function
  60   | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl)
  61   | t -> t
  62
  63 let rec split l n =
  64  match (l,n) with
  65     (l,0) -> ([], l)
  66   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  67   | (_,_) -> assert false
  68
  69   (** build elimination principle part related to a single constructor
  70   * @param paramsno number of Prod to ignore in this constructor (i.e. number of
  71   * inductive parameters)
  72   * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *)
  73 let rec delta (uri, typeno) dependent paramsno consno t p args =
  74   match t with
  75   | Cic.MutInd (uri', typeno', []) when
  76     UriManager.eq uri uri' && typeno = typeno' ->
  77       if dependent then
  78         (match args with
  79         | [] -> assert false
  80         | [arg] -> unfold_appl (Cic.Appl [p; arg])
  81         | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)]))
  82       else
  83         p
  84   | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when
  85     UriManager.eq uri uri' && typeno = typeno' ->
  86       let (lparams, rparams) = split tl paramsno in
  87       if dependent then
  88         (match args with
  89         | [] -> assert false
  90         | [arg] -> unfold_appl (Cic.Appl (p :: rparams @ [arg]))
  91         | _ ->
  92             unfold_appl (Cic.Appl (p ::
  93               rparams @ [unfold_appl (Cic.Appl args)])))
  94       else  (* non dependent *)
  95         (match rparams with
  96         | [] -> p
  97         | _ -> Cic.Appl (p :: rparams))
  98   | Cic.Prod (binder, src, tgt) ->
  99       if recursive uri typeno src then
 100         let args = List.map (CicSubstitution.lift 2) args in
 101         let phi =
 102           let src = CicSubstitution.lift 1 src in
 103           delta (uri, typeno) dependent paramsno consno src
 104             (CicSubstitution.lift 1 p) [Cic.Rel 1]
 105         in
 106         let tgt = CicSubstitution.lift 1 tgt in
 107         Cic.Prod (fresh_binder (), src,
 108           Cic.Prod (Cic.Anonymous, phi,
 109             delta (uri, typeno) dependent paramsno consno tgt
 110               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
 111       else  (* non recursive *)
 112         let args = List.map (CicSubstitution.lift 1) args in
 113         Cic.Prod (fresh_binder (), src,
 114           delta (uri, typeno) dependent paramsno consno tgt
 115             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
 116   | _ -> assert false
 117
 118 let rec strip_left_params consno leftno = function
 119   | t when leftno = 0 -> t (* no need to lift, the term is (hopefully) closed *)
 120   | Cic.Prod (_, _, tgt) (* when leftno > 0 *) ->
 121       (* after stripping the parameters we lift of consno. consno is 1 based so,
 122       * the first constructor will be lifted by 1 (for P), the second by 2 (1
 123       * for P and 1 for the 1st constructor), and so on *)
 124       if leftno = 1 then
 125         CicSubstitution.lift consno tgt
 126       else
 127         strip_left_params consno (leftno - 1) tgt
 128   | _ -> assert false
 129
 130 let delta (ury, typeno) dependent paramsno consno t p args =
 131   let t = strip_left_params consno paramsno t in
 132   delta (ury, typeno) dependent paramsno consno t p args
 133
 134 let rec add_params binder indno ty eliminator =
 135   if indno = 0 then
 136     eliminator
 137   else
 138     match ty with
 139     | Cic.Prod (name, src, tgt) ->
 140        let name =
 141         match name with
 142            Cic.Name _ -> name
 143          | Cic.Anonymous -> fresh_binder ()
 144        in
 145         binder name src (add_params binder (indno - 1) tgt eliminator)
 146     | _ -> assert false
 147
 148 let rec mk_rels consno = function
 149   | 0 -> []
 150   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
 151
 152 let rec strip_pi = function
 153   | Cic.Prod (_, _, tgt) -> strip_pi tgt
 154   | t -> t
 155
 156 let rec count_pi = function
 157   | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
 158   | t -> 0
 159
 160 let rec type_of_p sort dependent leftno indty = function
 161   | Cic.Prod (n, src, tgt) when leftno = 0 ->
 162       let n =
 163        if dependent then
 164         match n with
 165            Cic.Name _ -> n
 166          | Cic.Anonymous -> fresh_binder ()
 167        else
 168         n
 169       in
 170        Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
 171   | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
 172   | t ->
 173       if dependent then
 174         Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort)
 175       else
 176         Cic.Sort sort
 177
 178 let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
 179   | Cic.Prod (_, src, tgt) when strip = 0 ->
 180       Cic.Prod (fresh_binder (),
 181         CicSubstitution.lift_from liftfrom liftno src,
 182         add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
 183   | Cic.Prod (_, _, tgt) ->
 184       add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
 185   | t ->
 186       if dependent then
 187         Cic.Prod (fresh_binder (),
 188           CicSubstitution.lift_from (rightno + 1) liftno indty,
 189           Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
 190       else
 191         Cic.Prod (Cic.Anonymous,
 192           CicSubstitution.lift_from (rightno + 1) liftno indty,
 193           if rightno = 0 then
 194             Cic.Rel (1 + liftno + rightno)
 195           else
 196             Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
 197
 198 let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
 199 function
 200   | Cic.Prod (_, src, tgt) when strip = 0 ->
 201       Cic.Lambda (fresh_binder (),
 202         CicSubstitution.lift_from liftfrom liftno src,
 203         add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
 204           case tgt)
 205   | Cic.Prod (_, _, tgt) ->
 206       add_right_lambda true (strip - 1) liftno liftfrom rightno indty
 207         case tgt
 208   | t ->
 209       Cic.Lambda (fresh_binder (),
 210         CicSubstitution.lift_from (rightno + 1) liftno indty, case)
 211
 212 let rec branch (uri, typeno) insource paramsno t fix head args =
 213   match t with
 214   | Cic.MutInd (uri', typeno', []) when
 215     UriManager.eq uri uri' && typeno = typeno' ->
 216       if insource then
 217         (match args with
 218         | [arg] -> Cic.Appl (fix :: args)
 219         | _ -> Cic.Appl (head :: [Cic.Appl args]))
 220       else
 221         (match args with
 222         | [] -> head
 223         | _ -> Cic.Appl (head :: args))
 224   | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when
 225     UriManager.eq uri uri' && typeno = typeno' ->
 226       if insource then
 227         let (lparams, rparams) = split tl paramsno in
 228         match args with
 229         | [arg] -> Cic.Appl (fix :: rparams @ args)
 230         | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args])
 231       else
 232         (match args with
 233         | [] -> head
 234         | _ -> Cic.Appl (head :: args))
 235   | Cic.Prod (binder, src, tgt) ->
 236       if recursive uri typeno src then
 237         let args = List.map (CicSubstitution.lift 1) args in
 238         let phi =
 239           let fix = CicSubstitution.lift 1 fix in
 240           let src = CicSubstitution.lift 1 src in
 241           branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
 242         in
 243         Cic.Lambda (fresh_binder (), src,
 244           branch (uri, typeno) insource paramsno tgt
 245             (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
 246             (args @ [Cic.Rel 1; phi]))
 247       else  (* non recursive *)
 248         let args = List.map (CicSubstitution.lift 1) args in
 249         Cic.Lambda (fresh_binder (), src,
 250           branch (uri, typeno) insource paramsno tgt
 251           (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
 252             (args @ [Cic.Rel 1]))
 253   | _ -> assert false
 254
 255 let branch (uri, typeno) insource liftno paramsno t fix head args =
 256   let t = strip_left_params liftno paramsno t in
 257   branch (uri, typeno) insource paramsno t fix head args
 258
 259 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 260   counter := ~-1;
 261   let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
 262   match obj with
 263   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
 264       let (name, inductive, ty, constructors) =
 265         try
 266           List.nth indTypes typeno
 267         with Failure _ -> assert false
 268       in
 269       let paramsno = count_pi ty in (* number of (left or right) parameters *)
 270       let rightno = paramsno - leftno in
 271       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
 272       let conslen = List.length constructors in
 273       let consno = ref (conslen + 1) in
 274       if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
 275         raise Can_t_eliminate;
 276       let indty =
 277         let indty = Cic.MutInd (uri, typeno, []) in
 278         if paramsno = 0 then
 279           indty
 280         else
 281           Cic.Appl (indty :: mk_rels 0 paramsno)
 282       in
 283       let mk_constructor consno =
 284         let constructor = Cic.MutConstruct (uri, typeno, consno, []) in
 285         if leftno = 0 then
 286           constructor
 287         else
 288           Cic.Appl (constructor :: mk_rels consno leftno)
 289       in
 290       let p_ty = type_of_p sort dependent leftno indty ty in
 291       let final_ty =
 292         add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
 293       in
 294       let eliminator_type =
 295         let cic =
 296           Cic.Prod (Cic.Name "P", p_ty,
 297             (List.fold_right
 298               (fun (_, constructor) acc ->
 299                 decr consno;
 300                 let p = Cic.Rel !consno in
 301                 Cic.Prod (Cic.Anonymous,
 302                   (delta (uri, typeno) dependent leftno !consno
 303                     constructor p [mk_constructor !consno]),
 304                   acc))
 305               constructors final_ty))
 306         in
 307         add_params (fun b s t -> Cic.Prod (b, s, t)) leftno ty cic
 308       in
 309       let consno = ref (conslen + 1) in
 310       let eliminator_body =
 311         let fix = Cic.Rel (rightno + 2) in
 312         let is_recursive = recursive_type uri typeno constructors in
 313         let recshift = if is_recursive then 1 else 0 in
 314         let (_, branches) =
 315           List.fold_right
 316             (fun (_, ty) (shift, branches) ->
 317               let head = Cic.Rel (rightno + shift + 1 + recshift) in
 318               let b =
 319                 branch (uri, typeno) false
 320                   (rightno + conslen + 2 + recshift) leftno ty fix head []
 321               in
 322               (shift + 1,  b :: branches))
 323             constructors (1, [])
 324         in
 325         let shiftno  = conslen + rightno + 2 + recshift in
 326         let outtype =
 327          if dependent then
 328           Cic.Rel shiftno
 329          else
 330           let head =
 331            if rightno = 0 then
 332             CicSubstitution.lift 1 (Cic.Rel shiftno)
 333            else
 334             Cic.Appl
 335              ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) ::
 336               mk_rels 1 rightno)
 337           in
 338            add_right_lambda true leftno shiftno 1 rightno indty head ty
 339         in
 340         let mutcase =
 341           Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches)
 342         in
 343         let body =
 344           if is_recursive then
 345             let fixfun =
 346               add_right_lambda dependent leftno (conslen + 2) 1 rightno
 347                 indty mutcase ty
 348             in
 349             (* rightno is the decreasing argument, i.e. the argument of
 350              * inductive type *)
 351             Cic.Fix (0, ["f", rightno, final_ty, fixfun])
 352           else
 353             add_right_lambda dependent leftno (conslen + 1) 1 rightno indty
 354               mutcase ty
 355         in
 356         let cic =
 357           Cic.Lambda (Cic.Name "P", p_ty,
 358             (List.fold_right
 359               (fun (_, constructor) acc ->
 360                 decr consno;
 361                 let p = Cic.Rel !consno in
 362                 Cic.Lambda (fresh_binder (),
 363                   (delta (uri, typeno) dependent leftno !consno
 364                     constructor p [mk_constructor !consno]),
 365                   acc))
 366               constructors body))
 367         in
 368         add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic
 369       in
 370 debug_print (CicPp.ppterm eliminator_type);
 371 debug_print (CicPp.ppterm eliminator_body);
 372       let eliminator_type =
 373         FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in
 374       let eliminator_body =
 375         FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in
 376 debug_print (CicPp.ppterm eliminator_type);
 377 debug_print (CicPp.ppterm eliminator_body);
 378       let (computed_type, ugraph) =
 379         try
 380           CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
 381         with CicTypeChecker.TypeCheckerFailure msg ->
 382           raise (Elim_failure (sprintf
 383             "type checker failure while type checking:\n%s\nerror:\n%s"
 384             (CicPp.ppterm eliminator_body) msg))
 385       in
 386       if not (fst (CicReduction.are_convertible []
 387         eliminator_type computed_type ugraph))
 388       then
 389         raise (Failure (sprintf
 390           "internal error: type mismatch on eliminator type\n%s\n%s"
 391           (CicPp.ppterm eliminator_type) (CicPp.ppterm computed_type)));
 392       let suffix =
 393         match sort with
 394         | Cic.Prop -> "_ind"
 395         | Cic.Set -> "_rec"
 396         | Cic.Type _ -> "_rect"
 397         | _ -> assert false
 398       in
 399       let name = UriManager.name_of_uri uri ^ suffix in
 400       let buri = UriManager.buri_of_uri uri in
 401       let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
 402       let obj_attrs = [`Class (`Elim sort); `Generated] in
 403        uri,
 404        Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs)
 405   | _ ->
 406       failwith (sprintf "not an inductive definition (%s)"
 407         (UriManager.string_of_uri uri))
 408