diff options
Diffstat (limited to 'checker')
40 files changed, 263 insertions, 228 deletions
diff --git a/checker/check.ml b/checker/check.ml index 21c8f1c5bb..93eb2a0d25 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -111,15 +111,14 @@ let check_one_lib admit (dir,m) = also check if it carries a validation certificate (yet to be implemented). *) if LibrarySet.mem dir admit then - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Admitting library: " ++ pr_dirpath dir); Safe_typing.unsafe_import file md m.library_extra_univs dig) else - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Checking library: " ++ pr_dirpath dir); Safe_typing.import file md m.library_extra_univs dig); - Flags.if_verbose pp (fnl()); - pp_flush (); + Flags.if_verbose Feedback.msg_notice (fnl()); register_loaded_library m (*************************************************************************) @@ -173,7 +172,7 @@ let remove_load_path dir = let add_load_path (phys_path,coq_path) = if !Flags.debug then - ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = canonical_path_name phys_path in let physical, logical = !load_paths in @@ -188,7 +187,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); @@ -299,7 +298,7 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); + Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in @@ -323,7 +322,7 @@ let intern_from_file (dir, f) = errorlabstrm "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - pp (str " (was a vio file) "); + Feedback.msg_notice(str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then errorlabstrm "intern_from_file" (str "The file "++str f++str " is still a .vio")) @@ -334,12 +333,12 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; - Flags.if_verbose ppnl (str" done]"); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str" done]"); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in sd,md,table,opaque_csts,digest - with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in + with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> @@ -407,11 +406,11 @@ let recheck_library ~norec ~admit ~check = let nochk = List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in (* *) - Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ + Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; - Flags.if_verbose ppnl (str"Modules were successfully checked") + Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") open Printf diff --git a/checker/check.mllib b/checker/check.mllib index 3725989e87..2fa4d57977 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -22,21 +22,24 @@ CList CString Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode CObj CArray CStack Util +Pp Ppstyle +Xml_datatype +Richpp +Feedback +Segmenttree +Unicodetable +Unicode Errors -Ephemeron +CEphemeron Future CUnix +Minisys System Profile RemoteCounter diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d041f1b7e1..a26c93a30d 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,7 +28,7 @@ let pr_engagement (impr_set,type_in_type) = match impr_set with | ImpredicativeSet -> str "Theory: Set is impredicative" | PredicativeSet -> str "Theory: Set is predicative" - end ++ + end ++ fnl() ++ begin match type_in_type with | StratifiedType -> str "Theory: Stratified type hierarchy" @@ -57,12 +57,13 @@ let print_context env = env_modules=mods; env_modtypes=mtys}; env_stratification= {env_universes=univ; env_engagement=engt}} = env in - ppnl(hov 0 + Feedback.msg_notice + (hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_ax csts) ++ - fnl())); pp_flush() + fnl())); end let stats () = diff --git a/checker/check_stat.mli b/checker/check_stat.mli index 10908f0cc3..39e19d10e4 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/checker.ml b/checker/checker.ml index da93685f98..61b13c60bb 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,7 +17,7 @@ open Check let () = at_exit flush_all let fatal_error info anomaly = - flush_all (); pperrnl info; flush_all (); + flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -67,12 +67,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str "Cannot open " ++ str dir) + Feedback.msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d with Errors.UserError _ -> - if_verbose msg_warning + if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str "Cannot open " ++ str unix_path) + Feedback.msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -123,7 +123,7 @@ let init_load_path () = add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) - (xdg_dirs ~warn:(fun x -> msg_warning (str x))); + (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -288,7 +288,7 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Pp.pp (Univ.pr_universes + Feedback.msg_notice (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" diff --git a/checker/cic.mli b/checker/cic.mli index bd75111a2c..00ac2f56c3 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint (** {6 Type of assumptions and contexts} *) -type rel_declaration = Name.t * constr option * constr +type rel_declaration = LocalAssum of Name.t * constr (* name, type *) + | LocalDef of Name.t * constr * constr (* name, value, type *) type rel_context = rel_declaration list (** The declarations below in .vo should be outside sections, diff --git a/checker/closure.ml b/checker/closure.ml index c6cc2185d3..cef1d31a68 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,7 @@ let reset () = beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 let stop() = - msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") @@ -217,10 +217,10 @@ let ref_value_cache info ref = let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context - (fun (id,b,t) (i,subs) -> - match b with - | None -> (i+1, subs) - | Some body -> (i+1, (i,body) :: subs)) + (fun decl (i,subs) -> + match decl with + | LocalAssum _ -> (i+1, subs) + | LocalDef (_,body,_) -> (i+1, (i,body) :: subs)) (rel_context env) ~init:(0,[]) (* else (0,[])*) diff --git a/checker/closure.mli b/checker/closure.mli index 376e9fef7d..8b1f246c28 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 32d1713a88..1fe02c8b60 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 @@ -517,11 +519,8 @@ let map_decl_arity f g = function | RegularArity a -> RegularArity (f a) | TemplateArity a -> TemplateArity (g a) - -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') +let subst_rel_declaration sub = + Term.map_rel_decl (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) diff --git a/checker/environ.ml b/checker/environ.ml index f8f5c29b79..9352f71ef7 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -80,7 +80,7 @@ let push_rel d env = let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) @@ -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/esubst.ml b/checker/esubst.ml new file mode 120000 index 0000000000..b82bd24f1e --- /dev/null +++ b/checker/esubst.ml @@ -0,0 +1 @@ +../kernel/esubst.ml
\ No newline at end of file diff --git a/checker/esubst.mli b/checker/esubst.mli new file mode 120000 index 0000000000..e30eaae5d3 --- /dev/null +++ b/checker/esubst.mli @@ -0,0 +1 @@ +../kernel/esubst.mli
\ No newline at end of file diff --git a/checker/indtypes.ml b/checker/indtypes.ml index f02f03dcb1..a667bb8a3e 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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. @@ -56,10 +56,10 @@ let is_constructor_head t = let conv_ctxt_prefix env (ctx1:rel_context) ctx2 = let rec chk env rctx1 rctx2 = match rctx1, rctx2 with - (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' -> + (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' -> conv env ty1 ty2; chk (push_rel d1 env) rctx1' rctx2' - | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' -> + | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' -> conv env ty1 ty2; conv env bd1 bd2; chk (push_rel d1 env) rctx1' rctx2' @@ -94,10 +94,10 @@ let rec sorts_of_constr_args env t = match t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in varj :: sorts_of_constr_args env1 c2 | LetIn (name,def,ty,c) -> - let env1 = push_rel (name,Some def,ty) env in + let env1 = push_rel (LocalDef (name,def,ty)) env in sorts_of_constr_args env1 c | _ when is_constructor_head t -> [] | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") @@ -167,7 +167,7 @@ let typecheck_arity env params inds = full_arity is used as argument or subject to cast, an upper universe will be generated *) let id = ind.mind_typename in - let env_ar' = push_rel (Name id, None, arity) env_ar in + let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in env_ar') env inds in @@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | (_,Some _,_)::hyps -> check k (index+1) hyps + | LocalDef _ :: hyps -> check k (index+1) hyps | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps @@ -340,7 +340,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs = | ([],_) -> () | (_,[]) -> failwith "number of recursive parameters cannot be greater than the number of parameters." - | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps) + | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps) | (p::lp,_::hyps) -> (match whd_betadeltaiota env p with | Rel w when w = index -> find (index-1) (lp,hyps) @@ -370,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc = [lra] is the list of recursive tree of each variable *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = - (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra) let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -527,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 Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* 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/indtypes.mli b/checker/indtypes.mli index 5188f80d13..071eecbbcd 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/inductive.ml b/checker/inductive.ml index 21b80f323e..43a32ea24d 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -88,10 +88,10 @@ let instantiate_params full t u args sign = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = fold_rel_context - (fun (_,copt,_) (largs,subs,ty) -> - match (copt, largs, ty) with - | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> + (fun decl (largs,subs,ty) -> + match (decl, largs, ty) with + | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) + | (LocalDef (_,b,_),_,LetIn(_,_,_,t)) -> (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) @@ -161,7 +161,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let rec make_subst env = let rec make subst = function - | (_,Some _,_)::sign, exp, args -> + | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) | d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in @@ -174,7 +174,7 @@ let rec make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env a)) in make (cons_subst u s subst) (sign, exp, args) - | (na,None,t)::sign, Some u::exp, [] -> + | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -319,8 +319,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -345,12 +345,12 @@ let is_correct_arity env c (p,pj) ind specif params = let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), LocalAssum (_,a1')::ar' -> (try conv env a1 a1' with NotConvertible -> raise (LocalArity None)); - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (na1,None,a1) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match (whd_betadeltaiota env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in @@ -362,8 +362,8 @@ let is_correct_arity env c (p,pj) ind specif params = | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false - | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + | _, (LocalDef _ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in @@ -527,10 +527,10 @@ type guard_env = let make_renv env recarg tree = { env = env; rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) - genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } + genv = [Lazy.from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = - { env = push_rel (x,None,ty) renv.env; + { env = push_rel (LocalAssum (x,ty)) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -538,7 +538,7 @@ let assign_var_spec renv (i,spec) = { renv with genv = List.assign renv.genv (i-1) spec } let push_var_renv renv (x,ty) = - push_var renv (x,ty,Lazy.lazy_from_val Not_subterm) + push_var renv (x,ty,Lazy.from_val Not_subterm) (* Fetch recursive information about a variable p *) let subterm_var p renv = @@ -549,13 +549,13 @@ let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } let push_fix_renv renv (_,v,_ as recdef) = let n = Array.length v in { env = push_rec_types recdef renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } (* Definition and manipulation of the stack *) @@ -628,14 +628,15 @@ let check_inductive_codomain env p = (* The following functions are almost duplicated from indtypes.ml, except that they carry here a poorer environment (containing less information). *) let ienv_push_var (env, lra) (x,a,ra) = -(push_rel (x,None,a) env, (Norec,ra)::lra) +(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra) let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -861,7 +862,7 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] + | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -902,7 +903,7 @@ let filter_stack_domain env ci p stack = let t = whd_betadeltaiota env ar in match stack, t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in let ty, args = decompose_app (whd_betadeltaiota env a) in let elt = match ty with | Ind ind -> @@ -956,10 +957,10 @@ let check_one_fix renv recpos trees def = end else begin - match pi2 (lookup_rel p renv.env) with - | None -> + match lookup_rel p renv.env with + | LocalAssum _ -> List.iter (check_rec_call renv []) l - | Some c -> + | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> check_rec_call renv stack (applist(lift p c,l)) @@ -1078,7 +1079,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match (whd_betadeltaiota env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in if n = k+1 then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1127,7 +1128,7 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1168,7 +1169,7 @@ let check_one_cofix env nbfix def deftype = | Lambda (x,a,b) -> assert (args = []); if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in check_rec_call env' alreadygrd (n+1) tree vlra b else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) diff --git a/checker/inductive.mli b/checker/inductive.mli index 78fb0bdd13..ed3a7b53ce 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3ea5ed0d34..7f93e15609 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 @@ -26,7 +26,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); let env' = if cb.const_polymorphic then let inst = Univ.make_abstract_instance cb.const_universes 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/mod_checking.mli b/checker/mod_checking.mli index ae28caed09..5c7b392ffd 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/modops.ml b/checker/modops.ml index 7f07f8bf84..442f999bb3 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/modops.mli b/checker/modops.mli index e22c2656c8..26a088f32b 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/names.ml b/checker/names.ml new file mode 120000 index 0000000000..f0bf2f83f6 --- /dev/null +++ b/checker/names.ml @@ -0,0 +1 @@ +../kernel/names.ml
\ No newline at end of file diff --git a/checker/names.mli b/checker/names.mli new file mode 120000 index 0000000000..10459f3b29 --- /dev/null +++ b/checker/names.mli @@ -0,0 +1 @@ +../kernel/names.mli
\ No newline at end of file diff --git a/checker/print.ml b/checker/print.ml index 7624fd3257..c0d1ac3688 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,7 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let print_instance i = Feedback.msg_notice (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +108,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) @@ -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/reduction.ml b/checker/reduction.ml index 384d883ea3..f1aa5d9194 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -490,7 +490,7 @@ let dest_prod env = let t = whd_betadeltaiota env c in match t with | Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in decrec (push_rel d env) (d::m) c0 | _ -> m,t in @@ -502,10 +502,10 @@ let dest_prod_assum env = let rty = whd_betadeltaiota_nolet env ty in match rty with | Prod (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> @@ -520,10 +520,10 @@ let dest_lam_assum env = let rty = whd_betadeltaiota_nolet env ty in match rty with | Lambda (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty diff --git a/checker/reduction.mli b/checker/reduction.mli index 2e87346980..2f551f4a6c 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index ee33051676..1071e2f930 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -81,7 +81,7 @@ let stamp_library file digest = () warning is issued in case of mismatch *) let import file clib univs digest = let env = !genv in - check_imports msg_warning clib.comp_name env clib.comp_deps; + check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module @@ -93,7 +93,7 @@ let import file clib univs digest = (* When the module is admitted, digests *must* match *) let unsafe_import file clib univs digest = let env = !genv in - if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps + if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 892a8d2cc9..8724f8e014 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 372c314247..46d21f6ccb 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/subtyping.mli b/checker/subtyping.mli index 03242cbcfc..cc66fc5382 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/term.ml b/checker/term.ml index 430be49519..56cc9cdc22 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -222,24 +222,29 @@ let rel_context_length = List.length let rel_context_nhyps hyps = let rec nhyps acc = function | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in + | LocalAssum _ :: hyps -> nhyps (1+acc) hyps + | LocalDef _ :: hyps -> nhyps acc hyps in nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init -let map_rel_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl l +let map_rel_decl f = function + | LocalAssum (n, typ) as decl -> + let typ' = f typ in + if typ' == typ then decl else + LocalAssum (n, typ') + | LocalDef (n, body, typ) as decl -> + let body' = f body in + let typ' = f typ in + if body' == body && typ' == typ then decl else + LocalDef (n, body', typ') + +let map_rel_context f = + List.smartmap (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -272,8 +277,8 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match c with - | Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c + | Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in @@ -282,18 +287,18 @@ let decompose_lam_n_assum n = (* Iterate products, with or without lets *) (* Constructs either [(x:t)c] or [[x=b:t]c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> Prod (na, t, c) - | Some b -> LetIn (na, b, t, c) +let mkProd_or_LetIn decl c = + match decl with + | LocalAssum (na,t) -> Prod (na, t, c) + | LocalDef (na,b,t) -> LetIn (na, b, t, c) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let decompose_prod_assum = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in @@ -305,8 +310,8 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if Int.equal n 0 then l,c else match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in @@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign let destArity = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t)::l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") diff --git a/checker/term.mli b/checker/term.mli index ab488b2b7c..0af83e05d7 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -35,12 +35,13 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int val fold_rel_context : (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list val compose_lam : (name * constr) list -> constr -> constr val decompose_lam : constr -> (name * constr) list * constr val decompose_lam_n_assum : int -> constr -> rel_context * constr -val mkProd_or_LetIn : name * constr option * constr -> constr -> constr +val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr val decompose_prod_assum : constr -> rel_context * constr val decompose_prod_n_assum : int -> constr -> rel_context * constr diff --git a/checker/type_errors.ml b/checker/type_errors.ml index c4c6528651..b7718e02da 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/type_errors.mli b/checker/type_errors.mli index 036ff45462..d9d1479580 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/typeops.ml b/checker/typeops.ml index 21819992a9..da9842a8db 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u)) let judge_of_relative env n = try - let (_,_,typ) = lookup_rel n env in + let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in lift n typ with Not_found -> error_unbound_rel env n @@ -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 @@ -296,13 +296,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let j' = execute env1 c2 in Prod(name,c1,j') | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let varj' = execute_type env1 c2 in Sort (sort_of_product env varj varj') @@ -314,7 +314,7 @@ let rec execute env cstr = let env',c2' = (* refresh_arity env *) env, c2 in let _ = execute_type env' c2' in judge_of_cast env' (c1,j1) DEFAULTcast c2' in - let env1 = push_rel (name,Some c1,c2) env in + let env1 = push_rel (LocalDef (name,c1,c2)) env in let j' = execute env1 c3 in subst1 c1 j' @@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr let check_ctxt env rels = fold_rel_context (fun d env -> match d with - (_,None,ty) -> + | LocalAssum (_,ty) -> let _ = infer_type env ty in push_rel d env - | (_,Some bd,ty) -> + | LocalDef (_,bd,ty) -> let j1 = infer env bd in let _ = infer env ty in conv_leq env j1 ty; @@ -399,9 +399,9 @@ let check_polymorphic_arity env params par = let pl = par.template_param_levels in let rec check_p env pl params = match pl, params with - Some u::pl, (na,None,ty)::params -> + Some u::pl, LocalAssum (na,ty)::params -> check_kind env ty u; - check_p (push_rel (na,None,ty) env) pl params + check_p (push_rel (LocalAssum (na,ty)) env) pl params | None::pl,d::params -> check_p (push_rel d env) pl params | [], _ -> () | _ -> failwith "check_poly: not the right number of params" in diff --git a/checker/typeops.mli b/checker/typeops.mli index 39d6604188..db8e467a33 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/univ.ml b/checker/univ.ml index 648e478176..96d8270137 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val equal : t -> t -> bool + val eq : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let equal l1 l2 = match l1, l2 with + let eq l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.equal x y then l + if H.eq x y then l else cons y (remove x l) end @@ -229,7 +229,7 @@ module Level = struct type _t = t type t = _t type u = unit - let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -320,7 +320,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -339,7 +339,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let equal x y = x == y || + let eq x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1089,7 +1089,7 @@ struct a end - let equal t1 t2 = + let eq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = diff --git a/checker/univ.mli b/checker/univ.mli index f3216feac4..7d4c629ab9 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/validate.ml b/checker/validate.ml index 63180f055e..c434ef09d3 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/values.ml b/checker/values.ml index 34de511c8a..19cbb50606 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli +MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli *) @@ -154,8 +154,8 @@ and v_prec = Tuple ("prec_declaration", and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) - -let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|] +let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|]; (* LocalAssum *) + [|v_name; v_constr; v_constr|] |] (* LocalDef *) let v_rctxt = List v_rdecl let v_section_ctxt = v_enum "emptylist" 1 diff --git a/checker/votour.ml b/checker/votour.ml index f8264ca684..48f9f45e7e 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,6 +10,26 @@ open Values (** {6 Interactive visit of a vo} *) +let rec read_num max = + let quit () = + Printf.printf "\nGoodbye!\n%!"; + exit 0 in + Printf.printf "# %!"; + let l = try read_line () with End_of_file -> quit () in + if l = "u" then None + else if l = "x" then quit () + else + try + let v = int_of_string l in + if v < 0 || v >= max then + let () = + Printf.printf "Out-of-range input! (only %d children)\n%!" max in + read_num max + else Some v + with Failure "int_of_string" -> + Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!"; + read_num max + type 'a repr = | INT of int | STRING of string @@ -255,15 +275,13 @@ let rec visit v o pos = (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop)) children; Printf.printf "-------------\n"; - Printf.printf ("# %!"); - let l = read_line () in try - if l = "u" then let info = pop () in visit info.typ info.obj info.pos - else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0) - else - let v',o',pos' = children.(int_of_string l) in - push (get_name v) v o pos; - visit v' o' pos' + match read_num (Array.length children) with + | None -> let info = pop () in visit info.typ info.obj info.pos + | Some child -> + let v',o',pos' = children.(child) in + push (get_name v) v o pos; + visit v' o' pos' with | Failure "empty stack" -> () | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos @@ -350,13 +368,13 @@ let visit_vo f = let size = if Sys.word_size = 64 then header.size64 else header.size32 in Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size) segments; - Printf.printf "# %!"; - let l = read_line () in - let seg = int_of_string l in - seek_in ch segments.(seg).pos; - let o = Repr.input ch in - let () = Visit.init () in - Visit.visit segments.(seg).typ o [] + match read_num (Array.length segments) with + | Some seg -> + seek_in ch segments.(seg).pos; + let o = Repr.input ch in + let () = Visit.init () in + Visit.visit segments.(seg).typ o [] + | None -> () done let main = |