helm/ocaml/cic_omdoc/eta_fixing.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 ReferenceToVariable;;
  27 exception RferenceToCurrentProof;;
  28 exception ReferenceToInductiveDefinition;;
  29
  30 let rec fix_lambdas_wrt_type ty te =
  31  let module C = Cic in
  32  let module S = CicSubstitution in
  33 (*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
  34    flush stderr ; *)
  35    (* cast e altra porcheria ???? *)
  36    match ty,te with
  37      C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
  38        C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
  39    | C.Prod (_,s,ty'), C.Appl l ->
  40        prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
  41        flush stderr ;
  42        let l' = List.map (S.lift 1) l in
  43         C.Lambda (C.Name "x",s,
  44          fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
  45    | C.Prod (_,s,ty'), _ ->
  46        prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
  47        flush stderr ;
  48        let te' = S.lift 1 te in
  49         C.Lambda (C.Name "x",s,
  50           fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
  51    | _, _ -> te
  52 ;;
  53
  54 let fix_according_to_type ty hd tl =
  55  let module C = Cic in
  56  let module S = CicSubstitution in
  57   let rec aux ty tl res =
  58    (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty);
  59    flush stderr ; *)
  60    match ty with
  61       C.Rel _
  62     | C.Var _
  63     | C.Meta _
  64     | C.Sort _
  65     | C.Implicit ->
  66       (match tl with
  67          [] -> C.Appl res
  68        |  _ ->
  69          prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
  70          flush stderr ;
  71          C.LetIn
  72           (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
  73     | C.Cast (v,t) -> aux v tl res
  74     | C.Prod (n,s,t) ->
  75        (match tl with
  76           [] ->
  77             prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
  78          flush stderr ;
  79            let res' = List.map (S.lift 1) res
  80            in
  81            C.Lambda
  82             (C.Name "x", (* Andrea: to do: generate a fresh name *)
  83              s,
  84              aux t [] (res'@[C.Rel 1]))
  85         | hd::tl' ->
  86            let hd' = fix_lambdas_wrt_type s hd
  87            in
  88             aux (S.subst hd' t) tl' (res@[hd']))
  89     | C.Lambda _ -> assert false
  90     | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
  91     | C.Appl _
  92     | C.Const _
  93     | C.MutInd _
  94     | C.MutConstruct _
  95     | C.MutCase _
  96     | C.Fix _
  97     | C.CoFix _ -> (* ???? *)
  98        (match tl with
  99          [] -> C.Appl res
 100        |  _ -> (* Andrea: to do: generate a fresh name *)
 101          C.LetIn
 102           (C.Name "H",
 103            C.Appl res,
 104            C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
 105   in
 106   aux ty tl [hd]
 107 ;;
 108
 109 let eta_fix metasenv t =
 110  let rec eta_fix' t =
 111 (*  prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
 112   flush stderr ; *)
 113   let module C = Cic in
 114   match t with
 115      C.Rel n -> C.Rel n
 116    | C.Var (uri,exp_named_subst) ->
 117       let exp_named_subst' =
 118        List.map
 119         (function i,t -> i, (eta_fix' t)) exp_named_subst
 120       in
 121       C.Var (uri,exp_named_subst')
 122    | C.Meta (n,l) ->
 123       let (_,canonical_context,_) =
 124        List.find (function (m,_,_) -> n = m) metasenv
 125        in
 126        let l' =
 127         List.map2
 128          (fun ct t ->
 129           match (ct, t) with
 130             None, _ -> None
 131           | _, Some t -> Some (eta_fix' t)
 132           | Some _, None -> assert false (* due to typing rules *))
 133         canonical_context l
 134        in
 135        C.Meta (n,l')
 136    | C.Sort s -> C.Sort s
 137    | C.Implicit -> C.Implicit
 138    | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t)
 139    | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
 140    | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
 141    | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
 142    | C.Appl l ->
 143        let l' =  List.map eta_fix' l
 144        in
 145        (match l' with
 146          C.Const(uri,exp_named_subst)::l'' ->
 147            let constant_type =
 148              (match CicEnvironment.get_obj uri with
 149                C.Constant (_,_,ty,_) -> ty
 150              | C.Variable _ -> raise ReferenceToVariable
 151              | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
 152              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 153              )
 154            in
 155            fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
 156         | _ -> C.Appl l' )
 157    | C.Const (uri,exp_named_subst) ->
 158        let exp_named_subst' =
 159        List.map
 160         (function i,t -> i, (eta_fix' t)) exp_named_subst
 161        in
 162        C.Const (uri,exp_named_subst')
 163    | C.MutInd (uri,tyno,exp_named_subst) ->
 164        let exp_named_subst' =
 165        List.map
 166         (function i,t -> i, (eta_fix' t)) exp_named_subst
 167        in
 168         C.MutInd (uri, tyno, exp_named_subst')
 169    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 170        let exp_named_subst' =
 171        List.map
 172         (function i,t -> i, (eta_fix' t)) exp_named_subst
 173        in
 174         C.MutConstruct (uri, tyno, consno, exp_named_subst')
 175    | C.MutCase (uri, tyno, outty, term, patterns) ->
 176        C.MutCase (uri, tyno, eta_fix' outty,
 177               eta_fix' term, List.map eta_fix' patterns)
 178    | C.Fix (funno, funs) ->
 179        C.Fix (funno,
 180         List.map
 181          (fun (name, no, ty, bo) ->
 182            (name, no, eta_fix' ty, eta_fix' bo)) funs)
 183    | C.CoFix (funno, funs) ->
 184        C.CoFix (funno,
 185         List.map
 186          (fun (name, ty, bo) ->
 187            (name, eta_fix' ty, eta_fix' bo)) funs)
 188    in
 189    eta_fix' t
 190 ;;
 191