From: Enrico Tassi Date: Thu, 27 Mar 2008 15:07:09 +0000 (+0000) Subject: more cases of the type checker honoured, still missing Match and Const. X-Git-Tag: make_still_working~5486 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e09650c5b9a0c1711c6bef7c42618d8def14a54;p=helm.git more cases of the type checker honoured, still missing Match and Const. lookup_meta added --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index a6a0a07f6..d28300802 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,4 +1,5 @@ nReference.cmi: nUri.cmi +nCicPp.cmi: nCic.cmo oCic2NCic.cmi: nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicTypeChecker.cmi: nCic.cmo @@ -12,6 +13,8 @@ nUri.cmo: nUri.cmi nUri.cmx: nUri.cmi nReference.cmo: nUri.cmi nReference.cmi nReference.cmx: nUri.cmx nReference.cmi +nCicPp.cmo: nCicPp.cmi +nCicPp.cmx: nCicPp.cmi oCic2NCic.cmo: nUri.cmi nReference.cmi nCic.cmo oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCic.cmx oCic2NCic.cmi nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCic.cmo \ diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 29e1fbe06..f00a5e38a 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -4,6 +4,7 @@ PREDICATES = INTERFACE_FILES = \ nUri.mli \ nReference.mli \ + nCicPp.mli \ oCic2NCic.mli \ nCicEnvironment.mli \ nCicTypeChecker.mli \ diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index b5a4ab583..baa82d033 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -2296,9 +2296,31 @@ let sort_of_prod ~subst context (name,s) (t1, t2) = (NCicPp.ppterm t1) (NCicPp.ppterm t2)))) ;; +let eat_prods ~subst ~metasenv context ty_he args_with_ty = + let rec aux ty_he = function + | [] -> ty_he + | (arg, ty_arg)::tl -> + (match R.whd ~subst context ty_he with + | C.Prod (n,s,t) -> + if R.are_convertible ~subst ~metasenv context ty_arg s then + aux (S.subst ~avoid_beta_redexes:true arg t) tl + else + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + ("Appl: wrong parameter-type, expected %s, found %s") + (NCicPp.ppterm ty_arg) (NCicPp.ppterm s)))) + | _ -> + raise + (TypeCheckerFailure + (lazy "Appl: this is not a function, it cannot be applied"))) + in + aux ty_he args_with_ty +;; + let typeof ~subst ~metasenv context term = - let rec aux context = function + let rec typeof_aux context = function | C.Rel n -> (try match List.nth context (n - 1) with @@ -2309,11 +2331,11 @@ let typeof ~subst ~metasenv context term = | C.Sort s -> C.Sort (C.Type 0) | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Prod (name,s,t) -> - let sort1 = aux context s in - let sort2 = aux ((name,(C.Decl s))::context) t in + 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 = aux context s in + let sort1 = typeof_aux context s in (match R.whd ~subst context sort1 with | C.Meta _ | C.Sort _ -> () | _ -> @@ -2323,11 +2345,11 @@ let typeof ~subst ~metasenv context term = "the source %s should be a type; instead it is a term " ^^ "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort1))))); let type2 = - aux ((n,(C.Decl s))::context) t + typeof_aux ((n,(C.Decl s))::context) t in C.Prod (n,s,type2) | C.LetIn (n,ty,t,bo) -> - let ty_t = aux context t in + let ty_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context ty ty_t) then raise (TypeCheckerFailure @@ -2343,83 +2365,29 @@ let typeof ~subst ~metasenv context term = 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 = aux ((n,C.Def (t,ty))::context) bo in + let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in S.subst ~avoid_beta_redexes:true t ty_bo - in - aux context term -(* - | C.Meta (n,l) -> - (try - let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in - let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in - (* assuming subst is well typed !!!!! *) - ((CicSubstitution.subst_meta l ty), ugraph1) - (* type_of_aux context (CicSubstitution.subst_meta l term) *) - with CicUtil.Subst_not_found _ -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in - ((CicSubstitution.subst_meta l ty),ugraph1)) - | C.Appl (he::tl) when List.length tl > 0 -> - let hetype,ugraph1 = type_of_aux ~logger context he ugraph in - let tlbody_and_type,ugraph2 = - 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*) - ((x,ty)::l,ugraph1)) - tl ([],ugraph1) - in - (* TASSI: questa c'era nel mio... ma non nel CVS... *) - (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) - eat_prods ~subst context hetype tlbody_and_type ugraph2 - | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments")) - | 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.MutInd (uri,i,exp_named_subst) -> - incr fdebug ; - let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph - in - (* TASSI: da me c'era anche questa, ma in CVS no *) - let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in - (* fine parte dubbia *) - let cty = - CicSubstitution.subst_vars exp_named_subst mty - in - decr fdebug ; - cty,ugraph2 - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph - in - (* TASSI: idem come sopra *) - let mty,ugraph2 = - type_of_mutual_inductive_constr ~logger uri i j ugraph1 - in - let cty = - CicSubstitution.subst_vars exp_named_subst mty - in - cty,ugraph2 - | C.MutCase (uri,i,outtype,term,pl) -> - let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in + | C.Appl (he::(_::_ as args)) -> + let ty_he = typeof_aux context he in + 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 (need_dummy, k) = let rec guess_args context t = - let outtype = CicReduction.whd ~subst context t in + let outtype = R.whd ~subst context t in match outtype with C.Sort _ -> (true, 0) | C.Prod (name, s, t) -> @@ -2603,6 +2571,72 @@ end; else CicReduction.head_beta_reduce (C.Appl arguments') 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 + in + typeof_aux context term +(* + | 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/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index 0ff437347..87dc48aa5 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -11,6 +11,9 @@ (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *) +exception Subst_not_found of int +exception Meta_not_found of int + let expand_local_context = function | NCic.Irl len -> let rec aux acc = function @@ -21,12 +24,17 @@ let expand_local_context = function | NCic.Ctx lctx -> lctx ;; -exception Subst_not_found of int - let lookup_subst n subst = try List.assoc n subst with Not_found -> raise (Subst_not_found n) +;; + +let lookup_meta index metasenv = + try + List.find (fun (index', _, _, _) -> index = index') metasenv + with Not_found -> raise (Meta_not_found index) +;; let fold f g acc k = function | NCic.Implicit _ diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index 7a9ce090b..f7bf45918 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -26,10 +26,12 @@ (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *) exception Subst_not_found of int +exception Meta_not_found of int val expand_local_context : NCic.lc_kind -> NCic.term list val lookup_subst: int -> NCic.substitution -> NCic.subst_entry +val lookup_meta: int -> NCic.metasenv -> NCic.conjecture (* both Meta agnostic, map attempts to preserve sharing. * call the 'a->'a function when a binder is crossed *)