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=dd25edac4fd0531e665ebfd26e444082cf4f1e0b;hpb=b22ad9b6f6330602742ca300370c3ff57c6bb3e9;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index dd25edac4..5f1c933f2 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -347,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) -> @@ -369,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 @@ -391,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) && @@ -437,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 @@ -463,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 && @@ -508,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 @@ -740,99 +741,24 @@ 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,ty,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst context n nn kl x safes ty && - check_is_really_smaller_arg ~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 (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 (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 @@ -852,7 +778,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:" ^ @@ -864,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 lefts_and_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 -> @@ -904,34 +822,18 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = ) ([],0) 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.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 (m-1) with @@ -969,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) @@ -1006,7 +904,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:" ^ @@ -1031,12 +929,13 @@ 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 lefts_and_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 -> @@ -1059,7 +958,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:" ^ @@ -1091,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 lefts_and_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 @@ -1107,24 +1007,45 @@ 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,_ = + 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 - 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 + ) ([],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 @@ -1144,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 *) @@ -1647,6 +1572,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | 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 _,ugraph1 = type_of_aux ~logger context ty ugraph1 in let b,ugraph1 = R.are_convertible ~subst ~metasenv context ty ty' ugraph1 in @@ -1943,7 +1869,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 @@ -2002,7 +1928,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 @@ -2028,7 +1954,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 @@ -2309,4 +2235,18 @@ let check_allowed_sort_elimination uri i s1 s2 = CicUniv.empty_ugraph) ;; -Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_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);;