From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 19:05:57 +0200
Subject: 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.
---
 plugins/syntax/nat_syntax.ml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'plugins/syntax/nat_syntax.ml')

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 524a5c5221..2f9870cf96 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)
-- 
cgit v1.2.3