diff options
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 23 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 12 | ||||
| -rw-r--r-- | pretyping/termops.ml | 8 |
6 files changed, 32 insertions, 19 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c4e88f5ae..7fb1bb2cc 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -158,7 +158,7 @@ let subst_cl_typ subst ct = match ct with | CL_FUN | CL_SECVAR _ -> ct | CL_CONST kn -> - let kn' = subst_kn subst kn in + let kn' = subst_con subst kn in if kn' == kn then ct else CL_CONST kn' | CL_IND (kn,i) -> diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 11cb50c83..60c9321ad 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -518,7 +518,7 @@ let lookup_eliminator ind_sp s = let id = add_suffix ind_id (elimination_suffix s) in (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) - let ref = ConstRef (make_kn mp dp (label_of_id id)) in + let ref = ConstRef (make_con mp dp (label_of_id id)) in try let _ = sp_of_global ref in constr_of_reference ref diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 339f76392..6d7921f0d 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -34,20 +34,20 @@ type struc_typ = { s_PROJ : constant option list } let structure_table = ref (Indmap.empty : struc_typ Indmap.t) -let projection_table = ref KNmap.empty +let projection_table = ref Cmap.empty let option_fold_right f p e = match p with Some a -> f a e | None -> e let cache_structure (_,(ind,struc)) = structure_table := Indmap.add ind struc !structure_table; projection_table := - List.fold_right (option_fold_right (fun proj -> KNmap.add proj struc)) + List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc)) struc.s_PROJ !projection_table let subst_structure (_,subst,((kn,i),struc as obj)) = let kn' = subst_kn subst kn in let proj' = list_smartmap - (option_smartmap (subst_kn subst)) + (option_smartmap (subst_con subst)) struc.s_PROJ in if proj' == struc.s_PROJ && kn' == kn then obj else @@ -67,7 +67,7 @@ let add_new_struc (s,c,n,l) = let find_structure indsp = Indmap.find indsp !structure_table let find_projection_nparams = function - | ConstRef cst -> (KNmap.find cst !projection_table).s_PARAM + | ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM | _ -> raise Not_found (*s Un "object" est une fonction construisant une instance d'une structure *) @@ -139,12 +139,23 @@ let add_new_objdef (o,c,la,lp,l) = let cache_objdef1 (_,sp) = () -let (inObjDef1,outObjDef1) = +let (inObjDef10,outObjDef10) = declare_object {(default_object "OBJDEF1") with open_function = (fun i o -> if i=1 then cache_objdef1 o); cache_function = cache_objdef1; export_function = (function x -> Some x) } +let outObjDef1 obj = constant_of_kn (outObjDef10 obj) + +let inObjDef1 con = + (*CSC: Here I am cheating by violating the fact that "constant" is an ADT + and this is the only place in the whole Coq code. My feeling is that the + implementation of "Canonical Structure"s should be improved to avoid this + situation (that is avoided for all the other non-logical objects). *) + let mp,sp,l = repr_con con in + let kn = make_kn mp sp l in + inObjDef10 kn + let objdef_info o = List.assoc o !object_table let freeze () = @@ -154,7 +165,7 @@ let unfreeze (s,p,o) = structure_table := s; projection_table := p; object_table := o let init () = - structure_table := Indmap.empty; projection_table := KNmap.empty; + structure_table := Indmap.empty; projection_table := Cmap.empty; object_table:=[] let _ = init() diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7dae554b6..949dc4e80 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -47,5 +47,5 @@ val add_new_objdef : val inStruc : inductive * struc_typ -> obj val outStruc : obj -> inductive * struc_typ -val inObjDef1 : kernel_name -> obj -val outObjDef1 : obj -> kernel_name +val inObjDef1 : constant -> obj +val outObjDef1 : obj -> constant diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e91ea75b7..5b150303c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -55,7 +55,7 @@ let is_evaluable env ref = match ref with EvalConstRef kn -> let (ids,kns) = Conv_oracle.freeze() in - KNpred.mem kn kns & + Cpred.mem kn kns & let cb = Environ.lookup_constant kn env in cb.const_body <> None & not cb.const_opaque | EvalVarRef id -> @@ -206,8 +206,8 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - let (mp,dp,_) = repr_kn kn in - Some (EvalConst (make_kn mp dp (label_of_id id))) in + let (mp,dp,_) = repr_con kn in + Some (EvalConst (make_con mp dp (label_of_id id))) in match refi with | None -> None | Some ref -> @@ -392,8 +392,8 @@ let reduce_mind_case_use_function func env mia = match names.(i) with | Name id -> if isConst func then - let (mp,dp,_) = repr_kn (destConst func) in - let kn = make_kn mp dp (label_of_id id) in + let (mp,dp,_) = repr_con (destConst func) in + let kn = make_con mp dp (label_of_id id) in (match constant_opt_value env kn with | None -> None | Some _ -> Some (mkConst kn)) @@ -664,7 +664,7 @@ let rec substlin env name n ol c = with NotEvaluableConst _ -> errorlabstrm "substlin" - (pr_kn kn ++ str " is not a defined constant") + (pr_con kn ++ str " is not a defined constant") else ((n+1), ol, c) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d89d5a879..d4e23af28 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -35,6 +35,7 @@ let pr_name = function | Anonymous -> str "_" let pr_sp sp = str(string_of_kn sp) +let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with | Rel n -> str "#"++int n @@ -63,7 +64,7 @@ let rec pr_constr c = match kind_of_term c with | Evar (e,l) -> hov 1 (str"Evar#" ++ int e ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const c -> str"Cst(" ++ pr_sp c ++ str")" + | Const c -> str"Cst(" ++ pr_con c ++ str")" | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" @@ -691,7 +692,7 @@ let hdchar env c = | Cast (c,_) -> hdrec k c | App (f,l) -> hdrec k f | Const kn -> - let c = lowercase_first_char (id_of_label (label kn)) in + let c = lowercase_first_char (id_of_label (con_label kn)) in if c = "?" then "y" else c | Ind ((kn,i) as x) -> if i=0 then @@ -799,7 +800,6 @@ let rec is_imported_modpath = function let is_imported_ref = function | VarRef _ -> false - | ConstRef kn | IndRef (kn,_) | ConstructRef ((kn,_),_) (* | ModTypeRef ln *) -> @@ -807,6 +807,8 @@ let is_imported_ref = function (* | ModRef mp -> is_imported_modpath mp *) + | ConstRef kn -> + let (mp,_,_) = repr_con kn in is_imported_modpath mp let is_global id = try |