diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |