From 2e9f7fa33a229634ec536b4dcdbf59ab666749fc Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 26 Jun 2015 21:54:11 +0200 Subject: minor clarifications in constrintern.ml:sort_fields Note that turning let boolean = not regular in if boolean && complete then ...; if boolean && complete then ...; into if not regular && complete then ...; if not regular && complete then ...; has absolutely no performance cost: negation inside a conditional is not computed as a boolean, it only flips the branches. The code is more readable because "boolean" was a terrible variable name. --- interp/constrintern.ml | 34 +++++++++++++++++++--------------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ff1fd929b1..e37de92a42 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1032,8 +1032,10 @@ let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) -let sort_fields mode loc l completer = -(*mode=false if pattern and true if constructor*) +let sort_fields ~complete loc l completer = + (* the 'complete' parameter is true when we require that all the + record fields be provided -- when building a new record value; + when pattern-matching, the list of fields may be partial. *) match l with | [] -> None | (refer, value)::rem -> @@ -1053,27 +1055,28 @@ let sort_fields mode loc l completer = let rec build_patt l m i acc = match l with | [] -> (i, acc) - | (Some name) :: b-> - (match m with + | (Some name) :: b -> + begin match m with | [] -> anomaly (Pp.str "Number of projections mismatch") | (_, regular)::tm -> - let boolean = not regular in begin match global_reference_of_reference refer with | ConstRef name' when eq_constant name name' -> - if boolean && mode then - user_err_loc (loc, "", str"No local fields allowed in a record construction.") + if not regular && complete then + user_err_loc (loc, "", str "No local fields allowed in a record construction.") else build_patt b tm (i + 1) (i, snd acc) (* we found it *) | _ -> - build_patt b tm (if boolean&&mode then i else i + 1) - (if boolean && mode then acc + build_patt b tm + (if not regular && complete then i else i + 1) + (if not regular && complete then acc else fst acc, (i, ConstRef name) :: snd acc) - end) + end + end | None :: b-> (* we don't want anonymous fields *) - if mode then + if complete then user_err_loc (loc, "", str "This record contains anonymous fields.") else build_patt b m (i+1) acc (* anonymous arguments don't appear in m *) - in + in let ind = record.Recordops.s_CONST in try (* insertion of Constextern.reference_global *) (record.Recordops.s_EXPECTEDPARAM, @@ -1109,7 +1112,8 @@ let sort_fields mode loc l completer = sf rem ([first_index, value], list_proj) in (* we sort them *) let sorted_indexed_pattern = - List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in + let cmp_by_index (i, _) (j, _) = Int.compare i j in + List.sort cmp_by_index unsorted_indexed_pattern in (* a function to complete with wildcards *) let rec complete_list n l = if n <= 1 then l else complete_list (n-1) (completer n l) in @@ -1220,7 +1224,7 @@ let drop_notations_pattern looked_for = | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id) | CPatRecord (loc, l) -> let sorted_fields = - sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in + sort_fields ~complete:false loc l (fun _ l -> (CPatAtom (loc, None))::l) in begin match sorted_fields with | None -> RCPatAtom (loc, None) | Some (n, head, pl) -> @@ -1587,7 +1591,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CRecord (loc, fs) -> let cargs = - sort_fields true loc fs + sort_fields ~complete:true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) in begin -- cgit v1.2.3 From ca3226f42346dbbb8e08ab0b6bc3024aecb0cc4a Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 26 Jun 2015 22:03:18 +0200 Subject: whitespace: untabity constrinternl.ml:sort_fields --- interp/constrintern.ml | 167 +++++++++++++++++++++++++------------------------ 1 file changed, 84 insertions(+), 83 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e37de92a42..dc80140d4b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1039,92 +1039,93 @@ let sort_fields ~complete loc l completer = match l with | [] -> None | (refer, value)::rem -> - let (nparams, (* the number of parameters *) - base_constructor, (* the reference constructor of the record *) - (max, (* number of params *) - (first_index, (* index of the first field of the record *) - list_proj))) (* list of projections *) - = - let record = - try Recordops.find_projection - (global_reference_of_reference refer) - with Not_found -> - user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection") - in - (* elimination of the first field from the projections *) - let rec build_patt l m i acc = - match l with - | [] -> (i, acc) - | (Some name) :: b -> - begin match m with - | [] -> anomaly (Pp.str "Number of projections mismatch") - | (_, regular)::tm -> + let (nparams, (* the number of parameters *) + base_constructor, (* the reference constructor of the record *) + (max, (* number of params *) + (first_index, (* index of the first field of the record *) + list_proj))) (* list of projections *) + = + let record = + try Recordops.find_projection + (global_reference_of_reference refer) + with Not_found -> + user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection") + in + (* elimination of the first field from the projections *) + let rec build_patt l m i acc = + match l with + | [] -> (i, acc) + | (Some name) :: b -> + begin match m with + | [] -> anomaly (Pp.str "Number of projections mismatch") + | (_, regular)::tm -> begin match global_reference_of_reference refer with - | ConstRef name' when eq_constant name name' -> - if not regular && complete then - user_err_loc (loc, "", str "No local fields allowed in a record construction.") - else build_patt b tm (i + 1) (i, snd acc) (* we found it *) + | ConstRef name' when eq_constant name name' -> + if not regular && complete then + user_err_loc (loc, "", str "No local fields allowed in a record construction.") + else build_patt b tm (i + 1) (i, snd acc) (* we found it *) | _ -> - build_patt b tm - (if not regular && complete then i else i + 1) - (if not regular && complete then acc - else fst acc, (i, ConstRef name) :: snd acc) - end - end - | None :: b-> (* we don't want anonymous fields *) - if complete then - user_err_loc (loc, "", str "This record contains anonymous fields.") - else build_patt b m (i+1) acc - (* anonymous arguments don't appear in m *) - in - let ind = record.Recordops.s_CONST in - try (* insertion of Constextern.reference_global *) - (record.Recordops.s_EXPECTEDPARAM, - Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)), - build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[])) - with Not_found -> anomaly (Pp.str "Environment corruption for records.") - in - (* now we want to have all fields of the pattern indexed by their place in - the constructor *) - let rec sf patts accpatt = - match patts with - | [] -> accpatt - | p::q-> - let refer, patt = p in - let glob_refer = try global_reference_of_reference refer - with |Not_found -> - user_err_loc (loc_of_reference refer, "intern", - str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in - let rec add_patt l acc = - match l with - | [] -> - user_err_loc - (loc, "", - str "This record contains fields of different records.") - | (i, a) :: b-> - if eq_gr glob_refer a - then (i,List.rev_append acc l) - else add_patt b ((i,a)::acc) - in - let (index, projs) = add_patt (snd accpatt) [] in - sf q ((index, patt)::fst accpatt, projs) in - let (unsorted_indexed_pattern, remainings) = - sf rem ([first_index, value], list_proj) in - (* we sort them *) - let sorted_indexed_pattern = + build_patt b tm + (if not regular && complete then i else i + 1) + (if not regular && complete then acc + else fst acc, (i, ConstRef name) :: snd acc) + end + end + | None :: b-> (* we don't want anonymous fields *) + if complete then + user_err_loc (loc, "", str "This record contains anonymous fields.") + else build_patt b m (i+1) acc + (* anonymous arguments don't appear in m *) + in + let ind = record.Recordops.s_CONST in + try (* insertion of Constextern.reference_global *) + (record.Recordops.s_EXPECTEDPARAM, + Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)), + build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[])) + with Not_found -> anomaly (Pp.str "Environment corruption for records.") + in + (* now we want to have all fields of the pattern indexed by their place in + the constructor *) + let rec sf patts accpatt = + match patts with + | [] -> accpatt + | p::q-> + let refer, patt = p in + let glob_refer = try global_reference_of_reference refer + with |Not_found -> + user_err_loc (loc_of_reference refer, "intern", + str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in + let rec add_patt l acc = + match l with + | [] -> + user_err_loc + (loc, "", + str "This record contains fields of different records.") + | (i, a) :: b-> + if eq_gr glob_refer a + then (i,List.rev_append acc l) + else add_patt b ((i,a)::acc) + in + let (index, projs) = add_patt (snd accpatt) [] in + sf q ((index, patt)::fst accpatt, projs) in + let (unsorted_indexed_pattern, remainings) = + sf rem ([first_index, value], list_proj) in + (* we sort them *) + let sorted_indexed_pattern = let cmp_by_index (i, _) (j, _) = Int.compare i j in - List.sort cmp_by_index unsorted_indexed_pattern in - (* a function to complete with wildcards *) - let rec complete_list n l = - if n <= 1 then l else complete_list (n-1) (completer n l) in - (* a function to remove indice *) - let rec clean_list l i acc = - match l with - | [] -> complete_list (max - i) acc - | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc)) - in - Some (nparams, base_constructor, - List.rev (clean_list sorted_indexed_pattern 0 [])) + List.sort cmp_by_index unsorted_indexed_pattern in + (* a function to complete with wildcards *) + let rec complete_list n l = + if n <= 1 then l else complete_list (n-1) (completer n l) in + (* a function to remove indice *) + let rec clean_list l i acc = + match l with + | [] -> complete_list (max - i) acc + | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc)) + in + Some (nparams, base_constructor, + List.rev (clean_list sorted_indexed_pattern 0 [])) + (** {6 Manage multiple aliases} *) -- cgit v1.2.3 From 39163205cc59b98028eaaeace86463bb8c990818 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sat, 27 Jun 2015 22:01:07 +0200 Subject: minor: in constrintern.ml:sort_fields, clarify build_patt The code was a big "try..with" defining all useful quantities at once. I tried to lift definitions out of this try..with to define them as early as possible: the record's information and the first field name are fetched before processing the other fields. There were two calls in the try..with body that could raise the Not_found exception (or at least I don't know the code well enough to be sure that either of them cannot): `shortest_qualid_of_global` and `build_patt`. They are now split in two separate try..with blocks, both raising the same exception (with a shared error message named `env_error_msg`). Someone familiar with the invariants at play could probably remove one of the two blocks, streamlining the code even further. I'm a bit surprised by the main logic part (the big (if .. else if .. else if ..) block in the new code), and there is a question in a comment. I hope to get it answered during code review and remove it (and maybe simplify the code). Finally, there was an apparently-stale comment in the code: (* insertion of Constextern.reference_global *) of course Constextern.reference_global corresponds to now function that I could find. After trying to understand the meaning of this comment, I decided to just remove it. --- interp/constrintern.ml | 96 ++++++++++++++++++++++++++++---------------------- 1 file changed, 54 insertions(+), 42 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index dc80140d4b..3bd03aecca 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1038,52 +1038,64 @@ let sort_fields ~complete loc l completer = when pattern-matching, the list of fields may be partial. *) match l with | [] -> None - | (refer, value)::rem -> - let (nparams, (* the number of parameters *) - base_constructor, (* the reference constructor of the record *) - (max, (* number of params *) - (first_index, (* index of the first field of the record *) - list_proj))) (* list of projections *) + | (first_field_ref, first_field_value):: other_fields -> + let env_error_msg = "Environment corruption for records." in + let first_field_glob_ref = + try global_reference_of_reference first_field_ref + with Not_found -> anomaly (Pp.str env_error_msg) in + let record = + try Recordops.find_projection first_field_glob_ref + with Not_found -> + user_err_loc (loc_of_reference first_field_ref, "intern", + pr_reference first_field_ref ++ str": Not a projection") + in + (* the number of parameters *) + let nparams = record.Recordops.s_EXPECTEDPARAM in + (* the reference constructor of the record *) + let base_constructor = + let global_record_id = ConstructRef record.Recordops.s_CONST in + try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) + with Not_found -> anomaly (Pp.str env_error_msg) in + let (end_index, (* one past the last field index *) + first_field_index, (* index of the first field of the record *) + proj_list) (* list of projections *) = - let record = - try Recordops.find_projection - (global_reference_of_reference refer) - with Not_found -> - user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection") - in - (* elimination of the first field from the projections *) - let rec build_patt l m i acc = - match l with - | [] -> (i, acc) - | (Some name) :: b -> - begin match m with + (* elimitate the first field from the projections, + but keep its index *) + let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc = + match projs with + | [] -> (idx, acc_first_idx, acc) + | (Some name) :: projs -> + let field_glob_ref = ConstRef name in + let first_field = eq_gr field_glob_ref first_field_glob_ref in + begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch") - | (_, regular)::tm -> - begin match global_reference_of_reference refer with - | ConstRef name' when eq_constant name name' -> - if not regular && complete then - user_err_loc (loc, "", str "No local fields allowed in a record construction.") - else build_patt b tm (i + 1) (i, snd acc) (* we found it *) - | _ -> - build_patt b tm - (if not regular && complete then i else i + 1) - (if not regular && complete then acc - else fst acc, (i, ConstRef name) :: snd acc) - end + | (_, regular) :: proj_kinds -> + if first_field && not regular && complete then + (* G.S.: why do we fail only in the + first-field case? I would expect to fail + whenever (not regular && complete), and + skip the fields only when (not complete *) + user_err_loc (loc, "", str "No local fields allowed in a record construction.") + else if first_field then + build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc + else if not regular && complete then + (* skip non-regular fields *) + build_proj_list projs proj_kinds idx ~acc_first_idx acc + else + build_proj_list projs proj_kinds (idx+1) ~acc_first_idx + ((idx, field_glob_ref) :: acc) end - | None :: b-> (* we don't want anonymous fields *) + | None :: projs -> if complete then + (* we don't want anonymous fields *) user_err_loc (loc, "", str "This record contains anonymous fields.") - else build_patt b m (i+1) acc - (* anonymous arguments don't appear in m *) - in - let ind = record.Recordops.s_CONST in - try (* insertion of Constextern.reference_global *) - (record.Recordops.s_EXPECTEDPARAM, - Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)), - build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[])) - with Not_found -> anomaly (Pp.str "Environment corruption for records.") + else + (* anonymous arguments don't appear in proj_kinds *) + build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc in + build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 [] + in (* now we want to have all fields of the pattern indexed by their place in the constructor *) let rec sf patts accpatt = @@ -1109,7 +1121,7 @@ let sort_fields ~complete loc l completer = let (index, projs) = add_patt (snd accpatt) [] in sf q ((index, patt)::fst accpatt, projs) in let (unsorted_indexed_pattern, remainings) = - sf rem ([first_index, value], list_proj) in + sf other_fields ([first_field_index, first_field_value], proj_list) in (* we sort them *) let sorted_indexed_pattern = let cmp_by_index (i, _) (j, _) = Int.compare i j in @@ -1120,7 +1132,7 @@ let sort_fields ~complete loc l completer = (* a function to remove indice *) let rec clean_list l i acc = match l with - | [] -> complete_list (max - i) acc + | [] -> complete_list (end_index - i) acc | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc)) in Some (nparams, base_constructor, -- cgit v1.2.3 From 56a7d450fb67268d121e69a5e111968d0dfb2a6a Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sat, 27 Jun 2015 22:01:38 +0200 Subject: add CList.extract_first we already have val remove_first : ('a -> bool) -> 'a list -> 'a list (** Remove the first element satisfying a predicate, or raise [Not_found] *) now we also have the more general val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a (** Remove and return the first element satisfying a predicate, or raise [Not_found] *) The implementation is tail-recursive. The code I'm hoping to factorize reimplements extract_first in a tail-recursive way, so it seemed good to preserve this. On the other hand remove_first is not tail-recursive itself, and that gives better constant factors in real-life cases. It's unclear what is the best choice. --- lib/cList.ml | 9 +++++++++ lib/cList.mli | 4 ++++ 2 files changed, 13 insertions(+) diff --git a/lib/cList.ml b/lib/cList.ml index 3a792d4168..602bba6a5c 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -65,6 +65,7 @@ sig val except : 'a eq -> 'a -> 'a list -> 'a list val remove : 'a eq -> 'a -> 'a list -> 'a list val remove_first : ('a -> bool) -> 'a list -> 'a list + val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val sep_last : 'a list -> 'a * 'a list @@ -461,6 +462,14 @@ let rec remove_first p = function | b::l -> b::remove_first p l | [] -> raise Not_found +let extract_first p li = + let rec loop rev_left = function + | [] -> raise Not_found + | x::right -> + if p x then List.rev_append rev_left right, x + else loop (x :: rev_left) right + in loop [] li + let insert p v l = let rec insrec = function | [] -> [v] diff --git a/lib/cList.mli b/lib/cList.mli index b19d1a80fc..bc8749b4f8 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -125,6 +125,10 @@ sig val remove_first : ('a -> bool) -> 'a list -> 'a list (** Remove the first element satisfying a predicate, or raise [Not_found] *) + val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a + (** Remove and return the first element satisfying a predicate, + or raise [Not_found] *) + val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list (** Insert at the (first) position so that if the list is ordered wrt to the total order given as argument, the order is preserved *) -- cgit v1.2.3 From 5a212ff444e9e231f5b56629e5cf15087bac69c6 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sat, 27 Jun 2015 22:23:41 +0200 Subject: minor: in constrintern.ml:sort_fields, clarify sf The internal `add_pat` function is replaced by a call to `CList.extract_first`. --- interp/constrintern.ml | 43 ++++++++++++++++++++----------------------- 1 file changed, 20 insertions(+), 23 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3bd03aecca..49758f4d54 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1098,30 +1098,27 @@ let sort_fields ~complete loc l completer = in (* now we want to have all fields of the pattern indexed by their place in the constructor *) - let rec sf patts accpatt = - match patts with - | [] -> accpatt - | p::q-> - let refer, patt = p in - let glob_refer = try global_reference_of_reference refer + let rec index_fields fields remaining_projs acc = + match fields with + | [] -> acc + | (field_ref, field_value) :: fields -> + let field_glob_ref = try global_reference_of_reference field_ref with |Not_found -> - user_err_loc (loc_of_reference refer, "intern", - str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in - let rec add_patt l acc = - match l with - | [] -> - user_err_loc - (loc, "", - str "This record contains fields of different records.") - | (i, a) :: b-> - if eq_gr glob_refer a - then (i,List.rev_append acc l) - else add_patt b ((i,a)::acc) - in - let (index, projs) = add_patt (snd accpatt) [] in - sf q ((index, patt)::fst accpatt, projs) in - let (unsorted_indexed_pattern, remainings) = - sf other_fields ([first_field_index, first_field_value], proj_list) in + user_err_loc (loc_of_reference field_ref, "intern", + str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in + let remaining_projs, (field_index, _) = + let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in + try CList.extract_first the_proj remaining_projs + with Not_found -> + user_err_loc + (loc, "", + str "This record contains fields of different records.") + in + index_fields fields remaining_projs ((field_index, field_value) :: acc) + in + let unsorted_indexed_pattern = + index_fields other_fields proj_list + [(first_field_index, first_field_value)] in (* we sort them *) let sorted_indexed_pattern = let cmp_by_index (i, _) (j, _) = Int.compare i j in -- cgit v1.2.3 From ed015ec083e298b2e65b7b61fcf924642d438ee4 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sat, 27 Jun 2015 22:37:23 +0200 Subject: minor: interp/constrintern.ml, clarify field completion The type of the user-defined function "completer" changes to be simpler and better reflect its purpose: provide values for missing field assignments. In the future we may want to also pass the name of the field as parameter (currently only the index is given, and both uses of the function ignore it), in particular if we want to implement { r with x = ...; y = ... }. --- interp/constrintern.ml | 37 ++++++++++++++++--------------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 49758f4d54..da7f551168 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1100,7 +1100,6 @@ let sort_fields ~complete loc l completer = the constructor *) let rec index_fields fields remaining_projs acc = match fields with - | [] -> acc | (field_ref, field_value) :: fields -> let field_glob_ref = try global_reference_of_reference field_ref with |Not_found -> @@ -1115,26 +1114,22 @@ let sort_fields ~complete loc l completer = str "This record contains fields of different records.") in index_fields fields remaining_projs ((field_index, field_value) :: acc) + | [] -> + (* the order does not matter as we sort them next, + List.rev_* is just for efficiency *) + let remaining_fields = + let complete_field (idx, _field_ref) = (idx, completer idx) in + List.rev_map complete_field remaining_projs in + List.rev_append remaining_fields acc in - let unsorted_indexed_pattern = + let unsorted_indexed_fields = index_fields other_fields proj_list [(first_field_index, first_field_value)] in - (* we sort them *) - let sorted_indexed_pattern = + let sorted_indexed_fields = let cmp_by_index (i, _) (j, _) = Int.compare i j in - List.sort cmp_by_index unsorted_indexed_pattern in - (* a function to complete with wildcards *) - let rec complete_list n l = - if n <= 1 then l else complete_list (n-1) (completer n l) in - (* a function to remove indice *) - let rec clean_list l i acc = - match l with - | [] -> complete_list (end_index - i) acc - | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc)) - in - Some (nparams, base_constructor, - List.rev (clean_list sorted_indexed_pattern 0 [])) - + List.sort cmp_by_index unsorted_indexed_fields in + let sorted_fields = List.map snd sorted_indexed_fields in + Some (nparams, base_constructor, sorted_fields) (** {6 Manage multiple aliases} *) @@ -1234,7 +1229,7 @@ let drop_notations_pattern looked_for = | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id) | CPatRecord (loc, l) -> let sorted_fields = - sort_fields ~complete:false loc l (fun _ l -> (CPatAtom (loc, None))::l) in + sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in begin match sorted_fields with | None -> RCPatAtom (loc, None) | Some (n, head, pl) -> @@ -1600,12 +1595,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (merge_impargs l args) loc | CRecord (loc, fs) -> - let cargs = + let fields = sort_fields ~complete:true loc fs - (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) + (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None)) in begin - match cargs with + match fields with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in -- cgit v1.2.3 From c11b7c5a34ea16a32a78c796a219d29edd117e74 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Mon, 29 Jun 2015 16:24:32 +0200 Subject: minor: documentation comment for constrintern.ml:sort_fields (Because the function is private to the module, it is documented in the .ml rather than the .mli) --- interp/constrintern.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index da7f551168..56a191262c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1032,11 +1032,21 @@ let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) -let sort_fields ~complete loc l completer = - (* the 'complete' parameter is true when we require that all the - record fields be provided -- when building a new record value; - when pattern-matching, the list of fields may be partial. *) - match l with +(** [sort_fields ~complete loc fields completer] expects a list + [fields] of field assignments [f = e1; g = e2; ...], where [f, g] + are fields of a record and [e1] are "values" (either terms, when + interning a record construction, or patterns, when intering record + pattern-matching). It will sort the fields according to the record + declaration order (which is important when type-checking them in + presence of dependencies between fields). If the parameter + [complete] is true, we require the assignment to be complete: all + the fields of the record must be present in the + assignment. Otherwise the record assignment may be partial + (in a pattern, we may match on some fields only), and we call the + function [completer] to fill the missing fields; the returned + field assignment list is always complete. *) +let sort_fields ~complete loc fields completer = + match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> let env_error_msg = "Environment corruption for records." in @@ -1096,13 +1106,13 @@ let sort_fields ~complete loc l completer = in build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 [] in - (* now we want to have all fields of the pattern indexed by their place in + (* now we want to have all fields assignments indexed by their place in the constructor *) let rec index_fields fields remaining_projs acc = match fields with | (field_ref, field_value) :: fields -> let field_glob_ref = try global_reference_of_reference field_ref - with |Not_found -> + with Not_found -> user_err_loc (loc_of_reference field_ref, "intern", str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = -- cgit v1.2.3 From c83fa10156545bce96ef4a0f93e8695ec353c834 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 30 Jun 2015 18:06:06 +0200 Subject: minor: comment on the meaning of the 'boolean' variable --- interp/constrintern.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 56a191262c..5c5a900fba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1081,11 +1081,10 @@ let sort_fields ~complete loc fields completer = begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch") | (_, regular) :: proj_kinds -> + (* "regular" is false when the field is defined + by a let-in in the record declaration + (its value is fixed from other fields). *) if first_field && not regular && complete then - (* G.S.: why do we fail only in the - first-field case? I would expect to fail - whenever (not regular && complete), and - skip the fields only when (not complete *) user_err_loc (loc, "", str "No local fields allowed in a record construction.") else if first_field then build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc -- cgit v1.2.3