diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-29 10:13:12 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-09 15:58:17 +0100 |
commit | 34ef02fac1110673ae74c41c185c228ff7876de2 (patch) | |
tree | a688eb9e2c23fc5353391f0c8b4ba1d7ba327844 /pretyping/typing.ml | |
parent | e9675e068f9e0e92bab05c030fb4722b146123b8 (diff) |
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.
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r-- | pretyping/typing.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb0c49320..8be28a620 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -18,6 +18,7 @@ open Inductive open Inductiveops open Typeops open Arguments_renaming +open Context.Rel.Declaration let meta_type evd mv = let ty = @@ -88,16 +89,16 @@ let e_is_correct_arity env evdref c pj ind specif params = let rec srec env pt ar = let pt' = whd_betadeltaiota env !evdref pt in match kind_of_term pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> if not (Evarconv.e_cumul env evdref a1 a1') then error (); - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Sort s, [] -> if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () | Evar (ev,_), [] -> let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in evdref := Evd.define ev (mkSort s) evd - | _, (_,Some _,_ as d)::ar' -> + | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> error () @@ -229,14 +230,14 @@ let rec execute env evdref cstr = | Lambda (name,c1,c2) -> let j = execute env evdref c1 in let var = e_type_judgment env evdref j in - let env1 = push_rel (name,None,var.utj_val) env in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> let j = execute env evdref c1 in let varj = e_type_judgment env evdref j 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 evdref c2 in let varj' = e_type_judgment env1 evdref j' in judge_of_product env name varj varj' @@ -246,7 +247,7 @@ let rec execute env evdref cstr = let j2 = execute env evdref c2 in let j2 = e_type_judgment env evdref j2 in let _ = e_judge_of_cast env evdref 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 j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 |