diff options
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 713 |
1 files changed, 290 insertions, 423 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 0deb80a2..890996d1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -20,7 +20,7 @@ type polymorphic_arity = { poly_level : Univ.universe; } let val_pol_arity = - val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] + val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] type constant_type = | NonPolymorphicType of constr @@ -29,256 +29,164 @@ type constant_type = let val_cst_type = val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] - -type substitution_domain = - | MBI of mod_bound_id - | MPI of module_path - -let val_subst_dom = - val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|] - -module Umap = Map.Make(struct - type t = substitution_domain - let compare = Pervasives.compare - end) - +(** Substitutions, code imported from kernel/mod_subst *) type delta_hint = - Inline of constr option + | Inline of int * constr option | Equiv of kernel_name - | Prefix_equiv of module_path - -type delta_key = - KN of kernel_name - | MP of module_path -module Deltamap = Map.Make(struct - type t = delta_key - let compare = Pervasives.compare - end) -type delta_resolver = delta_hint Deltamap.t +module Deltamap = struct + type t = module_path MPmap.t * delta_hint KNmap.t + let empty = MPmap.empty, KNmap.empty + let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) + let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km) + let remove_mp mp (mm,km) = (MPmap.remove mp mm, km) + let find_mp mp map = MPmap.find mp (fst map) + let find_kn kn map = KNmap.find kn (snd map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_kn kn map = KNmap.mem kn (snd map) + let fold_kn f map i = KNmap.fold f (snd map) i + let fold fmp fkn (mm,km) i = + MPmap.fold fmp mm (KNmap.fold fkn km i) + let join map1 map2 = fold add_mp add_kn map1 map2 +end + +type delta_resolver = Deltamap.t let empty_delta_resolver = Deltamap.empty +module MBImap = Map.Make + (struct + type t = mod_bound_id + let compare = Pervasives.compare + end) + +module Umap = struct + type 'a t = 'a MPmap.t * 'a MBImap.t + let empty = MPmap.empty, MBImap.empty + let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 + let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) + let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) + let find_mp mp map = MPmap.find mp (fst map) + let find_mbi mbi map = MBImap.find mbi (snd map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_mbi mbi map = MBImap.mem mbi (snd map) + let iter_mbi f map = MBImap.iter f (snd map) + let fold fmp fmbi (m1,m2) i = + MPmap.fold fmp m1 (MBImap.fold fmbi m2 i) + let join map1 map2 = fold add_mp add_mbi map1 map2 +end + type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res_dom = - val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|] +let empty_subst = Umap.empty -let val_res = - val_map ~name:"delta_resolver" - val_res_dom - (val_sum "delta_hint" 0 [|[|val_opt val_constr|];[|val_kn|];[|val_mp|]|]) +let is_empty_subst = Umap.is_empty -let val_subst = - val_map ~name:"substitution" - val_subst_dom (val_tuple "substition range" [|val_mp;val_res|]) +let val_delta_hint = + val_sum "delta_hint" 0 + [|[|val_int; val_opt val_constr|];[|val_kn|]|] +let val_res = + val_tuple ~name:"delta_resolver" + [|val_map ~name:"delta_resolver" val_mp val_mp; + val_map ~name:"delta_resolver" val_kn val_delta_hint|] -let fold_subst fb fp = - Umap.fold - (fun k (mp,_) acc -> - match k with - | MBI mbid -> fb mbid mp acc - | MPI mp1 -> fp mp1 mp acc) +let val_mp_res = val_tuple [|val_mp;val_res|] -let empty_subst = Umap.empty +let val_subst = + val_tuple ~name:"substitution" + [|val_map ~name:"substitution" val_mp val_mp_res; + val_map ~name:"substitution" val_uid val_mp_res|] -let add_mbid mbid mp = - Umap.add (MBI mbid) (mp,empty_delta_resolver) -let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,empty_delta_resolver) +let add_mbid mbid mp = Umap.add_mbi mbid (mp,empty_delta_resolver) +let add_mp mp1 mp2 = Umap.add_mp mp1 (mp2,empty_delta_resolver) let map_mbid mbid mp = add_mbid mbid mp empty_subst let map_mp mp1 mp2 = add_mp mp1 mp2 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 mp_in_delta mp = + Deltamap.mem_mp mp -let rec find_prefix resolve mp = +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" + | MPdot(mp,l) as mp_sup -> + (try Deltamap.find_mp mp_sup resolve + with Not_found -> MPdot(sub_mp mp,l)) + | p -> Deltamap.find_mp p resolve in - try - sub_mp mp - with - Not_found -> mp - + try sub_mp mp with Not_found -> mp + +(** Nota: the following function is slightly different in mod_subst + PL: Is it on purpose ? *) + let solve_delta_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> 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 - + try + match Deltamap.find_kn kn resolve with + | Equiv kn1 -> kn1 + | Inline _ -> raise Not_found + with Not_found -> + 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 gen_of_delta resolve x kn fix_can = + try + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then x else fix_can new_kn + with _ -> x let constant_of_delta resolve con = let kn = user_con con in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn new_kn - + gen_of_delta resolve con kn (constant_of_kn_equiv kn) + let constant_of_delta2 resolve con = - let kn = canonical_con con in - let kn1 = user_con con in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn1 new_kn + let kn, kn' = canonical_con con, user_con con in + gen_of_delta resolve con kn (constant_of_kn_equiv kn') let mind_of_delta resolve mind = let kn = user_mind mind in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn new_kn - -let mind_of_delta2 resolve mind = - let kn = canonical_mind mind in - let kn1 = user_mind mind in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn1 new_kn - + gen_of_delta resolve mind kn (mind_of_kn_equiv kn) +let mind_of_delta2 resolve mind = + let kn, kn' = canonical_mind mind, user_mind mind in + gen_of_delta resolve mind kn (mind_of_kn_equiv kn') -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 [] +let find_inline_of_delta kn resolve = + match Deltamap.find_kn kn resolve with + | Inline (_,o) -> o + | _ -> raise Not_found -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 + try find_inline_of_delta kn2 resolve + with Not_found -> + try find_inline_of_delta kn1 resolve + with Not_found -> None 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 + | MPfile sid -> Umap.find_mp mp sub | 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 + try Umap.find_mbi bid sub + with Not_found -> Umap.find_mp mp sub end | MPdot (mp1,l) as mp2 -> begin - try - let mp',resolve = Umap.find (MPI mp2) sub in - mp',resolve + try Umap.find_mp mp2 sub with Not_found -> let mp1',resolve = aux mp1 in - MPdot (mp1',l),resolve + MPdot (mp1',l),resolve end in - try - Some (aux mp) - with Not_found -> None + try Some (aux mp) with Not_found -> None let subst_mp sub mp = match subst_mp0 sub mp with @@ -305,127 +213,58 @@ type sideconstantsubst = | User | Canonical + +let gen_subst_mp f sub mp1 mp2 = + match subst_mp0 sub mp1, subst_mp0 sub mp2 with + | None, None -> raise No_subst + | Some (mp',resolve), None -> User, (f mp' mp2), resolve + | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve + | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 + let subst_ind sub mind = - let kn1,kn2 = user_mind mind,canonical_mind mind in + 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,Const con - |Canonical -> - let con = constant_of_delta2 resolve con' in - con,Const con - end - | Some t -> con',t - with No_subst -> con , Const con - + let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in + try + let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in + match side with + | User -> mind_of_delta resolve mind' + | Canonical -> mind_of_delta2 resolve mind' + with No_subst -> mind 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 + let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in + let dup con = con, Const con in + let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in + match constant_of_delta_with_inline resolve con' with + | Some t -> con', t + | None -> + let con'' = match side with + | User -> constant_of_delta resolve con' + | Canonical -> constant_of_delta2 resolve con' 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 (Const con) - |Canonical -> - let con = constant_of_delta2 resolve con' in - Some (Const con) - end - | t -> t - with No_subst -> Some (Const con) - + if con'' == con then raise No_subst else dup con'' let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> - (match f' kn with - None -> c - | Some const ->const) + | Const kn -> (try snd (f' kn) with No_subst -> c) | Ind (kn,i) -> - (match f kn with - None -> c - | Some kn' -> - Ind (kn',i)) + let kn' = f kn in + if kn'==kn then c else Ind (kn',i) | Construct ((kn,i),j) -> - (match f kn with - None -> c - | Some kn' -> - Construct ((kn',i),j)) + let kn' = f kn in + if kn'==kn then c else Construct ((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 kn' = f kn in + if kn'==kn then ci.ci_ind else kn',i + in let p' = func p in let ct' = func ct in let l' = array_smartmap func l in @@ -476,8 +315,9 @@ let rec map_kn f f' c = else CoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_mind0 sub) (subst_con0 sub) +let subst_mps sub c = + if is_empty_subst sub then c + else map_kn (subst_ind sub) (subst_con0 sub) c type 'a lazy_subst = @@ -507,125 +347,113 @@ let rec mp_in_mp mp mp1 = | _ 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 = - if mp_in_key mp key then - Deltamap.add key hint resolv - else - resolv + let mp_prefix mkey mequ rslv = + if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv + in + let kn_prefix kn hint rslv = + match hint with + | Inline _ -> rslv + | Equiv _ -> + if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv in - Deltamap.fold prefixmp resolver empty_delta_resolver + Deltamap.fold mp_prefix kn_prefix 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 + let mp_apply_subst mkey mequ rslv = + Deltamap.add_mp (subst_mp subst mkey) mequ rslv in - Deltamap.fold apply_subst resolver empty_delta_resolver + let kn_apply_subst kkey hint rslv = + Deltamap.add_kn (subst_kn subst kkey) hint rslv + in + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver -let subst_mp_delta sub mp key= +let subst_mp_delta sub mp mkey = match subst_mp0 sub mp with None -> empty_delta_resolver,mp - | Some (mp',resolve) -> + | 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) 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) -> - Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver - | Inline None -> - Deltamap.add key hint resolver - | Inline (Some t) -> - Deltamap.add key (Inline (Some (subst_mps subst t))) resolver + (subst_dom_delta_resolver + (map_mp mp1 mkey) resolve1),mp1 + +let gen_subst_delta_resolver dom subst resolver = + let mp_apply_subst mkey mequ rslv = + let mkey' = if dom then subst_mp subst mkey else mkey in + let rslv',mequ' = subst_mp_delta subst mequ mkey in + Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv) in - Deltamap.fold apply_subst resolver empty_delta_resolver + let kn_apply_subst kkey hint rslv = + let kkey' = if dom then subst_kn subst kkey else kkey in + let hint' = match hint with + | Equiv kequ -> Equiv (subst_kn_delta subst kequ) + | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (_,None) -> hint + in + Deltamap.add_kn kkey' hint' rslv + in + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver + +let subst_codom_delta_resolver = gen_subst_delta_resolver false +let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true -let subst_dom_codom_delta_resolver subst resolver = - subst_dom_delta_resolver subst - (subst_codom_delta_resolver subst resolver) - let update_delta_resolver resolver1 resolver2 = - let apply_res key hint res = - try - match hint with - Prefix_equiv mp -> - let new_hint = - Prefix_equiv (find_prefix resolver2 mp) - in Deltamap.add key new_hint res - | Equiv kn -> - let new_hint = - Equiv (solve_delta_kn resolver2 kn) - in Deltamap.add key new_hint res - | _ -> Deltamap.add key hint res - with Not_found -> - Deltamap.add key hint res - in - Deltamap.fold apply_res resolver1 empty_delta_resolver + let mp_apply_rslv mkey mequ rslv = + if Deltamap.mem_mp mkey resolver2 then rslv + else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv + in + let kn_apply_rslv kkey hint rslv = + if Deltamap.mem_kn kkey resolver2 then rslv + else + let hint' = match hint with + | Equiv kequ -> Equiv (solve_delta_kn resolver2 kequ) + | _ -> hint + in + Deltamap.add_kn kkey hint' rslv + in + Deltamap.fold mp_apply_rslv kn_apply_rslv 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 + Deltamap.join (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 + let mp_prefixmp kmp (mp_to,reso) sub = + if mp_in_mp mp kmp && mp <> kmp then + let new_key = replace_mp_in_mp mp k kmp in + Umap.add_mp new_key (mp_to,reso) sub + else sub + in + let mbi_prefixmp mbi _ sub = sub in - Umap.fold prefixmp subst empty_subst + Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst key (mp,resolve) res = +let join subst1 subst2 = + let apply_subst mpk add (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 = + | None -> mp, None + | Some (mp',resolve') -> mp', Some resolve' in + let resolve'' = match resolve' with - Some res -> - add_delta_resolver + | Some res -> + add_delta_resolver (subst_dom_codom_delta_resolver subst2 resolve) res - | None -> + | 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 prefixed_subst = substition_prefixed_by mpk mp' subst2 in + Umap.join prefixed_subst (add (mp',resolve'') res) + in + let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in + let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in + let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in + Umap.join subst2 subst let force fsubst r = match !r with @@ -650,25 +478,67 @@ let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted +(** Beware! In .vo files, lazy_constr are stored as integers + used as indexes for a separate table. The actual lazy_constr is restored + later, by [Safe_typing.LightenLibrary.load]. This allows us + to use here a different definition of lazy_constr than coqtop: + since the checker will inspect all proofs parts, even opaque + ones, no need to use Lazy.t here *) + +type lazy_constr = constr_substituted +let subst_lazy_constr = subst_substituted +let force_lazy_constr = force_constr +let lazy_constr_from_val c = c +let val_lazy_constr = val_cstr_subst + +(** Inlining level of parameters at functor applications. + This is ignored by the checker. *) + +type inline = int option + +(** A constant can have no body (axiom/parameter), or a + transparent body, or an opaque one *) + +type constant_def = + | Undef of inline + | Def of constr_substituted + | OpaqueDef of lazy_constr + +let val_cst_def = + val_sum "constant_def" 0 + [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|] + +let subst_constant_def sub = function + | Undef inl -> Undef inl + | Def c -> Def (subst_constr_subst sub c) + | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr_substituted option; + const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - (* const_type_code : Cemitcodes.to_patch; *) - const_constraints : Univ.constraints; - const_opaque : bool; - const_inline : bool} + const_constraints : Univ.constraints } -let val_cb = val_tuple "constant_body" +let body_of_constant cb = match cb.const_body with + | Undef _ -> None + | Def c -> Some c + | OpaqueDef c -> Some c + +let constant_has_body cb = match cb.const_body with + | Undef _ -> false + | Def _ | OpaqueDef _ -> true + +let is_opaque cb = match cb.const_body with + | OpaqueDef _ -> true + | Def _ | Undef _ -> false + +let val_cb = val_tuple ~name:"constant_body" [|val_nctxt; - val_opt val_cstr_subst; + val_cst_def; val_cst_type; no_val; - val_cstrs; - val_bool; - val_bool |] - + val_cstrs|] let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in @@ -679,14 +549,14 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) type recarg = | Norec - | Mrec of int + | Mrec of inductive | Imbr of inductive let val_recarg = val_sum "recarg" 1 (* Norec *) - [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|] + [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|] let subst_recarg sub r = match r with - | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_ind sub kn in + | Norec -> r + | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -724,7 +594,7 @@ type monomorphic_inductive_arity = { mind_sort : sorts; } let val_mono_ind_arity = - val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|] + val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|] type inductive_arity = | Monomorphic of monomorphic_inductive_arity @@ -784,7 +654,7 @@ type one_inductive_body = { mind_reloc_tbl : reloc_table; } -let val_one_ind = val_tuple "one_inductive_body" +let val_one_ind = val_tuple ~name:"one_inductive_body" [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr; val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int; val_wfp;val_int;val_int;no_val|] @@ -820,7 +690,7 @@ type mutual_inductive_body = { mind_constraints : Univ.constraints; } -let val_ind_pack = val_tuple "mutual_inductive_body" +let val_ind_pack = val_tuple ~name:"mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; val_int; val_int; val_rctxt;val_cstrs|] @@ -832,13 +702,10 @@ let subst_arity sub = function (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); - const_body = Option.map (subst_constr_subst sub) cb.const_body; + const_body = subst_constant_def sub cb.const_body; const_type = subst_arity sub cb.const_type; const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code; - (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) - const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque; - const_inline = cb.const_inline} + const_constraints = cb.const_constraints} let subst_arity sub = function | Monomorphic s -> @@ -923,7 +790,7 @@ let rec val_sfb o = val_sum "struct_field_body" 0 [|val_module|]; (* SFBmodule *) [|val_modtype|] (* SFBmodtype *) |] o -and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o +and val_sb o = val_list (val_tuple ~name:"label*sfb"[|val_id;val_sfb|]) o and val_seb o = val_sum "struct_expr_body" 0 [|[|val_mp|]; (* SEBident *) [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) @@ -934,10 +801,10 @@ and val_seb o = val_sum "struct_expr_body" 0 and val_with o = val_sum "with_declaration_body" 0 [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o -and val_module o = val_tuple "module_body" +and val_module o = val_tuple ~name:"module_body" [|val_mp;val_opt val_seb;val_seb; val_opt val_seb;val_cstrs;val_res;no_val|] o -and val_modtype o = val_tuple "module_type_body" +and val_modtype o = val_tuple ~name:"module_type_body" [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o |