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