aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--library/declare.ml2
-rw-r--r--library/impargs.ml2
-rw-r--r--library/lib.ml37
-rw-r--r--library/lib.mli2
-rw-r--r--library/states.ml16
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/reductionops.ml179
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--toplevel/discharge.ml2
-rw-r--r--toplevel/vernac.ml33
11 files changed, 49 insertions, 236 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1255e9787..32303a6fa 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -354,7 +354,7 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
let (lpar,auxlargs) = list_chop auxnpar largs in
if not (List.for_all (noccur_between n ntypes) auxlargs) then
raise (IllFormedInd (LocalNonPos n));
- let auxlc = arities_of_constructors env mi in
+ let auxlc = mip.mind_nf_lc in
let auxntyp = mib.mind_ntypes in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
let lrecargs = List.map (check_weak_pos env n) lpar in
@@ -407,7 +407,7 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
check_head=true, also check the head corresponds to a constructor of
the ith type *)
- and check_construct env check_head =
+ and check_construct env check_head n c =
let rec check_constr_rec env lrec n c =
let x,largs = decompose_app (whd_betadeltaiota env c) in
match kind_of_term x with
@@ -439,7 +439,7 @@ let listrec_mconstr env ntypes hyps nparams i indlc =
if not (List.for_all (noccur_between n ntypes) largs)
then raise (IllFormedInd (LocalNonPos n));
List.rev lrec
- in check_constr_rec env []
+ in check_constr_rec env [] n c
in
Array.map
(fun c ->
diff --git a/library/declare.ml b/library/declare.ml
index 1f5b69458..9fa7b1477 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -229,7 +229,7 @@ let declare_constant id cd =
sp
let redeclare_constant sp cd =
- add_absolutely_named_lead sp (in_constant cd);
+ add_absolutely_named_leaf sp (in_constant cd);
if is_implicit_args() then declare_constant_implicits sp
(* Inductives. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index fec4df020..d6a7859a9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -351,7 +351,7 @@ let _ =
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
- Summary.survive_section = true }
+ Summary.survive_section = false }
let rollback f x =
let fs = freeze () in
diff --git a/library/lib.ml b/library/lib.ml
index cd71de3a3..17b8fa8da 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -38,7 +38,6 @@ and library_segment = library_entry list
let lib_stk = ref ([] : (section_path * node) list)
-
let module_name = ref None
let path_prefix = ref (default_module : dir_path)
@@ -92,7 +91,7 @@ let add_anonymous_entry node =
add_entry sp node;
sp
-let add_absolutely_named_lead sp obj =
+let add_absolutely_named_leaf sp obj =
cache_object (sp,obj);
add_entry sp (Leaf obj)
@@ -114,18 +113,7 @@ let contents_after = function
| None -> !lib_stk
| Some sp -> let (after,_,_) = split_lib sp in after
-(* Sections. *)
-
-let open_section id =
- let dir = extend_dirpath !path_prefix id in
- let sp = make_path id in
- if Nametab.exists_section dir then
- errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
- add_entry sp (OpenedSection (dir, freeze_summaries()));
- (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
- Nametab.push_section dir;
- path_prefix := dir;
- sp
+(* Modules. *)
let check_for_module () =
let is_decl = function (_,FrozenState _) -> false | _ -> true in
@@ -134,6 +122,7 @@ let check_for_module () =
error "a module can not be started after some declarations"
with Not_found -> ()
+(* TODO: use check_for_module ? *)
let start_module s =
if !module_name <> None then
error "a module is already started";
@@ -153,6 +142,20 @@ let end_module s =
error ("The current open module has basename "^(string_of_id bm));
m
+(* Sections. *)
+
+let open_section id =
+ let dir = extend_dirpath !path_prefix id in
+ let sp = make_path id in
+ if Nametab.exists_section dir then
+ errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
+ let sum = freeze_summaries() in
+ add_entry sp (OpenedSection (dir, sum));
+ (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+ Nametab.push_section dir;
+ path_prefix := dir;
+ sp
+
let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
let sections_are_opened () =
@@ -172,6 +175,8 @@ let export_segment seg =
in
clean [] seg
+(* Restore lib_stk and summaries as before the section opening, and
+ add a ClosedSection object. *)
let close_section export id =
let sp,dir,fs =
try match find_entry_p is_opened_section with
@@ -185,9 +190,9 @@ let close_section export id =
in
let (after,_,before) = split_lib sp in
lib_stk := before;
- let after' = export_segment after in
pop_path_prefix ();
- add_entry (make_path id) (ClosedSection (export, dir, after'));
+ let closed_sec = ClosedSection (export, dir, export_segment after) in
+ add_entry (make_path id) closed_sec;
(dir,after,fs)
(* The following function exports the whole library segment, that will be
diff --git a/library/lib.mli b/library/lib.mli
index 832e6cff9..f335d48ad 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -34,7 +34,7 @@ and library_segment = library_entry list
current list of operations (most recent ones coming first). *)
val add_leaf : identifier -> obj -> section_path
-val add_absolutely_named_lead : section_path -> obj -> unit
+val add_absolutely_named_leaf : section_path -> obj -> unit
val add_anonymous_leaf : obj -> unit
val add_frozen_state : unit -> unit
diff --git a/library/states.ml b/library/states.ml
index 6bd8b7d64..9b1068a2b 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -9,17 +9,15 @@
(* $Id$ *)
open System
-open Lib
-open Summary
type state = Lib.frozen * Summary.frozen
let get_state () =
- (Lib.freeze(), freeze_summaries())
+ (Lib.freeze(), Summary.freeze_summaries())
let set_state (fl,fs) =
Lib.unfreeze fl;
- unfreeze_summaries fs
+ Summary.unfreeze_summaries fs
let state_magic_number = 19764
@@ -34,12 +32,8 @@ let freeze = get_state
let unfreeze = set_state
let with_heavy_rollback f x =
- let sum = freeze_summaries ()
- and flib = freeze() in
+ let st = get_state () in
try
f x
- with reraise -> begin
- unfreeze_summaries sum;
- unfreeze flib;
- raise reraise
- end
+ with reraise ->
+ (set_state st; raise reraise)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e717ffe95..c2f4b4bde 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -247,7 +247,7 @@ let rec pretype tycon env isevars lvar lmeta = function
| Some ty -> { uj_val = new_isevar isevars env ty; uj_type = ty }
| None ->
(match loc with
- None -> anomaly "There is an implicit argument I cannot solve"
+ None -> error "There is an implicit argument I cannot solve"
| Some loc ->
user_err_loc
(loc,"pretype",
@@ -351,7 +351,7 @@ let rec pretype tycon env isevars lvar lmeta = function
| ROldCase (loc,isrec,po,c,lf) ->
let cj = pretype empty_tycon env isevars lvar lmeta c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env (evars_of isevars) cj.uj_type
+ try find_rectype env Evd.empty (nf_evar (evars_of isevars) cj.uj_type)
with Induc ->
error_case_not_inductive_loc loc env (evars_of isevars) cj in
let pj = match po with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 410f8aa08..eb798ee44 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -20,6 +20,7 @@ open Environ
open Instantiate
open Closure
open Esubst
+open Reduction
exception Elimconst
@@ -459,10 +460,6 @@ type conversion_function =
type conversion_test = constraints -> constraints
-exception NotConvertible
-
-(* Convertibility of sorts *)
-
type conv_pb =
| CONV
| CUMUL
@@ -493,169 +490,12 @@ let base_sort_cmp pb s0 s1 =
| (Type u1, Type u2) -> true
| (_, _) -> false
-(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
- eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv
-
-(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *)
-and eqappr cv_pb infos appr1 appr2 cuniv =
- let (lft1,(n1,hd1,v1)) = appr1
- and (lft2,(n2,hd2,v2)) = appr2 in
- let el1 = el_shft n1 lft1
- and el2 = el_shft n2 lft2 in
- match (fterm_of hd1, fterm_of hd2) with
- (* case of leaves *)
- | (FAtom a1, FAtom a2) ->
- (match kind_of_term a1, kind_of_term a2 with
- | (Sort s1, Sort s2) ->
- if stack_args_size v1 = 0 && stack_args_size v2 = 0
- then sort_cmp cv_pb s1 s2 cuniv
- else raise NotConvertible
- | (Meta n, Meta m) ->
- if n=m
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
- else raise NotConvertible
- | _ -> raise NotConvertible)
-
- (* 2 index known to be bound to no constant *)
- | (FRel n, FRel m) ->
- if reloc_rel n el1 = reloc_rel m el2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
- else raise NotConvertible
-
- (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *)
- | (FFlex fl1, FFlex fl2) ->
- (try (* try first intensional equality *)
- if fl1 = fl2
- then
- convert_stacks infos lft1 lft2 v1 v2 cuniv
- else raise NotConvertible
- with NotConvertible ->
- (* else expand the second occurrence (arbitrary heuristic) *)
- match unfold_reference infos fl2 with
- | Some def2 ->
- eqappr cv_pb infos appr1
- (lft2, fhnf_apply infos n2 def2 v2) cuniv
- | None ->
- (match unfold_reference infos fl1 with
- | Some def1 ->
- eqappr cv_pb infos
- (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv
- | None -> raise NotConvertible))
-
- (* only one constant, existential, defined var or defined rel *)
- | (FFlex fl1, _) ->
- (match unfold_reference infos fl1 with
- | Some def1 ->
- eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1)
- appr2 cuniv
- | None -> raise NotConvertible)
- | (_, FFlex fl2) ->
- (match unfold_reference infos fl2 with
- | Some def2 ->
- eqappr cv_pb infos appr1
- (lft2, fhnf_apply infos n2 def2 v2)
- cuniv
- | None -> raise NotConvertible)
-
- (* other constructors *)
- | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) ->
- if stack_args_size v1 = 0 && stack_args_size v2 = 0
- then
- let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
- ccnv CONV infos
- (el_lift el1) (el_lift el2) c2 c'2 u1
- else raise NotConvertible
-
- | (FLetIn _, _) | (_, FLetIn _) ->
- anomaly "LetIn normally removed by fhnf"
-
- | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) ->
- if stack_args_size v1 = 0 && stack_args_size v2 = 0
- then (* Luo's system *)
- let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in
- ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1
- else raise NotConvertible
-
- (* Inductive types: Ind Construct Case Fix Cofix *)
-
- (* Les annotations du Case ne servent qu'à l'affichage *)
-
- | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) ->
- let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in
- let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in
- let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
- convert_stacks infos lft1 lft2 v1 v2 u3
-
- | (FInd op1, FInd op2) ->
- if op1 = op2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
- else raise NotConvertible
-
- | (FConstruct op1, FConstruct op2) ->
- if op1 = op2
- then convert_stacks infos lft1 lft2 v1 v2 cuniv
- else raise NotConvertible
-
- | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) ->
- if op1 = op2
- then
- let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in
- let n = Array.length cl1 in
- let u2 =
- convert_vect infos
- (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
- else raise NotConvertible
-
- | (FCoFix (op1,(_,tys1,cl1),_,_), FCoFix(op2,(_,tys2,cl2),_,_)) ->
- if op1 = op2
- then
- let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in
- let n = Array.length cl1 in
- let u2 =
- convert_vect infos
- (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in
- convert_stacks infos lft1 lft2 v1 v2 u2
- else raise NotConvertible
-
- | _ -> raise NotConvertible
-
-and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
- match (decomp_stack stk1, decomp_stack stk2) with
- (Some(a1,s1), Some(a2,s2)) ->
- let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in
- convert_stacks infos lft1 lft2 s1 s2 u1
- | (None, None) -> cuniv
- | _ -> raise NotConvertible
-
-and convert_vect infos lft1 lft2 v1 v2 cuniv =
- let lv1 = Array.length v1 in
- let lv2 = Array.length v2 in
- if lv1 = lv2
- then
- let rec fold n univ =
- if n >= lv1 then univ
- else
- let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
- fold (n+1) u1 in
- fold 0 cuniv
- else raise NotConvertible
-
-
-
-let fconv cv_pb env sigma t1 t2 =
- if eq_constr t1 t2 then
- Constraint.empty
- else
- let infos = create_clos_infos hnf_flags env in
- ccnv cv_pb infos ELID ELID
- (inject (nf_evar sigma t1))
- (inject (nf_evar sigma t2))
- Constraint.empty
-let conv env = fconv CONV env
-let conv_leq env = fconv CUMUL env
+let conv env sigma t1 t2 =
+ Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2)
+let conv_leq env sigma t1 t2 =
+ Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2)
+let fconv = function CONV -> conv | CUMUL -> conv_leq
(*
let convleqkey = Profile.declare_profile "conv_leq";;
@@ -680,10 +520,11 @@ let conv_forall2_i f env sigma v1 v2 =
v1 v2
let test_conversion f env sigma x y =
- try let _ = f env sigma x y in true with NotConvertible -> false
+ try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true
+ with NotConvertible -> false
-let is_conv env sigma = test_conversion conv env sigma
-let is_conv_leq env sigma = test_conversion conv_leq env sigma
+let is_conv env sigma = test_conversion Reduction.conv env sigma
+let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
(********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8bd3ab489..d545e96cb 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -157,8 +157,6 @@ val reduce_fix : local_state_reduction_function -> fixpoint
type conversion_test = constraints -> constraints
-exception NotConvertible
-
type conv_pb =
| CONV
| CUMUL
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b49c2004b..5e0132468 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -328,8 +328,6 @@ let close_section _ s =
(process_item oldenv newdir olddir) ([],[],([],[],[])) decls
in
let ids = last_section_hyps olddir in
- Global.pop_named_decls ids;
Summary.unfreeze_lost_summaries fs;
- add_frozen_state ();
catch_not_found (List.iter process_operation) (List.rev ops);
Nametab.push_section olddir
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8a1186086..7090384bc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,17 +100,10 @@ let rec vernac interpfun input =
let rec interp com =
match com with
| Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
- let verbosely = verbosely = "Verbose" in
- raw_load_vernac_file verbosely (make_suffix fname ".v")
+ let verbosely = (verbosely = "Verbose") in
+ let _ = read_vernac_file verbosely (make_suffix fname ".v") in
+ ()
-(* | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
- Str (_,mname); Str(_,fname)]) ->
- let verbosely = verbosely = "Verbose" in
- let only_spec = only_spec = "Specification" in
- States.with_heavy_rollback (* to roll back in case of error *)
- (raw_compile_module verbosely only_spec mname)
- (make_suffix fname ".v")
-*)
| Node(_,"VernacList",l) ->
List.iter interp l
@@ -127,22 +120,6 @@ let rec vernac interpfun input =
interp com
with e ->
raise (DuringCommandInterp (Ast.loc com, e))
-
-and raw_load_vernac_file verbosely s =
- let _ = read_vernac_file verbosely s in ()
-
-(*
-and raw_compile_module verbosely only_spec mname file =
- assert false; (* I bet this code is never used in practice. Judicael. *)
- Library.import_module mname; (* ??? *)
- let lfname = read_vernac_file verbosely file in
- let base = Filename.chop_suffix lfname ".v" in
- Pfedit.check_no_pending_proofs ();
- if only_spec then
- failwith ".vi not yet implemented"
- else
- Discharge.save_module_to mname base
-*)
and read_vernac_file verbosely s =
let interpfun =
@@ -171,7 +148,7 @@ let raw_do_vernac po =
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
try
- raw_load_vernac_file verb file
+ let _ = read_vernac_file verb file in ()
with e ->
raise_with_file file e
@@ -184,7 +161,7 @@ let compile verbosely f =
let ldir0 = Library.find_logical_path (Filename.dirname longf) in
let ldir = Nameops.extend_dirpath ldir0 m in
Lib.start_module ldir;
- load_vernac verbosely longf;
+ let _ = load_vernac verbosely longf in
let mid = Lib.end_module m in
assert (mid = ldir);
Library.save_module_to ldir (longf^"o")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:29:32 +0000