X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=0c0646d05a559dfc745c044d7fa1b2ced6a9e01a;hb=d356a5023cc06477b6d66a7b22a031ad7dffe947;hp=25fa7ef213cbda9df38a22c95186187bce20da38;hpb=fc4cf455977934bd737c3d6c8675ef7663a6a588;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 25fa7ef21..0c0646d05 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -377,7 +377,10 @@ and weakly_positive context n nn uri te = | t -> t in match CicReduction.whd context te with +(* C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true +*) + C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn @@ -389,13 +392,13 @@ and weakly_positive context n nn uri te = (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (name,(C.Decl source)))::context) + weakly_positive ((Some (name,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) -> - does_not_occur context n nn - (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((Some (name,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest + does_not_occur context n nn + (subst_inductive_type_with_dummy_mutind source)&& + weakly_positive ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) uri dest | _ -> raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) @@ -415,7 +418,8 @@ and strictly_positive context n nn te = let module C = Cic in let module U = UriManager in match CicReduction.whd context te with - C.Rel _ -> true + | t when does_not_occur context n nn t -> true + | C.Rel _ -> true | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) strictly_positive context n nn te @@ -427,37 +431,39 @@ and strictly_positive context n nn te = | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> let (ok,paramsno,ity,cl,name) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let (name,_,ity,cl) = List.nth tl i in - (List.length tl = 1, paramsno, ity, cl, name) - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) - in - let (params,arguments) = split tl paramsno in - let lifted_params = List.map (CicSubstitution.lift 1) params in - let cl' = + match o with + C.InductiveDefinition (tl,_,paramsno,_) -> + let (name,_,ity,cl) = List.nth tl i in + (List.length tl = 1, paramsno, ity, cl, name) + (* (true, paramsno, ity, cl, name) *) + | _ -> + raise + (TypeCheckerFailure + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) + in + let (params,arguments) = split tl paramsno in + let lifted_params = List.map (CicSubstitution.lift 1) params in + let cl' = List.map - (fun (_,te) -> - instantiate_parameters lifted_params - (CicSubstitution.subst_vars exp_named_subst te) - ) cl - in + (fun (_,te) -> + instantiate_parameters lifted_params + (CicSubstitution.subst_vars exp_named_subst te) + ) cl + in ok && - List.fold_right + List.fold_right (fun x i -> i && does_not_occur context n nn x) arguments true && (*CSC: MEGAPATCH3 (sara' quella giusta?)*) - List.fold_right + List.fold_right (fun x i -> - i && - weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri - x + i && + weakly_positive + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri + x ) cl' true - | t -> does_not_occur context n nn t - + | t -> false + (* the inductive type indexes are s.t. n < x <= nn *) and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in @@ -494,7 +500,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ UriManager.string_of_uri uri))) | C.Prod (C.Anonymous,source,dest) -> - strictly_positive context n nn source && + let b = strictly_positive context n nn source in + b && are_all_occurrences_positive ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest @@ -553,9 +560,12 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (are_all_occurrences_positive tys uri indparamsno i 0 len debrujinedte) then + begin + prerr_endline (UriManager.string_of_uri uri); + prerr_endline (string_of_int (List.length tys)); raise (TypeCheckerFailure - (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else ugraph' ) ugraph cl in @@ -762,7 +772,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = | C.MutCase (uri,i,outtype,term,pl) -> (match term with C.Rel m when List.mem m safes || m = x -> - let (tys,len,isinductive,paramsno,cl) = + let (lefts_and_tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> @@ -774,9 +784,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) in - (tys,List.length tl,isinductive,paramsno,cl') + (tys@lefts,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -799,7 +814,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (fun (p,(_,c)) i -> let rl' = let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte + recursive_args lefts_and_tys 0 len debrujinedte in let (e,safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x @@ -808,7 +823,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (tys,len,isinductive,paramsno,cl) = + let (lefts_and_tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> @@ -820,9 +835,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) in - (tys,List.length tl,isinductive,paramsno,cl') + (tys@lefts,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -847,7 +867,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (fun (p,(_,c)) i -> let rl' = let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte + recursive_args lefts_and_tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x @@ -942,7 +962,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | C.MutCase (uri,i,outtype,term,pl) -> (match CicReduction.whd ~subst context term with C.Rel m when List.mem m safes || m = x -> - let (tys,len,isinductive,paramsno,cl) = + let (lefts_and_tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> @@ -958,9 +978,14 @@ and guarded_by_destructors ~subst context n nn kl x safes = let debrujinedty = debrujin_constructor uri len ty in (id, snd (split_prods ~subst tys paramsno ty), snd (split_prods ~subst tys paramsno debrujinedty) - )) cl + )) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) in - (tys,len,isinductive,paramsno,cl') + (tys@lefts,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -986,7 +1011,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right (fun (p,(_,c,brujinedc)) i -> - let rl' = recursive_args tys 0 len brujinedc in + let rl' = recursive_args lefts_and_tys 0 len brujinedc in let (e,safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x in @@ -994,7 +1019,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst context' n' nn' kl x' safes' e ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (tys,len,isinductive,paramsno,cl) = + let (lefts_and_tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with C.InductiveDefinition (tl,_,paramsno,_) -> @@ -1006,9 +1031,14 @@ and guarded_by_destructors ~subst context n nn kl x safes = let cl' = List.map (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl + (id, snd (split_prods ~subst tys paramsno ty))) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) in - (tys,List.length tl,isinductive,paramsno,cl') + (tys@lefts,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1040,7 +1070,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = (fun (p,(_,c)) i -> let rl' = let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte + recursive_args lefts_and_tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x @@ -1393,10 +1423,10 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype = C.Appl l -> C.Appl (l@[C.Rel 1]) | t -> C.Appl [t ; C.Rel 1] in - C.Prod (C.Anonymous,so,type_of_branch ~subst + C.Prod (name,so,type_of_branch ~subst ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (AssertFailure (lazy "20")) + | _ -> raise (AssertFailure (lazy "20")) (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -1515,9 +1545,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let t' = CicUniv.fresh() in let ugraph1 = CicUniv.add_gt t' t ugraph in (C.Sort (C.Type t')),ugraph1 - (* TASSI: CONSTRAINTS *) | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Cast (te,ty) as t -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in @@ -1569,7 +1598,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = type_of_aux ~logger ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 in - (CicSubstitution.subst s ty1),ugraph2 + (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype,ugraph1 = type_of_aux ~logger context he ugraph in let tlbody_and_type,ugraph2 = @@ -1772,6 +1801,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = R.are_convertible ~subst ~metasenv context ty_p ty_branch ugraph3 in +(* Debugging code +if not b1 then +begin +prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype); +prerr_endline ("!CONS= " ^ CicPp.ppterm cons); +prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons); +prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch); +end; +*) if not b1 then debug_print (lazy ("#### " ^ CicPp.ppterm ty_p ^ @@ -1954,7 +1992,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = begin CicReduction.fdebug := -1 ; eat_prods ~subst context - (CicSubstitution.subst hete t) tl ugraph1 + (CicSubstitution.subst ~avoid_beta_redexes:true hete t) + tl ugraph1 (*TASSI: not sure *) end else