X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FcicTypeChecker.ml;h=ea1c28ca2bac4bd9d852ee6da2fd0c4ad59f5fd9;hb=fee0de0784e725071b9d0742c139c19845f83713;hp=63433937b39bafec7166e0567dc9d763bc3014bd;hpb=c01d2aaea05f7385bee46addd900cd0397756389;p=helm.git diff --git a/helm/interface/cicTypeChecker.ml b/helm/interface/cicTypeChecker.ml index 63433937b..ea1c28ca2 100644 --- a/helm/interface/cicTypeChecker.ml +++ b/helm/interface/cicTypeChecker.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + exception NotImplemented;; exception Impossible;; exception NotWellTyped of string;; @@ -14,7 +39,7 @@ let debug t env = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", + CicPp.ppobj (C.Variable ("DEBUG", None, C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0), C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0), C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0), @@ -93,12 +118,19 @@ let rec cooked_type_of_constant uri cookingsno = and type_of_variable uri = let module C = Cic in let module R = CicReduction in + let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) match CicCache.is_type_checked uri 0 with - CicCache.CheckedObj (C.Variable (_,ty)) -> ty - | CicCache.UncheckedObj (C.Variable (_,ty)) -> + CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty + | CicCache.UncheckedObj (C.Variable (_,bo,ty)) -> (* only to check that ty is well-typed *) let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri))) + ) ; CicCache.set_type_checking_info uri ; ty | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) @@ -120,6 +152,8 @@ and does_not_occur n nn te = does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest | C.Lambda (_,so,dest) -> does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + | C.LetIn (_,so,dest) -> + does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur n nn x) l true | C.Const _ @@ -394,6 +428,7 @@ and recursive_args n nn te = | C.Prod (_,so,de) -> (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de) | C.Lambda _ -> raise Impossible (* due to type-checking *) + | C.LetIn _ -> raise NotImplemented | C.Appl _ -> [] | C.Const _ | C.Abst _ -> raise Impossible @@ -466,6 +501,10 @@ and check_is_really_smaller_arg n nn kl x safes te = check_is_really_smaller_arg n nn kl x safes so && check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + check_is_really_smaller_arg n nn kl x safes so && + check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) @@ -594,6 +633,10 @@ and guarded_by_destructors n nn kl x safes = guarded_by_destructors n nn kl x safes so && guarded_by_destructors (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + guarded_by_destructors n nn kl x safes so && + guarded_by_destructors (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in if not (List.length tl > k) then false @@ -742,6 +785,9 @@ and guarded_by_constructors n nn h = | C.Lambda (_,so,de) -> does_not_occur n nn so && guarded_by_constructors (n + 1) (nn + 1) h de + | C.LetIn (_,so,de) -> + does_not_occur n nn so && + guarded_by_constructors (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h = 1 && List.fold_right (fun x i -> i && does_not_occur n nn x) tl true @@ -971,6 +1017,10 @@ and type_of t = (* only to check if the product is well-typed *) let _ = sort_of_prod (sort1,sort2) in C.Prod (n,s,type2) + | C.LetIn (n,s,t) -> + let type1 = type_of_aux env s in + let type2 = type_of_aux (type1::env) t in + type2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux env he and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in @@ -1189,10 +1239,15 @@ let typecheck uri = debug (type_of te) [] ; if not (R.are_convertible (type_of te) ty) then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) - | C.Variable (_,ty) -> + | C.Variable (_,bo,ty) -> (* only to check that ty is well-typed *) - (*CSC [] wrong *) - let _ = type_of ty in () + let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) + ) | C.InductiveDefinition _ -> cooked_mutual_inductive_defs uri uobj ) ;