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 let fresh_binder =
  27   let counter = ref ~-1 in
  28   fun () ->
  29     incr counter;
  30     "elim" ^ string_of_int !counter
  31
  32   (** verifies if a given uri occurs in a term in target position *)
  33 let rec recursive uri = function
  34   | Cic.Prod (_, _, target) -> recursive uri target
  35   | Cic.MutInd (uri', _, _)
  36   | Cic.Appl [ Cic.MutInd (uri', _, _); _ ] -> UriManager.eq uri uri'
  37   | _ -> false
  38
  39 let unfold_appl = function
  40   | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl)
  41   | t -> t
  42
  43   (** build elimination principle part related to a single constructor
  44   * @param strip number of Prod to ignore in this constructor (i.e. number of
  45   * inductive parameters) *)
  46 let rec delta (uri, typeno, subst) strip consno t p args =
  47   assert (subst = []);
  48   match t with
  49   | Cic.MutInd (uri', typeno', subst')
  50   | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) when
  51     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
  52       (match args with
  53       | [] -> assert false
  54       | [arg] -> unfold_appl (Cic.Appl [p; arg])
  55       | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)]))
  56 (*
  57   | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) when
  58     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
  59       Cic.Appl (Cic.Rel p_rel :: args)
  60 *)
  61   | Cic.Prod (binder, src, tgt) when strip = 0 ->
  62       if recursive uri src then
  63         let args = List.map (CicSubstitution.lift 2) args in
  64         let phi =
  65           (delta (uri, typeno, subst) strip consno src
  66             (CicSubstitution.lift 1 p) [Cic.Rel 1])
  67         in
  68         Cic.Prod (Cic.Name (fresh_binder ()), src,
  69           Cic.Prod (Cic.Anonymous, phi,
  70             delta (uri, typeno, subst) strip consno tgt
  71               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
  72       else  (* non recursive *)
  73         let args = List.map (CicSubstitution.lift 1) args in
  74         Cic.Prod (Cic.Name (fresh_binder ()), src,
  75           delta (uri, typeno, subst) strip consno tgt (CicSubstitution.lift 1 p)
  76             (args @ [Cic.Rel 1]))
  77   | Cic.Prod (_, _, tgt) (* when strip > 0 *) ->
  78       (* after stripping the parameters we lift of 1 since P has been inserted
  79       * in the way *)
  80       let tgt =
  81         if strip = 1 then CicSubstitution.lift consno tgt else tgt
  82       in
  83       delta (uri, typeno, subst) (strip - 1) consno tgt p args
  84   | _ -> assert false
  85
  86 let rec add_params indno ty eliminator =
  87   if indno = 0 then
  88     eliminator
  89   else
  90     match ty with
  91     | Cic.Prod (binder, src, tgt) ->
  92         Cic.Prod (binder, src, add_params (indno - 1) tgt eliminator)
  93     | _ -> assert false
  94
  95 let rec mk_rels consno = function
  96   | 0 -> []
  97   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
  98
  99 let elim_of uri typeno =
 100   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
 101   let subst = [] in
 102   match obj with
 103   | Cic.InductiveDefinition (indTypes, params, indno) ->
 104       let (name, inductive, ty, constructors) =
 105         try
 106           List.nth indTypes typeno
 107         with Failure _ -> assert false
 108       in
 109       let conslen = List.length constructors in
 110       let consno = ref (conslen + 1) in
 111       let indty =
 112         let indty = Cic.MutInd (uri, typeno, subst) in
 113         if indno = 0 then
 114           indty
 115         else
 116           Cic.Appl (indty :: mk_rels 0 indno)
 117       in
 118       let mk_constructor consno =
 119         let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
 120         if indno = 0 then
 121           constructor
 122         else
 123           Cic.Appl (constructor :: mk_rels consno indno)
 124       in
 125       let eliminator =
 126         Cic.Prod (Cic.Name "P",
 127           (Cic.Prod (Cic.Anonymous,
 128             indty,
 129             (* Cic.MutInd (uri, typeno, subst), *)
 130             Cic.Sort (Cic.Type (CicUniv.fresh ())))),
 131           (List.fold_right
 132             (fun (_, constructor) acc ->
 133               decr consno;
 134               let p = Cic.Rel !consno in
 135               Cic.Prod (Cic.Anonymous,
 136                 (delta (uri, typeno, subst) indno !consno constructor p
 137                   [mk_constructor !consno]),
 138                 acc)) (* lift acc? see assumption above on delta *)
 139             constructors
 140             (Cic.Prod (Cic.Name (fresh_binder ()),
 141               CicSubstitution.lift (conslen + 1) indty
 142               (* Cic.MutInd (uri, typeno, subst) *),
 143               Cic.Appl [Cic.Rel (2 + conslen); Cic.Rel 1]))))
 144       in
 145       add_params indno ty eliminator
 146   | _ -> assert false
 147