From e001f955d04398adca19bbc30dc5a162183f439f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Dec 2001 14:21:33 +0000 Subject: [PATCH] PARTIAL COMMIT: The whole logic of the guarded_by_constructors is being changed. The new idea is this one: 1) The guarded_by_constructors is applied to a term t which must always generate an inhabitant of an inductive data type or of a co-inductive data type. 2) When it find a constructor in head position, then the constructor must construct the inductive or co-inductive data type of 1). 3) The type of the formal parameter of a constructor determines what condition is checked on the actual parameters of the constructors: a) Not recursive: the function must not occur in the actual parameter b) Simply recursive (to be defined): the function must occur in the actual parameter only guarded by constructors (where the constructor has already been found). c) Imbricated (i.e. it is another inductive type applied to the one that is going to be recursively defined): in this case the guarded by constructors (where the constructor has already been found) must be called, but: I) the expected inductive data type is no more the old one, but the one of the inductive data type that is in head position in the type. II) Once (if) one constructor of I) will be found, its type must be considered only after the substitution of the left (?) parameters and considering recursion IN THE CO-INDUCTIVE TYPE THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX. What is still wrong with this commit is that we don't have the notion of imbricated argument yet. So, as soon as an imbricated argument is found, the invariant 1-3 are broken and sooner or later an exception is raised or false is returned. --- .../cic_proof_checking/cicTypeChecker.ml | 122 +++++++++++------- 1 file changed, 72 insertions(+), 50 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 6529fede1..144740013 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -778,94 +778,88 @@ and guarded_by_destructors n nn kl x safes = ) fl true (*CSC h = 0 significa non ancora protetto *) -and guarded_by_constructors n nn h = +and guarded_by_constructors n nn h te = let module C = Cic in - function + (*CSC: There is a lot of code replication between the cases X and *) + (*CSC: (C.Appl X tl). Maybe it will be better to define a function *) + (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) + match CicReduction.whd te with C.Rel m when m > n && m <= nn -> h = 1 | C.Rel _ - | C.Var _ + | C.Var _ -> true | C.Meta _ | C.Sort _ - | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *) - | C.Cast (te,ty) -> - guarded_by_constructors n nn h te && - guarded_by_constructors n nn h ty - | C.Prod (_,so,de) -> + | C.Implicit + | C.Cast _ + | C.Prod _ + | C.LetIn _ -> raise (Impossible 17) (* the term has just been type-checked *) | C.Lambda (_,so,de) -> does_not_occur n nn so && guarded_by_constructors (n + 1) (nn + 1) h de - | C.LetIn (_,so,de) -> - does_not_occur n nn so && - guarded_by_constructors (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h = 1 && List.fold_right (fun x i -> i && does_not_occur n nn x) tl true | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) -> - let (is_coinductive, rl) = + (* Invariant: we are sure that the constructor is a constructor *) + (* of the output inductive type of the whole co-fixpoint. *) + let rl = match CicEnvironment.get_cooked_obj uri cookingsno with C.InductiveDefinition (itl,_,_) -> let (_,is_inductive,_,cl) = List.nth itl i in let (_,cons,rrec_args) = List.nth cl (j - 1) in (match !rrec_args with None -> raise (Impossible 18) - | Some rec_args -> (not is_inductive, rec_args) + | Some rec_args -> assert (not is_inductive) ; rec_args ) | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) in - is_coinductive && List.fold_right (fun (x,r) i -> i && if r then +begin +let res = guarded_by_constructors n nn 1 x +in + if not res then + begin + prerr_endline ("BECCATO: " ^ CicPp.ppterm x) ; flush stderr ; assert false + end ; + res +end else does_not_occur n nn x ) (List.combine tl rl) true + | C.Appl ((C.CoFix (_,fl))::tl) -> + List.fold_left (fun i x -> i && does_not_occur n nn x) true tl && + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len in + List.fold_right + (fun (_,ty,bo) i -> + i && does_not_occur n_plus_len nn_plus_len ty && + guarded_by_constructors n_plus_len nn_plus_len h bo + ) fl true + | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) -> + List.fold_left (fun i x -> i && does_not_occur n nn x) true tl && + does_not_occur n nn out && + does_not_occur n nn te && + List.fold_right + (fun x i -> i && guarded_by_constructors n nn h x) pl true | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur n nn x) l true - | C.Const _ + | C.Const _ -> true | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *) + | C.MutInd _ -> assert false + | C.MutConstruct _ -> true | C.MutCase (_,_,_,out,te,pl) -> - let rec returns_a_coinductive = - function - (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *) - (*CSC: effettata solo una volta, per mangiarsi l'astrazione *) - (*CSC: non dummy *) - C.Lambda (_,_,de) -> returns_a_coinductive de - | C.MutInd (uri,_,i) -> - (*CSC: definire una funzioncina per questo codice sempre replicato *) - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (itl,_,_) -> - let (_,is_inductive,_,_) = List.nth itl i in - not is_inductive - | _ -> - raise (WrongUriToMutualInductiveDefinitions - (UriManager.string_of_uri uri)) - ) - (*CSC: bug nella prossima riga (manca la whd) *) - | C.Appl ((C.MutInd (uri,_,i))::_) -> - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (itl,_,_) -> - let (_,is_inductive,_,_) = List.nth itl i in - not is_inductive - | _ -> - raise (WrongUriToMutualInductiveDefinitions - (UriManager.string_of_uri uri)) - ) - | _ -> false - in does_not_occur n nn out && does_not_occur n nn te && - if returns_a_coinductive out then List.fold_right (fun x i -> i && guarded_by_constructors n nn h x) pl true - else - List.fold_right (fun x i -> i && does_not_occur n nn x) pl true | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len @@ -882,7 +876,7 @@ and guarded_by_constructors n nn h = List.fold_right (fun (_,ty,bo) i -> i && does_not_occur n_plus_len nn_plus_len ty && - does_not_occur n_plus_len nn_plus_len bo + guarded_by_constructors n_plus_len nn_plus_len h bo ) fl true and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = @@ -1165,7 +1159,9 @@ and type_of_aux' env t = begin (* let's control the guarded by constructors conditions C{f,M} *) if not (guarded_by_constructors 0 len 0 bo) then - raise (NotWellTyped "CoFix: not guarded by constructors") + raise (NotWellTyped "CoFix: not guarded by constructors") ; + if not (returns_a_coinductive ty) then + raise (NotWellTyped "CoFix: does not return a coinductive type") end else raise (NotWellTyped "CoFix: ill-typed bodies") @@ -1210,6 +1206,32 @@ and type_of_aux' env t = end | _ -> raise (NotWellTyped "Appl: wrong Prod-type") ) + + and returns_a_coinductive ty = + let module C = Cic in + match CicReduction.whd ty with + C.MutInd (uri,_,i) -> + (*CSC: definire una funzioncina per questo codice sempre replicato *) + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,is_inductive,_,_) = List.nth itl i in + not is_inductive + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri)) + ) + | C.Appl ((C.MutInd (uri,_,i))::_) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,is_inductive,_,_) = List.nth itl i in + not is_inductive + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri)) + ) + | C.Prod (_,_,de) -> returns_a_coinductive de + | _ -> assert false + in type_of_aux env t -- 2.39.2