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/ascii_syntax.ml | 20 +++++++------ plugins/syntax/int31_syntax.ml | 24 +++++++++------- plugins/syntax/nat_syntax.ml | 18 +++++++----- plugins/syntax/r_syntax.ml | 44 +++++++++++++++------------- plugins/syntax/string_syntax.ml | 20 +++++++------ plugins/syntax/z_syntax.ml | 64 ++++++++++++++++++++++------------------- 6 files changed, 107 insertions(+), 83 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index c41ec39cb..b299ff853 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -25,6 +25,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -42,9 +46,9 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string ?loc s = let p = @@ -60,12 +64,12 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try - let aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + let aux c = match DAst.get c with + | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -75,10 +79,10 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index af64b1479..0dff047a3 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -23,6 +23,10 @@ open Glob_term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let make_mind mp id = Names.MutInd.make2 mp (Label.make id) let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = @@ -49,9 +53,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint ?loc n = - let ref_construct = CAst.make ?loc (GRef (int31_construct, None)) in - let ref_0 = CAst.make ?loc (GRef (int31_0, None)) in - let ref_1 = CAst.make ?loc (GRef (int31_1, None)) in + let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in + let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in + let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in let rec args counter n = if counter <= 0 then [] @@ -59,7 +63,7 @@ let int31_of_pos_bigint ?loc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) + DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") @@ -76,15 +80,15 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur) + | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in - function - | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero + fun c -> match DAst.get c with + | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero | _ -> raise Non_closed -let uninterp_int31 i = +let uninterp_int31 (AnyGlobConstr i) = try Some (bigint_of_int31 i) with Non_closed -> @@ -94,6 +98,6 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([CAst.make (GRef (int31_construct, None))], + ([DAst.make (GRef (int31_construct, None))], uninterp_int31, true) 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) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 06117de79..88ff38c6d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -27,6 +27,10 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let positive_path = make_path binnums "positive" (* TODO: temporary hack *) @@ -42,13 +46,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make @@ GRef (glob_xI, None) in - let ref_xH = CAst.make @@ GRef (glob_xH, None) in - let ref_xO = CAst.make @@ GRef (glob_xO, None) in + let ref_xI = DAst.make @@ GRef (glob_xI, None) in + let ref_xH = DAst.make @@ GRef (glob_xH, None) in + let ref_xO = DAst.make @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -57,10 +61,10 @@ let pos_of_bignat ?loc x = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one +let rec bignat_of_pos c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -81,18 +85,18 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - CAst.make @@ GRef (glob_ZERO, None) + DAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero +let bigint_of_z c = match DAst.get c with + | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -108,18 +112,18 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int ?loc z = - CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) + DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bigint_of_r = function - | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> +let bigint_of_r c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_IZR -> bigint_of_z a | _ -> raise Non_closed_number -let uninterp_r p = +let uninterp_r (AnyGlobConstr p) = try Some (bigint_of_r p) with Non_closed_number -> @@ -128,6 +132,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([CAst.make @@ GRef (glob_IZR, None)], + ([DAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) 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) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index af3df2889..0d743a2b5 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in + let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -68,14 +68,18 @@ let interp_positive ?loc n = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos x = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + +let rec bignat_of_pos x = DAst.with_val (function + | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number ) x -let uninterp_positive p = +let uninterp_positive (AnyGlobConstr p) = try Some (bignat_of_pos p) with Non_closed_number -> @@ -88,9 +92,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([CAst.make @@ GRef (glob_xI, None); - CAst.make @@ GRef (glob_xO, None); - CAst.make @@ GRef (glob_xH, None)], + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -107,9 +111,9 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else GRef(glob_N0, None) @@ -124,13 +128,13 @@ let n_of_int ?loc n = (* Printing N via scopes *) (**********************************************************************) -let bignat_of_n = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a +let bignat_of_n n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number - ) + ) n -let uninterp_n p = +let uninterp_n (AnyGlobConstr p) = try Some (bignat_of_n p) with Non_closed_number -> None @@ -140,8 +144,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([CAst.make @@ GRef (glob_N0, None); - CAst.make @@ GRef (glob_Npos, None)], + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -163,22 +167,22 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) + DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - CAst.make ?loc @@ GRef(glob_ZERO, None) + DAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) +let bigint_of_z z = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number - ) + ) z -let uninterp_z p = +let uninterp_z (AnyGlobConstr p) = try Some (bigint_of_z p) with Non_closed_number -> None @@ -189,8 +193,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([CAst.make @@ GRef (glob_ZERO, None); - CAst.make @@ GRef (glob_POS, None); - CAst.make @@ GRef (glob_NEG, None)], + ([DAst.make @@ GRef (glob_ZERO, None); + DAst.make @@ GRef (glob_POS, None); + DAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) -- cgit v1.2.3