diff options
| author | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
| commit | 6467119bd15395bb5fae7d9c19dde17293842bd8 (patch) | |
| tree | 809a7156570542f796b4ed94d901a83468d78dc4 /interp/constrintern.ml | |
| parent | 9beec0fc6cc283294bbbda363a3f788ae56347d5 (diff) | |
| parent | 0b5ef21f936acbb89fa5b272efdcf3cf03de58cc (diff) | |
Merge PR#719: Constrexpr.Numeral without bigint
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 67fee62028..89827300c4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1219,6 +1219,11 @@ let alias_of als = match als.alias_ids with *) +let is_zero s = + let rec aux i = + Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) + in aux 0 + let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1331,9 +1336,9 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[]) - when Bigint.is_strictly_pos p -> - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in + | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[]) + when not (is_zero p) -> + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in rcp_of_glob pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a @@ -1639,9 +1644,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = CAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[])) - when Bigint.is_strictly_pos p -> - intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p))) + | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[])) + when not (is_zero p) -> + intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) | CNotation ("( _ )",([a],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args |