From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.
---
 interp/notation.ml | 47 ++++++++++++++++++++++++++++++-----------------
 1 file changed, 30 insertions(+), 17 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index c373faf68..176ac3bf6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -265,19 +265,28 @@ let keymap_find key map =
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 
-let prim_token_key_table = ref KeyMap.empty
-
-let glob_prim_constr_key = function
-  | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref)
+let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t)
+
+let glob_prim_constr_key c = match DAst.get c with
+  | GRef (ref, _) -> RefKey (canonical_gr ref)
+  | GApp (c, _) ->
+    begin match DAst.get c with
+    | GRef (ref, _) -> RefKey (canonical_gr ref)
+    | _ -> Oth
+    end
   | _ -> Oth
 
-let glob_constr_keys = function
-  | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth]
-  | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)]
+let glob_constr_keys c = match DAst.get c with
+  | GApp (c, _) ->
+    begin match DAst.get c with
+    | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth]
+    | _ -> [Oth]
+    end
+  | GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | _ -> [Oth]
 
-let cases_pattern_key = function
-  | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref))
+let cases_pattern_key c = match DAst.get c with
+  | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -300,7 +309,7 @@ type 'a prim_token_interpreter =
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
 type 'a prim_token_uninterpreter =
-    glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
+    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
     ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
@@ -496,11 +505,15 @@ let interp_prim_token_gen ?loc g p local_scopes =
 let interp_prim_token ?loc =
   interp_prim_token_gen ?loc (fun _ -> ())
 
-let rec check_allowed_ref_in_pat looked_for = CAst.(with_val (function
+let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function
   | GVar _ | GHole _ -> ()
   | GRef (g,_) -> looked_for g
-  | GApp ({ v = GRef (g,_) },l) ->
-    looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
+  | GApp (f, l) ->
+    begin match DAst.get f with
+    | GRef (g, _) ->
+      looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
+    | _ -> raise Not_found
+    end
   | _ -> raise Not_found))
 
 let interp_prim_token_cases_pattern_expr ?loc looked_for p =
@@ -532,7 +545,7 @@ let uninterp_prim_token c =
   try
     let (sc,numpr,_) =
       KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
-    match numpr c with
+    match numpr (AnyGlobConstr c) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
@@ -545,8 +558,8 @@ let uninterp_prim_token_ind_pattern ind args =
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = CAst.make @@ GRef (ref,None) in
-    match numpr (CAst.make @@ GApp (ref,args')) with
+    let ref = DAst.make @@ GRef (ref,None) in
+    match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
@@ -557,7 +570,7 @@ let uninterp_prim_token_cases_pattern c =
     let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
     if not b then raise Notation_ops.No_match;
     let na,c = glob_constr_of_closed_cases_pattern c in
-    match numpr c with
+    match numpr (AnyGlobConstr c) with
       | None -> raise Notation_ops.No_match
       | Some n -> (na,sc,n)
   with Not_found -> raise Notation_ops.No_match
-- 
cgit v1.2.3