X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=af98ff0efc72b53acfd7d7e8b225e45272a166f4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2f7075dacf34fca1004e1a1aeb7d7bcf50c1d851;hpb=8523a35427aa3fdf40a0e14b8aac3428c8aa13f0;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 2f7075dac..af98ff0ef 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1278,7 +1278,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy ind arity1 arity2 ugraph = let module C = Cic in let module U = UriManager in - match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with + let arity1 = CicReduction.whd ~subst context arity1 in + let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy = + match arity1, CicReduction.whd ~subst context arity2 with (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in @@ -1288,18 +1290,36 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i ugraph1 else false,ugraph1 + | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy -> + let b,ugraph1 = + CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in + if not b then + false,ugraph1 + else + check_allowed_sort_elimination_aux ugraph1 + ((Some (name,C.Decl so))::context) ta true | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph | (C.Sort C.Prop, C.Sort C.Set) | (C.Sort C.Prop, C.Sort C.CProp) | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> - (* TASSI: da verificare *) -(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (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) , ugraph + C.InductiveDefinition (itl,_,paramsno,_) -> + let itl_len = List.length itl in + let (name,_,ty,cl) = List.nth itl i in + let cl_len = List.length cl in + if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then + let non_informative,ugraph = + if cl_len = 0 then true,ugraph + else + is_non_informative ~logger [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) ugraph + in + (* is it a singleton or empty non recursive and non informative + definition? *) + non_informative, ugraph + else + false,ugraph | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1312,7 +1332,6 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) - (* TASSI: da verificare *) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -1334,68 +1353,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i UriManager.string_of_uri uri))) ) | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph - (* TASSI: da verificare *) - | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy -> - let b,ugraph1 = - CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in - if not b then - false,ugraph1 - else - (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with - 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 - (lazy - ("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 -> - let b,ugraph1 = - CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in - if not b then - false,ugraph1 - else - (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with - C.Sort C.Prop - | C.Sort C.Set -> true,ugraph1 - | C.Sort C.CProp -> true,ugraph1 - | C.Sort (C.Type _) -> - (* TASSI: da verificare *) - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,paramsno,_) -> - let (_,_,_,cl) = List.nth itl i in - let tys = - List.map - (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl - in - (List.fold_right - (fun (_,x) (i,ugraph) -> - if i then - is_small ~logger tys paramsno x ugraph - else - false,ugraph - ) cl (true,ugraph1)) - | _ -> - raise (TypeCheckerFailure (lazy - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - ) - | _ -> raise (AssertFailure (lazy "19")) - ) - | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy -> - (* TASSI: da verificare *) - CicReduction.are_convertible ~subst ~metasenv context so ind ugraph | (_,_) -> false,ugraph + in + check_allowed_sort_elimination_aux ugraph context arity2 need_dummy and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in @@ -2048,21 +2008,32 @@ in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res (* is a small constructor? *) (*CSC: ottimizzare calcolando staticamente *) -and is_small ~logger context paramsno c ugraph = - let rec is_small_aux ~logger context c ugraph = +and is_small_or_non_informative ~condition ~logger context paramsno c ugraph = + let rec is_small_or_non_informative_aux ~logger context c ugraph = let module C = Cic in match CicReduction.whd context c with C.Prod (n,so,de) -> let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in - let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in + let b = condition s in if b then - is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 + is_small_or_non_informative_aux + ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 else false,ugraph1 | _ -> true,ugraph (*CSC: we trust the type-checker *) in let (context',dx) = split_prods ~subst:[] context paramsno c in - is_small_aux ~logger context' dx ugraph + is_small_or_non_informative_aux ~logger context' dx ugraph + +and is_small ~logger = + is_small_or_non_informative + ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set) + ~logger + +and is_non_informative ~logger = + is_small_or_non_informative + ~condition:(fun s -> s=Cic.Sort Cic.Prop) + ~logger and type_of ~logger t ugraph = (*CSC @@ -2177,3 +2148,16 @@ let typecheck_obj uri obj = let logger = new CicLogger.logger in typecheck_obj ~logger uri obj +(* check_allowed_sort_elimination uri i s1 s2 + This function is used outside the kernel to determine in advance whether + a MutCase will be allowed or not. + [uri,i] is the type of the term to match + [s1] is the sort of the term to eliminate (i.e. the head of the arity + of the inductive type [uri,i]) + [s2] is the sort of the goal (i.e. the head of the type of the outtype + of the MutCase) *) +let check_allowed_sort_elimination uri i s1 s2 = + fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[] + ~logger:(new CicLogger.logger) [] uri i true + (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) + CicUniv.empty_ugraph)