matita/matita/lib/lambda-delta/language/weight.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda-delta/language/lenv.ma".
  13
  14 (* WEIGHTS ******************************************************************)
  15
  16 (* the weight of a term *)
  17 let rec tw T ≝ match T with
  18    [ TSort _     ⇒ 1
  19    | TLRef _     ⇒ 1
  20    | TCon2 _ V T ⇒ tw V + tw T + 1
  21    ].
  22
  23 interpretation "weight (term)" 'Weight T = (tw T).
  24
  25 (* the weight of a local environment *)
  26 let rec lw L ≝ match L with
  27    [ LSort       ⇒ 0
  28    | LCon2 L _ V ⇒ lw L + #V
  29    ].
  30
  31 interpretation "weight (local environment)" 'Weight L = (lw L).
  32
  33 (* the weight of a closure *)
  34 definition cw ≝ λL,T. #L + #T.
  35
  36 interpretation "weight (closure)" 'Weight L T = (cw L T).