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/typeops.ml | 39 ++++++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 17 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f31cba0a8..eeb12a2b4 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -77,8 +77,9 @@ let judge_of_type u = (*s Type of a de Bruijn index. *) let judge_of_relative env n = + let open Context.Rel.Declaration in try - let (_,_,typ) = lookup_rel n env in + let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -98,18 +99,20 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = + let open Context.Named.Declaration in Context.Named.fold_outside - (fun (id,b1,ty1) () -> + (fun d1 () -> + let id = get_id d1 in try - let (_,b2,ty2) = lookup_named id env in - conv env ty2 ty1; - (match b2,b1 with - | None, None -> () - | None, Some _ -> + let d2 = lookup_named id env in + conv env (get_type d2) (get_type d1); + (match d2,d1 with + | LocalAssum _, LocalAssum _ -> () + | LocalAssum _, LocalDef _ -> (* This is wrong, because we don't know if the body is needed or not for typechecking: *) () - | Some _, None -> raise NotConvertible - | Some b2, Some b1 -> conv env b2 b1); + | LocalDef _, LocalAssum _ -> raise NotConvertible + | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id c) sign @@ -124,9 +127,10 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let fold l (_, b, p) = match b with - | None -> extract_level env p :: l - | _ -> l + let open Context.Rel.Declaration in + let fold l = function + | LocalAssum (_,p) -> extract_level env p :: l + | LocalDef _ -> l in List.fold_left fold [] l @@ -416,6 +420,7 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -458,13 +463,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let j' = execute env1 c2 in judge_of_abstraction env name varj j' | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let varj' = execute_type env1 c2 in judge_of_product env name varj varj' @@ -472,7 +477,7 @@ let rec execute env cstr = let j1 = execute env c1 in let j2 = execute_type env c2 in let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in + let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in let j' = execute env1 c3 in judge_of_letin env name j1 j2 j' @@ -550,10 +555,10 @@ let infer_v env cv = let infer_local_decl env id = function | LocalDef c -> let j = infer env c in - (Name id, Some j.uj_val, j.uj_type) + Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type) | LocalAssum c -> let j = infer env c in - (Name id, None, assumption_of_judgment env j) + Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function -- cgit v1.2.3 From 1dddd062f35736285eb2940382df2b53224578a7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 16 Feb 2016 07:38:45 +0100 Subject: Renaming variants of Entries.local_entry The original datatype: Entries.local_entry = LocalDef of constr | LocalAssum of constr was changed to: Entries.local_entry = LocalDefEntry of constr | LocalAssumEntry of constr There are two advantages: 1. the new names are consistent with other variant names in the same module which also have this "*Entry" suffix 2. the new names do not collide with variants defined in the Context.{Rel,Named}.Declaration modules so both, "Entries" as well as "Context.{Rel,Named}.Declaration" can be open at the same time. The disadvantage is that those new variants are longer. But since those variants are rarely used, it it is not a big deal. --- kernel/entries.mli | 4 ++-- kernel/typeops.ml | 14 ++++++-------- toplevel/command.ml | 5 +++-- toplevel/discharge.ml | 5 +++-- toplevel/record.ml | 5 +++-- 5 files changed, 17 insertions(+), 16 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/entries.mli b/kernel/entries.mli index b2a77dd95..3ecfcca64 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -18,8 +18,8 @@ open Term (** {6 Local entries } *) type local_entry = - | LocalDef of constr - | LocalAssum of constr + | LocalDefEntry of constr + | LocalAssumEntry of constr (** {6 Declaration of inductive types. } *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index eeb12a2b4..0ea68e2bc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -18,6 +18,7 @@ open Entries open Reduction open Inductive open Type_errors +open Context.Rel.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -77,7 +78,6 @@ let judge_of_type u = (*s Type of a de Bruijn index. *) let judge_of_relative env n = - let open Context.Rel.Declaration in try let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; @@ -99,9 +99,9 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - let open Context.Named.Declaration in Context.Named.fold_outside (fun d1 () -> + let open Context.Named.Declaration in let id = get_id d1 in try let d2 = lookup_named id env in @@ -127,7 +127,6 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let open Context.Rel.Declaration in let fold l = function | LocalAssum (_,p) -> extract_level env p :: l | LocalDef _ -> l @@ -420,7 +419,6 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = - let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -553,12 +551,12 @@ let infer_v env cv = (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDef c -> + | LocalDefEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssum c -> + LocalDef (Name id, j.uj_val, j.uj_type) + | LocalAssumEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j) + LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function diff --git a/toplevel/command.ml b/toplevel/command.ml index 166fe94ea..284bcd75e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -38,6 +38,7 @@ open Misctypes open Vernacexpr open Sigma.Notations open Context.Rel.Declaration +open Entries let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l @@ -385,8 +386,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, Entries.LocalAssum t - | LocalDef (na,b,_) -> out_name na, Entries.LocalDef b + | LocalAssum (na,t) -> out_name na, LocalAssumEntry t + | LocalDef (na,b,_) -> out_name na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 5fa51e06e..ffa11679c 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -14,6 +14,7 @@ open Vars open Entries open Declarations open Cooking +open Entries open Context.Rel.Declaration (********************************) @@ -21,8 +22,8 @@ open Context.Rel.Declaration let detype_param = function - | LocalAssum (Name id, p) -> id, Entries.LocalAssum p - | LocalDef (Name id, p,_) -> id, Entries.LocalDef p + | LocalAssum (Name id, p) -> id, LocalAssumEntry p + | LocalDef (Name id, p,_) -> id, LocalDefEntry p | _ -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/record.ml b/toplevel/record.ml index 4cf81a250..c0bb9eb86 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,6 +26,7 @@ open Constrexpr_ops open Goptions open Sigma.Notations open Context.Rel.Declaration +open Entries (********** definition d'un record (structure) **************) @@ -164,8 +165,8 @@ let degenerate_decl decl = | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match decl with - | LocalAssum (_,t) -> (id, Entries.LocalAssum t) - | LocalDef (_,b,_) -> (id, Entries.LocalDef b) + | LocalAssum (_,t) -> (id, LocalAssumEntry t) + | LocalDef (_,b,_) -> (id, LocalDefEntry b) type record_error = | MissingProj of Id.t * Id.t list -- cgit v1.2.3