X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ee76389069b7456a89904c81e1728430476d7d91;hb=c11f4fe10591d568afb410e5d96061448a437254;hp=1db82a99fb48eeddcf63adb96c4a31575e2ca5e6;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 1db82a99f..ee7638906 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -186,7 +186,7 @@ let rec type_of_constant ~logger uri ugraph = CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError with Invalid_argument s -> - (*debug_print s;*) + (*debug_print (lazy s);*) uobj,ugraph_dust in match cobj,ugraph with @@ -227,7 +227,7 @@ and type_of_variable ~logger uri ugraph = | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError with Invalid_argument s -> - (*debug_print s;*) + (*debug_print (lazy s);*) ty,ugraph2) | _ -> raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) @@ -576,7 +576,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = ) with Invalid_argument s -> - (*debug_print s;*) + (*debug_print (lazy s);*) uobj,ugraph1_dust in match cobj with @@ -611,7 +611,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = raise CicEnvironmentError) with Invalid_argument s -> - (*debug_print s;*) + (*debug_print (lazy s);*) uobj,ugraph1_dust in match cobj with @@ -767,6 +767,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in List.fold_right (fun (p,(_,c)) i -> let rl' = @@ -778,7 +785,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = in i && check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -806,6 +813,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in (*CSC: supponiamo come prima che nessun controllo sia necessario*) (*CSC: sugli argomenti di una applicazione *) List.fold_right @@ -819,7 +833,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = in i && check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | _ -> List.fold_right (fun p i -> @@ -940,6 +954,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = i && guarded_by_destructors context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right @@ -950,7 +971,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = in i && guarded_by_destructors context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -981,6 +1002,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = i && guarded_by_destructors context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right @@ -998,7 +1026,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = in i && guarded_by_destructors context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | _ -> guarded_by_destructors context n nn kl x safes outtype && guarded_by_destructors context n nn kl x safes term && @@ -1299,21 +1327,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind false,ugraph1 else (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with - C.Sort C.Prop -> true,ugraph1 - | (C.Sort C.Set | C.Sort C.CProp) -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,_,_) -> - let (_,_,_,cl) = List.nth itl i in - (* is a singleton definition? *) - List.length cl = 1,ugraph1 - | _ -> - raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) - ) - | _ -> false,ugraph1 - ) + C.Sort C.Prop -> true,ugraph1 + | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) -> + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.InductiveDefinition (itl,_,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a singleton definition or the empty proposition? *) + (List.length cl = 1 || List.length cl = 0),ugraph1 + | _ -> + raise (TypeCheckerFailure + ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) + | _ -> false,ugraph1) | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta))) when not need_dummy -> @@ -1459,7 +1485,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Some (_,C.Decl t) -> S.lift n t,ugraph | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph | Some (_,C.Def (bo,None)) -> - debug_print "##### CASO DA INVESTIGARE E CAPIRE" ; + debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; type_of_aux ~logger context (S.lift n bo) ugraph | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") @@ -1757,9 +1783,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst ~metasenv context ty_p ty_branch ugraph3 in if not b1 then - debug_print + debug_print (lazy ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch); + " <==> " ^ CicPp.ppterm ty_branch)); (j + 1,b1,ugraph4) else (j,false,ugraph) @@ -1768,12 +1794,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if not branches_ok then raise (TypeCheckerFailure "Case analysys: wrong branch type"); - let arguments = + let arguments' = if not need_dummy then outtype::arguments@[term] else outtype::arguments in let outtype = - if arguments = [] then outtype - else CicReduction.head_beta_reduce (C.Appl arguments) + if need_dummy && arguments = [] then outtype + else CicReduction.head_beta_reduce (C.Appl arguments') in outtype,ugraph5 | C.Fix (i,fl) -> @@ -1995,12 +2021,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in (*CSC -debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ; +debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ; let res = *) type_of_aux ~logger context t ugraph (* -in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res +in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res *) (* is a small constructor? *) @@ -2024,12 +2050,12 @@ and is_small ~logger context paramsno c ugraph = and type_of ~logger t ugraph = (*CSC -debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ; +debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ; let res = *) type_of_aux' ~logger [] [] t ugraph (*CSC -in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res +in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res *) ;; @@ -2095,12 +2121,12 @@ let typecheck uri = (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *) match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> - (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) + (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*) cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; - (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *) + (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *) let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in try CicEnvironment.set_type_checking_info uri; @@ -2116,14 +2142,14 @@ let typecheck uri = object. *) Invalid_argument s -> - (*debug_print s;*) + (*debug_print (lazy s);*) uobj,ugraph ;; let typecheck_obj ~logger uri obj = let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_obj uri (obj,ugraph) + let ugraph, univlist = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist) (** wrappers which instantiate fresh loggers *) @@ -2134,3 +2160,4 @@ let type_of_aux' ?(subst = []) metasenv context t ugraph = let typecheck_obj uri obj = let logger = new CicLogger.logger in typecheck_obj ~logger uri obj +