From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- checker/check.ml | 28 ++++----- checker/check.mllib | 20 ++++--- checker/check_stat.ml | 15 ++--- checker/checker.ml | 48 ++++++---------- checker/cic.mli | 24 +++++--- checker/closure.ml | 10 ++-- checker/declarations.ml | 65 +++++++++++---------- checker/environ.ml | 35 ++++++------ checker/include | 2 +- checker/indtypes.ml | 47 ++++++++-------- checker/inductive.ml | 147 +++++++++++++++++------------------------------- checker/mod_checking.ml | 6 +- checker/modops.ml | 4 +- checker/print.ml | 10 ++-- checker/reduction.ml | 31 +++++----- checker/reduction.mli | 4 +- checker/safe_typing.ml | 25 ++++---- checker/subtyping.ml | 8 +-- checker/term.ml | 55 ++++++++++-------- checker/term.mli | 3 +- checker/typeops.ml | 32 +++++------ checker/univ.ml | 16 +++--- checker/values.ml | 18 +++--- checker/votour.ml | 59 +++++++++++++------ 24 files changed, 352 insertions(+), 360 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 3a5c9121..8b299bf2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -7,10 +7,12 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names +let chk_pp = Pp.pp_with Format.std_formatter + let pr_dirpath dp = str (DirPath.to_string dp) let default_root_prefix = DirPath.empty let split_dirpath d = @@ -111,15 +113,13 @@ 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 (); register_loaded_library m (*************************************************************************) @@ -173,7 +173,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 +188,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,12 +299,12 @@ 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 chk_pp (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 let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in @@ -323,7 +323,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) "); + chk_pp (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 +334,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 chk_pp (str" done]" ++ fnl ()); 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 chk_pp (str" failed!]" ++ fnl ()); 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 +407,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 0d36e3a0..488507a1 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store @@ -21,20 +22,25 @@ CList CString Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode CObj CArray CStack Util +Pp Ppstyle -Errors -Ephemeron +Xml_datatype +Richpp +Feedback +Segmenttree +Unicodetable +Unicode +CErrors +CWarnings +CEphemeron Future CUnix + +Minisys System Profile RemoteCounter diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d031975d..741f5328 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -18,21 +18,16 @@ let print_memory_stat () = if !memory_stat then begin Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ()); Format.print_newline(); - flush_all() + Format.print_flush() end let output_context = ref false -let pr_engagement (impr_set,type_in_type) = +let pr_engagement impr_set = begin match impr_set with | ImpredicativeSet -> str "Theory: Set is impredicative" | PredicativeSet -> str "Theory: Set is predicative" - end ++ - begin - match type_in_type with - | StratifiedType -> str "Theory: Stratified type hierarchy" - | TypeInType -> str "Theory: Type is of type Type" end let cst_filter f csts = @@ -57,12 +52,12 @@ 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() + str "* " ++ hov 0 (pr_ax csts))); end let stats () = diff --git a/checker/checker.ml b/checker/checker.ml index 825fb4dc..8dbb7e01 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open System open Flags @@ -16,8 +16,10 @@ open Check let () = at_exit flush_all +let chk_pp = Pp.pp_with Format.std_formatter + 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 +69,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 + with CErrors.UserError _ -> + if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -90,7 +92,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 +125,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 *) @@ -140,9 +142,7 @@ let set_debug () = Flags.debug := true let impredicative_set = ref Cic.PredicativeSet let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet -let type_in_type = ref Cic.StratifiedType -let set_type_in_type () = type_in_type := Cic.TypeInType -let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type) +let engage () = Safe_typing.set_engagement (!impredicative_set) let admit_list = ref ([] : section_path list) @@ -179,10 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir coqdir recursively map physical dir to logical coqdir\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -195,7 +192,6 @@ let print_usage_channel co command = \n -silent disable trace of constants being checked\ \n\ \n -impredicative-set set sort Set impredicative\ -\n -type-in-type collapse type hierarchy\ \n\ \n -h, --help print this list of options\ \n" @@ -215,14 +211,9 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") -let print_loc loc = - if loc = Loc.ghost then - (str"") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = str "\"" ++ str s ++ str "\"" let where s = @@ -294,7 +285,8 @@ 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 + chk_pp + (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" @@ -315,15 +307,13 @@ let rec explain_exn = function str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) - | e -> Errors.print e (* for anomalies and other uncaught exceptions *) + | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> set_impredicative_set (); parse rem - | "-type-in-type" :: rem -> - set_type_in_type (); parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then @@ -337,15 +327,13 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; print_endline (Envars.coqlib ()); exit 0 @@ -383,7 +371,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; if_verbose print_header (); init_load_path (); engage (); diff --git a/checker/cic.mli b/checker/cic.mli index 041394d4..36455875 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -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, @@ -166,9 +167,8 @@ type action (** Engagements *) type set_predicativity = ImpredicativeSet | PredicativeSet -type type_hierarchy = TypeInType | StratifiedType -type engagement = set_predicativity * type_hierarchy +type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) @@ -211,6 +211,16 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) + check_universes : bool; (** If [false] universe constraints are not checked *) +} + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -219,7 +229,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; +} (** {6 Representation of mutual inductive types } *) @@ -315,9 +327,7 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -(** {8 Data for native compilation } *) - - mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) + mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) } (** {6 Module declarations } *) diff --git a/checker/closure.ml b/checker/closure.ml index 400a535c..cef1d31a 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -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/declarations.ml b/checker/declarations.ml index 32d1713a..1fe02c8b 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 f8f5c29b..7b59c6b9 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,4 +1,4 @@ -open Errors +open CErrors open Util open Names open Cic @@ -33,26 +33,21 @@ let empty_env = { env_rel_context = []; env_stratification = { env_universes = Univ.initial_universes; - env_engagement = (PredicativeSet,StratifiedType)}; + env_engagement = PredicativeSet }; env_imports = MPmap.empty } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let rel_context env = env.env_rel_context -let set_engagement (impr_set,type_in_type as c) env = - let expected_impr_set,expected_type_in_type = +let set_engagement (impr_set as c) env = + let expected_impr_set = env.env_stratification.env_engagement in begin match impr_set,expected_impr_set with | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" | _ -> () end; - begin - match type_in_type,expected_type_in_type with - | StratifiedType, TypeInType -> error "Incompatible engagement" - | _ -> () - end; { env with env_stratification = { env.env_stratification with env_engagement = c } } @@ -80,7 +75,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 +107,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 +167,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 +183,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 +202,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 +212,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 +222,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/include b/checker/include index f5bd2984..6bea3c91 100644 --- a/checker/include +++ b/checker/include @@ -31,7 +31,7 @@ open Typeops;; open Check;; open Pp;; -open Errors;; +open CErrors;; open Util;; open Names;; open Term;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2865f5bd..27f79e79 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -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. @@ -44,7 +44,7 @@ let prcon c = let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else - let t' = whd_betadeltaiota env t in + let t' = whd_all env t in if noccur_between x nvars t' then Some t' else None @@ -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' @@ -90,14 +90,14 @@ exception InductiveError of inductive_error (* Typing the arities and constructor types *) let rec sorts_of_constr_args env t = - let t = whd_betadeltaiota_nolet env t in + let t = whd_allnolet env t in 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 @@ -176,7 +176,7 @@ let typecheck_arity env params inds = (* Allowed eliminations *) let check_predicativity env s small level = - match s, fst (engagement env) with + match s, engagement env with Type u, _ -> (* let u' = fresh_local_univ () in *) (* let cst = *) @@ -319,9 +319,9 @@ 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 + match whd_all env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l))) in check (nparams-1) (n-nhyps) hyps; @@ -340,9 +340,9 @@ 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 + (match whd_all env p with | Rel w when w = index -> find (index-1) (lp,hyps) | _ -> failwith "bad number of recursive parameters") in find (n-1) (lpar,List.rev 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 @@ -387,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if n=0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -400,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) let rec check_pos (env, n, ntypes, ra_env as ienv) c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -469,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc and check_constructors ienv check_head c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -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/inductive.ml b/checker/inductive.ml index 79dba4fa..c4ffc141 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) = (mib, mib.mind_packets.(tyi)) let find_rectype env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l) @@ -59,16 +59,6 @@ let inductive_instance mib = UContext.instance mib.mind_universes else Instance.empty -let inductive_context mib = - if mib.mind_polymorphic then - instantiate_univ_context mib.mind_universes - else UContext.empty - -let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - subst_instance_constraints u (UContext.constraints mib.mind_universes) - else Constraint.empty - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) @@ -88,10 +78,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 +151,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 +164,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 *) @@ -190,8 +180,6 @@ let rec make_subst env = in make Univ.LMap.empty -exception SingletonInductiveBecomesProp of Id.t - let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let subst = make_subst env (ctx,ar.template_param_levels,args) in @@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let is_prop_sort = function - | Prop Null -> true - | _ -> false - -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> if not mib.mind_polymorphic then a.mind_user_arity @@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) - -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] - -let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty = type_of_inductive_gen env pind [||] in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) + mkArity (List.rev ctx,s) let type_of_inductive_knowing_parameters env mip args = type_of_inductive_gen env mip args @@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = let type_of_constructor cstru mspec = type_of_constructor_gen cstru mspec -let type_of_constructor_in_ctx cstr (mib,mip as mspec) = - let u = Univ.UContext.instance mib.mind_universes in - let c = type_of_constructor_gen (cstr, u) mspec in - (c, mib.mind_universes) - -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn u mib) specif @@ -319,8 +275,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 @@ -343,15 +299,15 @@ let check_allowed_sort ksort specif = let is_correct_arity env c (p,pj) ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = - let pt' = whd_betadeltaiota env pt in + let pt' = whd_all 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 ksort = match (whd_betadeltaiota env' a2) with + let env' = push_rel (LocalAssum (na1,a1)) env in + let ksort = match (whd_all env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in @@ -362,8 +318,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 +483,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 +494,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 +505,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 *) @@ -622,20 +578,21 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,l' = decompose_app (whd_all env s) in match i with Ind _ -> true | _ -> false (* 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 @@ -645,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -675,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -734,7 +691,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> @@ -763,7 +720,7 @@ let restrict_spec env spec p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,args = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_all env s) in match i with | Ind i -> begin match spec with @@ -785,7 +742,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) - let f,l = decompose_app (whd_betadeltaiota renv.env t) in + let f,l = decompose_app (whd_all renv.env t) in match f with | Rel k -> subterm_var k renv @@ -861,7 +818,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 @@ -899,11 +856,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (rel_context_length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = - let t = whd_betadeltaiota env ar in + let t = whd_all env ar in match stack, t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in - let ty, args = decompose_app (whd_betadeltaiota env a) in + let d = LocalAssum (n,a) in + let ty, args = decompose_app (whd_all env a) in let elt = match ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -956,10 +913,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)) @@ -1032,6 +989,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -1041,8 +1002,6 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - | Proj (p, c) -> check_rec_call renv [] c - and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body @@ -1075,10 +1034,10 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match (whd_betadeltaiota env def) with + match (whd_all 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, _) = @@ -1124,10 +1083,10 @@ let anomaly_ill_typed () = anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in + let b = whd_all 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 -> @@ -1136,7 +1095,7 @@ let rec codomain_is_coind env c = let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then - let c,args = decompose_app (whd_betadeltaiota env t) in + let c,args = decompose_app (whd_all env t) in match c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive @@ -1168,7 +1127,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/mod_checking.ml b/checker/mod_checking.ml index 3ea5ed0d..7f93e156 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/modops.ml b/checker/modops.ml index 9f437526..b720fb62 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names @@ -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 9cd8fda5..7ef752b0 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,7 +10,9 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let chk_pp = Pp.pp_with Format.std_formatter + +let print_instance i = chk_pp (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -108,7 +110,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("; chk_pp (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) @@ -122,7 +124,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 +133,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 3a666a60..ec16aa26 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Cic open Term @@ -92,13 +92,13 @@ let whd_betaiotazeta x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t @@ -167,8 +167,9 @@ let sort_cmp env univ pb s0 s1 = CUMUL -> () | _ -> raise NotConvertible) | (Type u1, Type u2) -> - if snd (engagement env) == StratifiedType - && not + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with | CONV -> Univ.check_eq univ u1 u2 | CUMUL -> Univ.check_leq univ u1 u2) @@ -476,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true * error message. *) let hnf_prod_app env t n = - match whd_betadeltaiota env t with + match whd_all env t with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -487,10 +488,10 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all 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 @@ -499,17 +500,17 @@ let dest_prod env = (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet 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 | _ -> - let rty' = whd_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in @@ -517,13 +518,13 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet 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 2f551f4a..15a2df1f 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -16,8 +16,8 @@ open Environ (*s Reduction functions *) val whd_betaiotazeta : constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr (************************************************************************) (*s conversion functions *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index fa429755..11cd742b 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -7,12 +7,14 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Cic open Names open Environ +let pr_dirpath dp = str (DirPath.to_string dp) + (************************************************************************) (* * Global environment @@ -33,28 +35,23 @@ let full_add_module dp mb univs digest = genv := add_digest env dp digest (* Check that the engagement expected by a library extends the initial one *) -let check_engagement env (expected_impredicative_set,expected_type_in_type) = - let impredicative_set,type_in_type = Environ.engagement env in +let check_engagement env expected_impredicative_set = + let impredicative_set = Environ.engagement env in begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." + CErrors.error "Needs option -impredicative-set." | _ -> () end; - begin - match type_in_type, expected_type_in_type with - | StratifiedType, TypeInType -> - Errors.error "Needs option -type-in-type." - | _ -> () - end + () (* Libraries = Compiled modules *) let report_clash f caller dir = let msg = - str "compiled library " ++ str(DirPath.to_string caller) ++ + str "compiled library " ++ pr_dirpath caller ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(DirPath.to_string dir) ++ fnl() in + pr_dirpath dir ++ fnl() in f msg @@ -79,7 +76,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 @@ -91,7 +88,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/subtyping.ml b/checker/subtyping.ml index e4192257..7eae9b83 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Names open Cic @@ -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); @@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/checker/term.ml b/checker/term.ml index 6487d1a1..591348cb 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -8,7 +8,7 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) -open Errors +open CErrors open Util open Names open Esubst @@ -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 ab488b2b..0af83e05 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/typeops.ml b/checker/typeops.ml index d49c40a8..173e19ce 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -33,7 +33,7 @@ let check_constraints cst env = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env (c,ty as j) = - match whd_betadeltaiota env ty with + match whd_all env ty with | Sort s -> (c,s) | _ -> error_not_type env j @@ -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 @@ -107,7 +107,7 @@ let judge_of_apply env (f,funj) argjv = let rec apply_rec n typ = function | [] -> typ | (h,hj)::restjl -> - (match whd_betadeltaiota env typ with + (match whd_all env typ with | Prod (_,c1,c2) -> (try conv_leq env hj c1 with NotConvertible -> @@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - if fst (engagement env) = ImpredicativeSet then + if engagement env = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort else @@ -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/univ.ml b/checker/univ.ml index cb2eaced..668f3a05 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -14,7 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. @@ -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/values.ml b/checker/values.ml index c14e9223..c175aed6 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -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 7c050ff1db22f14ee3a4c44aae533082 checker/cic.mli +MD5 6466d8cc443b5896cb905776df0cc49e 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 @@ -194,8 +194,7 @@ let v_lazy_constr = (** kernel/declarations *) let v_impredicative_set = v_enum "impr-set" 2 -let v_type_in_type = v_enum "type-in-type" 2 -let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|] +let v_engagement = v_impredicative_set let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -213,6 +212,9 @@ let v_projbody = v_tuple "proj_eta" [|v_constr;v_constr|]; v_constr|] +let v_typing_flags = + v_tuple "typing_flags" [|v_bool; v_bool|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; @@ -221,7 +223,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] @@ -270,7 +273,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_typing_flags|] let v_with = Sum ("with_declaration_body",0, diff --git a/checker/votour.ml b/checker/votour.ml index 78978bb2..48f9f45e 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -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! enters the -th child, u goes up 1 level, x exits\n%!"; + read_num max + type 'a repr = | INT of int | STRING of string @@ -22,6 +42,7 @@ sig val input : in_channel -> obj val repr : obj -> obj repr val size : obj -> int + val oid : obj -> int option end module ReprObj : S = @@ -45,6 +66,7 @@ struct else INT (Obj.magic obj) let size (_, p) = CObj.shared_size_of_pos p + let oid _ = None end module ReprMem : S = @@ -97,6 +119,9 @@ struct let _ = init_size seen obj in obj + let oid = function + | Int _ | Atm _ | Fun _ -> None + | Ptr p -> Some p end module Visit (Repr : S) : @@ -149,9 +174,13 @@ let rec get_details v o = match v, Repr.repr o with |Annot (s,v), _ -> get_details v o |_ -> "" +let get_oid obj = match Repr.oid obj with +| None -> "" +| Some id -> Printf.sprintf " [0x%08x]" id + let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (Repr.size o)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) @@ -246,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 @@ -341,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 = -- cgit v1.2.3