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/string_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/string_syntax.ml')
-rw-r--r-- | plugins/syntax/string_syntax.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index b7f13b040..cc82fc94c 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -31,25 +31,29 @@ let make_reference id = find_reference "String interpretation" string_module id let glob_String = lazy (make_reference "String") let glob_EmptyString = lazy (make_reference "EmptyString") +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + open Lazy let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), + if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 -let uninterp_string r = +let uninterp_string (AnyGlobConstr r) = try let b = Buffer.create 16 in - let rec aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) -> + let rec aux c = match DAst.get c with + | GApp (k,[a;s]) when is_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -61,6 +65,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([CAst.make @@ GRef (static_glob_String,None); - CAst.make @@ GRef (static_glob_EmptyString,None)], + ([DAst.make @@ GRef (static_glob_String,None); + DAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) |