diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 198 |
1 files changed, 83 insertions, 115 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index cd376b69..16ddfac6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,14 +20,14 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) -open Errors +open CErrors open Util open Names open Term -open Context open Vars open Declarations open Pre_env +open Context.Rel.Declaration (* The type of environments. *) @@ -45,46 +45,43 @@ let empty_named_context_val = empty_named_context_val let empty_env = empty_env let engagement env = env.env_stratification.env_engagement +let typing_flags env = env.env_typing_flags let is_impredicative_set env = - match fst (engagement env) with + match engagement env with | ImpredicativeSet -> true | _ -> false -let type_in_type env = - match snd (engagement env) with - | TypeInType -> true - | _ -> false +let type_in_type env = not (typing_flags env).check_universes +let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes -let named_context env = env.env_named_context -let named_context_val env = env.env_named_context,env.env_named_vals +let named_context env = env.env_named_context.env_named_ctx +let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context with + match env.env_rel_context, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false (* Rel context *) let lookup_rel n env = - lookup_rel n env.env_rel_context + Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = - match lookup_rel n env with - | (_,Some _,_) -> true - | _ -> false + is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel let push_rel = push_rel -let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x +let push_rel_context ctxt x = Context.Rel.fold_outside 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 let fold_rel_context f env ~init = @@ -102,25 +99,14 @@ let fold_rel_context f env ~init = (* Named context *) -let named_context_of_val = fst -let named_vals_of_val = snd +let named_context_of_val c = c.env_named_ctx (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f (ctxt,ctxtv) = - let rec map ctx = match ctx with - | [] -> [] - | (id, body, typ) :: rem -> - let body' = Option.smartmap f body in - let typ' = f typ in - let rem' = map rem in - if body' == body && typ' == typ && rem' == rem then ctx - else (id, body', typ') :: rem' - in - (map ctxt, ctxtv) +let map_named_val = map_named_val -let empty_named_context = empty_named_context +let empty_named_context = Context.Named.empty let push_named = push_named let push_named_context = List.fold_right push_named @@ -130,30 +116,31 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.lookup_named id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt +let lookup_named = lookup_named +let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = - c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) +open Context.Named.Declaration + let named_type id env = - let (_,_,t) = lookup_named id env in t + get_type (lookup_named id env) let named_body id env = - let (_,b,_) = lookup_named id env in b + get_value (lookup_named id env) let evaluable_named id env = match named_body id env with | Some _ -> true | _ -> false -let reset_with_named_context (ctxt,ctxtv) env = +let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_named_vals = ctxtv; - env_rel_context = empty_rel_context; + env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -167,16 +154,16 @@ let pop_rel_context n env = let fold_named_context f env ~init = let rec fold_right env = - match env.env_named_context with - | [] -> init - | d::ctxt -> + match match_named_context_val env.env_named_context with + | None -> init + | Some (d, v, rem) -> let env = - reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + reset_with_named_context rem env in f env d (fold_right env) in fold_right env let fold_named_context_reverse f ~init env = - Context.fold_named_context_reverse f ~init:init (named_context env) + Context.Named.fold_inside f ~init:init (named_context env) (* Universe constraints *) @@ -188,10 +175,10 @@ let map_universes f env = let add_constraints c env = if Univ.Constraint.is_empty c then env - else map_universes (Univ.merge_constraints c) env + else map_universes (UGraph.merge_constraints c) env let check_constraints c env = - Univ.check_constraints c env.env_stratification.env_universes + UGraph.check_constraints c env.env_stratification.env_universes let push_constraints_to_env (_,univs) env = add_constraints univs env @@ -199,19 +186,19 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in - Univ.merge_constraints (Univ.UContext.constraints ctx) g + UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = let g = Univ.LSet.fold - (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g - in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env @@ -220,6 +207,9 @@ let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } +let set_typing_flags c env = (* Unsafe *) + { env with env_typing_flags = c } + (* Global constants *) let lookup_constant = lookup_constant @@ -337,6 +327,9 @@ let polymorphic_pconstant (cst,u) env = if Univ.Instance.is_empty u then false else polymorphic_constant cst env +let type_in_type_constant cst env = + not (lookup_constant cst env).const_typing_flags.check_universes + let template_polymorphic_constant cst env = match (lookup_constant cst env).const_type with | TemplateArity _ -> true @@ -366,6 +359,9 @@ let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false else polymorphic_ind ind env +let type_in_type_ind (mind,i) env = + not (lookup_mind mind env).mind_typing_flags.check_universes + let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -389,11 +385,11 @@ let add_mind kn mib env = let lookup_constant_variables c env = let cmap = lookup_constant c env in - Context.vars_of_named_context cmap.const_hyps + Context.Named.to_vars cmap.const_hyps let lookup_inductive_variables (kn,i) env = let mis = lookup_mind kn env in - Context.vars_of_named_context mis.mind_hyps + Context.Named.to_vars mis.mind_hyps let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env @@ -427,15 +423,15 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = - Context.fold_named_context_reverse - (fun need (id,copt,t) -> - if Id.Set.mem id need then + Context.Named.fold_inside + (fun need decl -> + if Id.Set.mem (get_id decl) need then let globc = - match copt with - | None -> Id.Set.empty - | Some c -> global_vars_set env c in + match decl with + | LocalAssum _ -> Id.Set.empty + | LocalDef (_,c,_) -> global_vars_set env c in Id.Set.union - (global_vars_set env t) + (global_vars_set env (get_type decl)) (Id.Set.union globc need) else need) ~init:needed @@ -443,9 +439,9 @@ let really_needed env needed = let keep_hyps env needed = let really_needed = really_needed env needed in - Context.fold_named_context - (fun (id,_,_ as d) nsign -> - if Id.Set.mem id really_needed then add_named_decl d nsign + Context.Named.fold_outside + (fun d nsign -> + if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign else nsign) (named_context env) ~init:empty_named_context @@ -494,66 +490,35 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found -let apply_to_hyp (ctxt,vals) id f = - let rec aux rtail ctxt vals = - match ctxt, vals with - | (idc,c,ct as d)::ctxt, v::vals -> - if Id.equal idc id then - (f ctxt d rtail)::ctxt, v::vals +let apply_to_hyp ctxt id f = + let rec aux rtail ctxt = + match match_named_context_val ctxt with + | Some (d, v, ctxt) -> + if Id.equal (get_id d) id then + push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt else - let ctxt',vals' = aux (d::rtail) ctxt vals in - d::ctxt', v::vals' - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux [] ctxt vals - -let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = - let rec aux ctxt vals = - match ctxt,vals with - | (idc,c,ct as d)::ctxt, v::vals -> - if Id.equal idc id then - let sign = ctxt,vals in - push_named_context_val (f d sign) sign - else - let (ctxt,vals as sign) = aux ctxt vals in - push_named_context_val (g d sign) sign - | [],[] -> raise Hyp_not_found - | _,_ -> assert false - in aux ctxt vals - -let insert_after_hyp (ctxt,vals) id d check = - let rec aux ctxt vals = - match ctxt, vals with - | (idc,c,ct)::ctxt', v::vals' -> - if Id.equal idc id then begin - check ctxt; - push_named_context_val d (ctxt,vals) - end else - let ctxt,vals = aux ctxt vals in - d::ctxt, v::vals - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux ctxt vals - + let ctxt' = aux (d::rtail) ctxt in + push_named_context_val_val d v ctxt' + | None -> raise Hyp_not_found + in aux [] ctxt (* To be used in Logic.clear_hyps *) -let remove_hyps ids check_context check_value (ctxt, vals) = - let rec remove_hyps ctxt vals = match ctxt, vals with - | [], [] -> [], [] - | d :: rctxt, (nid, v) :: rvals -> - let (id, _, _) = d in - let ans = remove_hyps rctxt rvals in - if Id.Set.mem id ids then ans +let remove_hyps ids check_context check_value ctxt = + let rec remove_hyps ctxt = match match_named_context_val ctxt with + | None -> empty_named_context_val, false + | Some (d, v, rctxt) -> + let (ans, seen) = remove_hyps rctxt in + if Id.Set.mem (get_id d) ids then (ans, true) + else if not seen then ctxt, false else - let (rctxt', rvals') = ans in + let rctxt' = ans in let d' = check_context d in let v' = check_value v in - if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then - ctxt, vals - else (d' :: rctxt', (nid, v') :: rvals') - | _ -> assert false + if d == d' && v == v' && rctxt == rctxt' then + ctxt, true + else push_named_context_val_val d' v' rctxt', true in - remove_hyps ctxt vals + fst (remove_hyps ctxt) (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module @@ -602,7 +567,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an |