From 0542386e10041791982e7240f281299677b1997b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Apr 2009 22:11:08 +0000 Subject: [PATCH] Refinement of inductive type implemented. Some functions have been exported from the kernel :-( to avoid code duplication. Note: the code seem to be bugged (wrong context), but the operations are taken verbatim from the kernel. Have we really tested it on inductive types? --- .../components/ng_kernel/nCicReduction.ml | 13 +- .../components/ng_kernel/nCicReduction.mli | 5 + .../components/ng_kernel/nCicTypeChecker.ml | 16 +- .../components/ng_kernel/nCicTypeChecker.mli | 5 +- .../components/ng_refiner/nCicRefiner.ml | 191 ++++++++++-------- .../components/ng_refiner/nCicUnification.ml | 6 +- .../components/ng_refiner/nCicUnification.mli | 1 + helm/software/matita/tests/ng_commands.ma | 2 - 8 files changed, 134 insertions(+), 105 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 2b1d4119b..1815ceedf 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -15,6 +15,8 @@ module C = NCic module Ref = NReference module E = NCicEnvironment +exception AssertFailure of string Lazy.t;; + module type Strategy = sig type stack_term type env_term @@ -404,7 +406,14 @@ let _ = NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t); ;; - - +(* if n < 0, then splits all prods from an arity, returning a sort *) +let rec split_prods ~subst context n te = + match (n, R.whd ~subst context te) with + | (0, _) -> context,te + | (n, C.Sort _) when n <= 0 -> context,te + | (n, C.Prod (name,so,ta)) -> + split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta + | (_, _) -> raise (AssertFailure (lazy "split_prods")) +;; (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 691d6605d..1455abd8d 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -11,6 +11,8 @@ (* $Id$ *) +exception AssertFailure of string Lazy.t;; + val whd : ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> @@ -42,3 +44,6 @@ val reduce_machine : val from_stack : stack_item -> machine val unwind : machine -> NCic.term +val split_prods: + subst:NCic.substitution -> NCic.context -> int -> NCic.term -> + NCic.context * NCic.term diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 61cda8a33..f459c6024 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -96,16 +96,6 @@ let fixed_args bos j n nn = (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos ;; -(* if n < 0, then splits all prods from an arity, returning a sort *) -let rec split_prods ~subst context n te = - match (n, R.whd ~subst context te) with - | (0, _) -> context,te - | (n, C.Sort _) when n <= 0 -> context,te - | (n, C.Prod (name,so,ta)) -> - split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta - | (_, _) -> raise (AssertFailure (lazy "split_prods")) -;; - let debruijn uri number_of_types context = let rec aux k t = match t with @@ -722,7 +712,7 @@ and is_non_informative ~metasenv ~subst paramsno c = let s = typeof ~metasenv ~subst context so in s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de | _ -> true in - let context',dx = split_prods ~subst [] paramsno c in + let context',dx = NCicReduction.split_prods ~subst [] paramsno c in aux context' dx and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = @@ -734,13 +724,13 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = ignore (List.fold_right (fun (it_relev,_,ty,cl) i -> - let context,ty_sort = split_prods ~subst [] ~-1 ty in + let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in List.iter (fun (k_relev,_,te) -> let _,k_relev = HExtlib.split_nth leftno k_relev in let te = debruijn uri len [] te in - let context,te = split_prods ~subst tys leftno te in + let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = HExtlib.split_nth (List.length tys) (List.rev context) in let sx_context_te_rev,_ = diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index 24701683e..6ad40b8bb 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -53,5 +53,8 @@ val check_allowed_sort_elimination : NReference.reference -> NCic.context -> NCic.term -> NCic.term -> NCic.term -> unit +(* Functions to be used by the refiner *) val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term - +val are_all_occurrences_positive: + subst:NCic.substitution -> + NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index d73b4fddb..4807e5271 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -536,21 +536,21 @@ let undebruijnate inductive ref t rev_fl = let typeof_obj hdb ?(localise=fun _ -> Stdpp.dummy_loc) - ~look_for_coercion (uri,height,metasenv,subst, obj) + ~look_for_coercion (uri,height,metasenv,subst,obj) = let check_type metasenv subst (ty as orig_ty) = (* XXX fattorizza *) let metasenv, subst, ty, sort = typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None in - let metasenv, subst, ty, _ = + let metasenv, subst, ty, sort = force_to_sort hdb ~look_for_coercion metasenv subst [] ty orig_ty localise sort in - metasenv, subst, ty + metasenv, subst, ty, sort in match obj with | C.Constant (relevance, name, bo, ty , attr) -> - let metasenv, subst, ty = check_type metasenv subst ty in + let metasenv, subst, ty, _ = check_type metasenv subst ty in let metasenv, subst, bo, ty, height = match bo with | Some bo -> @@ -569,7 +569,7 @@ let typeof_obj hdb let types, metasenv, subst, rev_fl = List.fold_left (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) -> - let metasenv, subst, ty = check_type metasenv subst ty in + let metasenv, subst, ty, _ = check_type metasenv subst ty in let dbo = NCicTypeChecker.debruijn uri len [] bo in let localise = relocalise localise dbo bo in (name,C.Decl ty)::types, @@ -601,85 +601,110 @@ let typeof_obj hdb in uri, height, metasenv, subst, C.Fixpoint (inductive, fl, attr) - - | C.Inductive (_ind, _leftno, _itl, _attr) -> assert false -(* - (* let's check if the arity of the inductive types are well formed *) - List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl; - (* let's check if the types of the inductive constructors are well formed. *) - let len = List.length tyl in - let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in - ignore - (List.fold_right - (fun (it_relev,_,ty,cl) i -> - let context,ty_sort = split_prods ~subst [] ~-1 ty in - let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in - List.iter - (fun (k_relev,_,te) -> - let _,k_relev = HExtlib.split_nth leftno k_relev in - let te = debruijn uri len [] te in - let context,te = split_prods ~subst tys leftno te in - let _,chopped_context_rev = - HExtlib.split_nth (List.length tys) (List.rev context) in - let sx_context_te_rev,_ = - HExtlib.split_nth leftno chopped_context_rev in - (try - ignore (List.fold_left2 - (fun context item1 item2 -> - let convertible = - match item1,item2 with - (n1,C.Decl ty1),(n2,C.Decl ty2) -> - n1 = n2 && - R.are_convertible ~metasenv ~subst context ty1 ty2 - | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> - n1 = n2 - && R.are_convertible ~metasenv ~subst context ty1 ty2 - && R.are_convertible ~metasenv ~subst context bo1 bo2 - | _,_ -> false - in - if not convertible then - raise (TypeCheckerFailure (lazy - ("Mismatch between the left parameters of the constructor " ^ - "and those of its inductive type"))) - else - item1::context - ) [] sx_context_ty_rev sx_context_te_rev) - with Invalid_argument "List.fold_left2" -> assert false); - let con_sort = typeof ~subst ~metasenv context te in - (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with - (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (E.universe_leq u1 u2) then - raise - (TypeCheckerFailure - (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^ - " of the constructor is not included in the inductive" ^ - " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2))) - | C.Sort _, C.Sort C.Prop - | C.Sort _, C.Sort C.Type _ -> () - | _, _ -> + | C.Inductive (ind, leftno, itl, attr) -> + let len = List.length itl in + let metasenv,subst,rev_itl,tys = + List.fold_left + (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) -> + let metasenv, subst, ty, _ = check_type metasenv subst ty in + metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx + ) (metasenv,subst,[],[]) itl in + let metasenv,subst,itl,_ = + List.fold_left + (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) -> + let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in + let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in + let metasenv,subst,cl = + List.fold_right + (fun (k_relev,n,te) (metasenv,subst,res) -> + let _,k_relev = HExtlib.split_nth leftno k_relev in + let te = NCicTypeChecker.debruijn uri len [] te in + let context,te = NCicReduction.split_prods ~subst tys leftno te in + let _,chopped_context_rev = + HExtlib.split_nth (List.length tys) (List.rev context) in + let sx_context_te_rev,_ = + HExtlib.split_nth leftno chopped_context_rev in + let metasenv,subst,_ = + try + List.fold_left2 + (fun (metasenv,subst,context) item1 item2 -> + let (metasenv,subst),convertible = + try + match item1,item2 with + (n1,C.Decl ty1),(n2,C.Decl ty2) -> + if n1 = n2 then + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context ty1 ty2,true + else + (metasenv,subst),false + | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> + if n1 = n2 then + let metasenv,subst = + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context ty1 ty2 + in + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context bo1 bo2,true + else + (metasenv,subst),false + | _,_ -> (metasenv,subst),false + with + | NCicUnification.Uncertain _ + | NCicUnification.UnificationFailure _ -> + (metasenv,subst),false + in + let term2 = + match item2 with + _,C.Decl t -> t + | _,C.Def (b,_) -> b in + if not convertible then + raise (RefineFailure (lazy (localise term2, + ("Mismatch between the left parameters of the constructor " ^ + "and those of its inductive type")))) + else + metasenv,subst,item1::context + ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev + with Invalid_argument "List.fold_left2" -> assert false + in + let metasenv, subst, te, con_sort = check_type metasenv subst te in + (match + NCicReduction.whd ~subst context con_sort, + NCicReduction.whd ~subst [] ty_sort + with + (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> + if not (NCicEnvironment.universe_leq u1 u2) then + raise + (RefineFailure + (lazy(localise te, "The type " ^ + NCicPp.ppterm ~metasenv ~subst ~context s1 ^ + " of the constructor is not included in the inductive"^ + " type sort " ^ + NCicPp.ppterm ~metasenv ~subst ~context s2))) + | C.Sort _, C.Sort C.Prop + | C.Sort _, C.Sort C.Type _ -> () + | _, _ -> + raise + (RefineFailure + (lazy (localise te, + "Wrong constructor or inductive arity shape")))); + (* let's check also the positivity conditions *) + if + not + (NCicTypeChecker.are_all_occurrences_positive + ~subst context uri leftno (i+leftno) leftno (len+leftno) te) + then raise - (TypeCheckerFailure - (lazy ("Wrong constructor or inductive arity shape")))); - (* let's check also the positivity conditions *) - if - not - (are_all_occurrences_positive ~subst context uri leftno - (i+leftno) leftno (len+leftno) te) - then - raise - (TypeCheckerFailure - (lazy ("Non positive occurence in "^NUri.string_of_uri - uri))) - else check_relevance ~subst ~metasenv context k_relev te) - cl; - check_relevance ~subst ~metasenv [] it_relev ty; - i+1) - tyl 1) -*) - - + (RefineFailure + (lazy (localise te, + "Non positive occurence in " ^ NUri.string_of_uri uri))) + else + metasenv,subst,(k_relev,n,te)::res + ) cl (metasenv,subst,[]) + in + metasenv,subst,(it_relev,n,ty,cl)::res,i-1 + ) (metasenv,subst,[],List.length rev_itl) rev_itl + in + uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr) ;; - - (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 3000b7311..f178fc4b7 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -612,8 +612,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify hdb = +let unify hdb ?(test_eq_only=false) = indent := ""; - unify hdb false;; - - + unify hdb test_eq_only;; diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 54ccf2143..a2d6c7d78 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -17,6 +17,7 @@ exception AssertFailure of string Lazy.t;; val unify : NCicUnifHint.db -> + ?test_eq_only:bool -> (* default: false *) NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> NCic.metasenv * NCic.substitution diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index 75d3eda6a..03d9df092 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -39,11 +39,9 @@ ntheorem nzero_ok: nzero (S (S O)) = O. napply (refl_eq ? O); nqed. -(* ninductive nnat: Type ≝ nO: nnat | nS: nnat → nnat. -*) (* testare anche i record e le ricorsioni/coricorsioni/(co)induttivi MUTUI *) -- 2.39.2