diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-29 21:21:52 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-29 21:21:52 +0000 |
commit | e7c20952e90d4f70ae84ab60b6aab62691c18aa0 (patch) | |
tree | def5eed04feeb6d147f0c91a619fe8a519527179 /kernel | |
parent | 6f3b7eb486426ef8104b9b958088315342845795 (diff) |
Inductifs avec polymorphisme de sorte (version initiale)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/inductive.ml | 116 | ||||
-rw-r--r-- | kernel/inductive.mli | 14 | ||||
-rw-r--r-- | kernel/type_errors.ml | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 92 | ||||
-rw-r--r-- | kernel/typeops.mli | 2 | ||||
-rw-r--r-- | kernel/univ.ml | 147 | ||||
-rw-r--r-- | kernel/univ.mli | 16 |
7 files changed, 289 insertions, 100 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3adbd6e36..8d6c3d9ea 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -59,13 +59,10 @@ let ind_subst mind mib = (* Instantiate inductives in constructor type *) let constructor_instantiate mind mib c = let s = ind_subst mind mib in - type_app (substl s) c + substl s c -(* Instantiate the parameters of the inductive type *) -(* TODO: verify the arg of LetIn correspond to the value in the - signature ? *) -let instantiate_params t args sign = - let fail () = +let instantiate_params full t args sign = + let fail () = anomaly "instantiate_params: type, ctxt and args mismatch" in let (rem_args, subs, ty) = Sign.fold_rel_context @@ -73,26 +70,125 @@ let instantiate_params t args sign = match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t) - | _ -> fail()) + | (_,[],_) -> if full then fail() else ([], subs, ty) + | _ -> fail ()) sign ~init:(args,[],t) in if rem_args <> [] then fail(); - type_app (substl subs) ty + substl subs ty + +let instantiate_partial_params = instantiate_params false let full_inductive_instantiate mib params t = - instantiate_params t params mib.mind_params_ctxt + instantiate_params true t params mib.mind_params_ctxt let full_constructor_instantiate (((mind,_),mib,_),params) = let inst_ind = constructor_instantiate mind mib in (fun t -> - instantiate_params (inst_ind t) params mib.mind_params_ctxt) + instantiate_params true (inst_ind t) params mib.mind_params_ctxt) (************************************************************************) (************************************************************************) (* Functions to build standard types related to inductive *) +(* For each inductive type of a block that is of level u_i, we have + the constraints that u_i >= v_i where v_i is the type level of the + types of the constructors of this inductive type. Each v_i depends + of some of the u_i and of an extra (maybe non variable) universe, + say w_i. Typically, for three inductive types, we could have + + u1,u2,u3,w1 <= u1 + u1 w2 <= u2 + u2,u3,w3 <= u3 + + From this system of inequations, we shall deduce + + w1,w2,w3 <= u1 + w1,w2 <= u2 + w1,w2,w3 <= u3 +*) + +let number_of_inductives mib = Array.length mib.mind_packets +let number_of_constructors mip = Array.length mip.mind_consnames + +(* +Computing the actual sort of an applied or partially applied inductive type: + +I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a) +uniformargs : utyps +otherargs : otyps +I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj +s'_k = max(..s_kj..) +merge(..s'_k..) = ..s''_k.. +-------------------------------------------------------------------- +Gamma |- I_i uniformargs otherargs : phi(s''_i) + +where + +- if p=0, phi() = Prop +- if p=1, phi(s) = s +- if p<>1, phi(s) = sup(Set,s) + +Remark: Set (predicative) is encoded as Type(0) +*) + +let find_constraint levels level_bounds i nci = + if nci = 0 then mk_Prop + else + let level_bounds' = solve_constraints_system levels level_bounds in + let level = level_bounds'.(i) in + if nci = 1 & is_empty_universe level then mk_Prop + else if Univ.is_base level then mk_Set else Type level + +let find_inductive_level env (mib,mip) (_,i) levels level_bounds = + find_constraint levels level_bounds i (number_of_constructors mip) + +let set_inductive_level env s t = + let sign,s' = dest_prod_assum env t in + if family_of_sort s <> family_of_sort (destSort s') then + (* This induces reductions if user_arity <> nf_arity *) + mkArity (sign,s) + else + t + +let constructor_instances env (mib,mip) (_,i) args = + let nargs = Array.length args in + let args = Array.to_list args in + let uargs = + if nargs > mib.mind_nparams_rec then + fst (list_chop mib.mind_nparams_rec args) + else args in + let arities = + Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in + (* Compute the minimal type *) + let levels = Array.init + (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in + let arities = list_tabulate (fun i -> + let ctx,s = arities.(i) in + let s = match s with Type _ -> Type (levels.(i)) | s -> s in + (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s))) + (number_of_inductives mib) in + (* Remark: all arities are closed hence no need for lift *) + let env_ar = push_rel_context (List.rev arities) env in + let uargs = List.map (lift (number_of_inductives mib)) uargs in + let lc = + Array.map (fun mip -> + Array.map (fun c -> + instantiate_partial_params c uargs mib.mind_params_ctxt) + mip.mind_nf_lc) + mib.mind_packets in + env_ar, lc, levels + +let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity)) + +let max_inductive_sort v = + let v = Array.map (function + | Type u -> u + | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in + Univ.sup_array v + (* Type of an inductive type *) let type_of_inductive (_,mip) = mip.mind_user_arity diff --git a/kernel/inductive.mli b/kernel/inductive.mli index f419bc3fa..a0ff0cefb 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -69,3 +69,17 @@ val scrape_mind : env -> mutual_inductive -> mutual_inductive (*s Guard conditions for fix and cofix-points. *) val check_fix : env -> fixpoint -> unit val check_cofix : env -> cofixpoint -> unit + +(*s Support for sort-polymorphic inductive types *) + +val constructor_instances : env -> mind_specif -> inductive -> + constr array -> env * types array array * universe array + +val set_inductive_level : env -> sorts -> types -> types + +val find_inductive_level : env -> mind_specif -> inductive -> + universe array -> universe array -> sorts + +val is_small_inductive : mind_specif -> bool + +val max_inductive_sort : sorts array -> universe diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 9e8d58fa8..7049a8afe 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -103,7 +103,7 @@ let error_cant_apply_not_functional env rator randl = raise (TypeError (env, CantApplyNonFunctional (rator,randl))) let error_cant_apply_bad_type env t rator randl = - raise(TypeError (env, CantApplyBadType (t,rator,randl))) + raise (TypeError (env, CantApplyBadType (t,rator,randl))) let error_ill_formed_rec_body env why lna i = raise (TypeError (env, IllFormedRecBody (why,lna,i))) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 89a1c1982..29ec5007a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -36,7 +36,7 @@ let conv_leq_vecti env v1 v2 = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env j = - match kind_of_term(whd_betadeltaiota env (body_of_type j.uj_type)) with + match kind_of_term(whd_betadeltaiota env j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -47,11 +47,9 @@ let assumption_of_judgment env j = with TypeError _ -> error_assumption env j -(* -let aojkey = Profile.declare_profile "assumption_of_judgment";; -let assumption_of_judgment env j - = Profile.profile2 aojkey assumption_of_judgment env j;; -*) +let sort_judgment env j = (type_judgment env j).utj_type + +let on_judgment_type f j = { j with uj_type = f j.uj_type } (************************************************) (* Incremental typing rules: builds a typing judgement given the *) @@ -62,11 +60,11 @@ let assumption_of_judgment env j (* Prop and Set *) let judge_of_prop = - { uj_val = body_of_type mkProp; + { uj_val = mkProp; uj_type = mkSort type_0 } let judge_of_set = - { uj_val = body_of_type mkSet; + { uj_val = mkSet; uj_type = mkSort type_0 } let judge_of_prop_contents = function @@ -77,7 +75,7 @@ let judge_of_prop_contents = function let judge_of_type u = let uu = super u in - { uj_val = body_of_type (mkType u); + { uj_val = mkType u; uj_type = mkType uu } (*s Type of a de Bruijn index. *) @@ -90,12 +88,6 @@ let judge_of_relative env n = with Not_found -> error_unbound_rel env n -(* -let relativekey = Profile.declare_profile "judge_of_relative";; -let judge_of_relative env n = - Profile.profile2 relativekey judge_of_relative env n;; -*) - (* Type of variables *) let judge_of_variable env id = try @@ -143,12 +135,6 @@ let judge_of_constant env cst = check_args env constr ce.const_hyps in make_judge constr (constant_type env cst) -(* -let tockey = Profile.declare_profile "type_of_constant";; -let type_of_constant env c - = Profile.profile3 tockey type_of_constant env c;; -*) - (* Type of a lambda-abstraction. *) (* [judge_of_abstraction env name var j] implements the rule @@ -214,9 +200,11 @@ let sort_of_product env domsort rangsort = rangsort else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - domsort + Type (sup u1 base_univ) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop _, Type _) -> rangsort + | (Prop Pos, Type u2) -> Type (sup base_univ u2) + (* Product rule (Prop,Type_i,Type_i) *) + | (Prop Null, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (sup u1 u2) @@ -266,12 +254,6 @@ let judge_of_inductive env i = let specif = lookup_mind_specif env i in make_judge constr (type_of_inductive specif) -(* -let toikey = Profile.declare_profile "judge_of_inductive";; -let judge_of_inductive env i - = Profile.profile2 toikey judge_of_inductive env i;; -*) - (* Constructors. *) let judge_of_constructor env c = @@ -283,12 +265,6 @@ let judge_of_constructor env c = let specif = lookup_mind_specif env (inductive_of_constructor c) in make_judge constr (type_of_constructor c specif) -(* -let tockey = Profile.declare_profile "judge_of_constructor";; -let judge_of_constructor env cstr - = Profile.profile2 tockey judge_of_constructor env cstr;; -*) - (* Case. *) let check_branch_types env cj (lfj,explft) = @@ -312,12 +288,6 @@ let judge_of_case env ci pj cj lfj = uj_type = rslty }, Constraint.union univ univ') -(* -let tocasekey = Profile.declare_profile "judge_of_case";; -let judge_of_case env ci pj cj lfj - = Profile.profile6 tocasekey judge_of_case env ci pj cj lfj;; -*) - (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) @@ -366,8 +336,12 @@ let rec execute env cstr cu = | App (f,args) -> let (j,cu1) = execute env f cu in let (jl,cu2) = execute_array env args cu1 in - univ_combinator cu2 - (judge_of_apply env j jl) + let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in + if isInd f then + (* Sort-polymorphism of inductive types *) + adjust_inductive_level env (destInd f) args (j',cu) + else + (j',cu) | Lambda (name,c1,c2) -> let (varj,cu1) = execute_type env c1 cu in @@ -395,6 +369,7 @@ let rec execute env cstr cu = let (tj,cu2) = execute_type env t cu1 in univ_combinator cu2 (judge_of_cast env cj k tj) + (* Inductive types *) | Ind ind -> (judge_of_inductive env ind, cu) @@ -442,18 +417,25 @@ and execute_recdef env (names,lar,vdef) i cu = univ_combinator cu2 ((lara.(i),(names,lara,vdefv)),cst) -and execute_array env v cu = - let (jl,cu1) = execute_list env (Array.to_list v) cu in - (Array.of_list jl, cu1) - -and execute_list env l cu = - match l with - | [] -> - ([], cu) - | c::r -> - let (j,cu1) = execute env c cu in - let (jr,cu2) = execute_list env r cu1 in - (j::jr, cu2) +and execute_array env = array_fold_map' (execute env) + +and execute_list env = list_fold_map' (execute env) + +and adjust_inductive_level env ind args (j,cu) = + let specif = lookup_mind_specif env ind in + if is_small_inductive specif then + (* No polymorphism *) + (j,cu) + else + (* Retyping constructor with the actual arguments *) + let env',llc,ls0 = constructor_instances env specif ind args in + let (llj,cu1) = array_fold_map' (execute_array env') llc cu in + let ls = + Array.map (fun lj -> + max_inductive_sort (Array.map (sort_judgment env) lj)) llj + in + let s = find_inductive_level env specif ind ls0 ls in + (on_judgment_type (set_inductive_level env s) j, cu1) (* Derived functions *) let infer env constr = diff --git a/kernel/typeops.mli b/kernel/typeops.mli index ed90c393e..412998f6e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -33,6 +33,8 @@ val infer_local_decls : val assumption_of_judgment : env -> unsafe_judgment -> types val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment +val on_judgment_type : + (types -> types) -> unsafe_judgment -> unsafe_judgment (*s Type of sorts. *) val judge_of_prop_contents : contents -> unsafe_judgment diff --git a/kernel/univ.ml b/kernel/univ.ml index 5f2f845aa..1e0991e3d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -36,11 +36,11 @@ open Util *) type universe_level = - { u_mod : Names.dir_path; - u_num : int } + | Base + | Level of Names.dir_path * int type universe = - | Variable of universe_level + | Atom of universe_level | Max of universe_level list * universe_level list module UniverseOrdered = struct @@ -48,30 +48,31 @@ module UniverseOrdered = struct let compare = Pervasives.compare end -let string_of_univ_level u = - Names.string_of_dirpath u.u_mod^"."^string_of_int u.u_num +let string_of_univ_level = function + | Base -> "0" + | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n -let make_univ (m,n) = Variable { u_mod=m; u_num=n } +let make_univ (m,n) = Atom (Level (m,n)) let pr_uni_level u = str (string_of_univ_level u) let pr_uni = function - | Variable u -> + | Atom u -> pr_uni_level u - | Max ([],[]) -> + | Max ([],[Base]) -> int 1 | Max (gel,gtl) -> - str "max(" ++ - prlist_with_sep pr_coma pr_uni_level gel ++ - (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++ - prlist_with_sep pr_coma - (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++ + str "max(" ++ hov 0 + (prlist_with_sep pr_coma pr_uni_level gel ++ + (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++ + prlist_with_sep pr_coma + (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++ str ")" (* Returns the formal universe that lies juste above the universe variable u. Used to type the sort u. *) let super = function - | Variable u -> + | Atom u -> Max ([],[u]) | Max _ -> anomaly ("Cannot take the successor of a non variable universes:\n"^ @@ -79,13 +80,19 @@ let super = function (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) -let sup u v = +let sup u v = match u,v with - | Variable u, Variable v -> Max ((if u = v then [u] else [u;v]),[]) - | Variable u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) - | Max (gel,gtl), Variable v -> Max (list_add_set v gel,gtl) + | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[]) + | u, Max ([],[]) -> u + | Max ([],[]), v -> v + | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) + | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl) | Max (gel,gtl), Max (gel',gtl') -> - Max (list_union gel gel',list_union gtl gtl') + let gel'' = list_union gel gel' in + let gtl'' = list_union gtl gtl' in + Max (list_subtract gel'' gtl'',gtl'') + +let sup_array ls = Array.fold_right sup ls (Max ([],[])) (* Comparison on this type is pointer equality *) type canonical_arc = @@ -115,11 +122,19 @@ let declare_univ u g = else g -(* When typing Prop and Set, there is no constraint on the level, - hence the definition of prop_univ *) +(* The level of Set *) +let base_univ = Atom Base + +let is_base = function + | Atom Base -> true + | Max ([Base],[]) -> warning "Non canonical Set"; true + | u -> false + +(* When typing [Prop] and [Set], there is no constraint on the level, + hence the definition of [prop_univ], the type of [Prop] *) let initial_universes = UniverseMap.empty -let prop_univ = Max ([],[]) +let prop_univ = Max ([],[Base]) (* Every universe_level has a unique canonical arc representative *) @@ -377,23 +392,84 @@ type constraints = Constraint.t type constraint_function = universe -> universe -> constraints -> constraints +let constraint_add_leq v u c = + if v = Base then c else Constraint.add (v,Leq,u) c + let enforce_geq u v c = - match u with - | Variable u -> (match v with - | Variable v -> Constraint.add (v,Leq,u) c - | Max (l1, l2) -> - let d = List.fold_right (fun v -> Constraint.add (v,Leq,u)) l1 c in - List.fold_right (fun v -> Constraint.add (v,Lt,u)) l2 d) - | Max _ -> anomaly "A universe bound can only be a variable" + match u, v with + | Atom u, Atom v -> constraint_add_leq v u c + | Atom u, Max (gel,gtl) -> + let d = List.fold_right (fun v -> constraint_add_leq v u) gel c in + List.fold_right (fun v -> Constraint.add (v,Lt,u)) gtl d + | _ -> anomaly "A universe bound can only be a variable" let enforce_eq u v c = match (u,v) with - | Variable u, Variable v -> Constraint.add (u,Eq,v) c + | Atom u, Atom v -> Constraint.add (u,Eq,v) c | _ -> anomaly "A universe comparison can only happen between variables" let merge_constraints c g = Constraint.fold enforce_constraint c g +(**********************************************************************) +(* Tools for sort-polymorphic inductive types *) + +(* Temporary inductive type levels *) + +let fresh_level = + let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n) + +let fresh_local_univ () = Atom (fresh_level ()) + +(* Miscellaneous functions to remove or test local univ assumed to + occur only in the le constraints *) + +let make_max = function + | ([u],[]) -> Atom u + | (le,lt) -> Max (le,lt) + +let remove_constraint u = function + | Atom u' as x -> if u = u' then Max ([],[]) else x + | Max (le,lt) -> make_max (list_remove u le,lt) + +let is_empty_universe = function + | Max ([],[]) -> true + | _ -> false + +let is_direct_constraint u = function + | Atom u' -> u = u' + | Max (le,lt) -> List.mem u le + +(* + Solve a system of universe constraint of the form + + u_s11, ..., u_s1p1, w1 <= u1 + ... + u_sn1, ..., u_snpn, wn <= un + +where + + - the ui (1 <= i <= n) are universe variables, + - the sjk select subsets of the ui for each equations, + - the wi are arbitrary complex universes that do not mention the ui. +*) + +let solve_constraints_system levels level_bounds = + let levels = + Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in + let v = Array.copy level_bounds in + let nind = Array.length v in + for i=0 to nind-1 do + for j=0 to nind-1 do + if i<>j & is_direct_constraint levels.(j) v.(i) then + v.(i) <- sup v.(i) v.(j) + done; + for j=0 to nind-1 do + v.(i) <- remove_constraint levels.(j) v.(i) + done + done; + v + (* Pretty-printing *) let num_universes g = @@ -446,19 +522,23 @@ let dump_universes output g = in UniverseMap.iter dump_arc g +(* Hash-consing *) + module Huniv = Hashcons.Make( struct type t = universe type u = Names.dir_path -> Names.dir_path - let hash_aux hdir u = { u with u_mod=hdir u.u_mod } + let hash_aux hdir = function + | Base -> Base + | Level (d,n) -> Level (hdir d,n) let hash_sub hdir = function - | Variable u -> Variable (hash_aux hdir u) + | Atom u -> Atom (hash_aux hdir u) | Max (gel,gtl) -> Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl) let equal u v = match u, v with - | Variable u, Variable v -> u == v + | Atom u, Atom v -> u == v | Max (gel,gtl), Max (gel',gtl') -> (list_for_all2eq (==) gel gel') && (list_for_all2eq (==) gtl gtl') @@ -469,4 +549,3 @@ module Huniv = let hcons1_univ u = let _,_,hdir,_,_,_ = Names.hcons_names() in Hashcons.simple_hcons Huniv.f hdir u - diff --git a/kernel/univ.mli b/kernel/univ.mli index 56442cbcc..0fb1a4ca8 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -12,14 +12,21 @@ type universe +val base_univ : universe val prop_univ : universe val make_univ : Names.dir_path * int -> universe +val is_base : universe -> bool + (* The type of a universe *) val super : universe -> universe + (* The max of 2 universes *) val sup : universe -> universe -> universe +(* The max of an array of universes *) +val sup_array : universe array -> universe + (*s Graphs of universes. *) type universes @@ -47,6 +54,15 @@ exception UniverseInconsistency val merge_constraints : constraints -> universes -> universes +(*s Support for sort-polymorphic inductive types *) + +val fresh_local_univ : unit -> universe + +val solve_constraints_system : universe array -> universe array -> + universe array + +val is_empty_universe : universe -> bool + (*s Pretty-printing of universes. *) val pr_uni : universe -> Pp.std_ppcmds |