X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=ccbebc27164a16afb088bfa131a252dca37fe472;hb=53b957fd45c47b20d698503c9bb67e2ef3ab98e1;hp=c4c2af477d3a510e33846f2bec5f827635a16ef3;hpb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index c4c2af477..ccbebc271 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -197,9 +197,9 @@ let does_not_occur ~subst context n nn t = perform substitution only if DoesOccur is raised *) let _,_,term,_ = U.lookup_subst mno subst in aux (k-s) () (S.subst_meta (0,l) term) - with U.Subst_not_found _ -> match l with + with U.Subst_not_found _ -> () (*match l with | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur - | C.Ctx lc -> List.iter (aux (k-s) ()) lc) + | C.Ctx lc -> List.iter (aux (k-s) ()) lc*)) | t -> U.fold (fun _ k -> k + 1) k aux () t in try aux 0 () t; true @@ -256,6 +256,10 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = let dummy = C.Sort C.Prop in (*CSC: to be moved in cicSubstitution? *) let rec subst_inductive_type_with_dummy _ = function + | C.Meta (_,(_,C.Irl _)) as x -> x + | C.Meta (i,(lift,C.Ctx ls)) -> + C.Meta (i,(lift,C.Ctx + (List.map (subst_inductive_type_with_dummy ()) ls))) | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) when NUri.eq uri' uri -> @@ -270,6 +274,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = let rec aux context n nn te = match R.whd ~subst context te with | t when t = dummy -> true + | C.Meta (i,lc) -> + (try + let _,_,term,_ = U.lookup_subst i subst in + let t = S.subst_meta lc term in + weakly_positive ~subst context n nn uri indparamsno posuri t + with U.Subst_not_found _ -> true) | C.Appl (te::rargs) when te = dummy -> List.for_all (does_not_occur ~subst context n nn) rargs | C.Prod (name,source,dest) when @@ -288,6 +298,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = and strictly_positive ~subst context n nn indparamsno posuri te = match R.whd ~subst context te with | t when does_not_occur ~subst context n nn t -> true + | C.Meta (i,lc) -> + (try + let _,_,term,_ = U.lookup_subst i subst in + let t = S.subst_meta lc term in + strictly_positive ~subst context n nn indparamsno posuri t + with U.Subst_not_found _ -> true) | C.Rel _ when indparamsno = 0 -> true | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn -> check_homogeneous_call ~subst context indparamsno n posuri reduct tl; @@ -379,11 +395,11 @@ let rec typeof ~subst ~metasenv context term = with Failure _ -> raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context)))) - | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u]) - | C.Sort (C.Type _) -> - raise (AssertFailure (lazy ("Cannot type an inferred type: "^ - NCicPp.ppterm ~subst ~metasenv ~context t))) - | C.Sort _ -> C.Sort (C.Type NCicEnvironment.type0) + | C.Sort s -> + (try C.Sort (NCicEnvironment.typeof_sort s) + with + | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg) + | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg)) | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Meta (n,l) as t -> let canonical_ctx,ty = @@ -643,9 +659,10 @@ and check_allowed_sort_elimination ~subst ~metasenv r = (PP.ppterm ~subst ~metasenv ~context so) ))); (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with - | (C.Sort C.Type _, C.Sort _) - | (C.Sort C.Prop, C.Sort C.Prop) -> () - | (C.Sort C.Prop, C.Sort C.Type _) -> + | C.Sort s1, (C.Sort s2 as arity2) -> + (match NCicEnvironment.allowed_sort_elimination s1 s2 with + | `Yes -> () + | `UnitOnly -> (* TODO: we should pass all these parameters since we * have them already *) let _,leftno,itl,_,i = E.get_checked_indtys r in @@ -663,8 +680,12 @@ and check_allowed_sort_elimination ~subst ~metasenv r = is_non_informative ~metasenv ~subst leftno constrty)) then raise (TypeCheckerFailure (lazy - ("Sort elimination not allowed"))); - | _,_ -> ()) + ("Sort elimination not allowed: " ^ + NCicPp.ppterm ~metasenv ~subst ~context arity1 + ^ " towards "^ + NCicPp.ppterm ~metasenv ~subst ~context arity2 + )))) + | _ -> ()) | _,_ -> () in aux @@ -721,7 +742,9 @@ and is_non_informative ~metasenv ~subst paramsno c = match R.whd ~subst context c with | C.Prod (n,so,de) -> let s = typeof ~metasenv ~subst context so in - s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de + (s = C.Sort C.Prop || + match s with C.Sort (C.Type ((`CProp,_)::_)) -> true | _ -> false) && + aux ((n,(C.Decl so))::context) de | _ -> true in let context',dx = NCicReduction.split_prods ~subst [] paramsno c in aux context' dx @@ -1033,10 +1056,7 @@ and is_really_smaller is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t | C.Appl (he::_) -> is_really_smaller r_uri r_len ~subst ~metasenv k he - | C.Rel _ - | C.Const (Ref.Ref (_,Ref.Con _)) -> false - | C.Appl [] - | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false + | C.Appl [] | C.Implicit _ -> assert false | C.Meta _ -> true | C.Match (Ref.Ref (_,Ref.Ind (isinductive,_,_)),_,term,pl) -> (match term with @@ -1054,7 +1074,7 @@ and is_really_smaller is_really_smaller r_uri r_len ~subst ~metasenv k e) pl dcl | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl) - | _ -> assert false + | _ -> false and returns_a_coinductive ~subst context ty = match R.whd ~subst context ty with @@ -1288,7 +1308,9 @@ let typecheck_obj (uri,height,metasenv,subst,kind) = | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as ref) :: _) -> let _,_,itl,_,_ = E.get_checked_indtys ref in uri, List.length itl - | _ -> assert false + | _ -> + raise (TypeCheckerFailure + (lazy "Fix: the recursive argument is not inductive")) in (* guarded by destructors conditions D{f,k,x,M} *) let rec enum_from k =