X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicTypeChecker.ml;h=8f36b9e1780e1d562c99939f7b791d181b615aec;hb=b7387d913f7dddf52d1e73173bca3fc8729723ba;hp=c0e90a5c6a20157284bf9de115611da4bef94bf6;hpb=8030b740ba0b84df1ae3a3e5878b447f3e4ec874;p=helm.git diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml index c0e90a5c6..8f36b9e17 100644 --- a/components/cic_proof_checking/cicTypeChecker.ml +++ b/components/cic_proof_checking/cicTypeChecker.ml @@ -772,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,_) -> @@ -784,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:" ^ @@ -809,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 @@ -818,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,_) -> @@ -830,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:" ^ @@ -857,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 @@ -952,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,_) -> @@ -968,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:" ^ @@ -996,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 @@ -1004,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,_) -> @@ -1016,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:" ^ @@ -1050,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 @@ -1523,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 @@ -1943,9 +1965,12 @@ end; | (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? *)