diff --git a/lambdapi.opam b/lambdapi.opam index 3bc98ec2c..921aafb93 100644 --- a/lambdapi.opam +++ b/lambdapi.opam @@ -41,6 +41,7 @@ depends: [ "lwt_ppx" {>= "1"} "uri" {>= "1.1"} "ppx_inline_test" + "ppx_deriving_yojson" { >= "3.7.0"} ] build: [ ["dune" "subst"] {dev} diff --git a/src/common/dune b/src/common/dune index 1876d48ed..0ef722dca 100644 --- a/src/common/dune +++ b/src/common/dune @@ -1,6 +1,7 @@ (library (name common) (public_name lambdapi.common) + (preprocess (pps ppx_deriving_yojson)) (modules :standard) (libraries camlp-streams str timed lambdapi.lplib) (flags -w +3)) diff --git a/src/common/path.ml b/src/common/path.ml index 1eb92a06f..00db7c1d3 100644 --- a/src/common/path.ml +++ b/src/common/path.ml @@ -5,7 +5,7 @@ open Lplib open Base module Path = struct (** Representation of a module name (roughly, a file path). *) - type t = string list + type t = string list [@@deriving yojson] (** [pp ppf p] prints path [p] on the formatter [ppf]. Remark: to be used in Common only as it does not escape identifiers that need to be @@ -15,6 +15,12 @@ module Path = (** [compare] is a standard comparison function on paths. *) let compare : t cmp = Stdlib.compare + let make (s : string) : t = + if s = "" then [] + else + s + |> String.split_on_char '.' + |> List.filter (fun x -> x <> "") end include Path diff --git a/src/common/pos.ml b/src/common/pos.ml index 7996894fe..240b649f8 100644 --- a/src/common/pos.ml +++ b/src/common/pos.ml @@ -14,7 +14,7 @@ type pos = ; end_col : int (** Column number (utf8) of the ending point. *) ; end_offset : int (** Number of chars since the beginning of the document for the ending point *) - } + } [@@deriving yojson] (** Total comparison function on pos. *) let cmp : pos cmp = fun p1 p2 -> @@ -77,7 +77,7 @@ let to_string : ?print_dirname:bool -> ?print_fname:bool -> pos -> string = (** Type of optional positions. *) -type popt = pos option +type popt = pos option [@@deriving yojson] (** [equal p1 p2] tells whether [p1] and [p2] denote the same position. *) let equal : popt -> popt -> bool = fun p1 p2 -> diff --git a/src/core/dune b/src/core/dune index 8cb3b6b72..e623551fc 100644 --- a/src/core/dune +++ b/src/core/dune @@ -9,5 +9,8 @@ (name core) (public_name lambdapi.core) (synopsis "LambdaPi interactive theorem prover [core]") + (inline_tests) +; (preprocess (pps )) + (preprocess (pps ppx_inline_test ppx_deriving_yojson)) (modules :standard) - (libraries lambdapi.common lambdapi.lplib pratter why3 unix)) + (libraries yojson lambdapi.common lambdapi.lplib pratter why3 unix)) diff --git a/src/core/sig_serialize.ml b/src/core/sig_serialize.ml new file mode 100644 index 000000000..e8dac70a9 --- /dev/null +++ b/src/core/sig_serialize.ml @@ -0,0 +1,384 @@ +open Sign +open Term +open Term_serializable +open Lplib.Extra +open Common +open Error +open Timed + + +let strmap_to_yojson to_elt (m : 'a StrMap.t) : Yojson.Safe.t = + `List ( + StrMap.bindings m + |> List.map (fun (k, v) -> + `List [`String k; to_elt v]) + ) + +let strmap_of_yojson of_elt (json : Yojson.Safe.t) + : ('a StrMap.t, string) result = + match json with + | `List lst -> + let rec aux acc = function + | [] -> Ok acc + | `List [`String k; v_json] :: tl -> + begin match of_elt v_json with + | Ok v -> aux (StrMap.add k v acc) tl + | Error e -> Error e + end + | _ -> Error "StrMap.of_yojson: invalid entry" + in + aux StrMap.empty lst + | _ -> Error "StrMap.of_yojson: expected list" + +let pathmap_to_yojson to_elt (m : 'a Path.Map.t) : Yojson.Safe.t = + `List ( + Path.Map.bindings m + |> List.map (fun (k, v) -> + `List [`String (Format.asprintf "%a" Path.Path.pp k); to_elt v] + )) + +let pathmap_of_yojson of_elt json = + match json with + | `List lst -> + let rec aux acc l = + match l with + | [] -> Ok acc + | `List [`String k; v_json] :: lt -> + begin match of_elt v_json with + | Ok v -> + aux (Path.Map.add (Path.Path.make k) v acc) lt + | Error e -> Error e + end + | _ -> Error "pas list" + in + aux Path.Map.empty lst + | _ -> Error "pathmap_of_yojson: expected list" + + +let symmap_to_yojson to_elt (m : 'a SymMap.t) : Yojson.Safe.t = + `List ( + SymMap.bindings m + |> List.map (fun (k, v) -> + `List [ sym_to_yojson k; to_elt v ]) + ) + +let symmap_of_yojson of_elt (json : Yojson.Safe.t) + : ('a SymMap.t, string) result = + match json with + | `List lst -> + let rec aux acc = function + | [] -> Ok acc + | `List [k_json; v_json] :: tl -> + begin match (sym_of_yojson k_json), of_elt v_json with + | Ok k, Ok v -> + aux (SymMap.add k v acc) tl + | Error e, _ -> Error e + | _, Error e -> Error e + end + | _ -> Error "SymMap.of_yojson: invalid entry" + in + aux SymMap.empty lst + | _ -> Error "SymMap.of_yojson: expected list" + + +module StrMap = struct +include StrMap + let to_yojson to_elt m = strmap_to_yojson to_elt m + let of_yojson of_elt json = strmap_of_yojson of_elt json +end + +module Path = struct + include Path + module Map = struct + include Map + let to_yojson to_elm m = + pathmap_to_yojson to_elm m + let of_yojson of_elm m = + pathmap_of_yojson of_elm m + end +end + +module SymMap = struct +include SymMap +let to_yojson to_elm m = + symmap_to_yojson to_elm m +let of_yojson of_elm m = + symmap_of_yojson of_elm m +end + +type ind_data = + { ind_cons : sym list + ; ind_prop : sym + ; ind_nb_params : int (** Number of parameters. *) + ; ind_nb_types : int (** Number of mutually defined types. *) + ; ind_nb_cons : int (** Number of constructors. *) } + [@@deriving yojson] + +let rule_to_yojson r = rule_serializable_to_yojson (to_rule_serializable r) +let rule_of_yojson j = + match rule_serializable_of_yojson j with + | Ok r -> Ok (of_rule_serializable r) + | Error e -> Error e + +type sym_data = + { rules : rule list + ; nota : float notation option }[@@deriving yojson] + +type dep_data = + { dep_symbols : sym_data StrMap.t + ; dep_open : bool } + [@@deriving yojson] + +let to_ind_data_serializable (i : Sign.ind_data) : ind_data = + { ind_cons = i.ind_cons + ; ind_prop = i.ind_prop + ; ind_nb_params = i.ind_nb_params + ; ind_nb_types = i.ind_nb_types + ; ind_nb_cons = i.ind_nb_cons + } + +let of_ind_data_serializable (i : ind_data) : Sign.ind_data = + { ind_cons = i.ind_cons + ; ind_prop = i.ind_prop + ; ind_nb_params = i.ind_nb_params + ; ind_nb_types = i.ind_nb_types + ; ind_nb_cons = i.ind_nb_cons + } + +let to_sym_data_serializable (s : Sign.sym_data) : sym_data = + { rules = s.rules + ; nota = s.nota} + + let of_sym_data_serializable (s : sym_data) : Sign.sym_data = + { rules = s.rules + ; nota = s.nota} + +let to_dep_data_serializable (d:Sign.dep_data) : dep_data = + { dep_symbols = StrMap.map to_sym_data_serializable d.dep_symbols + ; dep_open = d.dep_open + } + +let of_dep_data_serializable (d:dep_data) : Sign.dep_data = + { dep_symbols = StrMap.map of_sym_data_serializable d.dep_symbols + ; dep_open = d.dep_open + } + +type t = + { sign_symbols : sym StrMap.t + ; sign_path : Path.t + ; sign_deps : dep_data Path.Map.t + ; sign_builtins : sym StrMap.t + ; sign_ind : ind_data SymMap.t + ; sign_cp_pos : cp_pos list SymMap.t + } + [@@deriving yojson] + +let to_sign_serializable (s:Sign.t) : t = + { sign_symbols = Timed.(!)s.sign_symbols + ; sign_path = s.sign_path + ; sign_deps = (Path.Map.map + (fun d -> to_dep_data_serializable d) + (Timed.(!)s.sign_deps)) + ; sign_builtins = Timed.(!)s.sign_builtins + ; sign_ind = (SymMap.map + (fun c -> to_ind_data_serializable c) + (Timed.(!)(s.sign_ind))) + ; sign_cp_pos = Timed.(!)s.sign_cp_pos + } + +let of_sign_serializable (s:t) : Sign.t = + { sign_symbols = Timed.ref s.sign_symbols + ; sign_path = s.sign_path + ; sign_deps = Timed.ref (Path.Map.map + (fun d -> of_dep_data_serializable d) (s.sign_deps)) + ; sign_builtins = Timed.ref s.sign_builtins + ; sign_ind = Timed.ref (SymMap.map + (fun c -> of_ind_data_serializable c) s.sign_ind) + ; sign_cp_pos = Timed.ref s.sign_cp_pos + } + + +let to_yojson_with_version (t : Sign.t) (version : string) : Yojson.Safe.t = + match to_yojson (to_sign_serializable t) with + | `Assoc fields -> + `Assoc (("version", `String version) :: fields) + | _ -> assert false + +let of_yojson_with_version json = + let version = + json + |> Yojson.Safe.Util.member "version" + |> Yojson.Safe.Util.to_string in + + if version <> Version.version then + raise (Failure + ("Version " ^ version ^ " found but in lpo file but" ^ + Version.version ^ "expected (current)")); + + match json with + |`Assoc fields -> + begin match of_yojson (`Assoc (List.remove_assoc "version" fields)) + with + | Ok s -> Ok (of_sign_serializable s) + | Error e -> Error e + end + |_ -> raise (Failure "Unknown po format. + Field version missing or corrupted file") + + +(** [write sign file] writes the signature [sign] to the file [fname]. *) +let write : Sign.t -> string -> unit = fun sign fname -> + (* [Unix.fork] is used to safely [unlink] and write an object file, while + preserving a valid copy of the written signature in the parent + process. *) + match Unix.fork () with + | 0 -> let oc = open_out fname in + unlink sign; + let sign_json = to_yojson_with_version sign Version.version in + let _pp = Yojson.Safe.pretty_to_string sign_json in + Yojson.Safe.to_channel oc sign_json; + (* Marshal.to_channel oc sign [Marshal.Closures]; *) + close_out oc; Stdlib.(Debug.do_print_time := false); exit 0 + | i -> ignore (Unix.waitpid [] i); Stdlib.(Debug.do_print_time := true) + +let write s n = Debug.(record_time Writing (fun () -> write s n)) + +(** [read fname] reads a signature from the object file [fname]. Note that the + file can only be read properly if it was build with the same binary as the + one being evaluated. If this is not the case, the program gracefully fails + with an error message. *) +(* NOTE here, we rely on the fact that a marshaled closure can only be read by + processes running the same binary as the one that produced it. *) +let read : string -> Sign.t = fun fname -> + let ic = open_in fname in + let sign:Sign.t = + try + let json_sign = Yojson.Safe.from_channel ic in + let sign = of_yojson_with_version json_sign in + + (* READ sign_symbols and update sign *) + + (* let sign = Marshal.from_channel ic in *) + close_in ic; + match sign with + | Ok sign -> sign + | Error e -> raise (Failure e) + with Failure msg -> + close_in ic; + fatal_no_pos + "File \"%s\" is incompatible with current binary. %s" fname msg + in + (* Timed references need reset after unmarshaling (see [Timed] doc). *) + unsafe_reset sign.sign_symbols; + unsafe_reset sign.sign_deps; + unsafe_reset sign.sign_builtins; + unsafe_reset sign.sign_ind; + unsafe_reset sign.sign_cp_pos; + let shallow_reset_sym (s:sym) = + unsafe_reset s.sym_type; + unsafe_reset s.sym_def; + unsafe_reset s.sym_rules; + (* s.sym_dtree is not reset since it is recomputed. *) + in + let rec reset_term t = + match unfold t with + | Type + | Kind + | Vari _ -> () + | Symb s -> shallow_reset_sym s + | Prod(a,b) + | Abst(a,b) -> reset_term a; reset_term (snd (unbind b)) + | LLet(a,t,b) -> reset_term a; reset_term t; reset_term (snd(unbind b)) + | Appl(a,b) -> reset_term a; reset_term b + | Patt(_,_,ts) -> Array.iter reset_term ts + | Bvar _ -> assert false + | TRef _ -> assert false + | Wild -> assert false + | Meta _ -> assert false + | Plac _ -> assert false + in + let reset_rule (r:rule) = + List.iter reset_term r.lhs; + reset_term r.rhs + in + let reset_sym s = + shallow_reset_sym s; + reset_term !(s.sym_type); + Option.iter reset_term !(s.sym_def); + List.iter reset_rule !(s.sym_rules) + in + StrMap.iter (fun _ s -> reset_sym s) !(sign.sign_symbols); + StrMap.iter (fun _ s -> shallow_reset_sym s) !(sign.sign_builtins); + let f _ ({dep_symbols=sm; _}:Sign.dep_data) = + StrMap.iter + (fun _ (sd:Sign.sym_data) -> List.iter reset_rule sd.rules) + sm in + Path.Map.iter f !(sign.sign_deps); + let reset_ind (i:Sign.ind_data) = + shallow_reset_sym i.ind_prop; List.iter shallow_reset_sym i.ind_cons in + let f s (i : Sign.ind_data) = shallow_reset_sym s; reset_ind i in + SymMap.iter f !(sign.sign_ind); + let reset_cp_pos (_,l,r,_,l_p) = + reset_term l; reset_term r; reset_term l_p in + let f s cps = shallow_reset_sym s; List.iter reset_cp_pos cps in + SymMap.iter f !(sign.sign_cp_pos); + sign + +let read = + let open Stdlib in let r = ref Ghost.sign in fun n -> + Debug.(record_time Reading (fun () -> r := read n)); !r + + +let%test "rev" = + let rule = + {Term.lhs = [Term.dump_term] + ; names = [|"rule1"|] + ; rhs = Term.dump_term + ; arity = 0 + ; arities = [|1; 2|] + ; vars_nb = 5 + ; xvars_nb = 9 + ; rule_pos = Some { fname = Some "file" + ; start_line = 0 + ; start_col = 0 + ; start_offset = 0 + ; end_line = 1 + ; end_col = 1 + ; end_offset = 1 + } + } in + let sym_data:Sign.sym_data = {rules=[rule]; nota=None} in + let dep_data:Sign.dep_data = + {dep_symbols = (StrMap. add "key1" sym_data StrMap.empty) + ; dep_open = true + } in + let sign = Ghost.sign in + let symbols = Timed.(!) sign.sign_symbols in + let symbols = StrMap.add "" + { + sym_dump + with + sym_path = ["rep"; "file"] + } + symbols in + let sign = {sign + with sign_symbols = Timed.ref symbols + ; sign_deps = Timed.ref + (Path.Map.add (Path.ghost "path_here") dep_data Path.Map.empty) + ; sign_builtins = Timed.ref symbols + } in + write sign "/tmp/test_sign_read_write.json"; + let r_sign = read "/tmp/test_sign_read_write.json" in + + sign.sign_path = r_sign.sign_path && + (StrMap.equal + (fun a b -> + (Sym.compare a b) = 0 + (* Should compare : *) + (* a.sym_expo = b.sym_expo + && (Path.compare a.sym_path b.sym_path = 0) + && (a.sym_name = b.sym_name) *) + ) + (Timed.(!)(sign.sign_symbols)) + (Timed.(!)(r_sign.sign_symbols)) + ) \ No newline at end of file diff --git a/src/core/sign.ml b/src/core/sign.ml index d60eb99a3..c96a2604a 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -1,7 +1,7 @@ (** Signature for symbols. *) open Lplib open Extra -open Common open Error open Pos +open Common open Pos open Timed open Term @@ -13,7 +13,6 @@ type ind_data = ; ind_nb_types : int (** Number of mutually defined types. *) ; ind_nb_cons : int (** Number of constructors. *) } -(** Rules and notation added to an external symbol. *) type sym_data = { rules : rule list ; nota : float notation option } @@ -32,7 +31,8 @@ type t = ; sign_deps : dep_data Path.Map.t ref ; sign_builtins : sym StrMap.t ref ; sign_ind : ind_data SymMap.t ref - ; sign_cp_pos : cp_pos list SymMap.t ref } + ; sign_cp_pos : cp_pos list SymMap.t ref + } (** [mem sign name] checks whether a symbol named [name] exists in [sign]. *) let mem : t -> string -> bool = fun sign name -> @@ -249,93 +249,6 @@ let strip_private : t -> unit = fun sign -> sign.sign_symbols := StrMap.filter (fun _ s -> not_prv s) !(sign.sign_symbols) -(** [write sign file] writes the signature [sign] to the file [fname]. *) -let write : t -> string -> unit = fun sign fname -> - (* [Unix.fork] is used to safely [unlink] and write an object file, while - preserving a valid copy of the written signature in the parent - process. *) - match Unix.fork () with - | 0 -> let oc = open_out fname in - unlink sign; Marshal.to_channel oc sign [Marshal.Closures]; - close_out oc; Stdlib.(Debug.do_print_time := false); exit 0 - | i -> ignore (Unix.waitpid [] i); Stdlib.(Debug.do_print_time := true) - -let write s n = Debug.(record_time Writing (fun () -> write s n)) - -(** [read fname] reads a signature from the object file [fname]. Note that the - file can only be read properly if it was build with the same binary as the - one being evaluated. If this is not the case, the program gracefully fails - with an error message. *) -(* NOTE here, we rely on the fact that a marshaled closure can only be read by - processes running the same binary as the one that produced it. *) -let read : string -> t = fun fname -> - let ic = open_in fname in - let sign = - try - let sign = Marshal.from_channel ic in - close_in ic; sign - with Failure _ -> - close_in ic; - fatal_no_pos "File \"%s\" is incompatible with current binary." fname - in - (* Timed references need reset after unmarshaling (see [Timed] doc). *) - unsafe_reset sign.sign_symbols; - unsafe_reset sign.sign_deps; - unsafe_reset sign.sign_builtins; - unsafe_reset sign.sign_ind; - unsafe_reset sign.sign_cp_pos; - let shallow_reset_sym s = - unsafe_reset s.sym_type; - unsafe_reset s.sym_def; - unsafe_reset s.sym_rules; - (* s.sym_dtree is not reset since it is recomputed. *) - in - let rec reset_term t = - match unfold t with - | Type - | Kind - | Vari _ -> () - | Symb s -> shallow_reset_sym s - | Prod(a,b) - | Abst(a,b) -> reset_term a; reset_term (snd (unbind b)) - | LLet(a,t,b) -> reset_term a; reset_term t; reset_term (snd(unbind b)) - | Appl(a,b) -> reset_term a; reset_term b - | Patt(_,_,ts) -> Array.iter reset_term ts - | Bvar _ -> assert false - | TRef _ -> assert false - | Wild -> assert false - | Meta _ -> assert false - | Plac _ -> assert false - in - let reset_rule r = - List.iter reset_term r.lhs; - reset_term r.rhs - in - let reset_sym s = - shallow_reset_sym s; - reset_term !(s.sym_type); - Option.iter reset_term !(s.sym_def); - List.iter reset_rule !(s.sym_rules) - in - StrMap.iter (fun _ s -> reset_sym s) !(sign.sign_symbols); - StrMap.iter (fun _ s -> shallow_reset_sym s) !(sign.sign_builtins); - let f _ {dep_symbols=sm; _} = - StrMap.iter (fun _ sd -> List.iter reset_rule sd.rules) sm in - Path.Map.iter f !(sign.sign_deps); - let reset_ind i = - shallow_reset_sym i.ind_prop; List.iter shallow_reset_sym i.ind_cons in - let f s i = shallow_reset_sym s; reset_ind i in - SymMap.iter f !(sign.sign_ind); - let reset_cp_pos (_,l,r,_,l_p) = - reset_term l; reset_term r; reset_term l_p in - let f s cps = shallow_reset_sym s; List.iter reset_cp_pos cps in - SymMap.iter f !(sign.sign_cp_pos); - sign - -let read = - let open Stdlib in let r = ref Ghost.sign in fun n -> - Debug.(record_time Reading (fun () -> r := read n)); !r - (** [add_rule sign s r] adds the new rule [r] to the symbol [s]. When the rule does not correspond to a symbol of signature [sign], it is stored in its dependencies. /!\ does not update the decision tree or the critical diff --git a/src/core/term.ml b/src/core/term.ml index 7f4fc918c..13ace6237 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -22,13 +22,14 @@ type match_strat = | Eager (** Any rule that filters a term can be applied (even if a rule defined earlier filters the term as well). This is the default. *) + [@@deriving yojson] (** Specify the visibility and usability of symbols outside their module. *) type expo = | Public (** Visible and usable everywhere. *) | Protec (** Visible everywhere but usable in LHS arguments only. *) | Privat (** Not visible and thus not usable. *) - +[@@deriving yojson] (** Symbol properties. *) type prop = | Defin (** Definable. *) @@ -37,15 +38,19 @@ type prop = | Commu (** Commutative. *) | Assoc of bool (** Associative left if [true], right if [false]. *) | AC of bool (** Associative and commutative. *) + [@@deriving yojson] (** Data of a binder. *) -type binder_info = {binder_name : string; binder_bound : bool} -type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} +type binder_info = + {binder_name : string; binder_bound : bool} [@@deriving yojson] +type mbinder_info = + { mbinder_name : string array + ; mbinder_bound : bool array}[@@deriving yojson] let pr_bound = D.array (fun ppf b -> if b then out ppf "*" else out ppf "_") (** Type for free variables. *) -type var = int * string +type var = int * string [@@deriving yojson] (** [compare_vars x y] safely compares [x] and [y]. Note that it is unsafe to compare variables using [Pervasive.compare]. *) @@ -83,17 +88,30 @@ module VarMap = Map.Make(Var) substitution of the parent binder, [InEnv i] refers to the i-th slot in the closure environment of the parent binder (variables bound by a binder which is not the direct parent). *) -type bvar = InSub of int | InEnv of int +type bvar = InSub of int | InEnv of int [@@deriving yojson] (** The priority of an infix operator is a floating-point number. *) type priority = float +let associativity_to_yojson = function + | Pratter.Left -> `String "Left" + | Right -> `String "Right" + | Neither -> `String "Neither" + +let associativity_of_yojson = function + | `String "Left" -> Ok Pratter.Left + | `String "Right" -> Ok Right + | `String "Neither" -> Ok Neither + | _ -> Error "associativity_of_yojson" (** Notations. *) type 'a notation = | NoNotation | Prefix of 'a | Postfix of 'a - | Infix of Pratter.associativity * 'a + | Infix of (Pratter.associativity + [@to_yojson associativity_to_yojson] + [@of_yojson associativity_of_yojson]) + * 'a | Zero | Succ of 'a notation (* NoNotation, Prefix or Postfix only *) | Quant @@ -103,7 +121,7 @@ type 'a notation = | IntZero | IntPos | IntNeg - + [@@deriving yojson] (** Representation of a term (or types) in a general sense. Values of the type are also used, for example, in the representation of patterns or rewriting rules. Specific constructors are included for such applications, and they @@ -135,21 +153,6 @@ type term = | LLet of term * term * binder (** [LLet(a, t, u)] is [let x : a ≔ t in u] (with [x] bound in [u]). *) -(** Type for binders, implemented as closures. The bound variables of a - closure term always refer either to a variable bound by the parent binder - or to a slot in the closure environment of the parent binder. No direct - reference to variables bound by an ancestor binder! - - In a binder [(bi,u,e)] of arity [n], [Bvar(InSub i)] occurring in the - closure term [u] (with [i < n]) refers to the bound variable at position - [i] in the given substitution (e.g. argument [vs] of msubst), and - [Bvar(InEnv i)] refers to the term [e.(i)] - - For instance, the term [λx. λy. x y] is represented as - [Abst(_,(_,Abst(_,(_,Appl(Bvar(InSub 0)|Bvar(InEnv 0)), - [|Bvar(InSub 0)|])), - [||]))] - *) and binder = binder_info * term * term array and mbinder = mbinder_info * term * term array @@ -942,12 +945,10 @@ let rhs : sym_rule -> term = fun (_, r) -> r.rhs (** Positions in terms in reverse order. The i-th argument of a constructor has position i-1. *) type subterm_pos = int list + [@@deriving yojson] let subterm_pos : subterm_pos pp = fun ppf l -> D.(list int) ppf (List.rev l) -(** Type of critical pair positions (pos,l,r,p,l_p). *) -type cp_pos = Pos.popt * term * term * subterm_pos * term - (** Typing context associating a variable to a type and possibly a definition. The typing environment [x1:A1,..,xn:An] is represented by the list [xn:An;..;x1:A1] in reverse order (last added variable comes @@ -989,3 +990,222 @@ module Raw = struct let term = term let _ = term let ctxt = ctxt let _ = ctxt end + +let dump_term = Type +let sym_dump = +{ + sym_expo = Privat + ; sym_path = [] + ; sym_name = "" + ; sym_type = Timed.ref Type + ; sym_impl = [true; false] + ; sym_prop = Defin + ; sym_nota = Timed.ref NoNotation + ; sym_def = Timed.ref(Some Type) + ; sym_opaq = Timed.ref true + ; sym_rules = Timed.ref [] + ; sym_mstrat = Sequen + ; sym_dtree = Timed.ref Tree_type.empty_dtree + ; sym_pos = + Some { fname = Some "file" + ; start_line = 0 + ; start_col = 0 + ; start_offset = 0 + ; end_line = 1 + ; end_col = 1 + ; end_offset = 1 + } + ; sym_decl_pos = + Some { fname = Some "Another/file" + ; start_line = 2 + ; start_col = 2 + ; start_offset = 2 + ; end_line = 15 + ; end_col = 15 + ; end_offset = 15 + } +} + +module Term_serializable = struct + type term_serializable = + | Vari of var + | Type + | Kind + | Symb of sym_serializable + | Prod of term_serializable * binder_serializable + | Abst of term_serializable * binder_serializable + | Appl of term_serializable * term_serializable + | Patt of int option * string * term_serializable array + | LLet of term_serializable * term_serializable * binder_serializable + [@@deriving yojson] + + and binder_serializable = + binder_info + * term_serializable + * term_serializable array + [@@deriving yojson] + + and meta_serializable = + { meta_key : int + ; meta_type : term_serializable + ; meta_arity : int + ; meta_value : mbinder_serializable option + } [@@deriving yojson] + + and mbinder_serializable = + mbinder_info + * term_serializable + * term_serializable array + [@@deriving yojson] + + and rule_serializable = + { lhs : term_serializable list + ; names : string array + ; rhs : term_serializable + ; arity : int + ; arities : int array + ; vars_nb : int + ; xvars_nb : int + ; rule_pos : Pos.popt + }[@@deriving yojson] + + and dtree_serializable = + rule_serializable Tree_type.dtree_serializable [@@deriving yojson] + + and sym_serializable = + { sym_expo : expo + ; sym_path : Path.t + ; sym_name : string + ; sym_type : term_serializable + ; sym_impl : bool list + ; sym_prop : prop + ; sym_nota : float notation (*Timed.ref*) + ; sym_def : term_serializable option (*Timed.ref*) + ; sym_opaq : bool (*Timed.ref*) + ; sym_rules : rule_serializable list (* Timed.ref *) + ; sym_mstrat: match_strat + ; sym_pos : Pos.popt + ; sym_decl_pos : Pos.popt + } [@@deriving yojson] + + + let rec to_term_serializable (t:term):term_serializable = match t with + | Vari x -> Vari x + | Type -> Type + | Kind -> Kind + | Symb x -> Symb (to_sym_serializable x) + | Prod (x, y) ->Prod + (to_term_serializable x, to_binder_serializable y) + | Abst (x, y) ->Abst + (to_term_serializable x, to_binder_serializable y) + | Appl (x, y) ->Appl + (to_term_serializable x, to_term_serializable y) + | Patt (x, y, z) -> Patt (x, y, Array.map to_term_serializable z) + | LLet (x, y, z) -> LLet (to_term_serializable x + , to_term_serializable y + , to_binder_serializable z) + | _ -> assert false + + and to_binder_serializable (x, y, z) = + (x, to_term_serializable y, Array.map to_term_serializable z) + + and to_sym_serializable (s:sym) = + { + sym_expo = s.sym_expo + ; sym_path = s.sym_path + ; sym_name = s.sym_name + ; sym_type = (to_term_serializable (Timed.(!) s.sym_type)) + ; sym_impl = s.sym_impl + ; sym_prop = s.sym_prop + ; sym_nota = Timed.(!)s.sym_nota + ; sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) + ; sym_opaq = Timed.(!)s.sym_opaq + ; sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + ; sym_mstrat = s.sym_mstrat + ; sym_pos = s.sym_pos + ; sym_decl_pos = s.sym_decl_pos + } + + and to_rule_serializable (r : rule) : rule_serializable = + { + lhs = List.map to_term_serializable r.lhs; + names = r.names; + rhs = to_term_serializable r.rhs; + arity = r.arity; + arities = r.arities; + vars_nb = r.vars_nb; + xvars_nb = r.xvars_nb; + rule_pos = r.rule_pos; + } + let rec of_term_serializable t:term = match t with + | Vari x -> Vari x + | Type -> Type + | Kind -> Kind + | Symb x -> Symb (of_sym_serializable x) + | Prod (x, y) -> Prod + (of_term_serializable x, of_binder_serializable y) + | Abst (x, y) -> Abst + (of_term_serializable x, of_binder_serializable y) + | Appl (x, y) -> Appl + (of_term_serializable x, of_term_serializable y) + | Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) + | LLet (x, y, z) -> LLet + (of_term_serializable x + , of_term_serializable y + , of_binder_serializable z) + + and of_binder_serializable (x, y, z) = + (x, of_term_serializable y, Array.map of_term_serializable z) + + and of_sym_serializable (s:sym_serializable):sym = + { + sym_expo = s.sym_expo + ; sym_path = s.sym_path + ; sym_name = s.sym_name + ; sym_type = Timed.ref (of_term_serializable s.sym_type) + ; sym_impl = s.sym_impl + ; sym_prop = s.sym_prop + ; sym_nota = Timed.ref s.sym_nota + ; sym_def = Timed.ref (Option.map of_term_serializable s.sym_def) + ; sym_opaq = Timed.ref s.sym_opaq + ; sym_rules = Timed.ref (List.map of_rule_serializable s.sym_rules) + ; sym_mstrat = s.sym_mstrat + ; sym_dtree = Timed.ref (Tree_type.empty_dtree) + ; sym_pos = s.sym_pos + ; sym_decl_pos = s.sym_decl_pos + } + + and of_rule_serializable (r : rule_serializable) : rule = + { + lhs = List.map of_term_serializable r.lhs; + names = r.names; + rhs = of_term_serializable r.rhs; + arity = r.arity; + arities = r.arities; + vars_nb = r.vars_nb; + xvars_nb = r.xvars_nb; + rule_pos = r.rule_pos; + } + + let sym_to_yojson s = + sym_serializable_to_yojson (to_sym_serializable s) + + and sym_of_yojson j = + match (sym_serializable_of_yojson j) with + | Ok j -> Ok (of_sym_serializable j) + | Error s -> Error s + + and term_to_yojson t = term_serializable_to_yojson (to_term_serializable t) + and term_of_yojson (t : Yojson.Safe.t) : (term, string) result = + match term_serializable_of_yojson t with + | Ok t_ser -> + Ok (of_term_serializable t_ser) + | Error e -> + Error e +end + +let term_to_yojson = Term_serializable.term_to_yojson +let term_of_yojson = Term_serializable.term_of_yojson +(** Type of critical pair positions (pos,l,r,p,l_p). *) +type cp_pos = Pos.popt * term * term * subterm_pos * term + [@@deriving yojson] diff --git a/src/core/term.mli b/src/core/term.mli index ae3789269..454bd62a4 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -64,6 +64,7 @@ type 'a notation = | IntZero | IntPos | IntNeg + [@@deriving yojson] (** Representation of a term (or types) in a general sense. Values of the type are also used, for example, in the representation of patterns or rewriting @@ -447,11 +448,13 @@ val new_problem : unit -> problem (** Positions in terms in reverse order. The i-th argument of a constructor has position i-1. *) type subterm_pos = int list + (* [@@deriving yojson] *) val subterm_pos : subterm_pos pp (** Type of critical pair positions (pos,l,r,p,l_p). *) -type cp_pos = Pos.popt * term * term * subterm_pos * term +type cp_pos = Pos.popt * term * term * subterm_pos * term [@@deriving yojson] + (* [@@deriving yojson] *) (** Type of a symbol and a rule. *) type sym_rule = sym * rule @@ -465,3 +468,76 @@ module Raw : sig val term : term pp val ctxt : ctxt pp end + +type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} + +type binder_info = {binder_name : string; binder_bound : bool} + +val sym_dump : sym +val dump_term : term + +module Term_serializable : sig + +type term_serializable = + | Vari of var + | Type + | Kind + | Symb of sym_serializable + | Prod of term_serializable * binder_serializable + | Abst of term_serializable * binder_serializable + | Appl of term_serializable * term_serializable + | Patt of int option * string * term_serializable array + | LLet of term_serializable * term_serializable * binder_serializable + +and binder_serializable = + binder_info * term_serializable * term_serializable array + +and meta_serializable = + { meta_key : int + ; meta_type : term_serializable (**Timed.ref. *) + ; meta_arity : int + ; meta_value : mbinder_serializable option (** Timed.ref. *) } + +and mbinder_serializable = + mbinder_info * term_serializable * term_serializable array + +and rule_serializable = + { lhs : term_serializable list + ; names : string array + ; rhs : term_serializable + ; arity : int + ; arities : int array + ; vars_nb : int + ; xvars_nb : int + ; rule_pos : Pos.popt + } [@@deriving yojson] + +and sym_serializable = + { sym_expo : expo + ; sym_path : Path.t + ; sym_name : string + ; sym_type : term_serializable + ; sym_impl : bool list + ; sym_prop : prop + ; sym_nota : float notation (*Timed.ref*) + ; sym_def : term_serializable option (* Timed.ref *) + ; sym_opaq : bool (* Timed.ref *) + ; sym_rules : rule_serializable list (* Timed.ref*) + ; sym_mstrat: match_strat + ; sym_pos : Pos.popt + ; sym_decl_pos : Pos.popt + } + +and dtree_serializable = rule_serializable Tree_type.dtree_serializable +val sym_to_yojson : sym -> Yojson.Safe.t + val sym_of_yojson : Yojson.Safe.t -> (sym, string) result + + val to_sym_serializable : sym -> sym_serializable + val of_sym_serializable : sym_serializable -> sym + + val to_rule_serializable : rule -> rule_serializable + val of_rule_serializable : rule_serializable -> rule + + val term_to_yojson : term -> Yojson.Safe.t + val term_of_yojson : Yojson.Safe.t -> (term, string) result +end \ No newline at end of file diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index 5b8a439ee..b19225851 100644 --- a/src/core/tree_type.ml +++ b/src/core/tree_type.ml @@ -22,6 +22,7 @@ module TC = in the environment builder to refer to the higher order variables a term may depend on. *) | Type + [@@deriving yojson] (** {b NOTE} the effective arity carried by the representation of a symbol is specific to a given symbol instance. Indeed, a symbol (in the sense @@ -54,6 +55,7 @@ type tree_cond = | CondFV of int * int array (** Are the (indexed) bound variables (which are free at the time of the checking) of the term at the given index in the array? *) + [@@deriving yojson] (** {b NOTE} that when performing a [tree_cond.CondFV] check, we are concerned about variables that were bound in the term being reduced @@ -73,7 +75,7 @@ let tree_cond : tree_cond pp = fun ppf tc -> substitutes variable [v] of the RHS by term [p] of array [v]. In the case of higher order patterns, [p] may need to be itself subsituted with {e bound} variables [xs] collected when traversing binders. *) -type rhs_substit = (int * (int * int array)) list +type rhs_substit = (int * (int * int array)) list [@@deriving yojson] (** Representation of a tree. The definition relies on parameters since module [Term] depends on the current module, and that would thus produce @@ -154,6 +156,127 @@ let rec tree_capacity : 'r tree -> int = fun tr -> not given in one go. *) type 'a dtree = int Lazy.t * 'a tree Lazy.t + +(* ---------------------------------------------- *) + + +type 'a tree_serializable = + | Fail_s + | Leaf_s of rhs_substit * 'a + | Cond_s of + { ok : 'a tree_serializable + ; cond : tree_cond + ; fail : 'a tree_serializable + } + | Eos_s of 'a tree_serializable * 'a tree_serializable + | Node_s of + { swap : int + ; store : bool + ; children : (TC.t * 'a tree_serializable) list + ; abstraction : (int * 'a tree_serializable) option + ; product : (int * 'a tree_serializable) option + ; default : 'a tree_serializable option + } +[@@deriving yojson] + +let rec to_tree_serializable (f : 'a -> 'b) (t : 'a tree) + : 'b tree_serializable = + match t with + | Fail -> Fail_s + + | Leaf (subst, x) -> + Leaf_s (subst, f x) + + | Cond { ok; cond; fail } -> + Cond_s + { ok = to_tree_serializable f ok + ; cond + ; fail = to_tree_serializable f fail + } + + | Eos (t1, t2) -> + Eos_s + ( to_tree_serializable f t1 + , to_tree_serializable f t2 ) + + | Node { swap; store; children; abstraction; product; default } -> + Node_s + { swap + ; store + ; children = + TCMap.bindings children + |> List.map (fun (k, v) -> + (k, to_tree_serializable f v)) + ; abstraction = + Option.map (fun (i, t) -> + (i, to_tree_serializable f t)) abstraction + ; product = + Option.map (fun (i, t) -> + (i, to_tree_serializable f t)) product + ; default = + Option.map (to_tree_serializable f) default + } + +let rec of_tree_serializable + (f : 'a -> 'a_serializable) (t : 'a tree_serializable) + : 'a_serializabe tree = + match t with + | Fail_s -> Fail + + | Leaf_s (subst, x) -> + Leaf (subst, f x) + + | Cond_s { ok; cond; fail } -> + Cond + { ok = of_tree_serializable f ok + ; cond + ; fail = of_tree_serializable f fail + } + + | Eos_s (t1, t2) -> + Eos + ( of_tree_serializable f t1 + , of_tree_serializable f t2 ) + + | Node_s { swap; store; children; abstraction; product; default } -> + Node + { swap + ; store + ; children = + List.fold_left + (fun acc (k, v) -> + TCMap.add k (of_tree_serializable f v) acc) + TCMap.empty + children + ; abstraction = + Option.map (fun (i, t) -> + (i, of_tree_serializable f t)) abstraction + ; product = + Option.map (fun (i, t) -> + (i, of_tree_serializable f t)) product + ; default = + Option.map (of_tree_serializable f) default + } + +type 'a dtree_serializable = + int * 'a tree_serializable +[@@deriving yojson] + +let to_dtree_serializable + ((f : 'a -> 'a_serialisable))((n_lazy, t_lazy) : 'a dtree) + : 'a_serialisable dtree_serializable = + let n = Lazy.force n_lazy in + let t = Lazy.force t_lazy in + ( n + , to_tree_serializable f t + ) +let of_dtree_serializable ((f : 'a_serialisable -> 'a)) + ((n, t) :'a_serialisable dtree_serializable) + : 'a dtree = + ( lazy n + , lazy (of_tree_serializable f t) + ) + (** [empty_dtree] is the empty decision tree. *) let empty_dtree : 'a dtree = (lazy 0, lazy Fail) diff --git a/src/handle/compile.ml b/src/handle/compile.ml index b2f3ff365..122d22c92 100644 --- a/src/handle/compile.ml +++ b/src/handle/compile.ml @@ -65,7 +65,8 @@ let rec compile_with : Console.out 1 (Color.blu "End checking \"%s\"%s") src forced; Sign.strip_private sign; if Stdlib.(!gen_obj) then begin - Console.out 2 (Color.blu "Writing \"%s\" ...")obj; Sign.write sign obj + Console.out 2 (Color.blu "Writing \"%s\" ...")obj; + Sig_serialize.write sign obj end; loading := List.tl !loading; sign @@ -73,7 +74,7 @@ let rec compile_with : else begin Console.out 2 (Color.blu "Loading \"%s\" ...") obj; - let sign = Sign.read obj in + let sign = Sig_serialize.read obj in (* We recursively load every module [mp'] on which [mp] depends. *) let compile mp' _ = ignore (compile_with ~handle ~force:false mp') in Path.Map.iter compile !(sign.sign_deps);