X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=8f36b9e1780e1d562c99939f7b791d181b615aec;hb=0e850ea466d664062ad1999e75c60b90aadaa084;hp=951f68dbd84b28043a100fe3c72c114d4f5927a7;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 951f68dbd..8f36b9e17 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -240,12 +240,16 @@ and type_of_variable ~logger uri ugraph = and does_not_occur ?(subst=[]) 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 ~subst context te with + match te with C.Rel m when m > n && m <= nn -> false - | C.Rel _ + | C.Rel m -> + (try + (match List.nth context (m-1) with + Some (_,C.Def (bo,_)) -> + does_not_occur ~subst context n nn (CicSubstitution.lift m bo) + | _ -> true) + with + Failure _ -> assert false) | C.Sort _ | C.Implicit _ -> true | C.Meta (_,l) -> @@ -253,7 +257,12 @@ and does_not_occur ?(subst=[]) context n nn te = (fun x i -> match x with None -> i - | Some x -> i && does_not_occur ~subst context n nn x) l true + | Some x -> i && does_not_occur ~subst context n nn x) l true && + (try + let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in + does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term) + with + CicUtil.Subst_not_found _ -> true) | C.Cast (te,ty) -> does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty | C.Prod (name,so,dest) -> @@ -368,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 @@ -380,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")) @@ -406,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 @@ -418,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 @@ -485,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 @@ -544,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 @@ -753,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,_) -> @@ -765,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:" ^ @@ -790,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 @@ -799,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,_) -> @@ -811,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:" ^ @@ -838,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 @@ -933,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,_) -> @@ -949,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:" ^ @@ -977,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 @@ -985,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,_) -> @@ -997,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:" ^ @@ -1031,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 @@ -1384,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 - @@ -1472,7 +1511,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with - _ -> + Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> @@ -1504,11 +1543,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt t' t ugraph in - (C.Sort (C.Type t')),ugraph1 - (* TASSI: CONSTRAINTS *) + (try + let ugraph1 = CicUniv.add_gt t' t ugraph in + (C.Sort (C.Type t')),ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | 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 @@ -1560,7 +1601,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 = @@ -1763,6 +1804,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 ^ @@ -1915,9 +1965,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),ugraph2 + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) @@ -1945,7 +1998,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 @@ -2147,9 +2201,12 @@ let typecheck_obj ~logger uri obj = (** wrappers which instantiate fresh loggers *) +let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'" + let type_of_aux' ?(subst = []) metasenv context t ugraph = let logger = new CicLogger.logger in - type_of_aux' ~logger ~subst metasenv context t ugraph + profiler.HExtlib.profile + (type_of_aux' ~logger ~subst metasenv context t) ugraph let typecheck_obj uri obj = let logger = new CicLogger.logger in