From: Claudio Sacerdoti Coen Date: Mon, 31 Mar 2008 17:02:48 +0000 (+0000) Subject: 1) Impredicative sort "Set" removed everywhere. X-Git-Tag: make_still_working~5484 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=013dba0f27e3e834bb2297bcd89a570df6372ef2;p=helm.git 1) Impredicative sort "Set" removed everywhere. 2) Sort "CProp" is now predicative. 3) Optimized case IRL in check_metasenv_consistency. --- diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index b2f3351c6..c4163edb4 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -13,7 +13,7 @@ (********************************* TERMS ************************************) -type sort = Prop | Set | Type of int | CProp +type sort = Prop | Type of int | CProp type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index d7011c8df..4686922df 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -16,7 +16,6 @@ let convert_term uri n_fl t = Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t) | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp - | NCic.Sort NCic.Set -> Cic.Sort Cic.Set | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) | NCic.Implicit _ -> assert false | NCic.Const (NReference.Ref (_,u,NReference.Ind i)) -> diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index baa82d033..c74b50edf 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -2282,14 +2282,14 @@ let sort_of_prod ~subst context (name,s) (t1, t2) = let t1 = R.whd ~subst context t1 in let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in match t1, t2 with - | C.Sort s1, C.Sort s2 - (* different from Coq manual, Impredicative Set! *) - when (s2 = C.Prop || s2 = C.Set || s2 = C.CProp) -> C.Sort s2 - | C.Sort (C.Type t1), C.Sort (C.Type t2) -> C.Sort (C.Type (max t1 t2)) - | C.Sort _,C.Sort (C.Type t1) -> C.Sort (C.Type t1) - | C.Meta _, C.Sort _ -> t2 - | C.Meta _, ((C.Meta _) as t) - | C.Sort _, ((C.Meta _) as t) when U.is_closed t -> t2 + | C.Sort s1, C.Sort C.Prop -> t2 + | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2)) + | C.Sort _,C.Sort (C.Type _) -> t2 + | C.Sort (C.Type _) , C.Sort C.CProp -> t1 + | C.Sort _, C.Sort C.CProp -> t2 + | C.Meta _, C.Sort _ + | C.Meta _, C.Meta _ + | C.Sort _, C.Meta _ when U.is_closed t2 -> t2 | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: expected two sorts, found = %s, %s" @@ -2319,7 +2319,7 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = ;; -let typeof ~subst ~metasenv context term = +let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = function | C.Rel n -> (try @@ -2330,24 +2330,35 @@ let typeof ~subst ~metasenv context term = | C.Sort (C.Type i) -> C.Sort (C.Type (i+1)) | C.Sort s -> C.Sort (C.Type 0) | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) + | C.Meta (n,l) as t -> + let canonical_context,ty = + try + let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty + with NCicUtils.Subst_not_found _ -> try + let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty + with NCicUtils.Meta_not_found _ -> + raise (AssertFailure (lazy (Printf.sprintf + "%s not found" (NCicPp.ppterm t)))) + in + check_metasenv_consistency t context canonical_context l; + S.subst_meta l ty + | C.Const ref -> type_of_constant ref | C.Prod (name,s,t) -> let sort1 = typeof_aux context s in let sort2 = typeof_aux ((name,(C.Decl s))::context) t in sort_of_prod ~subst context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> - let sort1 = typeof_aux context s in - (match R.whd ~subst context sort1 with + let sort = typeof_aux context s in + (match R.whd ~subst context sort with | C.Meta _ | C.Sort _ -> () | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf ("Not well-typed lambda-abstraction: " ^^ "the source %s should be a type; instead it is a term " ^^ - "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort1))))); - let type2 = - typeof_aux ((n,(C.Decl s))::context) t - in - C.Prod (n,s,type2) + "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort))))); + let ty = typeof_aux ((n,(C.Decl s))::context) t in + C.Prod (n,s,ty) | C.LetIn (n,ty,t,bo) -> let ty_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context ty ty_t) then @@ -2357,14 +2368,6 @@ let typeof ~subst ~metasenv context term = "The type of %s is %s but it is expected to be %s" (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty)))) else - (* Alternatives: - 1) The type of a LetIn is a LetIn, extremely slow since the computed - LetIn may be later reduced. - 2) The type of the LetIn is reduced, much faster than the previous - solution, moreover the inferred type is probably very different - from the expected one. - 3) One-step LetIn reduction, even faster than the previous solution, - moreover the inferred type is closer to the expected one. *) let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in S.subst ~avoid_beta_redexes:true t ty_bo | C.Appl (he::(_::_ as args)) -> @@ -2372,19 +2375,9 @@ let typeof ~subst ~metasenv context term = let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in eat_prods ~subst ~metasenv context ty_he args_with_ty | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) - | C.Meta (n,l) -> - (try - let _,canonical_context,term,ty = NCicUtils.lookup_subst n subst in - check_metasenv_consistency context canonical_context l; - (* assuming subst is well typed !!!!! *) - S.subst_meta l ty - with NCicUtils.Subst_not_found _ -> - let _,_,canonical_context,ty = NCicUtils.lookup_meta n metasenv in - check_metasenv_consistency context canonical_context l; - S.subst_meta l ty) | C.Match (r,outtype,term,pl) -> - let outsort = typeof_aux context outtype in assert false (* FINQUI + let outsort = typeof_aux context outtype in let (need_dummy, k) = let rec guess_args context t = let outtype = R.whd ~subst context t in @@ -2572,71 +2565,103 @@ end; in outtype,ugraph5 *) - and check_metasenv_consistency context canonical_context l = - let lifted_canonical_context = - let rec lift_metas i = function - | [] -> [] - | (n,C.Decl t)::tl -> - (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl) - | (n,C.Def (t,ty))::tl -> - (n,C.Def ((S.subst_meta l (S.lift i t)), - S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl) - in - lift_metas 1 canonical_context - in - (* we could optimize when l is an NCic.Irl *) - let l = - let shift, lc_kind = l in - List.map (S.lift shift) (NCicUtils.expand_local_context lc_kind) - in - List.iter2 - (fun t ct -> - match (t,ct) with - | t, (_,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 - | C.Rel n -> - (try - match List.nth context (n - 1) with - | (_,C.Def (te,_)) -> S.lift n te - | _ -> t - with Failure _ -> t) - | _ -> t - in - if not (R.are_convertible ~subst ~metasenv context optimized_t ct)then - raise - (TypeCheckerFailure - (lazy (Printf.sprintf - ("Not well typed metavariable local context: " ^^ - "expected a term convertible with %s, found %s") - (NCicPp.ppterm ct) (NCicPp.ppterm t)))) - | t, (_,C.Decl ct) -> - let type_t = typeof_aux context t in - if not (R.are_convertible ~subst ~metasenv context type_t ct) then - raise (TypeCheckerFailure - (lazy (Printf.sprintf - ("Not well typed metavariable local context: "^^ - "expected a term of type %s, found %s of type %s") - (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) - ) l lifted_canonical_context + and check_metasenv_consistency term context canonical_context l = + match l with + | shift, NCic.Irl n -> + let context = snd (HExtlib.split_nth shift context) in + let rec compare = function + | 0,_,[] -> () + | 0,_,_::_ + | _,_,[] -> + raise (AssertFailure (lazy (Printf.sprintf + "Local and canonical context %s have different lengths" + (NCicPp.ppterm term)))) + | m,[],_::_ -> + raise (TypeCheckerFailure (lazy (Printf.sprintf + "Unbound variable -%d in %s" m (NCicPp.ppterm term)))) + | m,t::tl,ct::ctl -> + (match t,ct with + (_,C.Decl t1), (_,C.Decl t2) + | (_,C.Def (t1,_)), (_,C.Def (t2,_)) + | (_,C.Def (_,t1)), (_,C.Decl t2) -> + if not (R.are_convertible ~subst ~metasenv tl t1 t2) then + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + ("Not well typed metavariable local context for %s: " ^^ + "%s expected, which is not convertible with %s") + (NCicPp.ppterm term) (NCicPp.ppterm t2) (NCicPp.ppterm t1) + ))) + | _,_ -> + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + ("Not well typed metavariable local context for %s: " ^^ + "a definition expected, but a declaration found") + (NCicPp.ppterm term))))); + compare (m - 1,tl,ctl) + in + compare (n,context,canonical_context) + | shift, lc_kind -> + (* we avoid useless lifting by shortening the context*) + let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in + let lifted_canonical_context = + let rec lift_metas i = function + | [] -> [] + | (n,C.Decl t)::tl -> + (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl) + | (n,C.Def (t,ty))::tl -> + (n,C.Def ((S.subst_meta l (S.lift i t)), + S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl) + in + lift_metas 1 canonical_context in + let l = NCicUtils.expand_local_context lc_kind in + try + List.iter2 + (fun t ct -> + match (t,ct) with + | t, (_,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 + | C.Rel n -> + (try + match List.nth context (n - 1) with + | (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with Failure _ -> t) + | _ -> t + in + if not (R.are_convertible ~subst ~metasenv context optimized_t ct) + then + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + ("Not well typed metavariable local context: " ^^ + "expected a term convertible with %s, found %s") + (NCicPp.ppterm ct) (NCicPp.ppterm t)))) + | t, (_,C.Decl ct) -> + let type_t = typeof_aux context t in + if not (R.are_convertible ~subst ~metasenv context type_t ct) then + raise (TypeCheckerFailure + (lazy (Printf.sprintf + ("Not well typed metavariable local context: "^^ + "expected a term of type %s, found %s of type %s") + (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) + ) l lifted_canonical_context + with + Invalid_argument _ -> + raise (AssertFailure (lazy (Printf.sprintf + "Local and canonical context %s have different lengths" + (NCicPp.ppterm term)))) in typeof_aux context term + +and type_of_constant ref = assert false (* - | C.Const (uri,exp_named_subst) -> - incr fdebug ; - let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph - in - let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in - let cty1 = - CicSubstitution.subst_vars exp_named_subst cty - in - decr fdebug ; - cty1,ugraph2 | C.Fix (i,fl) -> let types,kl,ugraph1,len = List.fold_left diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b900d169b..ac9ba639a 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -182,7 +182,6 @@ let convert_term uri t = let ty, fixpoints_ty = aux octx ctx n_fix uri ty in NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[] - | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[] | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[] | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] (* calculate depth in the univ_graph*)