X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=5f1c933f2f0e295e03904c6ca05348012f09dae8;hb=6a95acad523131e0775e703d5d4bfac756609fb0;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..5f1c933f2 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -75,7 +75,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) | C.Appl l -> C.Appl (List.map (aux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -240,20 +240,29 @@ 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) -> + | C.Meta (mno,l) -> List.fold_right (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 mno 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) -> @@ -264,10 +273,11 @@ and does_not_occur ?(subst=[]) context n nn te = does_not_occur ~subst context n nn so && does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest - | C.LetIn (name,so,dest) -> + | C.LetIn (name,so,ty,dest) -> does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context) - (n + 1) (nn + 1) dest + does_not_occur ~subst context n nn ty && + does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) + (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true | C.Var (_,exp_named_subst) @@ -283,8 +293,12 @@ and does_not_occur ?(subst=[]) context n nn te = 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 (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -295,8 +309,12 @@ and does_not_occur ?(subst=[]) context n nn te = 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 (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -329,6 +347,10 @@ and weakly_positive context n nn uri te = | C.Lambda (name,so,ta) -> C.Lambda (name, subst_inductive_type_with_dummy_mutind so, subst_inductive_type_with_dummy_mutind ta) + | C.LetIn (name,so,ty,ta) -> + C.LetIn (name, subst_inductive_type_with_dummy_mutind so, + subst_inductive_type_with_dummy_mutind ty, + subst_inductive_type_with_dummy_mutind ta) | C.Appl tl -> C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) | C.MutCase (uri,i,outtype,term,pl) -> @@ -351,6 +373,13 @@ and weakly_positive context n nn uri te = exp_named_subst in C.Const (uri,exp_named_subst') + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + exp_named_subst + in + C.Var (uri,exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map @@ -368,25 +397,23 @@ 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 - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 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 ((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 +433,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 @@ -415,40 +443,43 @@ and strictly_positive context n nn te = strictly_positive ((Some (name,(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 context n nn x) tl true - | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> + | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) + | (C.MutInd (uri,i,exp_named_subst)) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in 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 @@ -484,13 +515,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = raise (TypeCheckerFailure (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 && - are_all_occurrences_positive - ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno - (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn source && are_all_occurrences_positive @@ -544,9 +570,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 @@ -712,94 +741,25 @@ and eat_lambdas ~subst context n te = | (n, te) -> raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))) -(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and check_is_really_smaller_arg ~subst 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 + (*CSC: we could perform beta-iota(-zeta?) immediately, and + delta only on-demand when it fails without *) match CicReduction.whd ~subst context te with C.Rel m when List.mem m safes -> true - | C.Rel _ -> false - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -(* | C.Cast (te,ty) -> - check_is_really_smaller_arg ~subst n nn kl x safes te && - check_is_really_smaller_arg ~subst n nn kl x safes ty*) -(* | C.Prod (_,so,ta) -> - check_is_really_smaller_arg ~subst n nn kl x safes so && - check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta*) - | C.Prod _ -> raise (AssertFailure (lazy "10")) - | C.Lambda (name,so,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::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 ~subst context n nn kl x safes he - | C.Appl [] -> raise (AssertFailure (lazy "11")) + | C.Rel _ + | C.Appl _ + | C.MutConstruct _ | C.Const _ - | C.MutInd _ -> raise (AssertFailure (lazy "12")) - | C.MutConstruct _ -> false + | C.Var _ -> false + | C.Lambda (name,ty,ta) -> + check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context) + (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta | 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 o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let tys = - List.map - (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl - in - let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl - in - (tys,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - List.fold_right - (fun p i -> - i && check_is_really_smaller_arg ~subst context n nn kl x safes p) - pl true - else - let pl_and_cl = - try - List.combine pl cl - with - Invalid_argument _ -> - raise (TypeCheckerFailure (lazy "not enough patterns")) - in - List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte - in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - 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) = + C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x -> + 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 +771,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') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -825,27 +790,19 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else - let pl_and_cl = - try - List.combine pl cl - with - Invalid_argument _ -> - raise (TypeCheckerFailure (lazy "not enough patterns")) - in - (*CSC: supponiamo come prima che nessun controllo sia necessario*) - (*CSC: sugli argomenti di una applicazione *) - List.fold_right - (fun (p,(_,c)) i -> + List.for_all2 + (fun p (_,c) -> let rl' = let debrujinedte = debrujin_constructor uri len c in - recursive_args tys 0 len debrujinedte + recursive_args lefts_and_tys paramsno + (len+paramsno) debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x in - i && - check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true + check_is_really_smaller_arg + ~subst context' n' nn' kl x' safes' e + ) pl cl | _ -> List.fold_right (fun p i -> @@ -857,38 +814,32 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(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 ~subst (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 - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right - (fun (_,ty,bo) i -> + (fun (_,_,_,bo) i -> i && check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true + | t -> + raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t))) -and guarded_by_destructors ~subst context n nn kl x safes = +and guarded_by_destructors ~subst context n nn kl x safes t = let module C = Cic in let module U = UriManager in - function + match CicReduction.whd ~subst context t with C.Rel m when m > n && m <= nn -> false | C.Rel m -> - (match List.nth context (n-1) with + (match List.nth context (m-1) with Some (_,C.Decl _) -> true | Some (_,C.Def (bo,_)) -> - guarded_by_destructors ~subst context m nn kl x safes + guarded_by_destructors ~subst context n nn kl x safes (CicSubstitution.lift m bo) | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) ) @@ -906,10 +857,11 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst context n nn kl x safes so && guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> + | C.LetIn (name,so,ty,ta) -> guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + guarded_by_destructors ~subst context n nn kl x safes ty && + guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::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 if not (List.length tl > k) then false @@ -919,10 +871,6 @@ and guarded_by_destructors ~subst context n nn kl x safes = i && guarded_by_destructors ~subst context n nn kl x safes param ) tl true && check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) - | C.Appl tl -> - List.fold_right - (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - tl true | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) @@ -933,7 +881,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 +897,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') + (lefts@tys,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -976,16 +929,17 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst context n nn kl x safes outtype && (*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 + (fun (p,(name,c,brujinedc)) i -> + i && + let rl' = recursive_args + lefts_and_tys paramsno (len+paramsno) brujinedc in let (e,safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x in - i && 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 +951,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') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1031,7 +990,8 @@ 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 paramsno + (len+paramsno) debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x @@ -1047,25 +1007,56 @@ and guarded_by_destructors ~subst context n nn kl x safes = (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p) pl true ) - | C.Fix (_, fl) -> + | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t-> + let l = match t with C.Appl (_::tl) -> tl | _ -> [] in let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(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 ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true + let n_plus_len = n + len in + let nn_plus_len = nn + len in + let x_plus_len = x + len in + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in + let safes' = List.map (fun x -> x + len) safes in + List.for_all + (guarded_by_destructors ~subst context n nn kl x safes) l && + snd (List.fold_left + (fun (fixno',i) (_,recno,ty,bo) -> + fixno'+1, + i && + guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + if + fixno' = fixno && + List.length l > recno && + (*case where the recursive argument is already really_smaller *) + check_is_really_smaller_arg ~subst context n nn kl x safes + (List.nth l recno) + then + let bo_without_lambdas,_,context = + eat_lambdas ~subst (tys@context) (recno+1) bo + in + (* we assume the formal argument to be safe *) + guarded_by_destructors ~subst context (n_plus_len+recno+1) + (nn_plus_len+recno+1) kl (x_plus_len+recno+1) + (1::List.map (fun x -> x+recno+1) safes') + bo_without_lambdas + else + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len + kl x_plus_len safes' bo + ) (0,true) fl) | 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 - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1074,6 +1065,10 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true + | C.Appl tl -> + List.fold_right + (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) + tl true (* the boolean h means already protected *) (* args is the list of arguments the type of the constructor that may be *) @@ -1218,7 +1213,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len 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 (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1259,7 +1260,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len 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 (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1270,7 +1277,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let n_plus_len = n + len 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 (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1286,11 +1299,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let arity1 = CicReduction.whd ~subst context arity1 in let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy = match arity1, CicReduction.whd ~subst context arity2 with - (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> + (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger + ((Some (name,C.Decl so1))::context) uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 else @@ -1384,10 +1398,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 - @@ -1406,11 +1420,9 @@ and check_metasenv_consistency ~logger ~subst metasenv context [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1419,8 +1431,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context match (t,ct) with | _,None -> ugraph | Some t,Some (_,C.Def (ct,_)) -> + (*CSC: the following optimization is to avoid a possibly expensive + reduction that can be easily avoided and that is quite + frequent. However, this is better handled using levels to + control reduction *) + let optimized_t = + match t with + Cic.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with + Failure _ -> t) + | _ -> t + in +(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!" +else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*) let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t ct ugraph + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph in if not b then raise @@ -1465,14 +1494,11 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t,ugraph - | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph - | Some (_,C.Def (bo,None)) -> - debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; - type_of_aux ~logger context (S.lift n bo) ugraph + | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with - _ -> + Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> @@ -1504,11 +1530,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 @@ -1541,9 +1569,20 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 in (C.Prod (n,s,type2)),ugraph2 - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) - let ty,ugraph1 = type_of_aux ~logger context s ugraph in + let ty',ugraph1 = type_of_aux ~logger context s ugraph in + let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context ty ty' ugraph1 + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf + "The type of %s is %s but it is expected to be %s" + (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty)))) + else (* The type of a LetIn is a LetIn. Extremely slow since the computed LetIn is later reduced and maybe also re-checked. (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)) @@ -1558,16 +1597,16 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Moreover the inferred type is closer to the expected one. *) let ty1,ugraph2 = type_of_aux ~logger - ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 + ((Some (n,(C.Def (s,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 = List.fold_right ( fun x (l,ugraph) -> let ty,ugraph1 = type_of_aux ~logger context x ugraph in - let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) ((x,ty)::l,ugraph1)) tl ([],ugraph1) in @@ -1727,21 +1766,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in if not b then raise - (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed"))); + (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); (* let's check if the type of branches are right *) - let parsno = + let parsno,constructorsno = let obj,_ = try CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with - C.InductiveDefinition (_,_,parsno,_) -> parsno + C.InductiveDefinition (il,_,parsno,_) -> + let _,_,_,cl = + try List.nth il i with Failure _ -> assert false + in + parsno, List.length cl | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) - in + in + if List.length pl <> constructorsno then + raise (TypeCheckerFailure + (lazy ("Wrong number of cases in case analysis"))) ; let (_,branches_ok,ugraph5) = List.fold_left (fun (j,b,ugraph) p -> @@ -1763,6 +1809,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 ^ @@ -1784,16 +1839,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in outtype,ugraph5 | C.Fix (i,fl) -> - let types_times_kl,ugraph1 = - (* WAS: list rev list map *) + let types,kl,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,k,ty,_) -> + (fun (types,kl,ugraph,len) (n,k,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + k::kl,ugraph1,len+1) + ) ([],[],ugraph,0) fl in - let (types,kl) = List.split types_times_kl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (name,x,ty,bo) -> @@ -1816,7 +1869,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (len + eaten) kl 1 [] m) then raise (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors"))) + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) else ugraph2 end @@ -1827,15 +1880,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let (_,_,ty,_) = List.nth fl i in ty,ugraph2 | C.CoFix (i,fl) -> - let types,ugraph1 = + let types,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,ty,_) -> + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl ty))::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + ugraph1,len+1) + ) ([],ugraph,0) fl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (_,ty,bo) -> @@ -1875,7 +1928,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let (_,ty,_) = List.nth fl i in ty,ugraph2 - and check_exp_named_subst ~logger ~subst context ugraph = + and check_exp_named_subst ~logger ~subst context = let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with [] -> ugraph @@ -1901,7 +1954,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in - check_exp_named_subst_aux ~logger [] ugraph + check_exp_named_subst_aux ~logger [] and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in @@ -1915,9 +1968,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? *) @@ -1938,6 +1994,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> let b,ugraph1 = +(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then( +prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*) CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in @@ -1945,7 +2003,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 @@ -2070,6 +2129,9 @@ let typecheck_obj0 ~logger uri ugraph = let _,ugraph = type_of ~logger ty ugraph in ugraph | C.CurrentProof (_,conjs,te,ty,_,_) -> + (* this block is broken since the metasenv should + * be topologically sorted before typing metas *) + ignore(assert false); let _,ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> @@ -2147,9 +2209,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 @@ -2168,3 +2233,20 @@ let check_allowed_sort_elimination uri i s1 s2 = ~logger:(new CicLogger.logger) [] uri i true (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) CicUniv.empty_ugraph) +;; + +Deannotate.type_of_aux' := + fun context t -> + ignore ( + List.fold_right + (fun el context -> + (match el with + None -> () + | Some (_,Cic.Decl ty) -> + ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph) + | Some (_,Cic.Def (bo,ty)) -> + ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph); + ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph)); + el::context + ) context []); + fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;