From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- kernel/byterun/coq_fix_code.c | 10 +- kernel/byterun/coq_fix_code.h | 2 +- kernel/byterun/coq_gc.h | 4 +- kernel/byterun/coq_interp.c | 6 +- kernel/byterun/coq_interp.h | 4 + kernel/byterun/coq_memory.c | 7 +- kernel/byterun/coq_memory.h | 10 +- kernel/byterun/coq_values.c | 2 +- kernel/byterun/coq_values.h | 4 +- kernel/environ.ml | 31 +++--- kernel/environ.mli | 10 +- kernel/indtypes.ml | 18 +--- kernel/inductive.ml | 218 ++++++++++++++++++++---------------------- kernel/inductive.mli | 4 +- kernel/mod_typing.ml | 15 +-- kernel/modops.ml | 15 ++- kernel/modops.mli | 8 +- kernel/names.ml | 12 ++- kernel/names.mli | 5 +- kernel/subtyping.ml | 96 ++++++++++++++++++- kernel/typeops.mli | 3 +- kernel/univ.ml | 6 +- kernel/univ.mli | 3 +- kernel/vm.ml | 3 - 24 files changed, 289 insertions(+), 207 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 70648b44..affcccb3 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -10,11 +10,11 @@ #include #include -#include "config.h" -#include "misc.h" -#include "mlvalues.h" -#include "fail.h" -#include "memory.h" +#include +#include +#include +#include +#include #include "coq_instruct.h" #include "coq_fix_code.h" diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 035d5b9b..d1dac80f 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -12,7 +12,7 @@ #ifndef _COQ_FIX_CODE_ #define _COQ_FIX_CODE_ -#include "mlvalues.h" +#include void * coq_stat_alloc (asize_t sz); #ifdef THREADED_CODE diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h index 2f085326..ccccbe78 100644 --- a/kernel/byterun/coq_gc.h +++ b/kernel/byterun/coq_gc.h @@ -10,8 +10,8 @@ #ifndef _COQ_CAML_GC_ #define _COQ_CAML_GC_ -#include "mlvalues.h" -#include "alloc.h" +#include +#include typedef void (*scanning_action) (value, value *); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0f91a7e3..8f9c10e6 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -44,11 +44,7 @@ sp is a local copy of the global variable extern_sp. */ # ifdef DEBUG # define Next goto next_instr # else -# ifdef __ia64__ -# define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++) -# else -# define Next goto *(void *)(coq_jumptbl_base + *pc++) -# endif +# define Next goto *(void *)(coq_jumptbl_base + *pc++) # endif #else # define Instruct(name) case name: diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 76e68944..60865c32 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -19,5 +19,9 @@ value coq_push_vstack(value stk); value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete + (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); + value coq_eval_tcode (value tcode, value e); + diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index bfcb6812..91342108 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -14,6 +14,7 @@ #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" +#include "coq_interp.h" /* stack */ @@ -264,9 +265,3 @@ value coq_set_drawinstr(value unit) return Val_unit; } - -value coq_print_pointer(value p) -{ - printf("pointer = %X\n", p); - return Val_unit; -} diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 0d866dc7..edd05948 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -11,11 +11,11 @@ #ifndef _COQ_MEMORY_ #define _COQ_MEMORY_ -#include "config.h" -#include "fail.h" -#include "misc.h" -#include "memory.h" -#include "mlvalues.h" +#include +#include +#include +#include +#include #define Coq_stack_size (4096 * sizeof(value)) diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 34b885e8..007f61b2 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -13,7 +13,7 @@ #include "coq_instruct.h" #include "coq_memory.h" #include "coq_values.h" -#include "memory.h" +#include /* KIND OF VALUES */ #define Setup_for_gc diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a5176f3f..4c631fce 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -11,8 +11,8 @@ #ifndef _COQ_VALUES_ #define _COQ_VALUES_ -#include "alloc.h" -#include "mlvalues.h" +#include +#include #define Default_tag 0 #define Accu_tag 0 diff --git a/kernel/environ.ml b/kernel/environ.ml index e73f5848..87a6e485 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 9201 2006-10-03 16:47:40Z notin $ *) +(* $Id: environ.ml 9573 2007-01-31 20:18:18Z notin $ *) open Util open Names @@ -241,9 +241,9 @@ let global_vars_set env constr = let rec filtrec acc c = let vl = vars_of_global env c in let acc = List.fold_right Idset.add vl acc in - fold_constr filtrec acc c + fold_constr filtrec acc c in - filtrec Idset.empty constr + filtrec Idset.empty constr (* like [global_vars] but don't get through evars *) let global_vars_set_drop_evar env constr = @@ -339,18 +339,6 @@ type unsafe_type_judgment = { let compile_constant_body = Cbytegen.compile_constant_body -(*s Special functions for the refiner (logic.ml) *) - -let clear_hyps ids check (ctxt,vals) = - let ctxt,vals,rmv = - List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> - if List.mem id ids then (ctxt,vals,id::rmv) - else begin - check rmv d; - (d::ctxt,v::vals,rmv) - end) ctxt vals ([],[],[]) - in ((ctxt,vals),rmv) - exception Hyp_not_found let rec apply_to_hyp (ctxt,vals) id f = @@ -393,3 +381,16 @@ let insert_after_hyp (ctxt,vals) id d check = | [],[] -> raise Hyp_not_found | _, _ -> assert false in aux ctxt vals + +(* To be used in Logic.clear_hyps *) +let remove_hyps ids check (ctxt, vals) = + let ctxt,vals,rmv = + List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> + if List.mem id ids then + (ctxt,vals,id::rmv) + else + let nd = check d in + (nd::ctxt,v::vals,rmv)) + ctxt vals ([],[],[]) + in ((ctxt,vals),rmv) + diff --git a/kernel/environ.mli b/kernel/environ.mli index 3728eea3..478357d7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 9310 2006-10-28 19:35:09Z herbelin $ i*) +(*i $Id: environ.mli 9573 2007-01-31 20:18:18Z notin $ i*) (*i*) open Names @@ -195,11 +195,6 @@ val compile_constant_body : env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code (* opaque *) (* boxed *) -(*s Functions for proofs/logic.ml *) -val clear_hyps : - variable list -> (variable list -> named_declaration -> unit) -> - named_context_val -> named_context_val * variable list - exception Hyp_not_found (* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and @@ -221,3 +216,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable -> val insert_after_hyp : named_context_val -> variable -> named_declaration -> (named_context -> unit) -> named_context_val + +val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> named_context_val -> named_context_val * identifier list + diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1520e009..4fe90ffd 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *) open Util open Names @@ -97,19 +97,7 @@ let mind_check_arities env mie = (* Typing the arities and constructor types *) -let is_info_arity env c = - match dest_arity env c with - | (_,Prop Null) -> false - | (_,Prop Pos) -> true - | (_,Type _) -> true - -let is_info_type env t = - let s = t.utj_type in - if s = mk_Set then true - else if s = mk_Prop then false - else - try is_info_arity env t.utj_val - with UserError _ -> true +let is_logic_type t = (t.utj_type = mk_Prop) (* [infos] is a sequence of pair [islogic,issmall] for each type in the product of a constructor or arity *) @@ -132,7 +120,7 @@ let rec infos_and_sort env t = | Prod (name,c1,c2) -> let (varj,_) = infer_type env c1 in let env1 = Environ.push_rel (name,None,varj.utj_val) env in - let logic = not (is_info_type env varj) in + let logic = is_logic_type varj in let small = Term.is_small varj.utj_type in (logic,small) :: (infos_and_sort env1 c2) | Cast (c,_,_) -> infos_and_sort env c diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b7265e8c..2f17d659 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 9323 2006-10-30 23:05:29Z herbelin $ *) +(* $Id: inductive.ml 9421 2006-12-08 16:00:53Z barras $ *) open Util open Names @@ -519,6 +519,35 @@ let lookup_subterms env ind = (*********************************) +(* Propagation of size information through Cases: if the matched + object is a recursive subterm then compute the information + associated to its own subterms. + Rq: if branch is not eta-long, then the recursive information + is not propagated to the missing abstractions *) +let case_branches_specif renv c_spec ind lbr = + let rec push_branch_args renv lrec c = + match lrec with + ra::lr -> + let c' = whd_betadeltaiota renv.env c in + (match kind_of_term c' with + Lambda(x,a,b) -> + let renv' = push_var renv (x,a,ra) in + push_branch_args renv' lr b + | _ -> (* branch not in eta-long form: cannot perform rec. calls *) + (renv,c')) + | [] -> (renv, c) in + match c_spec with + Subterm (_,t) -> + let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in + assert (Array.length sub_spec = Array.length lbr); + array_map2 (push_branch_args renv) sub_spec lbr + | Dead_code -> + let t = dest_subterms (lookup_subterms renv.env ind) in + let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in + assert (Array.length sub_spec = Array.length lbr); + array_map2 (push_branch_args renv) sub_spec lbr + | Not_subterm -> Array.map (fun c -> (renv,c)) lbr + (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of the fixpoint we are checking. [renv] collects such information @@ -534,7 +563,8 @@ let rec subterm_specif renv t = | Case (ci,_,c,lbr) -> if Array.length lbr = 0 then Dead_code else - let lbr_spec = case_branches_specif renv c ci.ci_ind lbr in + let c_spec = subterm_specif renv c in + let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in let stl = Array.map (fun (renv',br') -> subterm_specif renv' br') lbr_spec in @@ -586,35 +616,6 @@ let rec subterm_specif renv t = (* Other terms are not subterms *) | _ -> Not_subterm -(* Propagation of size information through Cases: if the matched - object is a recursive subterm then compute the information - associated to its own subterms. - Rq: if branch is not eta-long, then the recursive information - is not propagated to the missing abstractions *) -and case_branches_specif renv c ind lbr = - let c_spec = subterm_specif renv c in - let rec push_branch_args renv lrec c = - match lrec with - ra::lr -> - let c' = whd_betadeltaiota renv.env c in - (match kind_of_term c' with - Lambda(x,a,b) -> - let renv' = push_var renv (x,a,ra) in - push_branch_args renv' lr b - | _ -> (* branch not in eta-long form: cannot perform rec. calls *) - (renv,c')) - | [] -> (renv, c) in - match c_spec with - Subterm (_,t) -> - let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in - assert (Array.length sub_spec = Array.length lbr); - array_map2 (push_branch_args renv) sub_spec lbr - | Dead_code -> - let t = dest_subterms (lookup_subterms renv.env ind) in - let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in - assert (Array.length sub_spec = Array.length lbr); - array_map2 (push_branch_args renv) sub_spec lbr - | Not_subterm -> Array.map (fun c -> (renv,c)) lbr (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm renv c = @@ -652,10 +653,10 @@ let check_one_fix renv recpos def = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - (* Rq: why not try and expand some definitions ? *) - let f,l = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in match kind_of_term f with | Rel p -> + List.iter (check_rec_call renv) l; (* Test if [p] is a fixpoint (recursive call) *) if renv.rel_min <= p & p < renv.rel_min+nfi then (* the position of the invoked fixpoint: *) @@ -668,87 +669,80 @@ let check_one_fix renv recpos def = (la,(z::lrest)) -> (* Check the decreasing arg is smaller *) if not (check_is_subterm renv z) then - error_illegal_rec_call renv glob z; - List.iter (check_rec_call renv) (la@lrest) + error_illegal_rec_call renv glob z | _ -> assert false) - (* otherwise check the arguments are guarded: *) - else List.iter (check_rec_call renv) l - - | Case (ci,p,c_0,lrest) -> - List.iter (check_rec_call renv) (c_0::p::l); - (* compute the recarg information for the arguments of - each branch *) - let lbr = case_branches_specif renv c_0 ci.ci_ind lrest in - Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr - - (* Enables to traverse Fixpoint definitions in a more intelligent - way, ie, the rule : - - if - g = Fix g/1 := [y1:T1]...[yp:Tp]e & - - f is guarded with respect to the set of pattern variables S - in a1 ... am & - - f is guarded with respect to the set of pattern variables S - in T1 ... Tp & - - ap is a sub-term of the formal argument of f & - - f is guarded with respect to the set of pattern variables S+{yp} - in e - then f is guarded with respect to S in (g a1 ... am). - - Eduardo 7/9/98 *) - - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> - List.iter (check_rec_call renv) l; - Array.iter (check_rec_call renv) typarray; - let decrArg = recindxs.(i) in - let renv' = push_fix_renv renv recdef in - if (List.length l < (decrArg+1)) then + + | Case (ci,p,c_0,lrest) -> + List.iter (check_rec_call renv) (c_0::p::l); + (* compute the recarg information for the arguments of + each branch *) + let c_spec = subterm_specif renv c_0 in + let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in + Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr + + (* Enables to traverse Fixpoint definitions in a more intelligent + way, ie, the rule : + if - g = Fix g/p := [y1:T1]...[yp:Tp]e & + - f is guarded with respect to the set of pattern variables S + in a1 ... am & + - f is guarded with respect to the set of pattern variables S + in T1 ... Tp & + - ap is a sub-term of the formal argument of f & + - f is guarded with respect to the set of pattern variables + S+{yp} in e + then f is guarded with respect to S in (g a1 ... am). + Eduardo 7/9/98 *) + + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + List.iter (check_rec_call renv) l; + Array.iter (check_rec_call renv) typarray; + let decrArg = recindxs.(i) in + let renv' = push_fix_renv renv recdef in + if (List.length l < (decrArg+1)) then + Array.iter (check_rec_call renv') bodies + else + Array.iteri + (fun j body -> + if i=j then + let theDecrArg = List.nth l decrArg in + let arg_spec = subterm_specif renv theDecrArg in + check_nested_fix_body renv' (decrArg+1) arg_spec body + else check_rec_call renv' body) + bodies + + | Const kn -> + if evaluable_constant kn renv.env then + try List.iter (check_rec_call renv) l + with (FixGuardError _ ) -> + check_rec_call renv(applist(constant_value renv.env kn, l)) + else List.iter (check_rec_call renv) l + + (* The cases below simply check recursively the condition on the + subterms *) + | Cast (a,_, b) -> + List.iter (check_rec_call renv) (a::b::l) + + | Lambda (x,a,b) -> + List.iter (check_rec_call renv) (a::l); + check_rec_call (push_var_renv renv (x,a)) b + + | Prod (x,a,b) -> + List.iter (check_rec_call renv) (a::l); + check_rec_call (push_var_renv renv (x,a)) b + + | CoFix (i,(_,typarray,bodies as recdef)) -> + List.iter (check_rec_call renv) l; + Array.iter (check_rec_call renv) typarray; + let renv' = push_fix_renv renv recdef in Array.iter (check_rec_call renv') bodies - else - Array.iteri - (fun j body -> - if i=j then - let theDecrArg = List.nth l decrArg in - let arg_spec = subterm_specif renv theDecrArg in - check_nested_fix_body renv' (decrArg+1) arg_spec body - else check_rec_call renv' body) - bodies - - | Const kn -> - if evaluable_constant kn renv.env then - try List.iter (check_rec_call renv) l - with (FixGuardError _ ) -> - check_rec_call renv(applist(constant_value renv.env kn, l)) - else List.iter (check_rec_call renv) l - - (* The cases below simply check recursively the condition on the - subterms *) - | Cast (a,_, b) -> - List.iter (check_rec_call renv) (a::b::l) - - | Lambda (x,a,b) -> - check_rec_call (push_var_renv renv (x,a)) b; - List.iter (check_rec_call renv) (a::l) - - | Prod (x,a,b) -> - check_rec_call (push_var_renv renv (x,a)) b; - List.iter (check_rec_call renv) (a::l) - - | CoFix (i,(_,typarray,bodies as recdef)) -> - Array.iter (check_rec_call renv) typarray; - List.iter (check_rec_call renv) l; - let renv' = push_fix_renv renv recdef in - Array.iter (check_rec_call renv') bodies - - | Evar _ -> - List.iter (check_rec_call renv) l - - (* l is not checked because it is considered as the meta's context *) - | Meta _ -> () - - | (Ind _ | Construct _ | Var _ | Sort _) -> - List.iter (check_rec_call renv) l - - | (App _ | LetIn _) -> assert false (* beta zeta reduction *) + + | (Ind _ | Construct _ | Var _ | Sort _) -> + List.iter (check_rec_call renv) l + + (* l is not checked because it is considered as the meta's context *) + | (Evar _ | Meta _) -> () + + | (App _ | LetIn _) -> assert false (* beta zeta reduction *) and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b9d0f984..58343dab 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductive.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) +(*i $Id: inductive.mli 9421 2006-12-08 16:00:53Z barras $ i*) (*i*) open Names @@ -106,5 +106,5 @@ type guard_env = } val subterm_specif : guard_env -> constr -> subterm_spec -val case_branches_specif : guard_env -> constr -> inductive -> +val case_branches_specif : guard_env -> subterm_spec -> inductive -> constr array -> (guard_env * constr) array diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 663434ec..352a1e46 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) +(*i $Id: mod_typing.ml 9558 2007-01-30 14:58:42Z soubiran $ i*) open Util open Names @@ -123,7 +123,7 @@ and merge_with env mtb with_decl = let _ = subst_modtype (map_msid msid (MPself msid)) mtb in () with - Failure _ -> error_circular_with_module id + Circularity _ -> error_circular_with_module id end; let cst = try check_subtypes env' mtb old.msb_modtype @@ -247,10 +247,8 @@ and translate_module env is_definition me = | None -> mtb1, None, Constraint.empty | Some mte -> let mtb2 = translate_modtype env mte in - let cst = - try check_subtypes env mtb1 mtb2 - with Failure _ -> error "not subtype" in - mtb2, Some mtb2, cst + let cst = check_subtypes env mtb1 mtb2 in + mtb2, Some mtb2, cst in { mod_type = mtb; mod_user_type = mod_user_type; @@ -274,10 +272,7 @@ and translate_mexpr env mexpr = match mexpr with let ftb = scrape_modtype env ftb in let farg_id, farg_b, fbody_b = destr_functor ftb in let meb,mtb = translate_mexpr env mexpr in - let cst = - try check_subtypes env mtb farg_b - with Failure _ -> - error "" in + let cst = check_subtypes env mtb farg_b in let mp = try path_of_mexpr mexpr diff --git a/kernel/modops.ml b/kernel/modops.ml index 5cc2a84d..8bab3c9d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 9138 2006-09-14 15:20:45Z jforest $ i*) +(*i $Id: modops.ml 9558 2007-01-30 14:58:42Z soubiran $ i*) (*i*) open Util @@ -20,6 +20,8 @@ open Entries open Mod_subst (*i*) +exception Circularity of string + let error_existing_label l = error ("The label "^string_of_label l^" is already declared") @@ -83,6 +85,13 @@ let error_local_context lo = let error_circular_with_module l = error ("The construction \"with Module "^(string_of_id l)^":=...\" is about to create\na circular module type. Their resolution is not implemented yet.\nIf you really need that feature, please report.") +let error_circularity_in_subtyping l l1 l2 = + error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".") + +let error_no_such_label_sub l l1 l2 = + error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".") + + let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb @@ -134,12 +143,12 @@ let rec subst_modtype sub = function M to M' I must substitute M' for X in "Module N := X". *) | MTBident ln -> MTBident (subst_kn sub ln) | MTBfunsig (arg_id, arg_b, body_b) -> - if occur_mbid arg_id sub then failwith "capture"; + if occur_mbid arg_id sub then raise (Circularity (string_of_mbid arg_id)); MTBfunsig (arg_id, subst_modtype sub arg_b, subst_modtype sub body_b) | MTBsig (sid1, msb) -> - if occur_msid sid1 sub then failwith "capture"; + if occur_msid sid1 sub then raise (Circularity (string_of_msid sid1)); MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = diff --git a/kernel/modops.mli b/kernel/modops.mli index 2aca6511..55f81079 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.mli 8721 2006-04-15 15:30:04Z herbelin $ i*) +(*i $Id: modops.mli 9558 2007-01-30 14:58:42Z soubiran $ i*) (*i*) open Util @@ -20,6 +20,8 @@ open Mod_subst (* Various operations on modules and module types *) +exception Circularity of string + (* recursively unfold MTBdent module types *) val scrape_modtype : env -> module_type_body -> module_type_body @@ -98,5 +100,9 @@ val error_local_context : label option -> 'a val error_circular_with_module : identifier -> 'a +val error_circularity_in_subtyping : string->string->string-> 'a + +val error_no_such_label_sub : label->string->string->'a + val resolver_of_environment : mod_bound_id -> module_type_body -> module_path -> env -> resolver diff --git a/kernel/names.ml b/kernel/names.ml index ae5afebd..383d7879 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 8852 2006-05-23 17:52:43Z notin $ *) +(* $Id: names.ml 9558 2007-01-30 14:58:42Z soubiran $ *) open Pp open Util @@ -73,8 +73,10 @@ let string_of_dirpath = function let u_number = ref 0 type uniq_ident = int * string * dir_path let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) -let string_of_uid (i,s,p) = +let debug_string_of_uid (i,s,p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" +let string_of_uid (i,s,p) = + string_of_dirpath p ^"."^s module Umap = Map.Make(struct type t = uniq_ident @@ -84,12 +86,14 @@ module Umap = Map.Make(struct type mod_self_id = uniq_ident let make_msid = make_uid -let debug_string_of_msid = string_of_uid +let debug_string_of_msid = debug_string_of_uid +let string_of_msid = string_of_uid let id_of_msid (_,s,_) = s type mod_bound_id = uniq_ident let make_mbid = make_uid -let debug_string_of_mbid = string_of_uid +let debug_string_of_mbid = debug_string_of_uid +let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s type label = string diff --git a/kernel/names.mli b/kernel/names.mli index 82a638c0..c9fef60a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: names.mli 8852 2006-05-23 17:52:43Z notin $ i*) +(*i $Id: names.mli 9558 2007-01-30 14:58:42Z soubiran $ i*) (*s Identifiers *) @@ -50,6 +50,7 @@ type mod_self_id val make_msid : dir_path -> string -> mod_self_id val id_of_msid : mod_self_id -> identifier val debug_string_of_msid : mod_self_id -> string +val string_of_msid : mod_self_id -> string (*s Unique names for bound modules *) type mod_bound_id @@ -57,12 +58,14 @@ type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id val id_of_mbid : mod_bound_id -> identifier val debug_string_of_mbid : mod_bound_id -> string +val string_of_mbid : mod_bound_id -> string (*s Names of structure elements *) type label val mk_label : string -> label val string_of_label : label -> string + val label_of_id : identifier -> label val id_of_label : label -> identifier diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 9a8de5a9..d1a10651 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) +(*i $Id: subtyping.ml 9558 2007-01-30 14:58:42Z soubiran $ i*) (*i*) open Util @@ -81,6 +81,41 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = | IndType ((_,0), mib) -> mib | _ -> error () in + let check_inductive_type cst env t1 t2 = + + (* Due to sort-polymorphism in inductive types, the conclusions of + t1 and t2, if in Type, are generated as the least upper bounds + of the types of the constructors. + + By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U + |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each + universe in the conclusion of t1 has an bounding universe in + the conclusion of t2, so that we don't need to check the + subtyping of the conclusions of t1 and t2. + + Even if we'd like to recheck it, the inference of constraints + is not designed to deal with algebraic constraints of the form + max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy + to recheck it (in short, we would need the actual graph of + constraints as input while type checking is currently designed + to output a set of constraints instead) *) + + (* So we cheat and replace the subtyping problem on algebraic + constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) + (that we know are necessary true) by trivial constraints that + the constraint generator knows how to deal with *) + + let (ctx1,s1) = dest_arity env t1 in + let (ctx2,s2) = dest_arity env t2 in + let s1,s2 = + match s1, s2 with + | Type _, Type _ -> (* shortcut here *) mk_Prop, mk_Prop + | (Prop _, Type _) | (Type _,Prop _) -> error () + | _ -> (s1, s2) in + check_conv cst conv_leq env + (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2)) + in + let check_packet cst p1 p2 = let check f = if f p1 <> f p2 then error () in check (fun p -> p.mind_consnames); @@ -96,7 +131,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) + let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in cst in @@ -160,13 +195,60 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let check_constant cst env msid1 l info1 cb2 spec2 = let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in + let check_type cst env t1 t2 = + + (* If the type of a constant is generated, it may mention + non-variable algebraic universes that the general conversion + algorithm is not ready to handle. Anyway, generated types of + constants are functions of the body of the constant. If the + bodies are the same in environments that are subtypes one of + the other, the types are subtypes too (i.e. if Gamma <= Gamma', + Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). + Hence they don't have to be checked again *) + + let t1,t2 = + if Sign.isArity t2 then + let (ctx2,s2) = Sign.destArity t2 in + match s2 with + | Type v when not (is_univ_variable v) -> + (* The type in the interface is inferred and is made of algebraic + universes *) + begin try + let (ctx1,s1) = dest_arity env t1 in + match s1 with + | Type u when not (is_univ_variable u) -> + (* Both types are inferred, no need to recheck them. We + cheat and collapse the types to Prop *) + Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop) + | Prop _ -> + (* The type in the interface is inferred, it may be the case + that the type in the implementation is smaller because + the body is more reduced. We safely collapse the upper + type to Prop *) + Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop) + | Type _ -> + (* The type in the interface is inferred and the type in the + implementation is not inferred or is inferred but from a + more reduced body so that it is just a variable. Since + constraints of the form "univ <= max(...)" are not + expressible in the system of algebraic universes: we fail + (the user has to use an explicit type in the interface *) + error () + with UserError _ (* "not an arity" *) -> + error () end + | _ -> t1,t2 + else + (t1,t2) in + check_conv cst conv_leq env t1 t2 + in + match info1 with | Constant cb1 -> assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; (*Start by checking types*) let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = check_conv cst conv_leq env typ1 typ2 in + let cst = check_type cst env typ1 typ2 in let con = make_con (MPself msid1) empty_dirpath l in let cst = match cb2.const_body with @@ -222,14 +304,18 @@ let rec check_modules cst env msid1 l msb1 msb2 = and check_signatures cst env (msid1,sig1) (msid2,sig2') = let mp1 = MPself msid1 in let env = add_signature mp1 sig1 env in - let sig2 = subst_signature_msid msid2 mp1 sig2' in + let sig2 = try + subst_signature_msid msid2 mp1 sig2' + with + | Circularity l -> + error_circularity_in_subtyping l (string_of_msid msid1) (string_of_msid msid2) in let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = try Labmap.find l map1 with - Not_found -> error_no_such_label l + Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2) in match spec2 with | SPBconst cb2 -> diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 64a2f650..1e73725f 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) +(*i $Id: typeops.mli 9551 2007-01-29 15:13:35Z bgregoir $ i*) (*i*) open Names @@ -106,3 +106,4 @@ val type_of_constant_knowing_parameters : (* Make a type polymorphic if an arity *) val make_polymorphic_if_arity : env -> types -> constant_type + diff --git a/kernel/univ.ml b/kernel/univ.ml index 775e505f..df06e9af 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *) +(* $Id: univ.ml 9507 2007-01-20 08:09:54Z herbelin $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -134,6 +134,10 @@ let is_base_univ = function | Max ([Base],[]) -> warning "Non canonical Set"; true | u -> false +let is_univ_variable = function + | Atom a when a<>Base -> true + | _ -> false + (* When typing [Prop] and [Set], there is no constraint on the level, hence the definition of [prop_univ], the type of [Prop] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index f3af0861..5f562a1d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: univ.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: univ.mli 9507 2007-01-20 08:09:54Z herbelin $ i*) (* Universes. *) @@ -18,6 +18,7 @@ val neutral_univ : universe val make_univ : Names.dir_path * int -> universe val is_base_univ : universe -> bool +val is_univ_variable : universe -> bool (* The type of a universe *) val super : universe -> universe diff --git a/kernel/vm.ml b/kernel/vm.ml index de9bd753..c1d3ca56 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -469,8 +469,6 @@ let check_cofix vcf1 vcf2 = (current_cofix vcf1 = current_cofix vcf2) && (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) -external print_point : Obj.t -> unit = "coq_print_pointer" - let reduce_cofix k vcf = let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in let ndef = Array.length fc_typ in @@ -478,7 +476,6 @@ let reduce_cofix k vcf = Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in (* Construction de l'environnement des corps des cofix *) - let max = k + ndef - 1 in let e = Obj.dup (Obj.repr vcf) in for i = 0 to ndef - 1 do Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) -- cgit v1.2.3