X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=4ff7d93921f8ed2b284a02961adac4d589f4c741;hb=7db7305941a97d43480cf58c08a154ed79f300cb;hp=ba72a37a2a6edbfe8300007f140358765a46e7cc;hpb=797425e905a9d26bb21f18d234a34ed211bcf92c;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index ba72a37a2..4ff7d9392 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -34,15 +34,15 @@ exception NotWellFormedTypeOfInductiveConstructor of string;; exception WrongRequiredArgument of string;; let fdebug = ref 0;; -let debug t env = +let debug t context = let rec debug_aux t i = let module C = Cic in let module U = UriManager in CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i in if !fdebug = 0 then - raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) "")) - (*print_endline ("\n" ^ List.fold_right debug_aux (t::env) "") ; flush stdout*) + raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) "")) + (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) ;; let rec split l n = @@ -1023,8 +1023,8 @@ and type_of_branch argsno need_dummy outtype term constype = (* type_of_aux' is just another name (with a different scope) for type_of_aux *) -and type_of_aux' metasenv env t = - let rec type_of_aux env = +and type_of_aux' metasenv context t = + let rec type_of_aux context = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -1033,7 +1033,7 @@ and type_of_aux' metasenv env t = C.Rel n -> let t = try - List.nth env (n - 1) + List.nth context (n - 1) with _ -> raise (NotWellTyped "Not a close term") in @@ -1048,25 +1048,25 @@ and type_of_aux' metasenv env t = | C.Implicit -> raise (Impossible 21) | C.Cast (te,ty) -> let _ = type_of ty in - if R.are_convertible (type_of_aux env te) ty then ty + if R.are_convertible (type_of_aux context te) ty then ty else raise (NotWellTyped "Cast") | C.Prod (_,s,t) -> - let sort1 = type_of_aux env s - and sort2 = type_of_aux (s::env) t in + let sort1 = type_of_aux context s + and sort2 = type_of_aux (s::context) t in sort_of_prod (sort1,sort2) | C.Lambda (n,s,t) -> - let sort1 = type_of_aux env s - and type2 = type_of_aux (s::env) t in - let sort2 = type_of_aux (s::env) type2 in + let sort1 = type_of_aux context s + and type2 = type_of_aux (s::context) t in + let sort2 = type_of_aux (s::context) type2 in (* 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 t' = CicSubstitution.subst s t in - type_of_aux env t' + type_of_aux context t' | 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 + let hetype = type_of_aux context he + and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in eat_prods hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") | C.Const (uri,cookingsno) -> @@ -1085,7 +1085,7 @@ and type_of_aux' metasenv env t = in cty | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> - let outsort = type_of_aux env outtype in + let outsort = type_of_aux context outtype in let (need_dummy, k) = let rec guess_args t = match CicReduction.whd t with @@ -1109,7 +1109,7 @@ and type_of_aux' metasenv env t = if not b then (b, k - 1) else (b, k) in let (parameters, arguments) = - match R.whd (type_of_aux env term) with + match R.whd (type_of_aux context term) with (*CSC manca il caso dei CAST *) C.MutInd (uri',_,i') -> (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*) @@ -1134,7 +1134,7 @@ and type_of_aux' metasenv env t = C.Appl ((C.MutInd (uri,cookingsno,i))::parameters) in if not (check_allowed_sort_elimination uri i need_dummy - sort_of_ind_type (type_of_aux env sort_of_ind_type) outsort) + sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) then raise (NotWellTyped "MutCase: not allowed sort elimination") ; @@ -1156,9 +1156,9 @@ and type_of_aux' metasenv env t = (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) in (j + 1, b && - R.are_convertible (type_of_aux env p) + R.are_convertible (type_of_aux context p) (type_of_branch parsno need_dummy outtype cons - (type_of_aux env cons)) + (type_of_aux context cons)) ) ) (1,true) (List.combine pl cl) in @@ -1174,13 +1174,14 @@ and type_of_aux' metasenv env t = | C.Fix (i,fl) -> let types_times_kl = List.rev - (List.map (fun (_,k,ty,_) -> let _ = type_of_aux env ty in (ty,k)) fl) + (List.map + (fun (_,k,ty,_) -> let _ = type_of_aux context ty in (ty,k)) fl) in let (types,kl) = List.split types_times_kl in let len = List.length types in List.iter (fun (name,x,ty,bo) -> - if (R.are_convertible (type_of_aux (types @ env) bo) + if (R.are_convertible (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) then begin @@ -1198,12 +1199,13 @@ and type_of_aux' metasenv env t = ty | C.CoFix (i,fl) -> let types = - List.rev (List.map (fun (_,ty,_) -> let _ = type_of_aux env ty in ty) fl) + List.rev + (List.map (fun (_,ty,_) -> let _ = type_of_aux context ty in ty) fl) in let len = List.length types in List.iter (fun (_,ty,bo) -> - if (R.are_convertible (type_of_aux (types @ env) bo) + if (R.are_convertible (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) then begin @@ -1286,19 +1288,19 @@ and type_of_aux' metasenv env t = | _ -> None in - type_of_aux env t + type_of_aux context t (* is a small constructor? *) (*CSC: ottimizzare calcolando staticamente *) and is_small paramsno c = - let rec is_small_aux env c = + let rec is_small_aux context c = let module C = Cic in match CicReduction.whd c with C.Prod (_,so,de) -> (*CSC: [] is an empty metasenv. Is it correct? *) - let s = type_of_aux' [] env so in + let s = type_of_aux' [] context so in (s = C.Sort C.Prop || s = C.Sort C.Set) && - is_small_aux (so::env) de + is_small_aux (so::context) de | _ -> true (*CSC: we trust the type-checker *) in let (sx,dx) = split_prods paramsno c in @@ -1347,3 +1349,19 @@ let typecheck uri = Logger.log (`Type_checking_completed uri) ;; +(*******************************************************) +(*CSC: Da qua in avanti deve sparire tutto *) +exception NotImplemented +let wrong_context_of_context context = + let module C = Cic in + List.map + (function + C.Decl bt -> bt + | C.Def bt -> raise NotImplemented + ) context +;; + +let type_of_aux' metasenv context t = + let context' = wrong_context_of_context context in + type_of_aux' metasenv context' t +;;