From 756c1e676368d9addc75438bce97a71e34287f18 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 May 2002 09:15:42 +0000 Subject: [PATCH] Experimental commit: we can now have definitions in contexts. As a consequence the context is now required by CicReduction.whd --- .../ocaml/cic_proof_checking/cicReduction.mli | 4 +- .../cic_proof_checking/cicReductionNaif.ml | 191 +++--- .../cic_proof_checking/cicTypeChecker.ml | 646 ++++++++++-------- helm/ocaml/cic_unification/cicUnification.ml | 6 +- 4 files changed, 468 insertions(+), 379 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli index d61bc7251..c4332a2ed 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.mli +++ b/helm/ocaml/cic_proof_checking/cicReduction.mli @@ -30,5 +30,5 @@ exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition val fdebug : int ref -val whd : Cic.term -> Cic.term -val are_convertible : Cic.term -> Cic.term -> bool +val whd : Cic.context -> Cic.term -> Cic.term +val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index b4296f1c1..1ab5e92bc 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -48,12 +48,16 @@ exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; (* takes a well-typed term *) -let whd = +let whd context = let rec whdaux l = let module C = Cic in let module S = CicSubstitution in function - C.Rel _ as t -> if l = [] then t else C.Appl (t::l) + C.Rel n as t -> + (match List.nth context (n-1) with + C.Decl _ -> if l = [] then t else C.Appl (t::l) + | C.Def bo -> whdaux l (S.lift n bo) + ) | C.Var uri as t -> (match CicEnvironment.get_cooked_obj uri 0 with C.Definition _ -> raise ReferenceToDefinition @@ -171,102 +175,109 @@ let whd = | None -> if l = [] then t else C.Appl (t::l) ) | C.CoFix (i,fl) as t -> - (*CSC vecchio codice - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - whdaux l body' - *) if l = [] then t else C.Appl (t::l) in +(*CSC +function t -> +prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ; +List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline " n1 = n2 - | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 - | (C.Meta n1, C.Meta n2) -> n1 = n2 - | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) - | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> - aux s1 s2 && aux t1 t2 - | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> - aux s1 s2 && aux t1 t2 - | (C.Appl l1, C.Appl l2) -> - (try - List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true - with - Invalid_argument _ -> false - ) - | (C.Const (uri1,_), C.Const (uri2,_)) -> - (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *) - (*CSC: mentre sono delirante, quindi ... *) - (* WARNING: it is really important that the two cookingsno are not *) - (* checked for equality. This allows not to cook an object with no *) - (* ingredients only to update the cookingsno. E.g: if a term t has *) - (* a reference to a term t1 which does not depend on any variable *) - (* and t1 depends on a term t2 (that can't depend on any variable *) - (* because of t1), then t1 cooked at every level could be the same *) - (* as t1 cooked at level 0. Doing so, t2 will be extended in t *) - (* with cookingsno 0 and not 2. But this will not cause any trouble*) - (* if here we don't check that the two cookingsno are equal. *) - U.eq uri1 uri2 - | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> - (* WARNIG: see the previous warning *) - U.eq uri1 uri2 && i1 = i2 - | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> - (* WARNIG: see the previous warning *) - U.eq uri1 uri2 && i1 = i2 && j1 = j2 - | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), - C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> - (* WARNIG: see the previous warning *) - (* aux outtype1 outtype2 should be true if aux pl1 pl2 *) - U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 && - aux term1 term2 && - List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true - | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - i1 = i2 && - List.fold_right2 - (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> - b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2) - fl1 fl2 true - | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - i1 = i2 && - List.fold_right2 - (fun (_,ty1,bo1) (_,ty2,bo2) b -> - b && aux ty1 ty2 && aux bo1 bo2) - fl1 fl2 true - | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _) - | (C.Implicit, _) | (_, C.Implicit) -> - raise (Impossible 3) (* we don't trust our whd ;-) *) - | (_,_) -> false - end - in - if aux2 t1 t2 then true - else - begin - debug t1 [t2] "PREWHD"; - let t1' = whd t1 - and t2' = whd t2 in - debug t1' [t2'] "POSTWHD"; - aux2 t1' t2' - end + let rec aux context t1 t2 = + let aux2 t1 t2 = + (* this trivial euristic cuts down the total time of about five times ;-) *) + (* this because most of the time t1 and t2 are "sintactically" the same *) + if t1 = t2 then + true + else + begin + let module C = Cic in + match (t1,t2) with + (C.Rel n1, C.Rel n2) -> n1 = n2 + | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 + | (C.Meta n1, C.Meta n2) -> n1 = n2 + | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> + aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> + aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2 + | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) -> + aux context s1 s2 && aux ((C.Def s1)::context) t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true + with + Invalid_argument _ -> false + ) + | (C.Const (uri1,_), C.Const (uri2,_)) -> + (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *) + (*CSC: mentre sono delirante, quindi ... *) + (* WARNING: it is really important that the two cookingsno are not*) + (* checked for equality. This allows not to cook an object with no*) + (* ingredients only to update the cookingsno. E.g: if a term t has*) + (* a reference to a term t1 which does not depend on any variable *) + (* and t1 depends on a term t2 (that can't depend on any variable *) + (* because of t1), then t1 cooked at every level could be the same*) + (* as t1 cooked at level 0. Doing so, t2 will be extended in t *) + (* with cookingsno 0 and not 2. But this will not cause any *) + (* trouble if here we don't check that the two cookingsno are *) + (* equal. *) + U.eq uri1 uri2 + | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 + | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 && j1 = j2 + | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), + C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> + (* WARNIG: see the previous warning *) + (* aux context outtype1 outtype2 should be true if *) + (* aux context pl1 pl2 *) + U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 && + aux context term1 term2 && + List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> +(*CSC: C.Decl e' giusto? *) + let tys = List.map (function (_,_,ty,_) -> C.Decl ty) fl1 in + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux context ty1 ty2 && + aux (tys@context) bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> +(*CSC: C.Decl e' giusto? *) + let tys = List.map (function (_,ty,_) -> C.Decl ty) fl1 in + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux context ty1 ty2 && aux (tys@context) bo1 bo2) + fl1 fl2 true + | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _) + | (C.Implicit, _) | (_, C.Implicit) -> + raise (Impossible 3) (* we don't trust our whd ;-) *) + | (_,_) -> false + end + in + if aux2 t1 t2 then true + else + begin + debug t1 [t2] "PREWHD"; + let t1' = whd context t1 + and t2' = whd context t2 in + debug t1' [t2'] "POSTWHD"; + aux2 t1' t2' + end in aux ;; diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 884eb1944..34eb7d23f 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -67,14 +67,15 @@ let rec cooked_type_of_constant uri cookingsno = (match uobj with C.Definition (_,te,ty,_) -> let _ = type_of ty in - if not (R.are_convertible (type_of te) ty) then + if not (R.are_convertible [] (type_of te) ty) then raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) | C.Axiom (_,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in () | C.CurrentProof (_,conjs,te,ty) -> let _ = type_of_aux' conjs [] ty in - if not (R.are_convertible (type_of_aux' conjs [] te) ty) then + if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) + then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) ) ; @@ -104,7 +105,7 @@ and type_of_variable uri = (match bo with None -> () | Some bo -> - if not (R.are_convertible (type_of bo) ty) then + if not (R.are_convertible [] (type_of bo) ty) then raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri))) ) ; CicEnvironment.set_type_checking_info uri ; @@ -112,51 +113,57 @@ and type_of_variable uri = ty | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) -and does_not_occur n nn te = +and does_not_occur context n nn te = let module C = Cic in (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *) (*CSC: venga mangiata durante la whd sembra presentare problemi di *) (*CSC: universi *) - match CicReduction.whd te with + match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> false | C.Rel _ | C.Var _ | C.Meta _ | C.Sort _ | C.Implicit -> true - | C.Cast (te,ty) -> does_not_occur n nn te && does_not_occur n nn ty + | C.Cast (te,ty) -> + does_not_occur context n nn te && does_not_occur context n nn ty | C.Prod (_,so,dest) -> - does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + does_not_occur context n nn so && + does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest | C.Lambda (_,so,dest) -> - does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + does_not_occur context n nn so && + does_not_occur ((C.Decl so)::context) (n + 1) (nn + 1) dest | C.LetIn (_,so,dest) -> - does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + does_not_occur context n nn so && + does_not_occur ((C.Def so)::context) (n + 1) (nn + 1) dest | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur n nn x) l true + List.fold_right (fun x i -> i && does_not_occur context n nn x) l true | C.Const _ | C.Abst _ | C.MutInd _ | C.MutConstruct _ -> true | C.MutCase (_,_,_,out,te,pl) -> - does_not_occur n nn out && does_not_occur n nn te && - List.fold_right (fun x i -> i && does_not_occur n nn x) pl true + does_not_occur context n nn out && does_not_occur context n nn te && + List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) fl in 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 + i && does_not_occur context n nn ty && + does_not_occur (tys @ context) n_plus_len nn_plus_len bo ) fl true | C.CoFix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in + let tys = List.map (fun (_,ty,_) -> Cic.Decl ty) fl in 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 + i && does_not_occur context n nn ty && + does_not_occur (tys @ context) n_plus_len nn_plus_len bo ) fl true (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) @@ -164,52 +171,60 @@ and does_not_occur n nn te = (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *) (*CSC strictly_positive *) (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) -and weakly_positive n nn uri te = +and weakly_positive context n nn uri te = let module C = Cic in +(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) + let dummy_mutind = + C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,0) + in (*CSC mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_rel = + let rec subst_inductive_type_with_dummy_mutind = function C.MutInd (uri',_,0) when UriManager.eq uri' uri -> - C.Rel 0 (* dummy rel *) + dummy_mutind | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> - C.Rel 0 (* dummy rel *) - | C.Cast (te,ty) -> subst_inductive_type_with_dummy_rel te + dummy_mutind + | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te | C.Prod (name,so,ta) -> - C.Prod (name, subst_inductive_type_with_dummy_rel so, - subst_inductive_type_with_dummy_rel ta) + C.Prod (name, subst_inductive_type_with_dummy_mutind so, + subst_inductive_type_with_dummy_mutind ta) | C.Lambda (name,so,ta) -> - C.Lambda (name, subst_inductive_type_with_dummy_rel so, - subst_inductive_type_with_dummy_rel ta) + C.Lambda (name, subst_inductive_type_with_dummy_mutind so, + subst_inductive_type_with_dummy_mutind ta) | C.Appl tl -> - C.Appl (List.map subst_inductive_type_with_dummy_rel tl) + C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> C.MutCase (uri,cookingsno,i, - subst_inductive_type_with_dummy_rel outtype, - subst_inductive_type_with_dummy_rel term, - List.map subst_inductive_type_with_dummy_rel pl) + subst_inductive_type_with_dummy_mutind outtype, + subst_inductive_type_with_dummy_mutind term, + List.map subst_inductive_type_with_dummy_mutind pl) | C.Fix (i,fl) -> C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i, - subst_inductive_type_with_dummy_rel ty, - subst_inductive_type_with_dummy_rel bo)) fl) + subst_inductive_type_with_dummy_mutind ty, + subst_inductive_type_with_dummy_mutind bo)) fl) | C.CoFix (i,fl) -> C.CoFix (i,List.map (fun (name,ty,bo) -> (name, - subst_inductive_type_with_dummy_rel ty, - subst_inductive_type_with_dummy_rel bo)) fl) + subst_inductive_type_with_dummy_mutind ty, + subst_inductive_type_with_dummy_mutind bo)) fl) | t -> t in - match CicReduction.whd te with + match CicReduction.whd context te with C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true | C.Prod (C.Anonimous,source,dest) -> - strictly_positive n nn (subst_inductive_type_with_dummy_rel source) && - weakly_positive (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) when does_not_occur 0 n dest -> - (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive n nn (subst_inductive_type_with_dummy_rel source) && - weakly_positive (n + 1) (nn + 1) uri dest + strictly_positive context n nn + (subst_inductive_type_with_dummy_mutind source) && + weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest + | C.Prod (name,source,dest) when + does_not_occur ((C.Decl source)::context) 0 n dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive context n nn + (subst_inductive_type_with_dummy_mutind source) && + weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest | C.Prod (_,source,dest) -> - does_not_occur n nn (subst_inductive_type_with_dummy_rel source) && - weakly_positive (n + 1) (nn + 1) uri dest + does_not_occur context n nn + (subst_inductive_type_with_dummy_mutind source)&& + weakly_positive ((C.Decl source)::context) (n + 1) (nn + 1) uri dest | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)")) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) @@ -224,25 +239,25 @@ and instantiate_parameters params c = | (C.Cast (te,_), _) -> instantiate_parameters params te | (t,l) -> raise (Impossible 1) -and strictly_positive n nn te = +and strictly_positive context n nn te = let module C = Cic in let module U = UriManager in - match CicReduction.whd te with + match CicReduction.whd context te with C.Rel _ -> true | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) - strictly_positive n nn te + strictly_positive context n nn te | C.Prod (_,so,ta) -> - does_not_occur n nn so && - strictly_positive (n+1) (nn+1) ta + does_not_occur context n nn so && + strictly_positive ((C.Decl so)::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutInd (uri,_,i))::tl) -> - let (ok,paramsno,cl) = + let (ok,paramsno,ity,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> - let (_,_,_,cl) = List.nth tl i in - (List.length tl = 1, paramsno, cl) + let (_,_,ity,cl) = List.nth tl i in + (List.length tl = 1, paramsno, ity, cl) | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in let (params,arguments) = split tl paramsno in @@ -252,20 +267,20 @@ and strictly_positive n nn te = in ok && List.fold_right - (fun x i -> i && does_not_occur n nn x) + (fun x i -> i && does_not_occur context n nn x) arguments true && (*CSC: MEGAPATCH3 (sara' quella giusta?)*) List.fold_right (fun x i -> i && - weakly_positive (n+1) (nn+1) uri x + weakly_positive ((Cic.Decl ity)::context) (n+1) (nn+1) uri x ) cl' true - | t -> does_not_occur n nn t + | t -> does_not_occur context n nn t (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) -and are_all_occurrences_positive uri indparamsno i n nn te = +and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in - match CicReduction.whd te with + match CicReduction.whd context te with C.Appl ((C.Rel m)::tl) when m = i -> (*CSC: riscrivere fermandosi a 0 *) (* let's check if the inductive type is applied at least to *) @@ -275,13 +290,13 @@ and are_all_occurrences_positive uri indparamsno i n nn te = (fun k x -> if k = 0 then 0 else - match CicReduction.whd x with + match CicReduction.whd context x with C.Rel m when m = n - (indparamsno - k) -> k - 1 | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri)) ) indparamsno tl in if last = 0 then - List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true else raise (WrongRequiredArgument (UriManager.string_of_uri uri)) | C.Rel m when m = i -> @@ -290,15 +305,19 @@ and are_all_occurrences_positive uri indparamsno i n nn te = else raise (WrongRequiredArgument (UriManager.string_of_uri uri)) | C.Prod (C.Anonimous,source,dest) -> - strictly_positive n nn source && - are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest - | C.Prod (name,source,dest) when does_not_occur 0 n dest -> + strictly_positive context n nn source && + are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno + (i+1) (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) when + does_not_occur ((C.Decl source)::context) 0 n dest -> (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive n nn source && - are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest + strictly_positive context n nn source && + are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno + (i+1) (n + 1) (nn + 1) dest | C.Prod (_,source,dest) -> - does_not_occur n nn source && - are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest + does_not_occur context n nn source && + are_all_occurrences_positive ((C.Decl source)::context) uri indparamsno + (i+1) (n + 1) (nn + 1) dest | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)) (*CSC: cambiare il nome, torna unit! *) @@ -317,6 +336,10 @@ and cooked_mutual_inductive_defs uri = (* constructors using Prods *) (*CSC: piccola??? inefficienza *) let len = List.length itl in +(*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *) +(*CSC: si manifesterebbe solamene con tipi veramente mutualmente *) +(*CSC: induttivi... *) + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in let _ = List.fold_right (fun (_,_,_,cl) i -> @@ -329,13 +352,15 @@ and cooked_mutual_inductive_defs uri = in let _ = type_of augmented_term in (* let's check also the positivity conditions *) - if not (are_all_occurrences_positive uri indparamsno i 0 len te) + if + not + (are_all_occurrences_positive tys uri indparamsno i 0 len te) then raise (NotPositiveOccurrences (U.string_of_uri uri)) else match !r with Some _ -> raise (Impossible 2) - | None -> r := Some (recursive_args 0 len te) + | None -> r := Some (recursive_args tys 0 len te) ) cl ; (i + 1) ) itl 1 @@ -391,9 +416,9 @@ and cooked_type_of_mutual_inductive_constr uri cookingsno i j = ty | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -and recursive_args n nn te = +and recursive_args context n nn te = let module C = Cic in - match CicReduction.whd te with + match CicReduction.whd context te with C.Rel _ -> [] | C.Var _ | C.Meta _ @@ -401,7 +426,8 @@ and recursive_args n nn te = | C.Implicit | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *) | C.Prod (_,so,de) -> - (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de) + (not (does_not_occur context n nn so)) :: + (recursive_args ((C.Decl so)::context) (n+1) (nn + 1) de) | C.Lambda _ | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *) | C.Appl _ -> [] @@ -413,12 +439,12 @@ and recursive_args n nn te = | C.Fix _ | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *) -and get_new_safes p c rl safes n nn x = +and get_new_safes context p c rl safes n nn x = let module C = Cic in let module U = UriManager in let module R = CicReduction in - match (R.whd c, R.whd p, rl) with - (C.Prod (_,_,ta1), C.Lambda (_,_,ta2), b::tl) -> + match (R.whd context c, R.whd context p, rl) with + (C.Prod (_,so,ta1), C.Lambda (_,_,ta2), b::tl) -> (* we are sure that the two sources are convertible because we *) (* have just checked this. So let's go along ... *) let safes' = @@ -427,11 +453,12 @@ and get_new_safes p c rl safes n nn x = let safes'' = if b then 1::safes' else safes' in - get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) + get_new_safes ((C.Decl so)::context) ta2 ta1 tl safes'' (n+1) (nn+1) + (x+1) | (C.Prod _, (C.MutConstruct _ as e), _) | (C.Prod _, (C.Rel _ as e), _) | (C.MutInd _, e, []) - | (C.Appl _, e, []) -> (e,safes,n,nn,x) + | (C.Appl _, e, []) -> (e,safes,n,nn,x,context) | (_,_,_) -> (* CSC: If the next exception is raised, it just means that *) (* CSC: the proof-assistant allows to use very strange things *) @@ -440,33 +467,32 @@ and get_new_safes p c rl safes n nn x = (* CSC: must be considered in this match. (e.g. x = MutCase) *) raise (Impossible 7) -and split_prods n te = +and split_prods context n te = let module C = Cic in let module R = CicReduction in - match (n, R.whd te) with - (0, _) -> [],te + match (n, R.whd context te) with + (0, _) -> context,te | (n, C.Prod (_,so,ta)) when n > 0 -> - let (l1,l2) = split_prods (n - 1) ta in - (so::l1,l2) + split_prods ((C.Decl so)::context) (n - 1) ta | (_, _) -> raise (Impossible 8) -and eat_lambdas n te = +and eat_lambdas context n te = let module C = Cic in let module R = CicReduction in - match (n, R.whd te) with - (0, _) -> (te, 0) - | (n, C.Lambda (_,_,ta)) when n > 0 -> - let (te, k) = eat_lambdas (n - 1) ta in - (te, k + 1) + match (n, R.whd context te) with + (0, _) -> (te, 0, context) + | (n, C.Lambda (_,so,ta)) when n > 0 -> + let (te, k, context') = eat_lambdas ((C.Decl so)::context) (n - 1) ta in + (te, k + 1, context') | (_, _) -> raise (Impossible 9) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) -and check_is_really_smaller_arg n nn kl x safes te = +and check_is_really_smaller_arg context n nn kl x safes te = (*CSC: forse la whd si puo' fare solo quando serve veramente. *) (*CSC: cfr guarded_by_destructors *) let module C = Cic in let module U = UriManager in - match CicReduction.whd te with + match CicReduction.whd context te with C.Rel m when List.mem m safes -> true | C.Rel _ -> false | C.Var _ @@ -483,17 +509,17 @@ and check_is_really_smaller_arg n nn kl x safes te = (List.map (fun x -> x + 1) safes) ta*) | C.Prod _ -> raise (Impossible 10) | C.Lambda (_,so,ta) -> - check_is_really_smaller_arg n nn kl x safes so && - check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + check_is_really_smaller_arg context n nn kl x safes so && + check_is_really_smaller_arg ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (_,so,ta) -> - check_is_really_smaller_arg n nn kl x safes so && - check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + check_is_really_smaller_arg context n nn kl x safes so && + check_is_really_smaller_arg ((C.Def so)::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) - check_is_really_smaller_arg n nn kl x safes he + check_is_really_smaller_arg context n nn kl x safes he | C.Appl [] -> raise (Impossible 11) | C.Const _ | C.Abst _ @@ -505,17 +531,21 @@ and check_is_really_smaller_arg n nn kl x safes te = let (isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> - let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl - in - (isinductive,paramsno,cl') + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map + (fun (id,ty,r) -> + (id, snd (split_prods tys paramsno ty), r)) cl + in + (isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in if not isinductive then List.fold_right - (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) + (fun p i -> + i && check_is_really_smaller_arg context n nn kl x safes p) pl true else List.fold_right @@ -527,27 +557,31 @@ and check_is_really_smaller_arg n nn kl x safes te = rl'' | None -> raise (Impossible 13) in - let (e,safes',n',nn',x') = - get_new_safes p c rl' safes n nn x + let (e,safes',n',nn',x',context') = + get_new_safes context p c rl' safes n nn x in i && - check_is_really_smaller_arg n' nn' kl x' safes' e + check_is_really_smaller_arg context' n' nn' kl x' safes' e ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl - in + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let cl' = + List.map + (fun (id,ty,r) -> + (id, snd (split_prods tys paramsno ty), r)) cl + in (isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in if not isinductive then List.fold_right - (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) + (fun p i -> + i && check_is_really_smaller_arg context n nn kl x safes p) pl true else (*CSC: supponiamo come prima che nessun controllo sia necessario*) @@ -561,66 +595,75 @@ and check_is_really_smaller_arg n nn kl x safes te = rl'' | None -> raise (Impossible 14) in - let (e, safes',n',nn',x') = - get_new_safes p c rl' safes n nn x + let (e, safes',n',nn',x',context') = + get_new_safes context p c rl' safes n nn x in i && - check_is_really_smaller_arg n' nn' kl x' safes' e + check_is_really_smaller_arg context' n' nn' kl x' safes' e ) (List.combine pl cl) true | _ -> List.fold_right - (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) - pl true + (fun p i -> + i && check_is_really_smaller_arg context n nn kl x safes p + ) pl true ) | C.Fix (_, fl) -> let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> i && - check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len - safes' bo + check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo ) fl true | C.CoFix (_, fl) -> let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> i && - check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len - safes' bo + check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo ) fl true -and guarded_by_destructors n nn kl x safes = +and guarded_by_destructors context n nn kl x safes = let module C = Cic in let module U = UriManager in function C.Rel m when m > n && m <= nn -> false - | C.Rel _ + | C.Rel n -> + (match List.nth context (n-1) with + C.Decl _ -> true + | C.Def bo -> guarded_by_destructors context n nn kl x safes bo + ) | C.Var _ | C.Meta _ | C.Sort _ | C.Implicit -> true | C.Cast (te,ty) -> - guarded_by_destructors n nn kl x safes te && - guarded_by_destructors n nn kl x safes ty + guarded_by_destructors context n nn kl x safes te && + guarded_by_destructors context n nn kl x safes ty | C.Prod (_,so,ta) -> - guarded_by_destructors n nn kl x safes so && - guarded_by_destructors (n+1) (nn+1) kl (x+1) + guarded_by_destructors context n nn kl x safes so && + guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Lambda (_,so,ta) -> - guarded_by_destructors n nn kl x safes so && - guarded_by_destructors (n+1) (nn+1) kl (x+1) + guarded_by_destructors context n nn kl x safes so && + guarded_by_destructors ((C.Decl so)::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (_,so,ta) -> - guarded_by_destructors n nn kl x safes so && - guarded_by_destructors (n+1) (nn+1) kl (x+1) + guarded_by_destructors context n nn kl x safes so && + guarded_by_destructors ((C.Def so)::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in @@ -628,11 +671,12 @@ and guarded_by_destructors n nn kl x safes = else List.fold_right (fun param i -> - i && guarded_by_destructors n nn kl x safes param + i && guarded_by_destructors context n nn kl x safes param ) tl true && - check_is_really_smaller_arg n nn kl x safes (List.nth tl k) + check_is_really_smaller_arg context n nn kl x safes (List.nth tl k) | C.Appl tl -> - List.fold_right (fun t i -> i && guarded_by_destructors n nn kl x safes t) + List.fold_right + (fun t i -> i && guarded_by_destructors context n nn kl x safes t) tl true | C.Const _ | C.Abst _ @@ -645,22 +689,26 @@ and guarded_by_destructors n nn kl x safes = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl - in - (isinductive,paramsno,cl') + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let cl' = + List.map + (fun (id,ty,r) -> + (id, snd (split_prods tys paramsno ty), r)) cl + in + (isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in if not isinductive then - guarded_by_destructors n nn kl x safes outtype && - guarded_by_destructors n nn kl x safes term && + guarded_by_destructors context n nn kl x safes outtype && + guarded_by_destructors context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun p i -> i && guarded_by_destructors n nn kl x safes p) + (fun p i -> + i && guarded_by_destructors context n nn kl x safes p) pl true else - guarded_by_destructors n nn kl x safes outtype && + guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun (p,(_,c,rl)) i -> @@ -671,36 +719,41 @@ and guarded_by_destructors n nn kl x safes = rl'' | None -> raise (Impossible 15) in - let (e,safes',n',nn',x') = - get_new_safes p c rl' safes n nn x + let (e,safes',n',nn',x',context') = + get_new_safes context p c rl' safes n nn x in i && - guarded_by_destructors n' nn' kl x' safes' e + guarded_by_destructors context' n' nn' kl x' safes' e ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl - in - (isinductive,paramsno,cl') + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) tl in + let cl' = + List.map + (fun (id,ty,r) -> + (id, snd (split_prods tys paramsno ty), r)) cl + in + (isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in if not isinductive then - guarded_by_destructors n nn kl x safes outtype && - guarded_by_destructors n nn kl x safes term && + guarded_by_destructors context n nn kl x safes outtype && + guarded_by_destructors context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun p i -> i && guarded_by_destructors n nn kl x safes p) + (fun p i -> + i && guarded_by_destructors context n nn kl x safes p) pl true else - guarded_by_destructors n nn kl x safes outtype && + guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun t i -> i && guarded_by_destructors n nn kl x safes t) + (fun t i -> + i && guarded_by_destructors context n nn kl x safes t) tl true && List.fold_right (fun (p,(_,c,rl)) i -> @@ -711,18 +764,18 @@ and guarded_by_destructors n nn kl x safes = rl'' | None -> raise (Impossible 16) in - let (e, safes',n',nn',x') = - get_new_safes p c rl' safes n nn x + let (e, safes',n',nn',x',context') = + get_new_safes context p c rl' safes n nn x in i && - guarded_by_destructors n' nn' kl x' safes' e + guarded_by_destructors context' n' nn' kl x' safes' e ) (List.combine pl cl) true | _ -> - guarded_by_destructors n nn kl x safes outtype && - guarded_by_destructors n nn kl x safes term && + guarded_by_destructors context n nn kl x safes outtype && + guarded_by_destructors context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun p i -> i && guarded_by_destructors n nn kl x safes p) + (fun p i -> i && guarded_by_destructors context n nn kl x safes p) pl true ) | C.Fix (_, fl) -> @@ -730,38 +783,41 @@ and guarded_by_destructors n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> - i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len - safes' ty && - guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len - safes' bo + i && guarded_by_destructors context n nn kl x_plus_len safes' ty && + guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo ) fl true | C.CoFix (_, fl) -> let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> - i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len - safes' ty && - guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len safes' - bo + i && + guarded_by_destructors context n nn kl x_plus_len safes' ty && + guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo ) fl true (* 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 = +and guarded_by_constructors context 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 + match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> h | C.Rel _ | C.Var _ -> true @@ -773,11 +829,12 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = | 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 args coInductiveTypeURI + does_not_occur context n nn so && + guarded_by_constructors ((C.Decl so)::context) (n + 1) (nn + 1) h de args + coInductiveTypeURI | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && - List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) -> let consty = match CicEnvironment.get_cooked_obj uri cookingsno with @@ -788,32 +845,32 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) in - let rec analyse_branch ty te = - match CicReduction.whd ty with + let rec analyse_branch context ty te = + match CicReduction.whd context ty with C.Meta _ -> raise (Impossible 34) | C.Rel _ | C.Var _ | C.Sort _ -> - does_not_occur n nn te + does_not_occur context n nn te | C.Implicit | C.Cast _ -> raise (Impossible 24) (* due to type-checking *) - | C.Prod (_,_,de) -> - analyse_branch de te + | C.Prod (_,so,de) -> + analyse_branch ((C.Decl so)::context) 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 + guarded_by_constructors context n nn true te [] coInductiveTypeURI | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> - guarded_by_constructors n nn true te tl coInductiveTypeURI + guarded_by_constructors context n nn true te tl coInductiveTypeURI | C.Appl _ -> - does_not_occur n nn te + does_not_occur context n nn te | C.Const _ | C.Abst _ -> raise (Impossible 26) | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors n nn true te [] coInductiveTypeURI + guarded_by_constructors context n nn true te [] coInductiveTypeURI | C.MutInd _ -> - does_not_occur n nn te + does_not_occur context n nn te | C.MutConstruct _ -> raise (Impossible 27) (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) @@ -821,8 +878,8 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = | C.Fix _ | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *) in - let rec analyse_instantiated_type ty l = - match CicReduction.whd ty with + let rec analyse_instantiated_type context ty l = + match CicReduction.whd context ty with C.Rel _ | C.Var _ | C.Meta _ @@ -834,17 +891,19 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = match l with [] -> true | he::tl -> - analyse_branch so he && - analyse_instantiated_type de tl + analyse_branch context so he && + analyse_instantiated_type ((C.Decl so)::context) 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 + List.fold_left + (fun i x -> i && does_not_occur context 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 + List.fold_left + (fun i x -> i && does_not_occur context 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. *) @@ -856,7 +915,7 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = function [] -> true | tlhe::tltl as l -> - let consty' = CicReduction.whd consty in + let consty' = CicReduction.whd context consty in match args with he::tl -> begin @@ -864,78 +923,84 @@ and guarded_by_constructors n nn h te args coInductiveTypeURI = 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 & + does_not_occur context 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 + | [] -> analyse_instantiated_type context 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 && + List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl && let len = List.length fl in let n_plus_len = n + len - and nn_plus_len = nn + len in + and nn_plus_len = nn + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl 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 args - coInductiveTypeURI + i && does_not_occur context n nn ty && + guarded_by_constructors (tys@context) 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_left (fun i x -> i && does_not_occur context n nn x) true tl && + does_not_occur context n nn out && + does_not_occur context n nn te && List.fold_right (fun x i -> i && - guarded_by_constructors n nn h x args coInductiveTypeURI + guarded_by_constructors context 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 + List.fold_right (fun x i -> i && does_not_occur context n nn x) l true | C.Const _ -> true | C.Abst _ | C.MutInd _ -> assert false | C.MutConstruct _ -> true | C.MutCase (_,_,_,out,te,pl) -> - does_not_occur n nn out && - does_not_occur n nn te && + does_not_occur context n nn out && + does_not_occur context n nn te && List.fold_right (fun x i -> i && - guarded_by_constructors n nn h x args coInductiveTypeURI + guarded_by_constructors context n nn h x args coInductiveTypeURI ) pl true | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len - and nn_plus_len = nn + len in + and nn_plus_len = nn + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,_,ty,_) -> C.Decl ty) fl in 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 + i && does_not_occur context n nn ty && + does_not_occur (tys@context) n_plus_len nn_plus_len bo ) fl true | C.CoFix (_,fl) -> let len = List.length fl in let n_plus_len = n + len - and nn_plus_len = nn + len in + and nn_plus_len = nn + len + (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) + and tys = List.map (fun (_,ty,_) -> C.Decl ty) fl 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 args - coInductiveTypeURI + i && does_not_occur context n nn ty && + guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo + args coInductiveTypeURI ) fl true -and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = +and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = let module C = Cic in let module U = UriManager in - match (CicReduction.whd arity1, CicReduction.whd arity2) with + match (CicReduction.whd context arity1, CicReduction.whd context arity2) with (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) - when CicReduction.are_convertible so1 so2 -> - check_allowed_sort_elimination uri i need_dummy + when CicReduction.are_convertible context so1 so2 -> + check_allowed_sort_elimination context uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Prop, C.Sort C.Set) when need_dummy -> @@ -952,17 +1017,19 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = | (C.Sort C.Set, C.Sort C.Type) when need_dummy -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> - let (_,_,_,cl) = List.nth itl i in - List.fold_right (fun (_,x,_) i -> i && is_small paramsno x) cl true + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in + let (_,_,_,cl) = List.nth itl i in + List.fold_right + (fun (_,x,_) i -> i && is_small tys paramsno x) cl true | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ) | (C.Sort C.Type, C.Sort _) when need_dummy -> true | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy -> - let res = CicReduction.are_convertible so ind + let res = CicReduction.are_convertible context so ind in res && - (match CicReduction.whd ta with + (match CicReduction.whd ((C.Decl so)::context) ta with C.Sort C.Prop -> true | C.Sort C.Set -> (match CicEnvironment.get_obj uri with @@ -977,18 +1044,19 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = | _ -> false ) | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy -> - let res = CicReduction.are_convertible so ind + let res = CicReduction.are_convertible context so ind in res && - (match CicReduction.whd ta with + (match CicReduction.whd ((C.Decl so)::context) ta with C.Sort C.Prop | C.Sort C.Set -> true | C.Sort C.Type -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> let (_,_,_,cl) = List.nth itl i in - List.fold_right - (fun (_,x,_) i -> i && is_small paramsno x) cl true + let tys = List.map (fun (_,_,ty,_) -> Cic.Decl ty) itl in + List.fold_right + (fun (_,x,_) i -> i && is_small tys paramsno x) cl true | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -996,13 +1064,13 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = | _ -> raise (Impossible 19) ) | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy -> - CicReduction.are_convertible so ind + CicReduction.are_convertible context so ind | (_,_) -> false -and type_of_branch argsno need_dummy outtype term constype = +and type_of_branch context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in - match R.whd constype with + match R.whd context constype with C.MutInd (_,_,_) -> if need_dummy then outtype @@ -1016,8 +1084,8 @@ and type_of_branch argsno need_dummy outtype term constype = else C.Appl (outtype::arguments@(if need_dummy then [] else [term])) | C.Prod (name,so,de) -> - C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy - (CicSubstitution.lift 1 outtype) + C.Prod (C.Anonimous,so,type_of_branch ((C.Decl so)::context) argsno + need_dummy (CicSubstitution.lift 1 outtype) (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de) | _ -> raise (Impossible 20) @@ -1031,13 +1099,13 @@ and type_of_aux' metasenv context t = let module U = UriManager in function C.Rel n -> - let t = - try - List.nth context (n - 1) + (try + match List.nth context (n - 1) with + C.Decl t -> S.lift n t + | C.Def bo -> type_of_aux context (S.lift n bo) with _ -> raise (NotWellTyped "Not a close term") - in - S.lift n t + ) | C.Var uri -> incr fdebug ; let ty = type_of_variable uri in @@ -1048,16 +1116,16 @@ and type_of_aux' metasenv context t = | C.Implicit -> raise (Impossible 21) | C.Cast (te,ty) -> let _ = type_of_aux context ty in - if R.are_convertible (type_of_aux context te) ty then ty + if R.are_convertible context (type_of_aux context te) ty then ty else raise (NotWellTyped "Cast") | C.Prod (_,s,t) -> let sort1 = type_of_aux context s - and sort2 = type_of_aux (s::context) t in + and sort2 = type_of_aux ((C.Decl s)::context) t in sort_of_prod (sort1,sort2) | C.Lambda (n,s,t) -> let sort1 = type_of_aux context s - and type2 = type_of_aux (s::context) t in - let sort2 = type_of_aux (s::context) type2 in + and type2 = type_of_aux ((C.Decl s)::context) t in + let sort2 = type_of_aux ((C.Decl s)::context) type2 in (* only to check if the product is well-typed *) let _ = sort_of_prod (sort1,sort2) in C.Prod (n,s,type2) @@ -1067,7 +1135,7 @@ and type_of_aux' metasenv context t = | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux context he and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in - eat_prods hetype tlbody_and_type + eat_prods context hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") | C.Const (uri,cookingsno) -> incr fdebug ; @@ -1087,14 +1155,14 @@ and type_of_aux' metasenv context t = | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> let outsort = type_of_aux context outtype in let (need_dummy, k) = - let rec guess_args t = - match CicReduction.whd t with + let rec guess_args context t = + match CicReduction.whd context t with C.Sort _ -> (true, 0) | C.Prod (_, s, t) -> - let (b, n) = guess_args t in + let (b, n) = guess_args ((C.Decl s)::context) t in if n = 0 then (* last prod before sort *) - match CicReduction.whd s with + match CicReduction.whd context s with (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1) | C.Appl ((C.MutInd (uri',_,i')) :: _) @@ -1105,11 +1173,11 @@ and type_of_aux' metasenv context t = | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") in (*CSC whd non serve dopo type_of_aux ? *) - let (b, k) = guess_args outsort in + let (b, k) = guess_args context outsort in if not b then (b, k - 1) else (b, k) in let (parameters, arguments) = - match R.whd (type_of_aux context term) with + match R.whd context (type_of_aux context term) with (*CSC manca il caso dei CAST *) C.MutInd (uri',_,i') -> (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*) @@ -1133,7 +1201,7 @@ and type_of_aux' metasenv context t = else C.Appl ((C.MutInd (uri,cookingsno,i))::parameters) in - if not (check_allowed_sort_elimination uri i need_dummy + if not (check_allowed_sort_elimination context uri i need_dummy sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) then raise (NotWellTyped "MutCase: not allowed sort elimination") ; @@ -1156,8 +1224,8 @@ and type_of_aux' metasenv context t = (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) in (j + 1, b && - R.are_convertible (type_of_aux context p) - (type_of_branch parsno need_dummy outtype cons + R.are_convertible context (type_of_aux context p) + (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons)) ) ) (1,true) (List.combine pl cl) @@ -1175,19 +1243,26 @@ and type_of_aux' metasenv context t = let types_times_kl = List.rev (List.map - (fun (_,k,ty,_) -> let _ = type_of_aux context ty in (ty,k)) fl) + (fun (_,k,ty,_) -> + let _ = type_of_aux context ty in (C.Decl ty,k)) fl) in let (types,kl) = List.split types_times_kl in let len = List.length types in List.iter (fun (name,x,ty,bo) -> - if (R.are_convertible (type_of_aux (types @ context) bo) - (CicSubstitution.lift len ty)) + if + (R.are_convertible (types@context) (type_of_aux (types@context) bo) + (CicSubstitution.lift len ty)) then begin - let (m, eaten) = eat_lambdas (x + 1) bo in + let (m, eaten, context') = + eat_lambdas (types @ context) (x + 1) bo + in (*let's control the guarded by destructors conditions D{f,k,x,M}*) - if not (guarded_by_destructors eaten (len + eaten) kl 1 [] m) then + if + not + (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m) + then raise (NotWellTyped "Fix: not guarded by destructors") end else @@ -1200,13 +1275,15 @@ and type_of_aux' metasenv context t = | C.CoFix (i,fl) -> let types = List.rev - (List.map (fun (_,ty,_) -> let _ = type_of_aux context ty in ty) fl) + (List.map + (fun (_,ty,_) -> let _ = type_of_aux context ty in C.Decl ty) fl) in let len = List.length types in List.iter (fun (_,ty,bo) -> - if (R.are_convertible (type_of_aux (types @ context) bo) - (CicSubstitution.lift len ty)) + if + (R.are_convertible (types @ context) + (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) then begin (* let's control that the returned type is coinductive *) @@ -1215,7 +1292,11 @@ and type_of_aux' metasenv context t = 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 + if + not + (guarded_by_constructors (types @ context) 0 len false bo + [] uri) + then raise (NotWellTyped "CoFix: not guarded by constructors") end else @@ -1227,8 +1308,8 @@ and type_of_aux' metasenv context t = and sort_of_prod (t1, t2) = let module C = Cic in - let t1' = CicReduction.whd t1 in - let t2' = CicReduction.whd t2 in + let t1' = CicReduction.whd context t1 in + let t2' = CicReduction.whd context t2 in match (t1', t2') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) @@ -1239,22 +1320,22 @@ and type_of_aux' metasenv context t = (NotWellTyped ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) - and eat_prods hetype = + and eat_prods context hetype = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) (*CSC: cucinati *) function [] -> hetype | (hete, hety)::tl -> - (match (CicReduction.whd hetype) with + (match (CicReduction.whd context hetype) with Cic.Prod (n,s,t) -> - if CicReduction.are_convertible s hety then + if CicReduction.are_convertible context s hety then (CicReduction.fdebug := -1 ; - eat_prods (CicSubstitution.subst hete t) tl + eat_prods context (CicSubstitution.subst hete t) tl ) else begin CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible s hety) ; + ignore (CicReduction.are_convertible context s hety) ; fdebug := 0 ; debug s [hety] ; raise (NotWellTyped "Appl: wrong parameter-type") @@ -1264,7 +1345,7 @@ and type_of_aux' metasenv context t = and returns_a_coinductive ty = let module C = Cic in - match CicReduction.whd ty with + match CicReduction.whd context ty with C.MutInd (uri,cookingsno,i) -> (*CSC: definire una funzioncina per questo codice sempre replicato *) (match CicEnvironment.get_cooked_obj uri cookingsno with @@ -1288,26 +1369,40 @@ and type_of_aux' metasenv context t = | _ -> None in +(*CSC +prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ; +let res = +*) type_of_aux context t +(* +in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res +*) (* is a small constructor? *) (*CSC: ottimizzare calcolando staticamente *) -and is_small paramsno c = +and is_small context paramsno c = let rec is_small_aux context c = let module C = Cic in - match CicReduction.whd c with + match CicReduction.whd context c with C.Prod (_,so,de) -> (*CSC: [] is an empty metasenv. Is it correct? *) let s = type_of_aux' [] context so in (s = C.Sort C.Prop || s = C.Sort C.Set) && - is_small_aux (so::context) de + is_small_aux ((C.Decl so)::context) de | _ -> true (*CSC: we trust the type-checker *) in - let (sx,dx) = split_prods paramsno c in - is_small_aux (List.rev sx) dx + let (context',dx) = split_prods context paramsno c in + is_small_aux context' dx and type_of t = +(*CSC +prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ; +let res = +*) type_of_aux' [] [] t +(*CSC +in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res +*) ;; let typecheck uri = @@ -1322,7 +1417,7 @@ let typecheck uri = (match uobj with C.Definition (_,te,ty,_) -> let _ = type_of ty in - if not (R.are_convertible (type_of te ) ty) then + if not (R.are_convertible [] (type_of te ) ty) then raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) | C.Axiom (_,ty,_) -> (* only to check that ty is well-typed *) @@ -1331,7 +1426,7 @@ let typecheck uri = (*CSC [] wrong *) let _ = type_of_aux' conjs [] ty in debug (type_of_aux' conjs [] te) [] ; - if not (R.are_convertible (type_of_aux' conjs [] te) ty) then + if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) | C.Variable (_,bo,ty) -> (* only to check that ty is well-typed *) @@ -1339,7 +1434,7 @@ let typecheck uri = (match bo with None -> () | Some bo -> - if not (R.are_convertible (type_of bo) ty) then + if not (R.are_convertible [] (type_of bo) ty) then raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) ) | C.InductiveDefinition _ -> @@ -1348,20 +1443,3 @@ let typecheck uri = CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ;; - -(*******************************************************) -(*CSC: Da qua in avanti deve sparire tutto *) -exception NotImplemented -let wrong_context_of_context context = - let module C = Cic in - List.map - (function - C.Decl bt -> bt - | C.Def bt -> raise NotImplemented - ) context -;; - -let type_of_aux' metasenv context t = - let context' = wrong_context_of_context context in - type_of_aux' metasenv context' t -;; diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index ce7aa5280..4126d0446 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -130,7 +130,7 @@ let fo_unif_new metasenv context t1 t2 = | (C.Sort _ ,_) | (_, C.Sort _) | (C.Implicit, _) - | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst + | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst else raise UnificationFailed | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2 | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te @@ -163,7 +163,7 @@ let fo_unif_new metasenv context t1 t2 = | (C.MutInd _, _) | (_, C.MutInd _) | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst + | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst else raise UnificationFailed | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> let subst' = fo_unif_aux subst k outt1 outt2 in @@ -172,7 +172,7 @@ let fo_unif_new metasenv context t1 t2 = | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) - | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst + | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst else raise UnificationFailed | (_,_) -> raise UnificationFailed in fo_unif_aux [] 0 t1 t2;; -- 2.39.2