From 97de13c52f24e7e7e7d0a9a43116750739d056f1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 12 Dec 2001 18:43:17 +0000 Subject: [PATCH] Fixing of guarded_by_constructors completed. This is the idea of the implementation: 1) The guarded_by_constructors is called on a term which is going to produce an inductive type (in every branch). 2) The guarded_by_constructors now has also a parameter which is the list of arguments that are applied to the inductive type that the term we are cheking is going to produce. 3) Once the constructor is found, its type is "applied" to the list of arguments its inductive type is applied to. This operation gives us an instantiated constructor type. 4) Depending on the type of every argument in the instantiated constructor type, we call either the does_not_occur or the guarded_by_constructors on every term the constructor is applied to. In case we call the guarded_by_constructors, we also compute the new parameter (list of arguments the new inductive type was applied to). Note that the analysis of the type of the constructors is based very closely on the analysis of positivy of an inductive type. Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position in the backbone of the type of a constructor) has not been considered and raises an exception. --- .../cic_proof_checking/cicTypeChecker.ml | 170 +++++++++++++----- 1 file changed, 124 insertions(+), 46 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 144740013..63366b4b9 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -777,14 +777,17 @@ and guarded_by_destructors n nn kl x safes = bo ) fl true -(*CSC h = 0 significa non ancora protetto *) -and guarded_by_constructors n nn h te = +(* the boolean h means already protected *) +(* args is the list of arguments the type of the constructor that may be *) +(* found in head position must be applied to. *) +(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *) +and guarded_by_constructors n nn h te args coInductiveTypeURI = let module C = Cic in (*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 m when m > n && m <= nn -> h | C.Rel _ | C.Var _ -> true | C.Meta _ @@ -796,43 +799,107 @@ and guarded_by_constructors n nn h te = 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 + guarded_by_constructors (n + 1) (nn + 1) h de args coInductiveTypeURI | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - h = 1 && + h && List.fold_right (fun x i -> i && does_not_occur n nn x) tl true | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) -> - (* Invariant: we are sure that the constructor is a constructor *) - (* of the output inductive type of the whole co-fixpoint. *) - let rl = + let consty = 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 -> assert (not is_inductive) ; rec_args - ) + let (_,_,_,cl) = List.nth itl i in + let (_,cons,_) = List.nth cl (j - 1) in cons | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) in - 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 + let rec analyse_branch ty te = + match CicReduction.whd ty with + C.Meta _ -> raise (Impossible 34) + | C.Rel _ + | C.Var _ + | C.Sort _ -> + does_not_occur n nn te + | C.Implicit + | C.Cast _ -> raise (Impossible 24) (* due to type-checking *) + | C.Prod (_,_,de) -> + analyse_branch de te + | C.Lambda _ + | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *) + | C.Appl ((C.MutInd (uri,_,_))::tl) as ty + when uri == coInductiveTypeURI -> + guarded_by_constructors n nn true te [] coInductiveTypeURI + | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> + guarded_by_constructors n nn true te tl coInductiveTypeURI + | C.Appl _ -> + does_not_occur n nn te + | C.Const _ + | C.Abst _ -> raise (Impossible 26) + | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> + guarded_by_constructors n nn true te [] coInductiveTypeURI + | C.MutInd _ -> + does_not_occur n nn te + | C.MutConstruct _ -> raise (Impossible 27) + (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) + (*CSC: in head position. *) + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *) + in + let rec analyse_instantiated_type ty l = + match CicReduction.whd ty with + C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit + | C.Cast _ -> raise (Impossible 29) (* due to type-checking *) + | C.Prod (_,so,de) -> + begin + match l with + [] -> true + | he::tl -> + analyse_branch so he && + analyse_instantiated_type de tl + end + | C.Lambda _ + | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *) + | C.Appl _ -> + List.fold_left (fun i x -> i && does_not_occur n nn x) true l + | C.Const _ + | C.Abst _ -> raise (Impossible 31) + | C.MutInd _ -> + List.fold_left (fun i x -> i && does_not_occur n nn x) true l + | C.MutConstruct _ -> raise (Impossible 32) + (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) + (*CSC: in head position. *) + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *) + in + let rec instantiate_type args consty = + function + [] -> true + | tlhe::tltl as l -> + let consty' = CicReduction.whd consty in + match args with + he::tl -> + begin + match consty' with + C.Prod (_,_,de) -> + let instantiated_de = CicSubstitution.subst he de in + (*CSC: siamo sicuri che non sia troppo forte? *) + does_not_occur n nn tlhe & + instantiate_type tl instantiated_de tltl + | _ -> + (*CSC:We do not consider backbones with a MutCase, a *) + (*CSC:FixPoint, a CoFixPoint and so on in head position.*) + raise (Impossible 23) + end + | [] -> analyse_instantiated_type consty' l + (* These are all the other cases *) + in + instantiate_type args consty tl | 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 @@ -841,14 +908,18 @@ end 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 + guarded_by_constructors n_plus_len nn_plus_len h bo args + coInductiveTypeURI ) 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 + (fun x i -> + i && + guarded_by_constructors n nn h x args coInductiveTypeURI + ) pl true | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur n nn x) l true | C.Const _ -> true @@ -859,7 +930,10 @@ end 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 + (fun x i -> + i && + guarded_by_constructors n nn h x args coInductiveTypeURI + ) pl true | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len @@ -876,7 +950,8 @@ end 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 + guarded_by_constructors n_plus_len nn_plus_len h bo args + coInductiveTypeURI ) fl true and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = @@ -1157,11 +1232,14 @@ and type_of_aux' env t = (CicSubstitution.lift len ty)) then 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") ; - if not (returns_a_coinductive ty) then - raise (NotWellTyped "CoFix: does not return a coinductive type") + (* let's control that the returned type is coinductive *) + match returns_a_coinductive ty with + None -> + raise(NotWellTyped "CoFix: does not return a coinductive type") + | Some uri -> + (*let's control the guarded by constructors conditions C{f,M}*) + if not (guarded_by_constructors 0 len false bo [] uri) then + raise (NotWellTyped "CoFix: not guarded by constructors") end else raise (NotWellTyped "CoFix: ill-typed bodies") @@ -1210,12 +1288,12 @@ and type_of_aux' env t = and returns_a_coinductive ty = let module C = Cic in match CicReduction.whd ty with - C.MutInd (uri,_,i) -> + C.MutInd (uri,cookingsno,i) -> (*CSC: definire una funzioncina per questo codice sempre replicato *) - (match CicEnvironment.get_obj uri with + (match CicEnvironment.get_cooked_obj uri cookingsno with C.InductiveDefinition (itl,_,_) -> - let (_,is_inductive,_,_) = List.nth itl i in - not is_inductive + let (_,is_inductive,_,cl) = List.nth itl i in + if is_inductive then None else (Some uri) | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) @@ -1224,13 +1302,13 @@ and type_of_aux' env t = (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in - not is_inductive + if is_inductive then None else (Some uri) | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) ) | C.Prod (_,_,de) -> returns_a_coinductive de - | _ -> assert false + | _ -> None in type_of_aux env t -- 2.39.2