(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* debug_string_of_mbid mbid | MPI mp -> string_of_mp mp module Umap = Map.Make(struct type t = substitution_domain let compare = Pervasives.compare end) type substitution = (module_path * delta_resolver) Umap.t let empty_subst = Umap.empty let string_of_subst_domain = function | MBI mbid -> debug_string_of_mbid mbid | MPI mp -> string_of_mp mp let add_mbid mbid mp resolve = Umap.add (MBI mbid) (mp,resolve) let add_mp mp1 mp2 resolve = Umap.add (MPI mp1) (mp2,resolve) let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst let add_inline_delta_resolver con = Deltamap.add (KN(user_con con)) (Inline None) let add_inline_constr_delta_resolver con cstr = Deltamap.add (KN(user_con con)) (Inline (Some cstr)) let add_constant_delta_resolver con = Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) let add_mind_delta_resolver mind = Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) let add_mp_delta_resolver mp1 mp2 = Deltamap.add (MP mp1) (Prefix_equiv mp2) let mp_in_delta mp = Deltamap.mem (MP mp) let con_in_delta con resolver = try match Deltamap.find (KN(user_con con)) resolver with | Inline _ | Prefix_equiv _ -> false | Equiv _ -> true with Not_found -> false let mind_in_delta mind resolver = try match Deltamap.find (KN(user_mind mind)) resolver with | Inline _ | Prefix_equiv _ -> false | Equiv _ -> true with Not_found -> false let delta_of_mp resolve mp = try match Deltamap.find (MP mp) resolve with | Prefix_equiv mp1 -> mp1 | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> mp let delta_of_kn resolve kn = try match Deltamap.find (KN kn) resolve with | Equiv kn1 -> kn1 | Inline _ -> kn | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> kn let remove_mp_delta_resolver resolver mp = Deltamap.remove (MP mp) resolver exception Inline_kn let rec find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> (try match Deltamap.find (MP mp_sup) resolve with | Prefix_equiv mp1 -> mp1 | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found -> MPdot(sub_mp mp,l)) | p -> match Deltamap.find (MP p) resolve with | Prefix_equiv mp1 -> mp1 | _ -> anomaly "mod_subst: bad association in delta_resolver" in try sub_mp mp with Not_found -> mp exception Change_equiv_to_inline of constr let solve_delta_kn resolve kn = try match Deltamap.find (KN kn) resolve with | Equiv kn1 -> kn1 | Inline (Some c) -> raise (Change_equiv_to_inline c) | Inline None -> raise Inline_kn | _ -> anomaly "mod_subst: bad association in delta_resolver" with Not_found | Inline_kn -> let mp,dir,l = repr_kn kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else make_kn new_mp dir l let constant_of_delta resolve con = let kn = user_con con in try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then con else constant_of_kn_equiv kn new_kn with _ -> con let constant_of_delta2 resolve con = let kn = canonical_con con in let kn1 = user_con con in try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then con else constant_of_kn_equiv kn1 new_kn with _ -> con let mind_of_delta resolve mind = let kn = user_mind mind in try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then mind else mind_of_kn_equiv kn new_kn with _ -> mind let mind_of_delta2 resolve mind = let kn = canonical_mind mind in let kn1 = user_mind mind in try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then mind else mind_of_kn_equiv kn1 new_kn with _ -> mind let inline_of_delta resolver = let extract key hint l = match key,hint with |KN kn, Inline _ -> kn::l | _,_ -> l in Deltamap.fold extract resolver [] exception Not_inline let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in try match Deltamap.find (KN kn2) resolve with | Inline None -> None | Inline (Some const) -> Some const | _ -> raise Not_inline with Not_found | Not_inline -> try match Deltamap.find (KN kn1) resolve with | Inline None -> None | Inline (Some const) -> Some const | _ -> raise Not_inline with Not_found | Not_inline -> None let string_of_key = function | KN kn -> string_of_kn kn | MP mp -> string_of_mp mp let string_of_hint = function | Inline _ -> "inline" | Equiv kn -> string_of_kn kn | Prefix_equiv mp -> string_of_mp mp let debug_string_of_delta resolve = let to_string key hint s = s^", "^(string_of_key key)^"=>"^(string_of_hint hint) in Deltamap.fold to_string resolve "" let list_contents sub = let one_pair uid (mp,reso) l = (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l in Umap.fold one_pair sub [] let debug_string_of_subst sub = let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]") (list_contents sub) in "{" ^ String.concat "; " l ^ "}" let debug_pr_delta resolve = str (debug_string_of_delta resolve) let debug_pr_subst sub = let l = list_contents sub in let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++ spc () ++ str "[" ++ str s3 ++ str "]") in str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}" let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with | MPfile sid -> let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> begin try let mp',resolve = Umap.find (MBI bid) sub in mp',resolve with Not_found -> let mp',resolve = Umap.find (MPI mp) sub in mp',resolve end | MPdot (mp1,l) as mp2 -> begin try let mp',resolve = Umap.find (MPI mp2) sub in mp',resolve with Not_found -> let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end in try Some (aux mp) with Not_found -> None let subst_mp sub mp = match subst_mp0 sub mp with None -> mp | Some (mp',_) -> mp' let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with Some (mp',resolve) -> solve_delta_kn resolve (make_kn mp' dir l) | None -> kn let subst_kn sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with Some (mp',_) -> (make_kn mp' dir l) | None -> kn exception No_subst type sideconstantsubst = | User | Canonical let subst_ind sub mind = let kn1,kn2 = user_mind mind,canonical_mind mind in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in try let side,mind',resolve = match subst_mp0 sub mp1,subst_mp0 sub mp2 with None,None ->raise No_subst | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, (make_mind_equiv mp1' mp2' dir l), resolve2 in match side with |User -> let mind = mind_of_delta resolve mind' in mind |Canonical -> let mind = mind_of_delta2 resolve mind' in mind with No_subst -> mind let subst_mind0 sub mind = let kn1,kn2 = user_mind mind,canonical_mind mind in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in try let side,mind',resolve = match subst_mp0 sub mp1,subst_mp0 sub mp2 with None,None ->raise No_subst | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, (make_mind_equiv mp1' mp2' dir l), resolve2 in match side with |User -> let mind = mind_of_delta resolve mind' in Some mind |Canonical -> let mind = mind_of_delta2 resolve mind' in Some mind with No_subst -> Some mind let subst_con sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in try let side,con',resolve = match subst_mp0 sub mp1,subst_mp0 sub mp2 with None,None ->raise No_subst | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, (make_con_equiv mp1' mp2' dir l), resolve2 in match constant_of_delta_with_inline resolve con' with None -> begin match side with |User -> let con = constant_of_delta resolve con' in con,mkConst con |Canonical -> let con = constant_of_delta2 resolve con' in con,mkConst con end | Some t -> con',t with No_subst -> con , mkConst con let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in try let side,con',resolve = match subst_mp0 sub mp1,subst_mp0 sub mp2 with None,None ->raise No_subst | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, (make_con_equiv mp1' mp2' dir l), resolve2 in match constant_of_delta_with_inline resolve con' with None ->begin match side with |User -> let con = constant_of_delta resolve con' in Some (mkConst con) |Canonical -> let con = constant_of_delta2 resolve con' in Some (mkConst con) end | t -> t with No_subst -> Some (mkConst con) (* 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" where X.t is later on instantiated with y? I choose the first interpretation (i.e. an evaluable reference is never expanded). *) let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn)) let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with | Const kn -> (match f' kn with None -> c | Some const ->const) | Ind (kn,i) -> (match f kn with None -> c | Some kn' -> mkInd (kn',i)) | Construct ((kn,i),j) -> (match f kn with None -> c | Some kn' -> 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_mind0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with | _ when mp = mpfrom -> mpto | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1==mp1' then mp else MPdot (mp1',l) | _ -> mp let replace_mp_in_kn mpfrom mpto kn = let mp,dir,l = repr_kn kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn else make_kn mp'' dir l let rec mp_in_mp mp mp1 = match mp1 with | _ when mp1 = mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false let mp_in_key mp key = match key with | MP mp1 -> mp_in_mp mp mp1 | KN kn -> let mp1,dir,l = repr_kn kn in mp_in_mp mp mp1 let subset_prefixed_by mp resolver = let prefixmp key hint resolv = match hint with | Inline _ -> resolv | _ -> if mp_in_key mp key then Deltamap.add key hint resolv else resolv in Deltamap.fold prefixmp resolver empty_delta_resolver let subst_dom_delta_resolver subst resolver = let apply_subst key hint resolver = match key with (MP mp) -> Deltamap.add (MP (subst_mp subst mp)) hint resolver | (KN kn) -> Deltamap.add (KN (subst_kn subst kn)) hint resolver in Deltamap.fold apply_subst resolver empty_delta_resolver let subst_mp_delta sub mp key= match subst_mp0 sub mp with None -> empty_delta_resolver,mp | Some (mp',resolve) -> let mp1 = find_prefix resolve mp' in let resolve1 = subset_prefixed_by mp1 resolve in match key with MP mpk -> (subst_dom_delta_resolver (map_mp mp1 mpk empty_delta_resolver) resolve1),mp1 | _ -> anomaly "Mod_subst: Bad association in resolver" let subst_codom_delta_resolver subst resolver = let apply_subst key hint resolver = match hint with Prefix_equiv mp -> let derived_resolve,mpnew = subst_mp_delta subst mp key in Deltamap.fold Deltamap.add derived_resolve (Deltamap.add key (Prefix_equiv mpnew) resolver) | (Equiv kn) -> (try Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver with Change_equiv_to_inline c -> Deltamap.add key (Inline (Some c)) resolver) | Inline None -> Deltamap.add key hint resolver | Inline (Some t) -> Deltamap.add key (Inline (Some (subst_mps subst t))) resolver in Deltamap.fold apply_subst resolver empty_delta_resolver let subst_dom_codom_delta_resolver subst resolver = let apply_subst key hint resolver = match key,hint with (MP mp1),Prefix_equiv mp -> let key = MP (subst_mp subst mp1) in let derived_resolve,mpnew = subst_mp_delta subst mp key in Deltamap.fold Deltamap.add derived_resolve (Deltamap.add key (Prefix_equiv mpnew) resolver) | (KN kn1),(Equiv kn) -> let key = KN (subst_kn subst kn1) in (try Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver with Change_equiv_to_inline c -> Deltamap.add key (Inline (Some c)) resolver) | (KN kn),Inline None -> let key = KN (subst_kn subst kn) in Deltamap.add key hint resolver | (KN kn),Inline (Some t) -> let key = KN (subst_kn subst kn) in Deltamap.add key (Inline (Some (subst_mps subst t))) resolver | _,_ -> anomaly "Mod_subst: Bad association in resolver" in Deltamap.fold apply_subst resolver empty_delta_resolver let update_delta_resolver resolver1 resolver2 = let apply_res key hint res = try if Deltamap.mem key resolver2 then res else match hint with Prefix_equiv mp -> let new_hint = Prefix_equiv (find_prefix resolver2 mp) in Deltamap.add key new_hint res | Equiv kn -> (try let new_hint = Equiv (solve_delta_kn resolver2 kn) in Deltamap.add key new_hint res with Change_equiv_to_inline c -> Deltamap.add key (Inline (Some c)) res) | _ -> Deltamap.add key hint res with not_found -> Deltamap.add key hint res in Deltamap.fold apply_res resolver1 empty_delta_resolver let add_delta_resolver resolver1 resolver2 = if resolver1 == resolver2 then resolver2 else if resolver2 = empty_delta_resolver then resolver1 else Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) resolver2 let substition_prefixed_by k mp subst = let prefixmp key (mp_to,reso) sub = match key with | MPI mpk -> if mp_in_mp mp mpk && mp <> mpk then let new_key = replace_mp_in_mp mp k mpk in Umap.add (MPI new_key) (mp_to,reso) sub else sub | _ -> sub in Umap.fold prefixmp subst empty_subst let join (subst1 : substitution) (subst2 : substitution) = let apply_subst key (mp,resolve) res = let mp',resolve' = match subst_mp0 subst2 mp with None -> mp, None | Some (mp',resolve') -> mp' ,Some resolve' in let resolve'' : delta_resolver = match resolve' with Some res -> add_delta_resolver (subst_dom_codom_delta_resolver subst2 resolve) res | None -> subst_codom_delta_resolver subst2 resolve in let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in let prefixed_subst = substition_prefixed_by k mp subst2 in Umap.fold Umap.add prefixed_subst (Umap.add key (mp',resolve'') res) in let subst = Umap.fold apply_subst subst1 empty_subst in (Umap.fold Umap.add subst2 subst) let rec occur_in_path uid path = match uid,path with | MBI bid,MPbound bid' -> bid = bid' | _,MPdot (mp1,_) -> occur_in_path uid mp1 | _ -> false let occur_uid uid sub = let check_one uid' (mp,_) = if uid = uid' || occur_in_path uid mp then raise Exit in try Umap.iter check_one sub; false with Exit -> true let occur_mbid uid = occur_uid (MBI uid) type 'a lazy_subst = | LSval of 'a | LSlazy of substitution list * 'a type 'a substituted = 'a lazy_subst ref let from_val a = ref (LSval a) let force fsubst r = match !r with | LSval a -> a | LSlazy(s,a) -> let subst = List.fold_left join empty_subst (List.rev s) in let a' = fsubst subst a in r := LSval a'; a' let subst_substituted s r = match !r with | LSval a -> ref (LSlazy([s],a)) | LSlazy(s',a) -> ref (LSlazy(s::s',a))