From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/environ.ml | 64 ++++++++++++++++++++++++++----------------------------- 1 file changed, 30 insertions(+), 34 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 847e1d08f..1089dff92 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -72,9 +72,8 @@ let lookup_rel n env = Context.Rel.lookup n env.env_rel_context let evaluable_rel n env = - match lookup_rel n env with - | (_,Some _,_) -> true - | _ -> false + let open Context.Rel.Declaration in + lookup_rel n env |> is_local_def let nb_rel env = env.env_nb_rel @@ -83,7 +82,8 @@ let push_rel = push_rel 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 open Context.Rel.Declaration 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 = @@ -107,17 +107,8 @@ let named_vals_of_val = snd (* [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 f = + on_fst (Context.Named.map f) let empty_named_context = Context.Named.empty @@ -138,10 +129,10 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) let named_type id env = - let (_,_,t) = lookup_named id env in t + lookup_named id env |> Context.Named.Declaration.get_type let named_body id env = - let (_,b,_) = lookup_named id env in b + lookup_named id env |> Context.Named.Declaration.get_value let evaluable_named id env = match named_body id env with @@ -426,15 +417,16 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = + let open Context.Named.Declaration in Context.Named.fold_inside - (fun need (id,copt,t) -> - if Id.Set.mem id need then + (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,8 +435,9 @@ let really_needed env needed = let keep_hyps env needed = let really_needed = really_needed env needed in Context.Named.fold_outside - (fun (id,_,_ as d) nsign -> - if Id.Set.mem id really_needed then Context.Named.add d nsign + (fun d nsign -> + let open Context.Named.Declaration in + 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,11 +487,12 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found let apply_to_hyp (ctxt,vals) id f = + let open Context.Named.Declaration in 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 + | d::ctxt, v::vals -> + if Id.equal (get_id d) id then + (f ctxt d rtail)::ctxt, v::vals else let ctxt',vals' = aux (d::rtail) ctxt vals in d::ctxt', v::vals' @@ -507,10 +501,11 @@ let apply_to_hyp (ctxt,vals) id f = in aux [] ctxt vals let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = + let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt,vals with - | (idc,c,ct as d)::ctxt, v::vals -> - if Id.equal idc id then + | d::ctxt, v::vals -> + if Id.equal (get_id d) id then let sign = ctxt,vals in push_named_context_val (f d sign) sign else @@ -521,10 +516,11 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = in aux ctxt vals let insert_after_hyp (ctxt,vals) id d check = + let open Context.Named.Declaration in let rec aux ctxt vals = match ctxt, vals with - | (idc,c,ct)::ctxt', v::vals' -> - if Id.equal idc id then begin + | decl::ctxt', v::vals' -> + if Id.equal (get_id decl) id then begin check ctxt; push_named_context_val d (ctxt,vals) end else @@ -537,12 +533,12 @@ let insert_after_hyp (ctxt,vals) id d check = (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value (ctxt, vals) = + let open Context.Named.Declaration in 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 + if Id.Set.mem (get_id d) ids then ans else let (rctxt', rvals') = ans in let d' = check_context d in -- cgit v1.2.3