From 4f1fda223f9b565267054361f0ec9bdedb86fe6a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 3 Nov 2005 13:47:36 +0000 Subject: [PATCH] 1. a simplified version of check_allowed_sort_elimination is now exported from CicTypeChecker to be used in CicElim :-| 2. check_allowed_sort_elimination fixed w.r.t. the case Prop unit vs * --- helm/ocaml/cic_proof_checking/cicElim.ml | 10 +++- helm/ocaml/cic_proof_checking/cicElim.mli | 4 +- .../cic_proof_checking/cicTypeChecker.ml | 58 ++++++++++++++----- .../cic_proof_checking/cicTypeChecker.mli | 11 ++++ 4 files changed, 65 insertions(+), 18 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 60cf5af2e..c668d1c9b 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -255,7 +255,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args = let t = strip_left_params liftno paramsno t in branch (uri, typeno) insource paramsno t fix head args -let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = +let elim_of ~sort uri typeno = counter := ~-1; let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in match obj with @@ -268,10 +268,14 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = let paramsno = count_pi ty in (* number of (left or right) parameters *) let rightno = paramsno - leftno in let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in +let head = match strip_pi ty with Cic.Sort s -> s in let conslen = List.length constructors in let consno = ref (conslen + 1) in - if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then - raise Can_t_eliminate; + if + not + (CicTypeChecker.check_allowed_sort_elimination uri typeno head sort) + then + raise Can_t_eliminate; let indty = let indty = Cic.MutInd (uri, typeno, []) in if paramsno = 0 then diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index a00ebff42..f1f84c92e 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -30,7 +30,7 @@ exception Can_t_eliminate (** internal error while generating elimination principle *) exception Elim_failure of string Lazy.t -(** @param sort target sort, defaults to Type +(** @param sort target sort * @param uri inductive type uri * @param typeno inductive type number * @raise Failure @@ -38,4 +38,4 @@ exception Elim_failure of string Lazy.t * @return Cic constant corresponding to the required elimination principle * and its uri *) -val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj +val elim_of: sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 168f6d6ae..6678d509c 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1302,14 +1302,24 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i | (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 (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 a singleton or empty non recursive and non informative + definition? *) + non_informative, ugraph + else + false,ugraph | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1322,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 @@ -1344,7 +1353,6 @@ 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 *) | (_,_) -> false,ugraph in check_allowed_sort_elimination_aux ugraph context arity2 need_dummy @@ -2000,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 @@ -2129,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) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 675b548dc..28f134e07 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -41,3 +41,14 @@ val type_of_aux': (* typechecks the obj and puts it in the environment *) val typecheck_obj : UriManager.uri -> Cic.obj -> unit + +(* 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) *) +val check_allowed_sort_elimination: + UriManager.uri -> int -> Cic.sort -> Cic.sort -> bool -- 2.39.2