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   function
  29     | true ->
  30         incr counter;
  31         Cic.Name ("elim" ^ string_of_int !counter)
  32     | _ -> Cic.Anonymous
  33
  34   (** verifies if a given uri occurs in a term in target position *)
  35 let rec recursive uri = function
  36   | Cic.Prod (_, _, target) -> recursive uri target
  37   | Cic.MutInd (uri', _, _) -> UriManager.eq uri uri'
  38   | Cic.Appl args -> List.exists (recursive uri) args
  39   | _ -> false
  40
  41 let unfold_appl = function
  42   | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl)
  43   | t -> t
  44
  45 let rec split l n =
  46  match (l,n) with
  47     (l,0) -> ([], l)
  48   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  49   | (_,_) -> assert false
  50
  51   (** build elimination principle part related to a single constructor
  52   * @param paramsno number of Prod to ignore in this constructor (i.e. number of
  53   * inductive parameters)
  54   * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *)
  55 let rec delta (uri, typeno, subst) dependent paramsno consno t p args =
  56   assert (subst = []);
  57   match t with
  58   | Cic.MutInd (uri', typeno', subst') ->
  59       if dependent then
  60         (match args with
  61         | [] -> assert false
  62         | [arg] -> unfold_appl (Cic.Appl [p; arg])
  63         | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)]))
  64       else
  65         p
  66   | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
  67     UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
  68       let (lparams, rparams) = split tl paramsno in
  69       if dependent then
  70         (match args with
  71         | [] -> assert false
  72         | [arg] -> unfold_appl (Cic.Appl (p :: rparams @ [arg]))
  73         | _ ->
  74             unfold_appl (Cic.Appl (p ::
  75               rparams @ [unfold_appl (Cic.Appl args)])))
  76       else  (* non dependent *)
  77         (match rparams with
  78         | [] -> p
  79         | _ -> Cic.Appl (p :: rparams))
  80   | Cic.Prod (binder, src, tgt) ->
  81       if recursive uri src then
  82         let args = List.map (CicSubstitution.lift 2) args in
  83         let phi =
  84           (delta (uri, typeno, subst) dependent paramsno consno src
  85             (CicSubstitution.lift 1 p) [Cic.Rel 1])
  86         in
  87         Cic.Prod (fresh_binder dependent, src,
  88           Cic.Prod (Cic.Anonymous, phi,
  89             delta (uri, typeno, subst) dependent paramsno consno tgt
  90               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
  91       else  (* non recursive *)
  92         let args = List.map (CicSubstitution.lift 1) args in
  93         Cic.Prod (fresh_binder dependent, src,
  94           delta (uri, typeno, subst) dependent paramsno consno tgt
  95             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
  96   | _ -> assert false
  97
  98 let rec strip_left_params consno leftno = function
  99   | t when leftno = 0 -> t (* no need to lift, the term is (hopefully) closed *)
 100   | Cic.Prod (_, _, tgt) (* when leftno > 0 *) ->
 101       (* after stripping the parameters we lift of consno. consno is 1 based so,
 102       * the first constructor will be lifted by 1 (for P), the second by 2 (1
 103       * for P and 1 for the 1st constructor), and so on *)
 104       if leftno = 1 then
 105         CicSubstitution.lift consno tgt
 106       else
 107         strip_left_params consno (leftno - 1) tgt
 108   | _ -> assert false
 109
 110 let delta (ury, typeno, subst) dependent paramsno consno t p args =
 111   let t = strip_left_params consno paramsno t in
 112   delta (ury, typeno, subst) dependent paramsno consno t p args
 113
 114 let rec add_params indno ty eliminator =
 115   if indno = 0 then
 116     eliminator
 117   else
 118     match ty with
 119     | Cic.Prod (binder, src, tgt) ->
 120         Cic.Prod (binder, src, add_params (indno - 1) tgt eliminator)
 121     | _ -> assert false
 122
 123 let rec mk_rels consno = function
 124   | 0 -> []
 125   | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1)
 126
 127 let rec strip_pi = function
 128   | Cic.Prod (_, _, tgt) -> strip_pi tgt
 129   | t -> t
 130
 131 let rec count_pi = function
 132   | Cic.Prod (_, _, tgt) -> count_pi tgt + 1
 133   | t -> 0
 134
 135 let rec type_of_p dependent leftno indty = function
 136   | Cic.Prod (n, src, tgt) when leftno = 0 ->
 137       Cic.Prod (n, src, type_of_p dependent leftno indty tgt)
 138   | Cic.Prod (_, _, tgt) -> type_of_p dependent (leftno - 1) indty tgt
 139   | t ->
 140       if dependent then
 141         Cic.Prod (Cic.Anonymous, indty,
 142           Cic.Sort (Cic.Type (CicUniv.fresh ())))
 143       else
 144         Cic.Sort (Cic.Type (CicUniv.fresh ()))
 145
 146 let rec add_right_pi dependent strip liftno rightno indty = function
 147   | Cic.Prod (_, src, tgt) when strip = 0 ->
 148       Cic.Prod (fresh_binder true,
 149         CicSubstitution.lift liftno src,
 150         add_right_pi dependent strip liftno rightno indty tgt)
 151   | Cic.Prod (_, _, tgt) ->
 152       add_right_pi dependent (strip - 1) liftno rightno indty tgt
 153   | t ->
 154       if dependent then
 155         Cic.Prod (fresh_binder dependent,
 156           CicSubstitution.lift_from (rightno + 1) liftno indty,
 157           Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
 158       else
 159         Cic.Prod (Cic.Anonymous,
 160           CicSubstitution.lift_from (rightno + 1) liftno indty,
 161           if rightno = 0 then
 162             Cic.Rel (1 + liftno + rightno)
 163           else
 164             Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno))
 165
 166 let elim_of uri typeno =
 167   let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
 168   let subst = [] in
 169   match obj with
 170   | Cic.InductiveDefinition (indTypes, params, leftno) ->
 171       let (name, inductive, ty, constructors) =
 172         try
 173           List.nth indTypes typeno
 174         with Failure _ -> assert false
 175       in
 176       let paramsno = count_pi ty in (* number of (left or right) parameters *)
 177       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
 178       let conslen = List.length constructors in
 179       let consno = ref (conslen + 1) in
 180       let indty =
 181         let indty = Cic.MutInd (uri, typeno, subst) in
 182         if leftno = 0 then
 183           indty
 184         else
 185           Cic.Appl (indty :: mk_rels 0 paramsno)
 186       in
 187       let mk_constructor consno =
 188         let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
 189         if leftno = 0 then
 190           constructor
 191         else
 192           Cic.Appl (constructor :: mk_rels consno leftno)
 193       in
 194       let eliminator =
 195         let p_ty = type_of_p dependent leftno indty ty in
 196         let final_ty =
 197           add_right_pi dependent leftno (conslen + 1) (paramsno - leftno)
 198             indty ty
 199         in
 200         Cic.Prod (Cic.Name "P", p_ty,
 201           (List.fold_right
 202             (fun (_, constructor) acc ->
 203               decr consno;
 204               let p = Cic.Rel !consno in
 205               Cic.Prod (Cic.Anonymous,
 206                 (delta (uri, typeno, subst) dependent leftno !consno
 207                   constructor p [mk_constructor !consno]),
 208                 acc))
 209             constructors
 210             final_ty))
 211       in
 212       add_params leftno ty eliminator
 213   | _ -> assert false
 214