diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 19:05:57 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-04 11:28:49 +0200 |
commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
tree | d8e35952cc8f6111875e664d8884dc2c7f908206 /plugins/syntax/nat_syntax.ml | |
parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) |
Making detyping potentially lazy.
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
-rw-r--r-- | plugins/syntax/nat_syntax.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 524a5c522..2f9870cf9 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -37,11 +37,11 @@ let warn_large_nat = let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in + let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -56,13 +56,17 @@ let nat_of_int ?loc n = exception Non_closed_number -let rec int_of_nat x = CAst.with_val (function - | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) +let rec int_of_nat x = DAst.with_val (function + | GApp (r, [a]) -> + begin match DAst.get r with + | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number ) x -let uninterp_nat p = +let uninterp_nat (AnyGlobConstr p) = try Some (int_of_nat p) with @@ -75,4 +79,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) + ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) |