From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- kernel/cemitcodes.ml | 24 ++++++- kernel/mod_subst.ml | 179 ++++++++++++++++++++++++++++++++++----------------- kernel/mod_typing.ml | 10 ++- kernel/modops.ml | 24 +++---- kernel/modops.mli | 5 +- kernel/names.ml | 4 +- kernel/subtyping.ml | 139 ++++++++++++++++++++++++++++----------- 7 files changed, 268 insertions(+), 117 deletions(-) (limited to 'kernel') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 71a9aa0e..4e09a0ed 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -23,7 +23,7 @@ let patch_int buff pos n = let out_buffer = ref(String.create 1024) and out_position = ref 0 - +(* let out_word b1 b2 b3 b4 = let p = !out_position in if p >= String.length !out_buffer then begin @@ -37,6 +37,28 @@ let out_word b1 b2 b3 b4 = String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); out_position := p + 4 +*) +let out_word b1 b2 b3 b4 = + let p = !out_position in + if p >= String.length !out_buffer then begin + let len = String.length !out_buffer in + let new_len = + if len <= Sys.max_string_length / 2 + then 2 * len + else + if len = Sys.max_string_length + then raise (Invalid_argument "String.create") (* Pas la bonne execption +.... *) + else Sys.max_string_length in + let new_buffer = String.create new_len in + String.blit !out_buffer 0 new_buffer 0 len; + out_buffer := new_buffer + end; + String.unsafe_set !out_buffer p (Char.unsafe_chr b1); + String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); + String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); + String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); + out_position := p + 4 let out opcode = out_word opcode 0 0 0 diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 6d2064bf..2942e101 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 7538 2005-11-08 17:14:52Z herbelin $ *) +(* $Id: mod_subst.ml 9874 2007-06-04 13:46:11Z soubiran $ *) open Pp open Util @@ -25,7 +25,7 @@ let apply_opt_resolver resolve kn = match resolve with None -> None | Some resolve -> - try List.assoc kn resolve with Not_found -> assert false + try List.assoc kn resolve with Not_found -> None type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id @@ -110,6 +110,16 @@ let subst_con sub con = None -> con',mkConst con' | Some t -> con',t +let subst_con0 sub con = + let mp,dir,l = repr_con con in + match subst_mp0 sub mp with + None -> None + | Some (mp',resolve) -> + let con' = make_con mp' dir l in + match apply_opt_resolver resolve con with + None -> Some (mkConst con') + | Some t -> Some t + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -119,16 +129,14 @@ let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn)) -(* -This should be rewritten to prevent duplication of constr's when not -necessary. -For now, it uses map_constr and is rather ineffective -*) let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with - | Const kn -> f' kn + | Const kn -> + (match f' kn with + None -> c + | Some const ->const) | Ind (kn,i) -> (match f kn with None -> c @@ -138,18 +146,64 @@ let rec map_kn f f' c = (match f kn with None -> c | Some kn' -> - mkConstruct ((kn',i),j)) - | Case (ci,p,c,l) -> - let ci' = - { ci with - ci_ind = - let (kn,i) = ci.ci_ind in - match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in - mkCase (ci', func p, func c, array_smartmap func l) - | _ -> map_constr func c + mkConstruct ((kn',i),j)) + | Case (ci,p,ct,l) -> + let ci_ind = + let (kn,i) = ci.ci_ind in + (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in + let p' = func p in + let ct' = func ct in + let l' = array_smartmap func l in + if (ci.ci_ind==ci_ind && p'==p + && l'==l && ct'==ct)then c + else + mkCase ({ci with ci_ind = ci_ind}, + p',ct', l') + | Cast (ct,k,t) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkCast (ct', k, t') + | Prod (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkProd (na, t', ct') + | Lambda (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkLambda (na, t', ct') + | LetIn (na,b,t,ct) -> + let ct' = func ct in + let t'= func t in + let b'= func b in + if (t'==t && ct'==ct && b==b') then c + else mkLetIn (na, b', t', ct') + | App (ct,l) -> + let ct' = func ct in + let l' = array_smartmap func l in + if (ct'== ct && l'==l) then c + else mkApp (ct',l') + | Evar (e,l) -> + let l' = array_smartmap func l in + if (l'==l) then c + else mkEvar (e,l') + | Fix (ln,(lna,tl,bl)) -> + let tl' = array_smartmap func tl in + let bl' = array_smartmap func bl in + if (bl == bl'&& tl == tl') then c + else mkFix (ln,(lna,tl',bl')) + | CoFix(ln,(lna,tl,bl)) -> + let tl' = array_smartmap func tl in + let bl' = array_smartmap func bl in + if (bl == bl'&& tl == tl') then c + else mkCoFix (ln,(lna,tl',bl')) + | _ -> c + let subst_mps sub = - map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con)) + map_kn (subst_kn0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with @@ -172,50 +226,57 @@ exception ChangeDomain of resolver let join (subst1 : substitution) (subst2 : substitution) = let apply_subst (sub : substitution) key (mp,resolve) = let mp',resolve' = - match subst_mp0 sub mp with - None -> mp, None - | Some (mp',resolve') -> mp',resolve' in + match subst_mp0 sub mp with + None -> mp, None + | Some (mp',resolve') -> mp',resolve' in let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - Some - ((List.map - (fun (kn,topt) -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid in - (* let's replace mp with key in kn *) - let kn' = replace_mp_in_con mp key' kn in - kn',topt)) res) + try + let res = + match resolve with + Some res -> res + | None -> + match resolve' with + None -> raise BothSubstitutionsAreIdentitySubstitutions + | Some res -> raise (ChangeDomain res) + in + Some + (List.map + (fun (kn,topt) -> + kn, + match topt with + None -> + (match key with + MSI msid -> + let kn' = replace_mp_in_con (MPself msid) mp kn in + apply_opt_resolver resolve' kn' + | MBI mbid -> + let kn' = replace_mp_in_con (MPbound mbid) mp kn in + apply_opt_resolver resolve' kn') + | Some t -> Some (subst_mps sub t)) res) + with + BothSubstitutionsAreIdentitySubstitutions -> None + | ChangeDomain res -> + let rec changeDom = function + | [] -> [] + | (kn,topt)::r -> + let key' = + match key with + MSI msid -> MPself msid + | MBI mbid -> MPbound mbid in + let kn' = replace_mp_in_con mp key' kn in + if kn==kn' then + (*the key does not appear in mp, we remove it + from the resolver that we are building*) + changeDom r + else + (kn',topt)::(changeDom r) + in + Some (changeDom res) in - mp',resolve'' in + mp',resolve'' in let subst = Umap.mapi (apply_subst subst2) subst1 in - Umap.fold Umap.add subst2 subst + Umap.fold Umap.add subst2 subst + let rec occur_in_path uid path = match uid,path with diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 352a1e46..70de3034 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 9558 2007-01-30 14:58:42Z soubiran $ i*) +(*i $Id: mod_typing.ml 9980 2007-07-12 13:32:37Z soubiran $ i*) open Util open Names @@ -131,8 +131,12 @@ and merge_with env mtb with_decl = let equiv = match old.msb_equiv with | None -> Some mp - | Some mp' -> - check_modpath_equiv env' mp mp'; + | Some mp' -> + begin + try + check_modpath_equiv env' mp mp' + with Not_equiv_path -> error_not_equal mp mp + end; Some mp in let msb = diff --git a/kernel/modops.ml b/kernel/modops.ml index 8bab3c9d..fb00cfcd 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 9558 2007-01-30 14:58:42Z soubiran $ i*) +(*i $Id: modops.ml 9980 2007-07-12 13:32:37Z soubiran $ i*) (*i*) open Util @@ -33,10 +33,11 @@ let error_not_a_functor _ = error "Application of not a functor" let error_incompatible_modtypes _ _ = error "Incompatible module types" -let error_not_equal _ _ = error "Not equal modules" - -let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match") +let error_not_equal p1 p2 = error ((string_of_mp p1)^" and "^(string_of_mp p2)^" are not equal modules") +let error_not_match l l1 l2 = error (l1^" is not a subtype of "^l2^": "^ + "Signature components for label "^(string_of_label l)^" do not match.") + let error_no_such_label l = error ("No such label "^string_of_label l) let error_incompatible_labels l l' = @@ -89,7 +90,7 @@ 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^".") + error (l1^" is not a subtype of "^l2^":"^"The field "^(string_of_label l)^" is missing in "^l1^".") let rec scrape_modtype env = function @@ -124,6 +125,7 @@ let destr_functor = function | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) | mtb -> error_not_a_functor mtb +exception Not_equiv_path let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else @@ -132,7 +134,7 @@ let rec check_modpath_equiv env mp1 mp2 = | None -> let mb2 = lookup_module mp2 env in (match mb2.mod_equiv with - | None -> error_not_equal mp1 mp2 + | None -> raise Not_equiv_path | Some mp2' -> check_modpath_equiv env mp2' mp1) | Some mp1' -> check_modpath_equiv env mp2 mp1' @@ -244,16 +246,16 @@ and constants_of_modtype env mp modtype = | MTBfunsig _ -> [] (* returns a resolver for kn that maps mbid to mp *) -(* Nota: Some delta-expansions used to happen here. - Browse SVN if you want to know more. *) +(* Desactivated until v8.2, waiting for the integration +of "Parameter Inline". *) let resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = List.map (fun (con,_) -> con,None) constants in - Mod_subst.make_resolver resolve + let _ = List.map (fun (con,_) -> con,None) constants in + Mod_subst.make_resolver [] let strengthen_const env mp l cb = - match cb.const_opaque, cb.const_body with + match cb.const_opaque, cb.const_body with | false, Some _ -> cb | true, Some _ | _, None -> diff --git a/kernel/modops.mli b/kernel/modops.mli index 55f81079..61761bb7 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 9558 2007-01-30 14:58:42Z soubiran $ i*) +(*i $Id: modops.mli 9980 2007-07-12 13:32:37Z soubiran $ i*) (*i*) open Util @@ -21,6 +21,7 @@ open Mod_subst (* Various operations on modules and module types *) exception Circularity of string +exception Not_equiv_path (* recursively unfold MTBdent module types *) val scrape_modtype : env -> module_type_body -> module_type_body @@ -70,7 +71,7 @@ val error_incompatible_modtypes : val error_not_equal : module_path -> module_path -> 'a -val error_not_match : label -> specification_body -> 'a +val error_not_match : label -> string -> string -> 'a val error_incompatible_labels : label -> label -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index 383d7879..4273fe14 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 9558 2007-01-30 14:58:42Z soubiran $ *) +(* $Id: names.ml 9980 2007-07-12 13:32:37Z soubiran $ *) open Pp open Util @@ -65,7 +65,7 @@ let repr_dirpath x = x let empty_dirpath = [] let string_of_dirpath = function - | [] -> "" + | [] -> "" | sl -> String.concat "." (List.map string_of_id (List.rev sl)) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d1a10651..2e6e5a34 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 9558 2007-01-30 14:58:42Z soubiran $ i*) +(*i $Id: subtyping.ml 10031 2007-07-19 18:05:46Z soubiran $ i*) (*i*) open Util @@ -72,9 +72,11 @@ let check_conv_error error cst f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive cst env msid1 l info1 mib2 spec2 = +let check_inductive cst env msid1 l info1 mib2 spec2 path1 path2 = let kn = make_kn (MPself msid1) empty_dirpath l in - let error () = error_not_match l spec2 in + let error () = error_not_match l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) in let check_conv cst f = check_conv_error error cst f in let mib1 = match info1 with @@ -192,8 +194,10 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = in cst -let check_constant cst env msid1 l info1 cb2 spec2 = - let error () = error_not_match l spec2 in +let check_constant cst env msid1 l info1 cb2 spec2 msid2 path1 path2 = + let error () = error_not_match l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -251,17 +255,53 @@ let check_constant cst env msid1 l info1 cb2 spec2 = 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 - | None -> cst - | Some lc2 -> - let c2 = Declarations.force lc2 in - let c1 = match cb1.const_body with - | Some lc1 -> Declarations.force lc1 - | None -> mkConst con - in - check_conv cst conv env c1 c2 + match cb2.const_body with + | None -> cst + | Some lc2 -> + let c2 = Declarations.force lc2 in + let c1 = match cb1.const_body with + | Some lc1 -> Declarations.force lc1 + | None -> mkConst con + in + begin + match cb1.const_opaque,cb2.const_opaque with + false,false |true,true -> + check_conv cst conv env c1 c2 + | false,true -> + begin + match kind_of_term c1 with + | Const con' -> + let c1 = + match (Pre_env.lookup_constant con' + (pre_env env)).const_body with + Some c -> Declarations.force c + | None -> mkConst con' + in + check_conv cst conv env c1 c2 + | _ -> + check_conv cst conv env c1 c2 + end + | true,false-> + begin + match (kind_of_term c2) with + | Const con'-> + if con' = con + then cst + else + let c2 = + match (Pre_env.lookup_constant con' + (pre_env env)).const_body with + Some c -> Declarations.force c + | None -> mkConst con' + in + check_conv cst conv env c1 c2 + | _ -> + check_conv cst conv env c1 c2 + end + end + in - cst + cst | IndType ((kn,i),mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -286,60 +326,77 @@ let check_constant cst env msid1 l info1 cb2 spec2 = check_conv cst conv env ty1 ty2 | _ -> error () -let rec check_modules cst env msid1 l msb1 msb2 = +let rec check_modules cst env msid1 l msb1 msb2 path1 path2 = let mp = (MPdot(MPself msid1,l)) in let mty1 = strengthen env msb1.msb_modtype mp in - let cst = check_modtypes cst env mty1 msb2.msb_modtype false in - begin - match msb1.msb_equiv, msb2.msb_equiv with - | _, None -> () - | None, Some mp2 -> - check_modpath_equiv env mp mp2 - | Some mp1, Some mp2 -> - check_modpath_equiv env mp1 mp2 - end; - cst + let cst = check_modtypes cst env mty1 msb2.msb_modtype false + path1 path2 in + begin + match msb1.msb_equiv, msb2.msb_equiv with + | _, None -> () + | None, Some mp2 -> + begin + try + check_modpath_equiv env mp mp2 + with Not_equiv_path -> error_not_equal mp mp2 + end + | Some mp1, Some mp2 -> try + check_modpath_equiv env mp1 mp2 + with Not_equiv_path -> error_not_equal mp1 mp2 + end; + cst -and check_signatures cst env (msid1,sig1) (msid2,sig2') = +and check_signatures cst env (msid1,sig1) (msid2,sig2') path1 path2= let mp1 = MPself msid1 in let env = add_signature mp1 sig1 env 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 + error_circularity_in_subtyping l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) + 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_sub l (string_of_msid msid1) (string_of_msid msid2) + Not_found -> error_no_such_label_sub l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) in match spec2 with | SPBconst cb2 -> - check_constant cst env msid1 l info1 cb2 spec2 + check_constant cst env msid1 l info1 cb2 spec2 msid2 path1 path2 | SPBmind mib2 -> - check_inductive cst env msid1 l info1 mib2 spec2 + check_inductive cst env msid1 l info1 mib2 spec2 path1 path2 | SPBmodule msb2 -> let msb1 = match info1 with | Module msb -> msb - | _ -> error_not_match l spec2 + | _ -> error_not_match l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) + in - check_modules cst env msid1 l msb1 msb2 + check_modules cst env msid1 l msb1 msb2 path1 path2 | SPBmodtype mtb2 -> let mtb1 = match info1 with | Modtype mtb -> mtb - | _ -> error_not_match l spec2 + | _ -> error_not_match l + (String.concat "." (List.map string_of_id (List.rev path1))) + (String.concat "." (List.map string_of_id (List.rev path2))) + in - check_modtypes cst env mtb1 mtb2 true + check_modtypes cst env mtb1 mtb2 true path1 path2 in List.fold_left check_one_body cst sig2 -and check_modtypes cst env mtb1 mtb2 equiv = +and check_modtypes cst env mtb1 mtb2 equiv path1 path2 = if mtb1==mtb2 then cst else (* just in case :) *) let mtb1' = scrape_modtype env mtb1 in let mtb2' = scrape_modtype env mtb2 in @@ -347,14 +404,17 @@ and check_modtypes cst env mtb1 mtb2 equiv = match mtb1', mtb2' with | MTBsig (msid1,list1), MTBsig (msid2,list2) -> - let cst = check_signatures cst env (msid1,list1) (msid2,list2) in + let cst = check_signatures cst env (msid1,list1) (msid2,list2) + ((id_of_msid msid1)::path1) ((id_of_msid msid2)::path2) in if equiv then check_signatures cst env (msid2,list2) (msid1,list1) + ((id_of_msid msid2)::path2) ((id_of_msid msid1)::path1) else cst | MTBfunsig (arg_id1,arg_t1,body_t1), MTBfunsig (arg_id2,arg_t2,body_t2) -> - let cst = check_modtypes cst env arg_t2 arg_t1 equiv in + let cst = check_modtypes cst env arg_t2 arg_t1 equiv + [] [] in (* contravariant *) let env = add_module (MPbound arg_id2) (module_body_of_type arg_t2) env @@ -367,9 +427,10 @@ and check_modtypes cst env mtb1 mtb2 equiv = body_t1 in check_modtypes cst env body_t1' body_t2 equiv + path1 path2 | MTBident _ , _ -> anomaly "Subtyping: scrape failed" | _ , MTBident _ -> anomaly "Subtyping: scrape failed" | _ , _ -> error_incompatible_modtypes mtb1 mtb2 let check_subtypes env sup super = - check_modtypes Constraint.empty env sup super false + check_modtypes Constraint.empty env sup super false [] [] -- cgit v1.2.3