From: Claudio Sacerdoti Coen Date: Thu, 3 Nov 2005 11:13:58 +0000 (+0000) Subject: Major code semplification in check_allowed_sort_elimination: the X-Git-Tag: V_0_7_2_3~152 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22ff3a49e742b4289c96d518479a8e08c9192b7c;p=helm.git Major code semplification in check_allowed_sort_elimination: the need_dummy and not need_dummy cases are now unified. --- diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 2f7075dac..168f6d6ae 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,6 +1290,14 @@ 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) @@ -1335,67 +1345,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i ) | (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