components/acic_procedural/proceduralConversion.ml

   1 (* Copyright (C) 2003-2005, 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 module C = Cic
  27
  28 let rec need_whd i = function
  29    | C.ACast (_, t, _)               -> need_whd i t
  30    | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
  31    | _                    when i > 0 -> true
  32    | _                               -> false
  33
  34 let lift k n =
  35    let rec lift_xns k (uri, t) = uri, lift_term k t
  36    and lift_ms k = function
  37       | None   -> None
  38       | Some t -> Some (lift_term k t)
  39    and lift_fix len k (id, name, i, ty, bo) =
  40       id, name, i, lift_term k ty, lift_term (k + len) bo
  41    and lift_cofix len k (id, name, ty, bo) =
  42       id, name, lift_term k ty, lift_term (k + len) bo
  43    and lift_term k = function
  44       | C.ASort _ as t -> t
  45       | C.AImplicit _ as t -> t
  46       | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
  47       | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
  48       | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
  49       | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
  50       | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
  51       | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
  52       | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
  53       | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
  54       | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
  55       | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
  56       | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
  57       | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
  58       | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
  59       | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
  60    in
  61    lift_term k