X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ad00c0eeb614bfc2ce958c9818386041a9fc084d;hb=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;hp=87a0ca0546f9b77f78b02da7a8380fd78f6cdc0f;hpb=4f3c06e2bf0cde557d8d2d3d59b4ed785741cf76;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 87a0ca054..ad00c0eeb 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) @@ -765,9 +766,10 @@ 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 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) -> + | 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 ((Some (name,(C.Def (so,None))))::context) + 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 *) @@ -953,10 +955,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 @@ -1371,11 +1374,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 @@ -1491,11 +1495,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 @@ -1504,8 +1506,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 @@ -1550,10 +1569,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 @@ -1628,9 +1644,19 @@ 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 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)) @@ -1645,7 +1671,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 -> @@ -1654,7 +1680,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 @@ -2042,6 +2068,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 @@ -2175,6 +2203,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) -> @@ -2276,3 +2307,6 @@ 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 -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;