X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgType.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgType.ml;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=f23da87d09fad4304838ccff99d8c5420756b5ae;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml
deleted file mode 100644
index f23da87d0..000000000
--- a/helm/software/lambda-delta/src/basic_rg/brgType.ml
+++ /dev/null
@@ -1,132 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module U  = NUri
-module C  = Cps
-module W  = Share
-module L  = Log
-module H  = Hierarchy
-module E  = Entity
-module N  = Level
-module B  = Brg
-module BE = BrgEnvironment
-module BS = BrgSubstitution
-module BR = BrgReduction
-
-type message = (BR.kam, B.term) Log.message
-
-(* Internal functions *******************************************************)
-
-let level = 4
-
-let message1 st1 m t1 =
-   L.et_items1 "In the environment" m st1 t1
-
-let log1 s m t =
-   let s =  s ^ " the term" in
-   L.log BR.specs level (message1 s m t) 
-
-let error1 err s m t =
-   err (message1 s m t)
-
-let message3 m t1 t2 ?mu t3 =    
-   let sm, st1, st2 = "In the environment", "the term", "is of type" in
-   match mu with
-      | Some mu ->
-         let smu, st3 = "but in the environment", "it must be of type" in
-         L.et_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3
-      | None    ->
-         let st3 = "but it must be of type" in
-         L.et_items3 sm m st1 t1 st2 t2 st3 t3
-   
-let error3 err m t1 t2 ?mu t3 =
-   err (message3 m t1 t2 ?mu t3)
-
-let assert_convertibility err f st m u w v =
-   if BR.are_convertible st m u m w then f () else
-   error3 err m v w u
-
-let assert_applicability err f st m u w v =
-   match BR.xwhd st m u with 
-      | _, B.Sort _                      ->
-         error1 err "not a function type" m u
-      | mu, B.Bind (_, B.Abst (_, u), _) -> 
-         if BR.are_convertible st mu u m w then f () else
-	 error3 err m v w ~mu u
-      | _                                -> assert false (**)
-
-let rec b_type_of err f st m x =
-   log1 "Now checking" m x;
-   match x with
-   | B.Sort (a, h)           ->
-      let h = H.apply h in f x (B.Sort (a, h)) 
-   | B.LRef (_, i)           ->
-      begin match BR.get m i with
-         | B.Abst (_, w)     ->
-	    f x (BS.lift (succ i) (0) w)
-	 | B.Abbr (B.Cast (_, w, _)) -> 
-	    f x (BS.lift (succ i) (0) w)
-	 | B.Abbr _                  -> assert false
-	 | B.Void                    -> 
-	    error1 err "reference to excluded variable" m x
-      end
-   | B.GRef (_, uri)         ->
-      begin match BE.get_entity uri with
-         | _, _, E.Abst (_, w)             -> f x w
-	 | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
-	 | _, _, E.Abbr _                  -> assert false
-	 | _, _, E.Void                    ->
-            error1 err "reference to unknown entry" m x
-      end
-   | B.Bind (a, B.Abbr v, t) ->
-      let f xv xt tt =
-         f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
-      in
-      let f xv m = b_type_of err (f xv) st m t in
-      let f xv = f xv (BR.push m a (B.abbr xv)) in
-      let f xv vv = match xv with 
-	 | B.Cast _ -> f xv
-         | _        -> f (B.Cast ([], vv, xv))
-      in
-      type_of err f st m v
-   | B.Bind (a, B.Abst (n, u), t) ->
-      let f xu xt tt =
-	 f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
-      in
-      let f xu m = b_type_of err (f xu) st m t in
-      let f xu _ = f xu (BR.push m a (B.abst n xu)) in
-      type_of err f st m u
-   | B.Bind (a, B.Void, t)   ->
-      let f xt tt = 
-         f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
-      in
-      b_type_of err f st (BR.push m a B.Void) t
-         
-   | B.Appl (a, v, t)        ->
-      let f xv vv xt tt = 
-         let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
-         assert_applicability err f st m tt vv xv
-      in
-      let f xv vv = b_type_of err (f xv vv) st m t in
-      type_of err f st m v
-   | B.Cast (a, u, t)        ->
-      let f xu xt tt =  
-	 let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
-         assert_convertibility err f st m xu tt xt
-      in
-      let f xu _ = b_type_of err (f xu) st m t in
-      type_of err f st m u
-
-(* Interface functions ******************************************************)
-
-and type_of err f st m x =
-   let f t u = L.unbox level; f t u in
-   L.box level; b_type_of err f st m x