diff options
72 files changed, 416 insertions, 272 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 0af215f25..359257c88 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -143,7 +143,7 @@ let create_modular_renamings struc = in (* 1) creates renamings of objects *) let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_modular_renamings mp in let s = modular_rename upper (id_of_global r) in global_ids := Idset.add (id_of_string s) !global_ids; @@ -184,7 +184,7 @@ let create_modular_renamings struc = List.iter contents_first_level used_modules; let used_modules' = List.rev used_modules in let needs_qualify r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in if (is_modfile mp) && mp <> current_module && (clash mp [] (List.hd (get_renamings r)) used_modules') then to_qualify := Refset.add r !to_qualify @@ -239,7 +239,7 @@ let rec mp_create_mono_renamings mp = let create_mono_renamings struc = let { up = u ; down = d } = struct_get_references_list struc in let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_mono_renamings mp in let mycase = if upper then uppercase_id else lowercase_id in let id = @@ -278,7 +278,7 @@ module StdParams = struct let pp_global mpl r = let ls = get_renamings r in let s = List.hd ls in - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let ls = if mp = List.hd mpl then [s] (* simpliest situation *) else diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index f9be3d9b0..78fb578e9 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -28,7 +28,7 @@ let toplevel_env () = | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with - | "CONSTANT" -> SEBconst (Global.lookup_constant kn) + | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn)) | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l))) | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn) @@ -52,14 +52,16 @@ let environment_until dir_opt = | _ -> assert false in parse (Library.loaded_libraries ()) -type visit = { mutable kn : KNset.t; mutable mp : MPset.t } +type visit = + { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t } let in_kn v kn = KNset.mem kn v.kn +let in_ref v ref = Refset.mem ref v.ref let in_mp v mp = MPset.mem mp v.mp let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn) -let visit_ref v r = visit_kn v (kn_of_r r) +let visit_ref v r = v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) exception Impossible @@ -102,7 +104,7 @@ let get_spec_references v s = let rec extract_msig env v mp = function | [] -> [] | (l,SPBconst cb) :: msig -> - let kn = make_kn mp empty_dirpath l in + let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in if logical_spec s then extract_msig env v mp msig else begin @@ -143,9 +145,9 @@ let rec extract_msb env v mp all = function | (l,SEBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in + let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in let ms = extract_msb env v mp all msb in - let b = array_exists (in_kn v) vkn in + let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in if all || b then let d = extract_fixpoint env vkn recd in if (not b) && (logical_decl d) then ms @@ -153,8 +155,8 @@ let rec extract_msb env v mp all = function else ms with Impossible -> let ms = extract_msb env v mp all msb in - let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let kn = make_con mp empty_dirpath l in + let b = in_ref v (ConstRef kn) in if all || b then let d = extract_constant env kn cb in if (not b) && (logical_decl d) then ms @@ -163,7 +165,7 @@ let rec extract_msb env v mp all = function | (l,SEBmind mib) :: msb -> let ms = extract_msb env v mp all msb in let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *) if all || b then let d = Dind (kn, extract_inductive env kn) in if (not b) && (logical_decl d) then ms @@ -217,12 +219,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = let l = environment_until None in let v = - let add_kn r = KNset.add (kn_of_r r) in - let kns = List.fold_right add_kn refs KNset.empty in + let add_ref r = Refset.add r in + let refs = List.fold_right add_ref refs Refset.empty in let add_mp mp = MPset.union (prefixes_mp mp) in let mps = List.fold_right add_mp mpl MPset.empty in - let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in - { kn = kns; mp = mps } + let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in + { kn = KNset.empty; ref = refs; mp = mps } in let env = Global.env () in List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) @@ -270,10 +272,9 @@ let extraction qid = else begin let prm = { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let kn = kn_of_r r in let struc = optimize_struct prm None (mono_environment [r] []) in let d = get_decl_in_structure r struc in - print_one_decl struc (modpath kn) d; + print_one_decl struc (modpath_of_r r) d; reset_tables () end @@ -315,7 +316,7 @@ let extraction_module m = let b = is_modfile mp in let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in let l = environment_until None in - let v = { kn = KNset.empty ; mp = prefixes_mp mp } in + let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in let env = Global.env () in let struc = List.rev_map @@ -350,7 +351,9 @@ let extraction_library is_rec m = | Scheme -> error_scheme () | _ -> let dir_m = dir_module_of_id m in - let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in + let v = + { kn = KNset.empty; ref = Refset.empty; + mp = MPset.singleton (MPfile dir_m) } in let l = environment_until (Some dir_m) in let struc = let env = Global.env () in diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 0bf5d6bcd..52ff05439 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -358,16 +358,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let field_names = list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); - let projs = ref KNset.empty in + let projs = ref Cset.empty in let mp,d,_ = repr_kn kn in let rec select_fields l typs = match l,typs with | [],[] -> [] | (Name id)::l, typ::typs -> if type_eq (mlt_env env) Tdummy typ then select_fields l typs else - let knp = make_kn mp d (label_of_id id) in + let knp = make_con mp d (label_of_id id) in if not (List.mem false (type_to_sign (mlt_env env) typ)) then - projs := KNset.add knp !projs; + projs := Cset.add knp !projs; (ConstRef knp) :: (select_fields l typs) | Anonymous::l, typ::typs -> if type_eq (mlt_env env) Tdummy typ then select_fields l typs @@ -382,7 +382,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let n = nb_default_params env mip0.mind_nf_arity in List.iter (option_iter - (fun kn -> if KNset.mem kn !projs then add_projection n kn)) + (fun kn -> if Cset.mem kn !projs then add_projection n kn)) (find_structure ip).s_PROJ with Not_found -> () end; @@ -417,7 +417,7 @@ and extract_type_cons env db dbmap c i = and mlt_env env r = match r with | ConstRef kn -> (try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; match lookup_term kn with | Dtype (_,vl,mlt) -> Some mlt | _ -> None @@ -446,7 +446,7 @@ let type_expunge env = type_expunge (mlt_env env) let record_constant_type env kn opt_typ = try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; lookup_type kn with Not_found -> let typ = match opt_typ with diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index 31fdd0580..b26a577e2 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -17,12 +17,12 @@ open Environ open Libnames open Miniml -val extract_constant : env -> kernel_name -> constant_body -> ml_decl +val extract_constant : env -> constant -> constant_body -> ml_decl -val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec +val extract_constant_spec : env -> constant -> constant_body -> ml_spec val extract_fixpoint : - env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl + env -> constant array -> (constr, types) prec_declaration -> ml_decl val extract_inductive : env -> kernel_name -> ml_ind diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 3d4ab11a6..b8764d85d 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -210,7 +210,7 @@ end let rec type_mem_kn kn = function | Tmeta _ -> assert false - | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l + | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b) | _ -> false @@ -594,11 +594,12 @@ let rec linear_beta_red a t = match a,t with linear beta reductions at modified positions. *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob (ConstRef kn)) as f, a) -> + | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (ast_glob_subst s) a in - (try linear_beta_red a (KNmap.find kn s) + (try linear_beta_red a (Refmap.find refe s) with Not_found -> MLapp (f, a)) - | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (try Refmap.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -1117,7 +1118,7 @@ let inline_test t = let manual_inline_list = let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in - List.map (fun s -> (make_kn mp empty_dirpath (mk_label s))) + List.map (fun s -> (make_con mp empty_dirpath (mk_label s))) [ "well_founded_induction_type"; "well_founded_induction"; "Acc_rect"; "Acc_rec" ; "Acc_iter" ] diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index bc4de489d..05e773c5d 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -101,7 +101,7 @@ val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast -val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast +val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index caa72b34f..1a40a8330 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -25,8 +25,9 @@ open Mlutil let add_structure mp msb env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match elem with - | SEBconst cb -> Environ.add_constant kn cb env + | SEBconst cb -> Environ.add_constant con cb env | SEBmind mib -> Environ.add_mind kn mib env | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env | SEBmodtype mtb -> Environ.add_modtype kn mtb env @@ -116,8 +117,15 @@ let rec parse_labels ll = function let labels_of_mp mp = parse_labels [] mp -let labels_of_kn kn = - let mp,_,l = repr_kn kn in parse_labels [l] mp +let labels_of_ref r = + let mp,_,l = + match r with + ConstRef con -> repr_con con + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_kn kn + | VarRef _ -> assert false + in + parse_labels [l] mp let rec add_labels_mp mp = function | [] -> mp @@ -307,8 +315,7 @@ let signature_of_structure s = let get_decl_in_structure r struc = try - let kn = kn_of_r r in - let base_mp,ll = labels_of_kn kn in + let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; let sel = List.assoc base_mp struc in let rec go ll sel = match ll with @@ -336,16 +343,16 @@ let get_decl_in_structure r struc = let dfix_to_mlfix rv av i = let rec make_subst n s = if n < 0 then s - else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s) + else make_subst (n-1) (Refmap.add rv.(n) (n+1) s) in - let s = make_subst (Array.length rv - 1) KNmap.empty + let s = make_subst (Array.length rv - 1) Refmap.empty in let rec subst n t = match t with - | MLglob (ConstRef kn) -> - (try MLrel (n + (KNmap.find kn s)) with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (try MLrel (n + (Refmap.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in - let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in + let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) @@ -356,7 +363,7 @@ let rec optim prm s = function | Dterm (r,t,typ) :: l -> let t = normalize (ast_glob_subst !s t) in let i = inline r t in - if i then s := KNmap.add (kn_of_r r) t !s; + if i then s := Refmap.add r t !s; if not i || prm.modular || List.mem r prm.to_appear then let d = match optimize_fix t with @@ -370,10 +377,9 @@ let rec optim prm s = function let rec optim_se top prm s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> - let kn = kn_of_r r in let a = normalize (ast_glob_subst !s a) in let i = inline r a in - if i then s := KNmap.add kn a !s; + if i then s := Refmap.add r a !s; if top && i && not prm.modular && not (List.mem r prm.to_appear) then optim_se top prm s lse else @@ -389,7 +395,7 @@ let rec optim_se top prm s = function let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body - then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s + then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; if !all && top && not prm.modular @@ -408,6 +414,6 @@ and optim_me prm s = function | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me) let optimize_struct prm before struc = - let subst = ref (KNmap.empty : ml_ast KNmap.t) in + let subst = ref (Refmap.empty : ml_ast Refmap.t) in option_iter (fun l -> ignore (optim prm subst l)) before; List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 17628698d..7c010ab4f 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -22,10 +22,23 @@ open Miniml (*S Utilities concerning [module_path] and [kernel_names] *) -let kn_of_r r = match r with - | ConstRef kn -> kn - | IndRef (kn,_) -> kn - | ConstructRef ((kn,_),_) -> kn +let occur_kn_in_ref kn = + function + | IndRef (kn',_) + | ConstructRef ((kn',_),_) -> kn = kn' + | ConstRef _ -> false + | VarRef _ -> assert false + +let modpath_of_r r = match r with + | ConstRef kn -> con_modpath kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> modpath kn + | VarRef _ -> assert false + +let label_of_r r = match r with + | ConstRef kn -> con_label kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> label kn | VarRef _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -45,21 +58,22 @@ let at_toplevel mp = is_modfile mp || is_toplevel mp let visible_kn kn = at_toplevel (base_mp (modpath kn)) +let visible_con kn = at_toplevel (base_mp (con_modpath kn)) (*S The main tables: constants, inductives, records, ... *) (*s Constants tables. *) -let terms = ref (KNmap.empty : ml_decl KNmap.t) -let init_terms () = terms := KNmap.empty -let add_term kn d = terms := KNmap.add kn d !terms -let lookup_term kn = KNmap.find kn !terms +let terms = ref (Cmap.empty : ml_decl Cmap.t) +let init_terms () = terms := Cmap.empty +let add_term kn d = terms := Cmap.add kn d !terms +let lookup_term kn = Cmap.find kn !terms -let types = ref (KNmap.empty : ml_schema KNmap.t) -let init_types () = types := KNmap.empty -let add_type kn s = types := KNmap.add kn s !types -let lookup_type kn = KNmap.find kn !types +let types = ref (Cmap.empty : ml_schema Cmap.t) +let init_types () = types := Cmap.empty +let add_type kn s = types := Cmap.add kn s !types +let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) @@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives (*s Recursors table. *) -let recursors = ref KNset.empty -let init_recursors () = recursors := KNset.empty +let recursors = ref Cset.empty +let init_recursors () = recursors := Cset.empty let add_recursors env kn = - let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in + let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in let mib = Environ.lookup_mind kn env in Array.iter (fun mip -> let id = mip.mind_typename in let kn_rec = make_kn (Nameops.add_suffix id "_rec") and kn_rect = make_kn (Nameops.add_suffix id "_rect") in - recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) + recursors := Cset.add kn_rec (Cset.add kn_rect !recursors)) mib.mind_packets let is_recursor = function - | ConstRef kn -> KNset.mem kn !recursors + | ConstRef kn -> Cset.mem kn !recursors | _ -> false (*s Record tables. *) @@ -109,7 +123,7 @@ let reset_tables () = done before. *) let id_of_global = function - | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index d2fcf67d7..0b69a7412 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -35,7 +35,9 @@ val check_inside_section : unit -> unit (*s utilities concerning [module_path]. *) -val kn_of_r : global_reference -> kernel_name +val occur_kn_in_ref : kernel_name -> global_reference -> bool +val modpath_of_r : global_reference -> module_path +val label_of_r : global_reference -> label val current_toplevel : unit -> module_path val base_mp : module_path -> module_path @@ -43,14 +45,15 @@ val is_modfile : module_path -> bool val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool +val visible_con : constant -> bool (*s Some table-related operations *) -val add_term : kernel_name -> ml_decl -> unit -val lookup_term : kernel_name -> ml_decl +val add_term : constant -> ml_decl -> unit +val lookup_term : constant -> ml_decl -val add_type : kernel_name -> ml_schema -> unit -val lookup_type : kernel_name -> ml_schema +val add_type : constant -> ml_schema -> unit +val lookup_type : constant -> ml_schema val add_ind : kernel_name -> ml_ind -> unit val lookup_ind : kernel_name -> ml_ind @@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_projection : int -> kernel_name -> unit +val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml index 418e6ce83..00a2260c6 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/first-order/ground.ml @@ -45,17 +45,17 @@ let update_flags ()= *) let update_flags ()= - let predref=ref Names.KNpred.empty in + let predref=ref Names.Cpred.empty in let f coe= try let kn=destConst (Classops.get_coercion_value coe) in - predref:=Names.KNpred.add kn !predref + predref:=Names.Cpred.add kn !predref with Invalid_argument "destConst"-> () in List.iter f (Classops.coercions ()); red_flags:= Closure.RedFlags.red_add_transparent Closure.betaiotazeta - (Names.Idpred.full,Names.KNpred.complement !predref) + (Names.Idpred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= update_flags (); diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index de7d0b133..33d6faad1 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -76,7 +76,7 @@ open Vernacexpr type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = - match Names.repr_kn kn with + match Names.repr_con kn with | MPfile dir, sec_dir, id when sec_dir = empty_dirpath && string_of_dirpath dir = "Coq.Reals.Rdefinitions" diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 758071bac..5797ec639 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -263,7 +263,7 @@ let def_of_const t = (* nom d'une constante. Must be a constante. x*) let name_of_const t = match (kind_of_term t) with - Const cst -> Names.string_of_label (Names.label cst) + Const cst -> Names.string_of_label (Names.con_label cst) |_ -> assert false ;; diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 3cc539063..ef3561a70 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -413,7 +413,7 @@ let inspect n = let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> - let {const_type=typ} = Global.lookup_constant kn in + let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index a08f2cd6f..0add95076 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -173,9 +173,9 @@ let constant_to_ast_list kn = let l = implicits_of_global (ConstRef kn) in (match c with None -> - make_variable_ast (id_of_label (label kn)) typ l + make_variable_ast (id_of_label (con_label kn)) typ l | Some c1 -> - make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) + make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = let (id, c, v) = get_variable sp in @@ -198,7 +198,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = let tag = object_tag lobj in match tag with | "VARIABLE" -> variable_to_ast_list (basename sp) - | "CONSTANT" -> constant_to_ast_list kn + | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn) | "INDUCTIVE" -> inductive_to_ast_list kn | s -> errorlabstrm diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 2f42af6b7..bf4539798 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -724,7 +724,7 @@ let constants_to_unfold = let transform s = let sp = path_of_string s in let dir, id = repr_path sp in - Libnames.encode_kn dir id + Libnames.encode_con dir id in List.map transform [ "Coq.ring.Ring_normalize.interp_cs"; diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index d379c5569..dca5963f9 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -83,16 +83,28 @@ let get_uri_of_var v pvars = ;; type tag = - Constant - | Inductive - | Variable + Constant of Names.constant + | Inductive of Names.kernel_name + | Variable of Names.kernel_name ;; +type etag = + TConstant + | TInductive + | TVariable +;; + +let etag_of_tag = + function + Constant _ -> TConstant + | Inductive _ -> TInductive + | Variable _ -> TVariable + let ext_of_tag = function - Constant -> "con" - | Inductive -> "ind" - | Variable -> "var" + TConstant -> "con" + | TInductive -> "ind" + | TVariable -> "var" ;; exception FunctorsXMLExportationNotImplementedYet;; @@ -147,23 +159,24 @@ let token_list_of_path dir id tag = List.rev_map N.string_of_id (N.repr_dirpath dirpath) in token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)] -let token_list_of_kernel_name kn tag = +let token_list_of_kernel_name tag = let module N = Names in let module LN = Libnames in - let dir = match tag with - | Variable -> - Lib.cwd () - | Constant -> - Lib.library_part (LN.ConstRef kn) - | Inductive -> + let id,dir = match tag with + | Variable kn -> + N.id_of_label (N.label kn), Lib.cwd () + | Constant con -> + N.id_of_label (N.con_label con), + Lib.library_part (LN.ConstRef con) + | Inductive kn -> + N.id_of_label (N.label kn), Lib.library_part (LN.IndRef (kn,0)) in - let id = N.id_of_label (N.label kn) in - token_list_of_path dir id tag + token_list_of_path dir id (etag_of_tag tag) ;; -let uri_of_kernel_name kn tag = - let tokens = token_list_of_kernel_name kn tag in +let uri_of_kernel_name tag = + let tokens = token_list_of_kernel_name tag in "cic:/" ^ String.concat "/" tokens let uri_of_declaration id tag = @@ -709,7 +722,7 @@ print_endline "PASSATO" ; flush stdout ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; let compute_result_if_eta_expansion_not_required _ _ = - A.AConst (fresh_id'', subst, (uri_of_kernel_name kn Constant)) + A.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn))) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] @@ -717,7 +730,7 @@ print_endline "PASSATO" ; flush stdout ; compute_result_if_eta_expansion_not_required | T.Ind (kn,i) -> let compute_result_if_eta_expansion_not_required _ _ = - A.AInd (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i) + A.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] @@ -729,7 +742,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; let compute_result_if_eta_expansion_not_required _ _ = A.AConstruct - (fresh_id'', subst, (uri_of_kernel_name kn Inductive), i, j) + (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] @@ -743,7 +756,7 @@ print_endline "PASSATO" ; flush stdout ; Array.fold_right (fun x i -> (aux' env idrefs x)::i) a [] in A.ACase - (fresh_id'', (uri_of_kernel_name kn Inductive), i, + (fresh_id'', (uri_of_kernel_name (Inductive kn)), i, aux' env idrefs ty, aux' env idrefs term, a') | T.Fix ((ai,i),(f,t,b)) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 46165871a..cf975b437 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -19,7 +19,7 @@ let prerr_endline _ = ();; let cprop = let module N = Names in - N.make_kn + N.make_con (N.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) (N.make_dirpath []) diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli index 33d3e5cd0..2e14b5580 100644 --- a/contrib/xml/doubleTypeInference.mli +++ b/contrib/xml/doubleTypeInference.mli @@ -14,7 +14,7 @@ type types = { synthesized : Term.types; expected : Term.types option; } -val cprop : Names.kernel_name +val cprop : Names.constant val whd_betadeltaiotacprop : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index ba9e87e0b..b9d8ac42b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -177,12 +177,12 @@ let rec join_dirs cwd = join_dirs newcwd tail ;; -let filename_of_path xml_library_root kn tag = +let filename_of_path xml_library_root tag = let module N = Names in match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> - let tokens = Cic2acic.token_list_of_kernel_name kn tag in + let tokens = Cic2acic.token_list_of_kernel_name tag in Some (join_dirs xml_library_root' tokens) ;; @@ -507,7 +507,7 @@ let print internal glob_ref kind xml_library_root = let module Ln = Libnames in (* Variables are the identifiers of the variables in scope *) let variables = search_variables () in - let kn,tag,obj = + let tag,obj = match glob_ref with Ln.VarRef id -> let sp = Declare.find_section_variable id in @@ -517,23 +517,22 @@ let print internal glob_ref kind xml_library_root = N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp)) in let (_,body,typ) = G.lookup_named id in - kn,Cic2acic.Variable,mk_variable_obj id body typ + Cic2acic.Variable kn,mk_variable_obj id body typ | Ln.ConstRef kn -> - let id = N.id_of_label (N.label kn) in + let id = N.id_of_label (N.con_label kn) in let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = G.lookup_constant kn in - kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps + Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> let {D.mind_packets=packs ; D.mind_hyps=hyps; D.mind_finite=finite} = G.lookup_mind kn in - kn,Cic2acic.Inductive, - mk_inductive_obj kn packs variables hyps finite + Cic2acic.Inductive kn,mk_inductive_obj kn packs variables hyps finite | Ln.ConstructRef _ -> Util.anomaly ("print: this should not happen") in - let fn = filename_of_path xml_library_root kn tag in - let uri = Cic2acic.uri_of_kernel_name kn tag in + let fn = filename_of_path xml_library_root tag in + let uri = Cic2acic.uri_of_kernel_name tag in if not internal then print_object_kind uri kind; print_object uri obj Evd.empty None fn ;; @@ -562,12 +561,13 @@ let show_pftreestate internal fn (kind,pftst) id = Decl_kinds.IsLocal -> let uri = "cic:/" ^ String.concat "/" - (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.Variable) in + (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable) + in let kind_of_var = "VARIABLE","LocalFact" in if not internal then print_object_kind uri kind_of_var; uri | Decl_kinds.IsGlobal _ -> - let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in + let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in if not internal then print_object_kind uri (kind_of_global_goal kind); uri in @@ -608,7 +608,7 @@ let _ = let _ = Declare.set_xml_declare_constant - (function (internal,(sp,kn)) -> + (function (internal,kn) -> match !proof_to_export with None -> print internal (Libnames.ConstRef kn) (kind_of_constant kn) @@ -616,9 +616,9 @@ let _ = | Some pftreestate -> (* It is a proof. Let's export it starting from the proof-tree *) (* I saved in the Pfedit.set_xml_cook_proof callback. *) - let fn = filename_of_path xml_library_root kn Cic2acic.Constant in + let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in show_pftreestate internal fn pftreestate - (Names.id_of_label (Names.label kn)) ; + (Names.id_of_label (Names.con_label kn)) ; proof_to_export := None) ;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 870d382f8..41151eb22 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -59,7 +59,7 @@ let prastpat c = pp(print_astpat c) let prastpatl c = pp(print_astlpat c) let safe_prglobal = function - | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")") + | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ @@ -119,7 +119,7 @@ let constr_display csr = ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")" - | Const c -> "Const("^(string_of_kn c)^")" + | Const c -> "Const("^(string_of_con c)^")" | Ind (sp,i) -> "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")" | Construct ((sp,i),j) -> @@ -200,7 +200,7 @@ let print_pure_constr csr = Array.iter (fun x -> print_space (); box_display x) l; print_string"}" | Const c -> print_string "Cons("; - sp_display c; + sp_con_display c; print_string ")" | Ind (sp,i) -> print_string "Ind("; @@ -273,6 +273,15 @@ let print_pure_constr csr = | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) print_string (string_of_kn sp) + and sp_con_display sp = +(* let dir,l = decode_kn sp in + let ls = + match List.rev (List.map string_of_id (repr_dirpath dir)) with + ("Top"::l)-> l + | ("Coq"::_::l) -> l + | l -> l + in List.iter (fun x -> print_string x; print_string ".") ls;*) + print_string (string_of_con sp) in try @@ -317,7 +326,7 @@ let ppripos (ri,pos) = | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> - print_string ("getglob "^(string_of_kn kn)^"\n")); + print_string ("getglob "^(string_of_con kn)^"\n")); print_flush () let print_vfix () = print_string "vfix" @@ -335,7 +344,7 @@ let print_idkey idk = match idk with | ConstKey sp -> print_string "Cons("; - print_string (string_of_kn sp); + print_string (string_of_con sp); print_string ")" | VarKey id -> print_string (string_of_id id) | RelKey i -> print_string "~";print_int i diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 77853ade8..87cc59b8f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -114,7 +114,7 @@ let extern_evar loc n = let raw_string_of_ref = function | ConstRef kn -> - "CONST("^(string_of_kn kn)^")" + "CONST("^(string_of_con kn)^")" | IndRef (kn,i) -> "IND("^(string_of_kn kn)^","^(string_of_int i)^")" | ConstructRef ((kn,i),j) -> diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 0d4a246a0..499554746 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -90,7 +90,7 @@ let rec instruction ppf = function print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; (* nb fv, init, lbl types, lbl bodies *) - | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id) + | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" | Kmakeblock(n, m) -> diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 421949163..1b93dc4b6 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -254,7 +254,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_kn s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv @@ -265,7 +265,7 @@ type body_code = let subst_body_code s = function | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) - | BCallias kn -> BCallias (subst_kn s kn) + | BCallias kn -> BCallias (subst_con s kn) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted diff --git a/kernel/closure.ml b/kernel/closure.ml index 51c355c9a..2f83657d0 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -51,8 +51,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Idpred.empty, KNpred.empty) -let all_transparent = (Idpred.full, KNpred.full) +let all_opaque = (Idpred.empty, Cpred.empty) +let all_transparent = (Idpred.full, Cpred.full) module type RedFlagsSig = sig type reds @@ -107,7 +107,7 @@ module RedFlags = (struct | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST kn -> let (l1,l2) = red.r_const in - { red with r_const = l1, KNpred.add kn l2 } + { red with r_const = l1, Cpred.add kn l2 } | IOTA -> { red with r_iota = true } | ZETA -> { red with r_zeta = true } | VAR id -> @@ -119,7 +119,7 @@ module RedFlags = (struct | DELTA -> { red with r_delta = false } | CONST kn -> let (l1,l2) = red.r_const in - { red with r_const = l1, KNpred.remove kn l2 } + { red with r_const = l1, Cpred.remove kn l2 } | IOTA -> { red with r_iota = false } | ZETA -> { red with r_zeta = false } | VAR id -> @@ -135,7 +135,7 @@ module RedFlags = (struct | BETA -> incr_cnt red.r_beta beta | CONST kn -> let (_,l) = red.r_const in - let c = KNpred.mem kn l in + let c = Cpred.mem kn l in incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) let (l,_) = red.r_const in @@ -149,7 +149,7 @@ module RedFlags = (struct let red_get_const red = let p1,p2 = red.r_const in let (b1,l1) = Idpred.elements p1 in - let (b2,l2) = KNpred.elements p2 in + let (b2,l2) = Cpred.elements p2 in if b1=b2 then let l1' = List.map (fun x -> EvalVarRef x) l1 in let l2' = List.map (fun x -> EvalConstRef x) l2 in diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 1504220ac..d0f5cf63e 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -11,12 +11,12 @@ open Names (* Opaque constants *) -let cst_transp = ref KNpred.full +let cst_transp = ref Cpred.full -let set_opaque_const kn = cst_transp := KNpred.remove kn !cst_transp -let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp +let set_opaque_const kn = cst_transp := Cpred.remove kn !cst_transp +let set_transparent_const kn = cst_transp := Cpred.add kn !cst_transp -let is_opaque_cst kn = not (KNpred.mem kn !cst_transp) +let is_opaque_cst kn = not (Cpred.mem kn !cst_transp) (* Opaque variables *) let var_transp = ref Idpred.full @@ -36,7 +36,7 @@ let is_opaque = function let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1) (* summary operations *) -type transparent_state = Idpred.t * KNpred.t -let init() = (cst_transp := KNpred.full; var_transp := Idpred.full) +type transparent_state = Idpred.t * Cpred.t +let init() = (cst_transp := Cpred.full; var_transp := Idpred.full) let freeze () = (!var_transp, !cst_transp) let unfreeze (vo,co) = (cst_transp := co; var_transp := vo) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 351df9d86..7fc3dabcd 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -18,8 +18,8 @@ open Names val oracle_order : 'a tableKey -> 'a tableKey -> bool (* Changing the oracle *) -val set_opaque_const : kernel_name -> unit -val set_transparent_const : kernel_name -> unit +val set_opaque_const : constant -> unit +val set_transparent_const : constant -> unit val set_opaque_var : identifier -> unit val set_transparent_var : identifier -> unit diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5c058b466..9869afcf5 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -102,7 +102,7 @@ let expmod_constr modlist c = if cb.const_opaque then errorlabstrm "expmod_constr" (str"Cannot unfold the value of " ++ - str(string_of_kn kn) ++ spc () ++ + str(string_of_con kn) ++ spc () ++ str"You cannot declare local lemmas as being opaque" ++ spc () ++ str"and then require that theorems which use them" ++ spc () ++ str"be transparent"); diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 402a0fb97..f9f03e348 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -55,9 +55,9 @@ let num_boxed = ref 0 let boxed_tbl = Hashtbl.create 53 -let cst_opaque = ref KNpred.full +let cst_opaque = ref Cpred.full -let is_opaque kn = KNpred.mem kn !cst_opaque +let is_opaque kn = Cpred.mem kn !cst_opaque let set_global_boxed kn v = let n = !num_boxed in @@ -163,12 +163,12 @@ and val_of_constr env c = eval_to_patch env (to_memory ccfv) let set_transparent_const kn = - cst_opaque := KNpred.remove kn !cst_opaque; + cst_opaque := Cpred.remove kn !cst_opaque; List.iter (fun n -> (global_boxed()).(n) <- false) (Hashtbl.find_all boxed_tbl kn) let set_opaque_const kn = - cst_opaque := KNpred.add kn !cst_opaque; + cst_opaque := Cpred.add kn !cst_opaque; List.iter (fun n -> (global_boxed()).(n) <- true) (Hashtbl.find_all boxed_tbl kn) diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 5fafbac49..4c56fc947 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -4,5 +4,5 @@ open Environ val val_of_constr : env -> constr -> values -val set_opaque_const : kernel_name -> unit -val set_transparent_const : kernel_name -> unit +val set_opaque_const : constant -> unit +val set_transparent_const : constant -> unit diff --git a/kernel/environ.ml b/kernel/environ.ml index d9569bca6..a6d7ff65b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -29,7 +29,7 @@ type constant_key = constant_body * key type engagement = ImpredicativeSet type globals = { - env_constants : constant_key KNmap.t; + env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body KNmap.t } @@ -57,7 +57,7 @@ and env = { let empty_env = { env_globals = { - env_constants = KNmap.empty; + env_constants = Cmap.empty; env_inductives = KNmap.empty; env_modules = MPmap.empty; env_modtypes = KNmap.empty }; @@ -218,13 +218,13 @@ let set_pos_constant (cb,r) bpos = else raise AllReadyEvaluated let lookup_constant_key kn env = - KNmap.find kn env.env_globals.env_constants + Cmap.find kn env.env_globals.env_constants let lookup_constant kn env = constant_key_body (lookup_constant_key kn env) let add_constant kn cs env = let new_constants = - KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in + Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index a3639ef98..9f5a5e9a8 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -143,13 +143,14 @@ and translate_entry_list env msid is_definition sig_e = let mp = MPself msid in let do_entry env (l,e) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match e with | SPEconst ce -> - let cb = translate_constant env kn ce in + let cb = translate_constant env con ce in begin match cb.const_hyps with | (_::_) -> error_local_context (Some l) | [] -> - add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb) + add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb) end | SPEmind mie -> let mib = translate_mind env mie in diff --git a/kernel/modops.ml b/kernel/modops.ml index 5a0694cbe..aca663e7c 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -163,8 +163,9 @@ let subst_signature_msid msid mp = let rec add_signature mp sign env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match elem with - | SPBconst cb -> Environ.add_constant kn cb env + | SPBconst cb -> Environ.add_constant con cb env | SPBmind mib -> Environ.add_mind kn mib env | SPBmodule mb -> add_module (MPdot (mp,l)) (module_body_of_spec mb) env @@ -189,7 +190,7 @@ let strengthen_const env mp l cb = | false, Some _ -> cb | true, Some _ | _, None -> - let const = mkConst (make_kn mp empty_dirpath l) in + let const = mkConst (make_con mp empty_dirpath l) in let const_subs = Some (Declarations.from_val const) in {cb with const_body = const_subs; diff --git a/kernel/names.ml b/kernel/names.ml index 8211cf845..db1b1b6df 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -273,6 +273,9 @@ end module KNmap = Map.Make(KNord) module KNpred = Predicate.Make(KNord) module KNset = Set.Make(KNord) +module Cmap = KNmap +module Cpred = KNpred +module Cset = KNset let default_module_name = id_of_string "If you see this, it's a bug" @@ -288,6 +291,15 @@ type mutual_inductive = kernel_name type inductive = mutual_inductive * int type constructor = inductive * int +let constant_of_kn kn = kn +let make_con mp dir l = (mp,dir,l) +let repr_con con = con +let string_of_con = string_of_kn +let con_label = label +let pr_con = pr_kn +let con_modpath = modpath +let subst_con = subst_kn + let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind @@ -373,12 +385,12 @@ let hcons_names () = let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in - (hkn,hdir,hname,hident,hstring) + (hkn,hkn,hdir,hname,hident,hstring) (*******) -type transparent_state = Idpred.t * KNpred.t +type transparent_state = Idpred.t * Cpred.t type 'a tableKey = | ConstKey of constant diff --git a/kernel/names.mli b/kernel/names.mli index a08d1be23..8cda7d958 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -158,13 +158,26 @@ module KNmap : Map.S with type key = kernel_name (*s Specific paths for declarations *) type variable = identifier -type constant = kernel_name +type constant type mutual_inductive = kernel_name (* Beware: first inductive has index 0 *) type inductive = mutual_inductive * int (* Beware: first constructor has index 1 *) type constructor = inductive * int +module Cmap : Map.S with type key = constant +module Cpred : Predicate.S with type elt = constant +module Cset : Set.S with type elt = constant + +val constant_of_kn : kernel_name -> constant +val make_con : module_path -> dir_path -> label -> constant +val repr_con : constant -> module_path * dir_path * label +val string_of_con : constant -> string +val con_label : constant -> label +val con_modpath : constant -> module_path +val pr_con : constant -> Pp.std_ppcmds +val subst_con : substitution -> constant -> constant + val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive @@ -177,6 +190,7 @@ type evaluable_global_reference = (* Hash-consing *) val hcons_names : unit -> + (constant -> constant) * (kernel_name -> kernel_name) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * (string -> string) @@ -188,7 +202,7 @@ type 'a tableKey = | VarKey of identifier | RelKey of 'a -type transparent_state = Idpred.t * KNpred.t +type transparent_state = Idpred.t * Cpred.t type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7e5e91944..737f77184 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -132,7 +132,7 @@ let hcons_constant_body cb = let add_constant dir l decl senv = check_label l senv.labset; - let kn = make_kn senv.modinfo.modpath dir l in + let kn = make_con senv.modinfo.modpath dir l in let cb = match decl with | ConstantEntry ce -> translate_constant senv.env kn ce diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f59b5c375..9b5d78870 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -44,7 +44,7 @@ type global_declaration = val add_constant : dir_path -> label -> global_declaration -> safe_environment -> - kernel_name * safe_environment + constant * safe_environment (* Adding an inductive type *) val add_mind : diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 6bd88c8cd..2f39dc61a 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -174,7 +174,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 = let c2 = Declarations.force lc2 in let c1 = match cb1.const_body with | Some lc1 -> Declarations.force lc1 - | None -> mkConst (make_kn (MPself msid1) empty_dirpath l) + | None -> mkConst (make_con (MPself msid1) empty_dirpath l) in check_conv cst conv env c1 c2 diff --git a/kernel/term.ml b/kernel/term.ml index 1855858ca..21ab2ea5d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -148,7 +148,7 @@ let comp_term t1 t2 = & array_for_all2 (==) bl1 bl2 | _ -> false -let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t = +let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t = match t with | Rel _ -> t | Meta x -> Meta x @@ -160,7 +160,7 @@ let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t = | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c) | App (c,l) -> App (sh_rec c, Array.map sh_rec l) | Evar (e,l) -> Evar (e, Array.map sh_rec l) - | Const c -> Const (sh_kn c) + | Const c -> Const (sh_con c) | Ind (kn,i) -> Ind (sh_kn kn,i) | Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j) | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *) @@ -179,15 +179,16 @@ module Hconstr = struct type t = constr type u = (constr -> constr) * - ((sorts -> sorts) * (kernel_name -> kernel_name) - * (name -> name) * (identifier -> identifier)) + ((sorts -> sorts) * (constant -> constant) * + (kernel_name -> kernel_name) * (name -> name) * + (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term let hash = Hashtbl.hash end) -let hcons_term (hsorts,hkn,hname,hident) = - Hashcons.recursive_hcons Hconstr.f (hsorts,hkn,hname,hident) +let hcons_term (hsorts,hcon,hkn,hname,hident) = + Hashcons.recursive_hcons Hconstr.f (hsorts,hcon,hkn,hname,hident) (* Constructs a DeBrujin index with number n *) let rels = @@ -797,11 +798,11 @@ necessary. For now, it uses map_constr and is rather ineffective *) -let rec map_kn f c = - let func = map_kn f in +let rec map_kn f f_con c = + let func = map_kn f f_con in match kind_of_term c with | Const kn -> - mkConst (f kn) + mkConst (f_con kn) | Ind (kn,i) -> mkInd (f kn,i) | Construct ((kn,i),j) -> @@ -812,7 +813,7 @@ let rec map_kn f c = | _ -> map_constr func c let subst_mps sub = - map_kn (subst_kn sub) + map_kn (subst_kn sub) (subst_con sub) (*********************) @@ -1178,9 +1179,9 @@ module Hsorts = let hsort = Hsorts.f -let hcons_constr (hkn,hdir,hname,hident,hstr) = +let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) = let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in - let hcci = hcons_term (hsortscci,hkn,hname,hident) in + let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in (hcci,htcci) diff --git a/kernel/term.mli b/kernel/term.mli index 5ef42f96c..2b84f79ba 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -512,6 +512,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool (*********************************************************************) val hcons_constr: + (constant -> constant) * (kernel_name -> kernel_name) * (dir_path -> dir_path) * (name -> name) * diff --git a/kernel/univ.ml b/kernel/univ.ml index 9d38c78f5..fb372d2f8 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -465,6 +465,6 @@ module Huniv = end) let hcons1_univ u = - let _,hdir,_,_,_ = Names.hcons_names() in + let _,_,hdir,_,_,_ = Names.hcons_names() in Hashcons.simple_hcons Huniv.f hdir u diff --git a/library/declare.ml b/library/declare.ml index ea986e3fb..ecf223ae0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -142,9 +142,9 @@ let cache_constant ((sp,kn),(cdt,kind)) = errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); let _,dir,_ = repr_kn kn in let kn' = Global.add_constant dir (basename sp) cdt in - if kn' <> kn then + if kn' <> (constant_of_kn kn) then anomaly "Kernel and Library names do not match"; - Nametab.push (Nametab.Until 1) sp (ConstRef kn); + Nametab.push (Nametab.Until 1) sp (ConstRef kn'); csttab := Spmap.add sp kind !csttab (* At load-time, the segment starting from the module name to the discharge *) @@ -154,11 +154,11 @@ let load_constant i ((sp,kn),(_,kind)) = let (_,id) = repr_path sp in errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); csttab := Spmap.add sp kind !csttab; - Nametab.push (Nametab.Until i) sp (ConstRef kn) + Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)) (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - Nametab.push (Nametab.Exactly i) sp (ConstRef kn) + Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) @@ -190,16 +190,17 @@ let hcons_constant_declaration = function let declare_constant_common id discharged_hyps (cd,kind) = let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in + let kn = constant_of_kn kn in declare_constant_implicits kn; Symbols.declare_ref_arguments_scope (ConstRef kn); Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; - oname + kn let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in - let oname = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant (internal,oname); - oname + let kn = declare_constant_common id [] (ConstantEntry cd,kind) in + !xml_declare_constant (internal,kn); + kn let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false diff --git a/library/declare.mli b/library/declare.mli index a025982ee..6af513888 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -52,10 +52,11 @@ type constant_declaration = constant_entry * global_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> object_name +val declare_constant : + identifier -> constant_declaration -> constant val declare_internal_constant : - identifier -> constant_declaration -> object_name + identifier -> constant_declaration -> constant val redeclare_constant : identifier -> Dischargedhypsmap.discharged_hyps -> @@ -98,5 +99,5 @@ val strength_of_global : global_reference -> strength (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (bool * object_name -> unit) -> unit +val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index 70ab9b563..9468f3ef5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -40,7 +40,7 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints functions verify that given names match those generated by kernel *) val add_constant : - dir_path -> identifier -> global_declaration -> kernel_name + dir_path -> identifier -> global_declaration -> constant val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name diff --git a/library/impargs.ml b/library/impargs.ml index 5bf920014..d77543367 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -289,7 +289,7 @@ let list_of_implicits = function (*s Constants. *) -let constants_table = ref KNmap.empty +let constants_table = ref Cmap.empty let compute_constant_implicits kn = let env = Global.env () in @@ -297,7 +297,7 @@ let compute_constant_implicits kn = auto_implicits env (body_of_type cb.const_type) let constant_implicits sp = - try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl + try Cmap.find sp !constants_table with Not_found -> No_impl,No_impl (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -349,7 +349,7 @@ let cache_implicits_decl (r,imps) = | VarRef id -> var_table := Idmap.add id imps !var_table | ConstRef kn -> - constants_table := KNmap.add kn imps !constants_table + constants_table := Cmap.add kn imps !constants_table | IndRef indp -> inductives_table := Indmap.add indp imps !inductives_table; | ConstructRef consp -> @@ -485,7 +485,7 @@ let test_if_implicit find a = with Not_found -> (false,false,false),(false,false,false) let is_implicit_constant sp = - test_if_implicit (KNmap.find sp) !constants_table + test_if_implicit (Cmap.find sp) !constants_table let is_implicit_inductive_definition indp = test_if_implicit (Indmap.find (indp,0)) !inductives_table @@ -496,7 +496,7 @@ let is_implicit_var id = (*s Registration as global tables *) let init () = - constants_table := KNmap.empty; + constants_table := Cmap.empty; inductives_table := Indmap.empty; constructors_table := Constrmap.empty; var_table := Idmap.empty diff --git a/library/lib.ml b/library/lib.ml index c27c9c04c..16521e627 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -105,6 +105,10 @@ let make_kn id = let mp,dir = current_prefix () in Names.make_kn mp dir (label_of_id id) +let make_con id = + let mp,dir = current_prefix () in + Names.make_con mp dir (label_of_id id) + let make_oname id = make_path id, make_kn id diff --git a/library/lib.mli b/library/lib.mli index d80822056..438754a38 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -82,6 +82,7 @@ val make_path : identifier -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path val make_kn : identifier -> kernel_name +val make_con : identifier -> constant (* Are we inside an opened section *) val sections_are_opened : unit -> bool diff --git a/library/libnames.ml b/library/libnames.ml index 17fd50b7f..2fe8f724c 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -23,7 +23,7 @@ type global_reference = let subst_global subst ref = match ref with | VarRef _ -> ref | ConstRef kn -> - let kn' = subst_kn subst kn in if kn==kn' then ref else + let kn' = subst_con subst kn in if kn==kn' then ref else ConstRef kn' | IndRef (kn,i) -> let kn' = subst_kn subst kn in if kn==kn' then ref else @@ -190,6 +190,8 @@ type extended_global_reference = let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) +let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) + let decode_kn kn = let mp,sec_dir,l = repr_kn kn in match mp,(repr_dirpath sec_dir) with @@ -197,6 +199,13 @@ let decode_kn kn = | _ , [] -> anomaly "MPfile expected!" | _ -> anomaly "Section part should be empty!" +let decode_con kn = + let mp,sec_dir,l = repr_con kn in + match mp,(repr_dirpath sec_dir) with + MPfile dir,[] -> (dir,id_of_label l) + | _ , [] -> anomaly "MPfile expected!" + | _ -> anomaly "Section part should be empty!" + (*s qualified names *) type qualid = section_path diff --git a/library/libnames.mli b/library/libnames.mli index ffb51ec0b..539aa0b96 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -86,6 +86,8 @@ type extended_global_reference = val encode_kn : dir_path -> identifier -> kernel_name val decode_kn : kernel_name -> dir_path * identifier +val encode_con : dir_path -> identifier -> constant +val decode_con : constant -> dir_path * identifier (*s A [qualid] is a partially qualified ident; it includes fully diff --git a/parsing/ast.ml b/parsing/ast.ml index 83cd633c1..e366600c8 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -28,6 +28,7 @@ let loc = function | Id (loc,_) -> loc | Str (loc,_) -> loc | Path (loc,_) -> loc + | ConPath (loc,_) -> loc | Dynamic (loc,_) -> loc (* patterns of ast *) @@ -58,6 +59,7 @@ let nvar s = Nvar(dummy_loc,s) let num n = Num(dummy_loc,n) let string s = Str(dummy_loc,s) let path sl = Path(dummy_loc,sl) +let conpath sl = ConPath(dummy_loc,sl) let dynamic d = Dynamic(dummy_loc,d) let rec set_loc loc = function @@ -70,11 +72,11 @@ let rec set_loc loc = function | Str(_,s) -> Str(loc,s) | Num(_,s) -> Num(loc,s) | Path(_,sl) -> Path(loc,sl) + | ConPath(_,sl) -> ConPath(loc,sl) | Dynamic(_,d) -> Dynamic(loc,d) let path_section loc sp = Coqast.Path(loc, sp) - -let section_path sp = sp +let conpath_section loc sp = Coqast.ConPath(loc, sp) (* ast destructors *) let num_of_ast = function @@ -129,19 +131,23 @@ let string_of_dirpath = function let pr_id id = str (string_of_id id) -let print_kn kn = - let (mp,dp,l) = repr_kn kn in +let print_kn_or_con repr kn = + let (mp,dp,l) = repr kn in let dpl = repr_dirpath dp in str (string_of_mp mp) ++ str "." ++ prlist_with_sep (fun _ -> str".") pr_id dpl ++ str (string_of_label l) +let print_kn = print_kn_or_con repr_kn +let print_con = print_kn_or_con repr_con + (* Pretty-printing *) let rec print_ast ast = match ast with | Num(_,n) -> int n | Str(_,s) -> qs s | Path(_,sl) -> print_kn sl + | ConPath(_,sl) -> print_con sl | Id (_,s) -> str "{" ++ str s ++ str "}" | Nvar(_,s) -> pr_id s | Nmeta(_,s) -> str s @@ -208,6 +214,7 @@ let check_cast loc a k = | (Tid, Id _) -> () | (Tvar, Nvar _) -> () | (Tpath, Path _) -> () + | (Tpath, ConPath _) -> () | (Tstr, Str _) -> () | (Tnum, Num _) -> () | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val") @@ -291,6 +298,7 @@ let rec alpha alp a1 a2 = | (Str(_,s1),Str(_,s2)) -> s1=s2 | (Num(_,n1),Num(_,n2)) -> n1=n2 | (Path(_,sl1),Path(_,sl2)) -> sl1=sl2 + | (ConPath(_,sl1),ConPath(_,sl2)) -> sl1=sl2 | ((Smetalam _ | Nmeta _ | Dynamic _), _) -> false | (_, (Smetalam _ | Nmeta _ | Dynamic _)) -> false | _ -> false @@ -356,6 +364,7 @@ let rec amatch alp sigma spat ast = | (Pmeta(pv,Tnum), Num _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tstr), Str _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tpath), Path _) -> bind_env_ast sigma pv ast + | (Pmeta(pv,Tpath), ConPath _) -> bind_env_ast sigma pv ast | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch") | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) -> amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b @@ -472,7 +481,7 @@ let rec pat_of_ast env ast = (Pnode(op,pargs), env') (* Compatibility with new parsing mode *) | Nvar(loc,id) when (string_of_id id).[0] = '$' -> make_astvar env loc (string_of_id id) Tany - | (Path _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env) + | (Path _|ConPath _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env) | Dynamic(loc,_) -> invalid_arg_loc(loc,"pat_of_ast: dynamic") @@ -546,7 +555,7 @@ let rec val_of_ast env = function | Smetalam(loc,s,a) -> let _ = type_of_meta env loc s in (* ids are coerced to id lists *) Pmeta_slam(s, val_of_ast env a) - | (Path _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast) + | (Path _|ConPath _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast) | Slam(_,os,b) -> Pslam(os, val_of_ast env b) | Node(loc,op,_) when isMeta op -> user_err_loc(loc,"Ast.val_of_ast", @@ -577,7 +586,7 @@ let rec occur_var_ast s = function | Node(loc,op,args) -> List.exists (occur_var_ast s) args | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here" | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body - | Id _ | Str _ | Num _ | Path _ -> false + | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false | Dynamic _ -> (* Hum... what to do here *) false diff --git a/parsing/ast.mli b/parsing/ast.mli index e6049f40e..28e8e132f 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -35,7 +35,7 @@ val dynamic : Dyn.t -> Coqast.t val set_loc : loc -> Coqast.t -> Coqast.t val path_section : loc -> kernel_name -> Coqast.t -val section_path : kernel_name -> kernel_name +val conpath_section : loc -> constant -> Coqast.t (* ast destructors *) val num_of_ast : Coqast.t -> int diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 71dfd9547..52681fe34 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -24,6 +24,7 @@ type t = | Str of loc * string | Id of loc * string | Path of loc * kernel_name + | ConPath of loc * constant | Dynamic of loc * Dyn.t type the_coq_ast = t @@ -62,8 +63,9 @@ module Hast = Hashcons.Make( type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string) - * (identifier -> identifier) * (kernel_name -> kernel_name)) - let hash_sub (hast,(hloc,hstr,hid,hsp)) = function + * (identifier -> identifier) * (kernel_name -> kernel_name) + * (constant -> constant)) + let hash_sub (hast,(hloc,hstr,hid,hsp,hcon)) = function | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al) | Nmeta(l,s) -> Nmeta(hloc l, hstr s) | Nvar(l,s) -> Nvar(hloc l, hid s) @@ -74,6 +76,7 @@ module Hast = Hashcons.Make( | Id(l,s) -> Id(hloc l, hstr s) | Str(l,s) -> Str(hloc l, hstr s) | Path(l,d) -> Path(hloc l, hsp d) + | ConPath(l,d) -> ConPath(hloc l, hcon d) | Dynamic(l,d) -> Dynamic(hloc l, d) let equal a1 a2 = match (a1,a2) with @@ -89,13 +92,14 @@ module Hast = Hashcons.Make( | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2 | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2 | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2) + | (ConPath(l1,d1), ConPath(l2,d2)) -> (l1==l2 & d1==d2) | _ -> false let hash = Hashtbl.hash end) -let hcons_ast (hstr,hid,hpath) = +let hcons_ast (hstr,hid,hpath,hconpath) = let hloc = Hashcons.simple_hcons Hloc.f () in - let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in + let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in (hast,hloc) let rec subst_ast subst ast = match ast with @@ -115,6 +119,10 @@ let rec subst_ast subst ast = match ast with let kn' = Names.subst_kn subst kn in if kn' == kn then ast else Path(loc,kn') + | ConPath (loc,kn) -> + let kn' = Names.subst_con subst kn in + if kn' == kn then ast else + ConPath(loc,kn') | Nmeta _ | Nvar _ -> ast | Num _ diff --git a/parsing/coqast.mli b/parsing/coqast.mli index 219e04f03..fcb029319 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -26,6 +26,7 @@ type t = | Str of loc * string | Id of loc * string | Path of loc * kernel_name + | ConPath of loc * constant | Dynamic of loc * Dyn.t (* returns the list of metas occuring in the ast *) @@ -38,7 +39,7 @@ val subst_meta : (int * t) list -> t -> t (* hash-consing function *) val hcons_ast: (string -> string) * (Names.identifier -> Names.identifier) - * (kernel_name -> kernel_name) + * (kernel_name -> kernel_name) * (constant -> constant) -> (t -> t) * (loc -> loc) val subst_ast: Names.substitution -> t -> t diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 77e5a7526..464c1fffd 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -41,7 +41,7 @@ type key = let warning_verbose = ref true let ast_keys = function - | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) -> + | Node(_,"APPLIST", Node(_,"CONST", [ConPath (_,sl)]) ::_) -> [Cst sl; Nod "APPLIST"; All] | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) -> [SecVar s; Nod "APPLIST"; All] @@ -57,7 +57,7 @@ let spat_key astp = match astp with | Pnode("APPLIST", Pcons(Pnode("CONST", - Pcons(Pquote(Path (_,sl)),_)), _)) + Pcons(Pquote(ConPath (_,sl)),_)), _)) -> Cst sl | Pnode("APPLIST", Pcons(Pnode("SECVAR", @@ -165,7 +165,7 @@ let _ = declare_primitive_printer "token" token_printer (* A printer for the tokens. *) let token_printer stdpr = function - | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast + | (Id _ | Num _ | Str _ | Path _ | ConPath _ as ast) -> print_ast ast | a -> stdpr a (* Unused ?? diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 8f5aad33b..72f54721a 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -175,7 +175,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] (* TODO: temporary hack *) -let make_path dir id = Libnames.encode_kn dir (id_of_string id) +let make_path dir id = Libnames.encode_con dir (id_of_string id) let glob_R = ConstRef (make_path rdefinitions "R") let glob_R1 = ConstRef (make_path rdefinitions "R1") diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f84aa664b..e30823078 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -363,7 +363,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = | (_,"VARIABLE") -> Some (print_section_variable (basename sp)) | (_,"CONSTANT") -> - Some (print_constant with_values sep kn) + Some (print_constant with_values sep (constant_of_kn kn)) | (_,"INDUCTIVE") -> Some (print_inductive kn) | (_,"MODULE") -> @@ -552,7 +552,7 @@ let print_local_context () = | (oname,Lib.Leaf lobj)::rest -> (match object_tag lobj with | "CONSTANT" -> - let kn = snd oname in + let kn = constant_of_kn (snd oname) in let {const_body=val_0;const_type=typ} = Global.lookup_constant kn in (print_last_const rest ++ diff --git a/parsing/printer.ml b/parsing/printer.ml index 06a1cc812..757b61aa1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -46,7 +46,7 @@ let dfltpr ast = (str"#GENTERM " ++ print_ast ast);; let global_const_name kn = try pr_global Idset.empty (ConstRef kn) with Not_found -> (* May happen in debug *) - (str ("CONST("^(string_of_kn kn)^")")) + (str ("CONST("^(string_of_con kn)^")")) let global_var_name id = try pr_global Idset.empty (VarRef id) @@ -67,14 +67,14 @@ let global_constr_name ((kn,tyi),i) = let globpr gt = match gt with | Nvar(_,s) -> (pr_id s) | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) - | Node(_,"CONST",[Path(_,sl)]) -> - global_const_name (section_path sl) + | Node(_,"CONST",[ConPath(_,sl)]) -> + global_const_name sl | Node(_,"SECVAR",[Nvar(_,s)]) -> global_var_name s | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> - global_ind_name (section_path sl, tyi) + global_ind_name (sl, tyi) | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> - global_constr_name ((section_path sl, tyi), i) + global_constr_name ((sl, tyi), i) | Dynamic(_,d) -> if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>") else dfltpr gt diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index ec1e6410e..e1bb51dd7 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -85,6 +85,14 @@ let rec mlexpr_of_ast = function let e = expr_list_of_var_list e in <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) (Names.id_of_string $str:Names.string_of_id a$)) >> + | Coqast.ConPath (loc, kn) -> + let l,a = Libnames.decode_con kn in + let mlexpr_of_modid id = + <:expr< Names.id_of_string $str:string_of_id id$ >> in + let e = List.map mlexpr_of_modid (repr_dirpath l) in + let e = expr_list_of_var_list e in + <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$) + (Names.id_of_string $str:Names.string_of_id a$)) >> | Coqast.Dynamic (_, _) -> failwith "Q_Coqast: dynamic: not implemented" diff --git a/parsing/termast.ml b/parsing/termast.ml index 021025f74..efa6c9206 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -119,7 +119,7 @@ let ast_body_of_binder bl t = bl t let ast_of_constant_ref sp = - ope("CONST", [path_section dummy_loc sp]) + ope("CONST", [conpath_section dummy_loc sp]) let ast_of_existential_ref ev = (* 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 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 00dc19332..d447a97e8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1860,7 +1860,7 @@ let subst_induction_arg subst = function let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_kn subst kn) + | EvalConstRef kn -> EvalConstRef (subst_con subst kn) let subst_and_short_name f (c,n) = assert (n=None); (* since tacdef are strictly globalized *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 0a0589e96..e30bb7e63 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -339,7 +339,7 @@ let general_elim_then_using | _ -> let name_elim = match kind_of_term elim with - | Const kn -> string_of_kn kn + | Const kn -> string_of_con kn | Var id -> string_of_id id | _ -> "\b" in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dc2865be4..314bcd55f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1880,9 +1880,9 @@ let abstract_subproof name tac gls = (delete_current_proof(); raise e) in (* Faudrait un peu fonctionnaliser cela *) let cd = Entries.DefinitionEntry const in - let sp = Declare.declare_internal_constant na (cd,IsProof Lemma) in + let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in let newenv = Global.env() in - constr_of_reference (ConstRef (snd sp)) + constr_of_reference (ConstRef con) in exact_no_check (applist (lemme, diff --git a/toplevel/class.ml b/toplevel/class.ml index 3d468d328..c9ed58c79 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -150,7 +150,7 @@ let uniform_cond nargs lt = let id_of_cl = function | CL_FUN -> id_of_string "FUNCLASS" | CL_SORT -> id_of_string "SORTCLASS" - | CL_CONST kn -> id_of_label (label kn) + | CL_CONST kn -> id_of_label (con_label kn) | CL_IND ind -> let (_,mip) = Global.lookup_inductive ind in mip.mind_typename @@ -271,7 +271,7 @@ let build_id_coercion idf_opt source = const_entry_type = Some typ_f; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()} in - let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in + let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in ConstRef kn let check_source = function @@ -390,13 +390,17 @@ let defined_in_sec kn olddir = let _,dir,_ = repr_kn kn in dir = olddir +let con_defined_in_sec kn olddir = + let _,dir,_ = repr_con kn in + dir = olddir + (* This moves the global path one step below *) let process_global olddir = function | VarRef _ -> anomaly "process_global only processes global surviving the section" | ConstRef kn as x -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in + if con_defined_in_sec kn olddir then + let newkn = Lib.make_con (id_of_label (con_label kn)) in ConstRef newkn else x | IndRef (kn,i) as x -> @@ -416,8 +420,8 @@ let process_class olddir ids_to_discard x = match cl with | CL_SECVAR _ -> x | CL_CONST kn -> - if defined_in_sec kn olddir then - let newkn = Lib.make_kn (id_of_label (label kn)) in + if con_defined_in_sec kn olddir then + let newkn = Lib.make_con (id_of_label (con_label kn)) in let hyps = (Global.lookup_constant kn).const_hyps in let n = count_extra_abstractions hyps ids_to_discard in (CL_CONST newkn,{cl_strength=stre;cl_param=p+n}) @@ -437,8 +441,8 @@ let process_cl sec_sp cl = match cl with | CL_SECVAR id -> cl | CL_CONST kn -> - if defined_in_sec kn sec_sp then - let newkn = Lib.make_kn (id_of_label (label kn)) in + if con_defined_in_sec kn sec_sp then + let newkn = Lib.make_con (id_of_label (con_label kn)) in CL_CONST newkn else cl diff --git a/toplevel/command.ml b/toplevel/command.ml index 8eaab89d3..a17d44666 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -113,7 +113,7 @@ let red_constant_entry ce = function reduction_of_redexp red (Global.env()) Evd.empty body } let declare_global_definition ident ce local = - let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in + let kn = declare_constant ident (DefinitionEntry ce,IsDefinition) in if local = Local then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; @@ -166,7 +166,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = str" is not visible from current goals"); VarRef ident | (Global|Local) -> - let (_,kn) = + let kn = declare_constant ident (ParameterEntry c, IsAssumption kind) in assumption_message ident; if local=Local & Options.is_verbose () then @@ -215,7 +215,7 @@ let declare_one_elimination ind = if List.mem InType kelim then let elim = make_elim (new_sort_in_family InType) in let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in - let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in + let c = mkConst cte and t = constant_type (Global.env()) cte in List.iter (fun (sort,suff) -> let (t',c') = Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort) @@ -514,7 +514,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = boxed} in - let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in + let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in (* declare the recursive definitions *) @@ -581,7 +581,7 @@ let build_corecursive lnameardef boxed = const_entry_opaque = false; const_entry_boxed = boxed } in - let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in + let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in let lrefrec = Array.mapi declare namerec in @@ -621,7 +621,7 @@ let build_scheme lnamedepindsort = const_entry_type = Some decltype; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions() } in - let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in + let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in ConstRef kn :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in @@ -666,11 +666,11 @@ let save id const kind hook = (Local, VarRef id) | IsLocal -> let k = IsDefinition in - let _,kn = declare_constant id (DefinitionEntry const, k) in + let kn = declare_constant id (DefinitionEntry const, k) in (Global, ConstRef kn) | IsGlobal k -> let k = theorem_kind_of_goal_kind k in - let _,kn = declare_constant id (DefinitionEntry const, k) in + let kn = declare_constant id (DefinitionEntry const, k) in (Global, ConstRef kn) in hook l r; Pfedit.delete_current_proof (); @@ -707,7 +707,7 @@ let admit () = if k <> IsGlobal (Proof Conjecture) then error "Only statements declared as conjecture can be admitted"; *) - let (_,kn) = + let kn = declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in hook Global (ConstRef kn); Pfedit.delete_current_proof (); diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index b1ba1f748..443fd61e1 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -41,6 +41,10 @@ let recalc_kn dir kn = let (mp,_,l) = Names.repr_kn kn in Names.make_kn mp dir l +let recalc_con dir con = + let (mp,_,l) = Names.repr_con con in + Names.make_con mp dir l + let rec find_var id = function | [] -> false | (x,b,_)::l -> if x = id then b=None else find_var id l @@ -214,10 +218,10 @@ let process_object oldenv olddir full_olddir newdir (* CONSTANT means never discharge (though visibility may vary) *) let kind = constant_kind sp in let kn = Nametab.locate_constant (qualid_of_sp sp) in - let lab = label kn in + let lab = con_label kn in let cb = Environ.lookup_constant kn oldenv in let imp = is_implicit_constant kn in - let newkn = recalc_kn newdir kn in + let newkn = recalc_con newdir kn in let abs_vars,discharged_hyps0 = build_abstract_list full_olddir cb.const_hyps ids_to_discard in (* let's add the new discharged hypothesis to those already discharged*) @@ -268,12 +272,12 @@ let process_object oldenv olddir full_olddir newdir let mib = Environ.lookup_mind newkn (Global.env ()) in { s_CONST = info.s_CONST; s_PARAM = mib.mind_packets.(0).mind_nparams; - s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in + s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist) | "OBJDEF1" -> let kn = outObjDef1 lobj in - let new_kn = recalc_kn newdir kn in + let new_kn = recalc_con newdir kn in ((Objdef new_kn)::ops, ids_to_discard, work_alist) | "REQUIRE" -> diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index bc037f851..de6778291 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1110,7 +1110,7 @@ let rec reify_meta_ast vars = function Smetalam (loc,string_of_id id,reify_meta_ast vars body) | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body) | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id) - | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a + | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ | ConPath _ as a -> a | Dynamic _ as a -> (* Hum... what to do here *) a (* For old ast syntax *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 91f5b4ad8..ee189377d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -176,7 +176,7 @@ let declare_projections indsp coers fields = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in - let (sp,kn) = + let kn = try let cie = { const_entry_body = proj; @@ -184,9 +184,9 @@ let declare_projections indsp coers fields = const_entry_opaque = false; const_entry_boxed = false } in let k = (DefinitionEntry cie,IsDefinition) in - let sp = declare_internal_constant fid k in + let kn = declare_internal_constant fid k in Options.if_verbose message (string_of_id fid ^" is defined"); - sp + kn with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = ConstRef kn in |