X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=787a0cb3c02e6c8549deb29a4793420c3b591055;hb=8c09c56656b3ce07d3f66e7d6ca848cb918b84bd;hp=0c0646d05a559dfc745c044d7fa1b2ced6a9e01a;hpb=d356a5023cc06477b6d66a7b22a031ad7dffe947;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 0c0646d05..787a0cb3c 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' = @@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te = 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 && (try - let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in + 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) @@ -273,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) @@ -292,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 -> @@ -304,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 -> @@ -338,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) -> @@ -360,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 @@ -382,13 +402,8 @@ and weakly_positive context n nn uri te = *) 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) && @@ -428,7 +443,9 @@ 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 @@ -454,7 +471,6 @@ and strictly_positive context n nn te = List.fold_right (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 && @@ -499,14 +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) -> - 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 | 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 @@ -731,98 +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.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 (lefts_and_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 - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,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 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 - 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 -> + 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 @@ -842,7 +779,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,List.length tl,isinductive,paramsno,cl') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -886,38 +823,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")) ) @@ -935,10 +866,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 @@ -948,10 +880,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) @@ -985,7 +913,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,len,isinductive,paramsno,cl') + (lefts@tys,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1010,12 +938,12 @@ 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 -> + (fun (p,(name,c,brujinedc)) i -> + i && 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 - 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 -> @@ -1038,7 +966,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | (_,_,ty,_)::_ -> fst (split_prods ~subst [] paramsno ty) in - (tys@lefts,List.length tl,isinductive,paramsno,cl') + (lefts@tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1086,25 +1014,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 -> @@ -1113,6 +1072,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 *) @@ -1257,7 +1220,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 && @@ -1298,7 +1267,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 && @@ -1309,7 +1284,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 && @@ -1325,11 +1306,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 @@ -1445,11 +1427,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 @@ -1458,8 +1438,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 @@ -1504,10 +1501,7 @@ 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 @@ -1543,8 +1537,11 @@ 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 + (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 "Implicit found")) | C.Cast (te,ty) as t -> @@ -1579,9 +1576,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)) @@ -1596,7 +1604,7 @@ 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 ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> @@ -1605,7 +1613,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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 @@ -1765,21 +1773,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 -> @@ -1831,16 +1846,14 @@ end; 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) -> @@ -1863,7 +1876,7 @@ end; (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 @@ -1874,15 +1887,15 @@ end; 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) -> @@ -1922,7 +1935,7 @@ end; 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 @@ -1948,7 +1961,7 @@ end; 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 @@ -1962,9 +1975,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? *) @@ -1985,6 +2001,8 @@ end; (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 @@ -2118,6 +2136,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) -> @@ -2219,3 +2240,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);;