diff options
| -rw-r--r-- | checker/declarations.ml | 58 | ||||
| -rw-r--r-- | checker/environ.ml | 20 | ||||
| -rw-r--r-- | checker/indtypes.ml | 8 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 4 | ||||
| -rw-r--r-- | checker/modops.ml | 2 | ||||
| -rw-r--r-- | checker/print.ml | 4 | ||||
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/typeops.ml | 8 | ||||
| -rw-r--r-- | kernel/names.mli | 2 |
9 files changed, 56 insertions, 52 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 3ce312533..1fe02c8b6 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -73,32 +73,32 @@ let solve_delta_kn resolve kn = | Equiv kn1 -> kn1 | Inline _ -> raise Not_found with Not_found -> - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - make_kn new_mp dir l + KerName.make new_mp dir l let gen_of_delta resolve x kn fix_can = let new_kn = solve_delta_kn resolve kn in if kn == new_kn then x else fix_can new_kn let constant_of_delta resolve con = - let kn = user_con con in - gen_of_delta resolve con kn (constant_of_kn_equiv kn) + let kn = Constant.user con in + gen_of_delta resolve con kn (Constant.make kn) let constant_of_delta2 resolve con = - let kn, kn' = canonical_con con, user_con con in - gen_of_delta resolve con kn (constant_of_kn_equiv kn') + let kn, kn' = Constant.canonical con, Constant.user con in + gen_of_delta resolve con kn (Constant.make kn') let mind_of_delta resolve mind = - let kn = user_mind mind in - gen_of_delta resolve mind kn (mind_of_kn_equiv kn) + let kn = MutInd.user mind in + gen_of_delta resolve mind kn (MutInd.make kn) let mind_of_delta2 resolve mind = - let kn, kn' = canonical_mind mind, user_mind mind in - gen_of_delta resolve mind kn (mind_of_kn_equiv kn') + let kn, kn' = MutInd.canonical mind, MutInd.user mind in + gen_of_delta resolve mind kn (MutInd.make kn') let find_inline_of_delta kn resolve = match Deltamap.find_kn kn resolve with @@ -106,7 +106,7 @@ let find_inline_of_delta kn resolve = | _ -> raise Not_found let constant_of_delta_with_inline resolve con = - let kn1,kn2 = canonical_con con,user_con con in + let kn1,kn2 = Constant.canonical con, Constant.user con in try find_inline_of_delta kn2 resolve with Not_found -> try find_inline_of_delta kn1 resolve @@ -137,17 +137,17 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (make_kn mp' dir l) + solve_delta_kn resolve (KerName.make mp' dir l) | None -> kn let subst_kn sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - make_kn mp' dir l + KerName.make mp' dir l | None -> kn exception No_subst @@ -165,14 +165,14 @@ let gen_subst_mp f sub mp1 mp2 = | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 let make_mind_equiv mpu mpc dir l = - let knu = make_kn mpu dir l in - if mpu == mpc then mind_of_kn knu - else mind_of_kn_equiv knu (make_kn mpc dir l) + let knu = KerName.make mpu dir l in + if mpu == mpc then MutInd.make1 knu + else MutInd.make knu (KerName.make mpc dir l) let subst_ind sub mind = - let kn1,kn2 = user_mind mind, canonical_mind mind in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in + let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in + let mp1,dir,l = KerName.repr kn1 in + let mp2,_,_ = KerName.repr kn2 in let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in try let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in @@ -182,14 +182,14 @@ let subst_ind sub mind = with No_subst -> mind let make_con_equiv mpu mpc dir l = - let knu = make_kn mpu dir l in - if mpu == mpc then constant_of_kn knu - else constant_of_kn_equiv knu (make_kn mpc dir l) + let knu = KerName.make mpu dir l in + if mpu == mpc then Constant.make1 knu + else Constant.make knu (KerName.make mpc dir l) let subst_con0 sub con u = - let kn1,kn2 = user_con con,canonical_con con in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in + let kn1,kn2 = Constant.user con, Constant.canonical con in + let mp1,dir,l = KerName.repr kn1 in + let mp2,_,_ = KerName.repr kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in @@ -304,7 +304,9 @@ let subset_prefixed_by mp resolver = match hint with | Inline _ -> rslv | Equiv _ -> - if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + if mp_in_mp mp (KerName.modpath kn) + then Deltamap.add_kn kn hint rslv + else rslv in Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver diff --git a/checker/environ.ml b/checker/environ.ml index 7040fdda4..9352f71ef 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -112,7 +112,7 @@ let anomaly s = anomaly (Pp.str s) let add_constant kn cs env = if Cmap_env.mem kn env.env_globals.env_constants then Printf.ksprintf anomaly ("Constant %s is already defined") - (string_of_con kn); + (Constant.to_string kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in let new_globals = @@ -172,12 +172,14 @@ let lookup_projection p env = let scrape_mind env kn= try KNmap.find kn env.env_globals.env_inductives_eq - with - Not_found -> kn + with + Not_found -> kn let mind_equiv env (kn1,i1) (kn2,i2) = Int.equal i1 i2 && - KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2)) + KerName.equal + (scrape_mind env (MutInd.user kn1)) + (scrape_mind env (MutInd.user kn2)) let lookup_mind kn env = @@ -186,9 +188,9 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then Printf.ksprintf anomaly ("Inductive %s is already defined") - (string_of_mind kn); + (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in - let kn1,kn2 = user_mind kn,canonical_mind kn in + let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq else @@ -205,7 +207,7 @@ let add_mind kn mib env = let add_modtype ln mtb env = if MPmap.mem ln env.env_globals.env_modtypes then Printf.ksprintf anomaly ("Module type %s is already defined") - (string_of_mp ln); + (ModPath.to_string ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = { env.env_globals with @@ -215,7 +217,7 @@ let add_modtype ln mtb env = let shallow_add_module mp mb env = if MPmap.mem mp env.env_globals.env_modules then Printf.ksprintf anomaly ("Module %s is already defined") - (string_of_mp mp); + (ModPath.to_string mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = { env.env_globals with @@ -225,7 +227,7 @@ let shallow_add_module mp mb env = let shallow_remove_module mp env = if not (MPmap.mem mp env.env_globals.env_modules) then Printf.ksprintf anomaly ("Module %s is unknown") - (string_of_mp mp); + (ModPath.to_string mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = { env.env_globals with diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 566df673c..fd5eaeb8b 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -32,11 +32,11 @@ let string_of_mp mp = if !Flags.debug then debug_string_of_mp mp else string_of_mp mp let prkn kn = - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in str(string_of_mp mp ^ "." ^ Label.to_string l) let prcon c = - let ck = canonical_con c in - let uk = user_con c in + let ck = Constant.canonical c in + let uk = Constant.user c in if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. @@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush (); + Flags.if_verbose ppnl (str " checking ind: " ++ MutInd.print kn); pp_flush (); (* check mind_constraints: should be consistent with env *) let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3ea5ed0d3..c07a35e35 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,7 +18,7 @@ let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in match hd with Sort (Type u) when not (Univ.is_univ_variable u) -> - let ul = Univ.Level.make empty_dirpath 1 in + let ul = Univ.Level.make DirPath.empty 1 in let u' = Univ.Universe.make ul in let cst = Univ.enforce_leq u u' Univ.empty_constraint in let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in @@ -70,7 +70,7 @@ let check_constant_declaration env kn cb = let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> - failwith ("Unknown module: "^string_of_mp mp) + failwith ("Unknown module: "^ModPath.to_string mp) let mk_mtb mp sign delta = { mod_mp = mp; diff --git a/checker/modops.ml b/checker/modops.ml index 9f4375262..442f999bb 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -28,7 +28,7 @@ let error_not_match l _ = let error_no_such_label l = error ("No such label "^Label.to_string l) let error_no_such_label_sub l l1 = - let l1 = string_of_mp l1 in + let l1 = ModPath.to_string l1 in error ("The field "^ Label.to_string l^" is missing in "^l1^".") diff --git a/checker/print.ml b/checker/print.ml index 9cd8fda5d..da8a6106f 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -122,7 +122,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_mind sp) + print_string (MutInd.debug_to_string sp) and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = @@ -131,7 +131,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_con sp) + print_string (Constant.debug_to_string sp) in try diff --git a/checker/subtyping.ml b/checker/subtyping.ml index e41922573..46d21f6cc 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -103,7 +103,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in - check eq_mind (fun x -> x.proj_ind); + check MutInd.equal (fun x -> x.proj_ind); check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); diff --git a/checker/typeops.ml b/checker/typeops.ml index 64afd21b2..da9842a8d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -92,7 +92,7 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = let _cb = try lookup_constant kn env with Not_found -> - failwith ("Cannot find constant: "^string_of_con kn) + failwith ("Cannot find constant: "^Constant.to_string kn) in let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in let () = check_constraints cu env in @@ -178,7 +178,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_mind (fst ind)) + failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -192,7 +192,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_mind (fst ind)) + failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif @@ -223,7 +223,7 @@ let judge_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (c, ct) in - assert(eq_mind pb.proj_ind (fst ind)); + assert(MutInd.equal pb.proj_ind (fst ind)); let ty = subst_instance_constr u pb.proj_type in substl (c :: List.rev args) ty diff --git a/kernel/names.mli b/kernel/names.mli index 1dfdd8290..56f0f8c60 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -766,7 +766,7 @@ val mind_of_kn : KerName.t -> mutual_inductive (** @deprecated Same as [MutInd.make1] *) val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive -(** @deprecated Same as [MutInd.make2] *) +(** @deprecated Same as [MutInd.make] *) val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive (** @deprecated Same as [MutInd.make3] *) |