diff options
author | Gabriel Scherer <gabriel.scherer@gmail.com> | 2015-06-26 21:54:11 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 12:45:41 +0200 |
commit | 2e9f7fa33a229634ec536b4dcdbf59ab666749fc (patch) | |
tree | f3828836b9a6f0a17dac69f9db870a9d90835010 | |
parent | c1caa158add73e6e6028ade81a0cb4540a845d18 (diff) |
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.
-rw-r--r-- | interp/constrintern.ml | 34 |
1 files changed, 19 insertions, 15 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ff1fd929b..e37de92a4 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 |