From 8905fc14f60f11a74fd778a24a4339fd4f463ab2 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 31 Mar 2026 17:28:42 +0200 Subject: [PATCH 01/26] a minimal export to lpo using Yojson --- src/core/dune | 4 +++- src/core/sign.ml | 47 +++++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 46 insertions(+), 5 deletions(-) diff --git a/src/core/dune b/src/core/dune index 8cb3b6b72..7889ee6c9 100644 --- a/src/core/dune +++ b/src/core/dune @@ -9,5 +9,7 @@ (name core) (public_name lambdapi.core) (synopsis "LambdaPi interactive theorem prover [core]") + (inline_tests) + (preprocess (pps ppx_inline_test)) (modules :standard) - (libraries lambdapi.common lambdapi.lplib pratter why3 unix)) + (libraries yojson lambdapi.common lambdapi.lplib pratter why3 unix)) diff --git a/src/core/sign.ml b/src/core/sign.ml index d60eb99a3..d59b28543 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -4,6 +4,7 @@ open Lplib open Extra open Common open Error open Pos open Timed open Term +module J = Yojson.Basic (** Data associated to inductive types. *) type ind_data = @@ -249,6 +250,12 @@ let strip_private : t -> unit = fun sign -> sign.sign_symbols := StrMap.filter (fun _ s -> not_prv s) !(sign.sign_symbols) +let toJson sign = + `Assoc [ + "version", `String Version.version; + "sign_path", `List (List.map (fun s -> `String s) sign.sign_path) + ] + (** [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 @@ -256,7 +263,10 @@ let write : t -> string -> unit = fun sign fname -> process. *) match Unix.fork () with | 0 -> let oc = open_out fname in - unlink sign; Marshal.to_channel oc sign [Marshal.Closures]; + unlink sign; + let sign_json = toJson sign in + J.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) @@ -272,11 +282,24 @@ let read : string -> t = fun fname -> let ic = open_in fname in let sign = try - let sign = Marshal.from_channel ic in + let json_sign = J.from_channel ic in + let version = + json_sign + |> J.Util.member "version" + |> J.Util.to_string in + if version <> Version.version then + raise (Failure ("Version " ^ version ^ " found but " ^ Version.version ^ "expected (current)")); + let sign_path = + json_sign + |> J.Util.member "sign_path" + |> J.Util.to_list + |> List.map J.Util.to_string in + let sign = create (sign_path) in + (* let sign = Marshal.from_channel ic in *) close_in ic; sign - with Failure _ -> + with Failure msg -> close_in ic; - fatal_no_pos "File \"%s\" is incompatible with current binary." fname + 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; @@ -432,3 +455,19 @@ let rec dependencies : t -> (Path.t * t) list = fun sign -> | d::deps -> minimize ((List.filter not_here d) :: acc) deps in List.concat (minimize [] deps) + +let dump = + { + sign_symbols = ref StrMap.empty + ; sign_path = ["/tmp/test_sign_read_write.lpo"] + ; sign_deps = ref Path.Map.empty + ; sign_builtins = ref StrMap.empty + ; sign_ind = ref SymMap.empty + ; sign_cp_pos = ref SymMap.empty } + +let%test "rev" = + let sign = dump in + write sign "/tmp/test_sign_read_write.lpo"; + let r_sign = read "/tmp/test_sign_read_write.lpo" in + false && + sign.sign_path = r_sign.sign_path \ No newline at end of file From 851c26b191408b4f87b6a499de6195a4293bb74c Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 1 Apr 2026 23:24:57 +0200 Subject: [PATCH 02/26] partial export with ppx_deriving --- src/core/dune | 3 ++- src/core/sign.ml | 59 ++++++++++++++++++++++++++++++++--------- src/core/term.ml | 67 ++++++++++++++++++++++++++++++++++++++++++++++- src/core/term.mli | 21 +++++++++++++++ 4 files changed, 135 insertions(+), 15 deletions(-) diff --git a/src/core/dune b/src/core/dune index 7889ee6c9..e623551fc 100644 --- a/src/core/dune +++ b/src/core/dune @@ -10,6 +10,7 @@ (public_name lambdapi.core) (synopsis "LambdaPi interactive theorem prover [core]") (inline_tests) - (preprocess (pps ppx_inline_test)) +; (preprocess (pps )) + (preprocess (pps ppx_inline_test ppx_deriving_yojson)) (modules :standard) (libraries yojson lambdapi.common lambdapi.lplib pratter why3 unix)) diff --git a/src/core/sign.ml b/src/core/sign.ml index d59b28543..268afae48 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -250,10 +250,15 @@ let strip_private : t -> unit = fun sign -> sign.sign_symbols := StrMap.filter (fun _ s -> not_prv s) !(sign.sign_symbols) -let toJson sign = +let toJson sign : Yojson.Safe.t = + let rules_assoc = + StrMap.bindings (Timed.(!)sign.sign_symbols) + |> List.map (fun (k, v) -> (k, sym_to_yojson v)) + in `Assoc [ - "version", `String Version.version; - "sign_path", `List (List.map (fun s -> `String s) sign.sign_path) + "version" , `String Version.version + ; "sign_path" , `List (List.map (fun s -> `String s) sign.sign_path) + ; ("sign_symbols", `Assoc rules_assoc) ] (** [write sign file] writes the signature [sign] to the file [fname]. *) @@ -265,7 +270,8 @@ let write : t -> string -> unit = fun sign fname -> | 0 -> let oc = open_out fname in unlink sign; let sign_json = toJson sign in - J.to_channel oc sign_json; + 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) @@ -282,19 +288,39 @@ let read : string -> t = fun fname -> let ic = open_in fname in let sign = try - let json_sign = J.from_channel ic in + let json_sign = Yojson.Safe.from_channel ic in let version = json_sign - |> J.Util.member "version" - |> J.Util.to_string in + |> Yojson.Safe.Util.member "version" + |> Yojson.Safe.Util.to_string in if version <> Version.version then raise (Failure ("Version " ^ version ^ " found but " ^ Version.version ^ "expected (current)")); let sign_path = json_sign - |> J.Util.member "sign_path" - |> J.Util.to_list - |> List.map J.Util.to_string in - let sign = create (sign_path) in + |> Yojson.Safe.Util.member "sign_path" + |> Yojson.Safe.Util.to_list + |> List.map Yojson.Safe.Util.to_string in + + let sign_symbols = + json_sign + |> Yojson.Safe.Util.member "sign_symbols" + |> Yojson.Safe.Util.to_assoc + |> List.fold_left (fun acc (k, v) -> + match sym_of_yojson v with + | Ok sym -> StrMap.add k sym acc + | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) + ) StrMap.empty + in + + + + + let sign = create (sign_path) in + let sign = {sign with sign_symbols = Timed.ref sign_symbols} in + + + (* READ sign_symbols and update sign *) + (* let sign = Marshal.from_channel ic in *) close_in ic; sign with Failure msg -> @@ -467,7 +493,14 @@ let dump = let%test "rev" = let sign = dump in + let symbols = Timed.(!) sign.sign_symbols in + let symbols = StrMap.add "" sym_dump symbols in + let sign = {sign with sign_symbols = Timed.ref symbols} in write sign "/tmp/test_sign_read_write.lpo"; let r_sign = read "/tmp/test_sign_read_write.lpo" in - false && - sign.sign_path = r_sign.sign_path \ No newline at end of file + (* false && *) + sign.sign_path = r_sign.sign_path && + (StrMap.equal (fun a b -> (Sym.compare a b) = 0) + (Timed.(!)(sign.sign_symbols)) + (Timed.(!)(r_sign.sign_symbols)) + ) (*FIX ME : Sym.compare does not seem to compare the entire structure *) \ No newline at end of file diff --git a/src/core/term.ml b/src/core/term.ml index 7f4fc918c..e71b0e03f 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -28,7 +28,7 @@ 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. *) @@ -989,3 +989,68 @@ module Raw = struct let term = term let _ = term let ctxt = ctxt let _ = ctxt end + +type sym_serializable = + { ser_sym_expo : expo + (* ; sym_path : Path.t *) + (* ; sym_name : string *) + (* ; sym_type : term Timed.ref *) + (* ; sym_impl : bool list *) + (* ; sym_prop : prop *) + (* ; sym_nota : float notation Timed.ref *) + (* ; sym_def : term option Timed.ref *) + (* ; sym_opaq : bool Timed.ref *) + (* ; sym_rules : rule list Timed.ref *) + (* ; sym_mstrat: match_strat *) + (* ; sym_dtree : dtree Timed.ref *) + (* ; sym_pos : Pos.popt *) + (* ; sym_decl_pos : Pos.popt *) + } [@@deriving yojson] + + let to_sym_serializable s = + { + ser_sym_expo = s.sym_expo + } + let of_sym_serializable s = + { + sym_expo = s.ser_sym_expo + ; sym_path = [] + ; sym_name = "" + ; sym_type = Timed.ref Type + ; sym_impl = [] + ; sym_prop = Defin + ; sym_nota = Timed.ref NoNotation + ; sym_def = Timed.ref None + ; sym_opaq = Timed.ref true + ; sym_rules = Timed.ref [] + ; sym_mstrat = Sequen + ; sym_dtree = Timed.ref Tree_type.empty_dtree + ; sym_pos = None + ; sym_decl_pos = None + } + + let sym_to_yojson s = + sym_serializable_to_yojson (to_sym_serializable s) + + let sym_of_yojson j = + match (sym_serializable_of_yojson j) with + | Ok j -> Ok (of_sym_serializable j) + | Error s -> Error s + +let sym_dump = + { + sym_expo = Privat + ; sym_path = [] + ; sym_name = "" + ; sym_type = Timed.ref Type + ; sym_impl = [] + ; sym_prop = Defin + ; sym_nota = Timed.ref NoNotation + ; sym_def = Timed.ref None + ; sym_opaq = Timed.ref true + ; sym_rules = Timed.ref [] + ; sym_mstrat = Sequen + ; sym_dtree = Timed.ref Tree_type.empty_dtree + ; sym_pos = None + ; sym_decl_pos = None + } \ No newline at end of file diff --git a/src/core/term.mli b/src/core/term.mli index ae3789269..26e671593 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -465,3 +465,24 @@ module Raw : sig val term : term pp val ctxt : ctxt pp end + +type sym_serializable = + { ser_sym_expo : expo + (* ; sym_path : Path.t *) + (* ; sym_name : string *) + (* ; sym_type : term Timed.ref *) + (* ; sym_impl : bool list *) + (* ; sym_prop : prop *) + (* ; sym_nota : float notation Timed.ref *) + (* ; sym_def : term option Timed.ref *) + (* ; sym_opaq : bool Timed.ref *) + (* ; sym_rules : rule list Timed.ref *) + (* ; sym_mstrat: match_strat *) + (* ; sym_dtree : dtree Timed.ref *) + (* ; sym_pos : Pos.popt *) + (* ; sym_decl_pos : Pos.popt *) + } + +val sym_dump : sym +val sym_to_yojson : sym -> Yojson.Safe.t +val sym_of_yojson : Yojson.Safe.t -> (sym, string) result \ No newline at end of file From 37c284dd2631f72e9081745800d41d80f1c020e5 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Fri, 3 Apr 2026 17:47:15 +0200 Subject: [PATCH 03/26] with sym_path --- src/common/dune | 1 + src/common/path.ml | 2 +- src/core/sign.ml | 36 +++++++++++++++++++++++------------- src/core/term.ml | 29 +++++++++++++++-------------- src/core/term.mli | 2 +- 5 files changed, 41 insertions(+), 29 deletions(-) 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..e2fd3acdc 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 diff --git a/src/core/sign.ml b/src/core/sign.ml index 268afae48..b46a48d5d 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -304,17 +304,13 @@ let read : string -> t = fun fname -> let sign_symbols = json_sign |> Yojson.Safe.Util.member "sign_symbols" - |> Yojson.Safe.Util.to_assoc - |> List.fold_left (fun acc (k, v) -> + |> Yojson.Safe.Util.to_assoc + |> List.fold_left (fun acc (k, v) -> match sym_of_yojson v with | Ok sym -> StrMap.add k sym acc | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) ) StrMap.empty in - - - - let sign = create (sign_path) in let sign = {sign with sign_symbols = Timed.ref sign_symbols} in @@ -494,13 +490,27 @@ let dump = let%test "rev" = let sign = dump in let symbols = Timed.(!) sign.sign_symbols in - let symbols = StrMap.add "" sym_dump symbols in + let symbols = StrMap.add "" + { + sym_dump + with + sym_path = ["rep"; "file"] + } + symbols in let sign = {sign with sign_symbols = Timed.ref symbols} in - write sign "/tmp/test_sign_read_write.lpo"; - let r_sign = read "/tmp/test_sign_read_write.lpo" in - (* false && *) - sign.sign_path = r_sign.sign_path && - (StrMap.equal (fun a b -> (Sym.compare a b) = 0) + 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_name = b.sym_name + && a.sym_expo = b.sym_expo + && (Path.compare a.sym_path b.sym_path = 0) + ) *) (Timed.(!)(sign.sign_symbols)) (Timed.(!)(r_sign.sign_symbols)) - ) (*FIX ME : Sym.compare does not seem to compare the entire structure *) \ No newline at end of file + ) \ No newline at end of file diff --git a/src/core/term.ml b/src/core/term.ml index e71b0e03f..9747edcc1 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -992,7 +992,7 @@ end type sym_serializable = { ser_sym_expo : expo - (* ; sym_path : Path.t *) + ; ser_sym_path : Path.t (* ; sym_name : string *) (* ; sym_type : term Timed.ref *) (* ; sym_impl : bool list *) @@ -1010,23 +1010,24 @@ type sym_serializable = let to_sym_serializable s = { ser_sym_expo = s.sym_expo + ; ser_sym_path = s.sym_path } let of_sym_serializable s = { sym_expo = s.ser_sym_expo - ; sym_path = [] - ; sym_name = "" - ; sym_type = Timed.ref Type - ; sym_impl = [] - ; sym_prop = Defin - ; sym_nota = Timed.ref NoNotation - ; sym_def = Timed.ref None - ; sym_opaq = Timed.ref true - ; sym_rules = Timed.ref [] - ; sym_mstrat = Sequen - ; sym_dtree = Timed.ref Tree_type.empty_dtree - ; sym_pos = None - ; sym_decl_pos = None + ; sym_path = s.ser_sym_path + ; sym_name = "" (*FIX ME*) + ; sym_type = Timed.ref Type (*FIX ME*) + ; sym_impl = [] (*FIX ME*) + ; sym_prop = Defin (*FIX ME*) + ; sym_nota = Timed.ref NoNotation (*FIX ME*) + ; sym_def = Timed.ref None (*FIX ME*) + ; sym_opaq = Timed.ref true (*FIX ME*) + ; sym_rules = Timed.ref [] (*FIX ME*) + ; sym_mstrat = Sequen (*FIX ME*) + ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) + ; sym_pos = None (*FIX ME*) + ; sym_decl_pos = None (*FIX ME*) } let sym_to_yojson s = diff --git a/src/core/term.mli b/src/core/term.mli index 26e671593..d78c2e1a9 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -468,7 +468,7 @@ end type sym_serializable = { ser_sym_expo : expo - (* ; sym_path : Path.t *) + ; ser_sym_path : Path.t (* ; sym_name : string *) (* ; sym_type : term Timed.ref *) (* ; sym_impl : bool list *) From b80bb1b232605e25180609db00a79677067c839d Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Fri, 3 Apr 2026 17:57:48 +0200 Subject: [PATCH 04/26] with sym_name --- src/core/sign.ml | 8 ++++---- src/core/term.ml | 27 ++++++++++++++------------- src/core/term.mli | 24 ++++++++++++------------ 3 files changed, 30 insertions(+), 29 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index b46a48d5d..6b961e703 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -505,12 +505,12 @@ let%test "rev" = (StrMap.equal (fun a b -> (Sym.compare a b) = 0 - ) - (* Should compare : - a.sym_name = b.sym_name + (* Should compare : *) + (* a.sym_name = b.sym_name && 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/term.ml b/src/core/term.ml index 9747edcc1..4702e35dd 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -993,30 +993,31 @@ end type sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t - (* ; sym_name : string *) - (* ; sym_type : term Timed.ref *) - (* ; sym_impl : bool list *) - (* ; sym_prop : prop *) - (* ; sym_nota : float notation Timed.ref *) - (* ; sym_def : term option Timed.ref *) - (* ; sym_opaq : bool Timed.ref *) - (* ; sym_rules : rule list Timed.ref *) - (* ; sym_mstrat: match_strat *) - (* ; sym_dtree : dtree Timed.ref *) - (* ; sym_pos : Pos.popt *) - (* ; sym_decl_pos : Pos.popt *) + ; ser_sym_name : string + (* ; ser_sym_type : term Timed.ref *) + (* ; ser_sym_impl : bool list *) + (* ; ser_sym_prop : prop *) + (* ; ser_sym_nota : float notation Timed.ref *) + (* ; ser_sym_def : term option Timed.ref *) + (* ; ser_sym_opaq : bool Timed.ref *) + (* ; ser_sym_rules : rule list Timed.ref *) + (* ; ser_sym_mstrat: match_strat *) + (* ; ser_sym_dtree : dtree Timed.ref *) + (* ; ser_sym_pos : Pos.popt *) + (* ; ser_sym_decl_pos : Pos.popt *) } [@@deriving yojson] let to_sym_serializable s = { ser_sym_expo = s.sym_expo ; ser_sym_path = s.sym_path + ; ser_sym_name = s.sym_name } let of_sym_serializable s = { sym_expo = s.ser_sym_expo ; sym_path = s.ser_sym_path - ; sym_name = "" (*FIX ME*) + ; sym_name = s.ser_sym_name ; sym_type = Timed.ref Type (*FIX ME*) ; sym_impl = [] (*FIX ME*) ; sym_prop = Defin (*FIX ME*) diff --git a/src/core/term.mli b/src/core/term.mli index d78c2e1a9..2489fd8dc 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -469,18 +469,18 @@ end type sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t - (* ; sym_name : string *) - (* ; sym_type : term Timed.ref *) - (* ; sym_impl : bool list *) - (* ; sym_prop : prop *) - (* ; sym_nota : float notation Timed.ref *) - (* ; sym_def : term option Timed.ref *) - (* ; sym_opaq : bool Timed.ref *) - (* ; sym_rules : rule list Timed.ref *) - (* ; sym_mstrat: match_strat *) - (* ; sym_dtree : dtree Timed.ref *) - (* ; sym_pos : Pos.popt *) - (* ; sym_decl_pos : Pos.popt *) + ; ser_sym_name : string + (* ; ser_sym_type : term Timed.ref *) + (* ; ser_sym_impl : bool list *) + (* ; ser_sym_prop : prop *) + (* ; ser_sym_nota : float notation Timed.ref *) + (* ; ser_sym_def : term option Timed.ref *) + (* ; ser_sym_opaq : bool Timed.ref *) + (* ; ser_sym_rules : rule list Timed.ref *) + (* ; ser_sym_mstrat: match_strat *) + (* ; ser_sym_dtree : dtree Timed.ref *) + (* ; ser_sym_pos : Pos.popt *) + (* ; ser_sym_decl_pos : Pos.popt *) } val sym_dump : sym From 919aff183077ca0d99826a21b74f8cca2a217366 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 7 Apr 2026 13:20:35 +0200 Subject: [PATCH 05/26] type t with type sim. type sym with type term --- src/core/term.ml | 122 ++++- src/core/term.ml.back | 1114 +++++++++++++++++++++++++++++++++++++++++ src/core/term.mli | 34 +- 3 files changed, 1242 insertions(+), 28 deletions(-) create mode 100644 src/core/term.ml.back diff --git a/src/core/term.ml b/src/core/term.ml index 4702e35dd..7a5120c16 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -39,13 +39,13 @@ type prop = | AC of bool (** Associative and commutative. *) (** 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,7 +83,7 @@ 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 @@ -135,21 +135,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 @@ -990,11 +975,38 @@ module Raw = struct let ctxt = ctxt let _ = ctxt end -type sym_serializable = +type term_serializable = + | Ser_Vari of var + | Ser_Bvar of bvar + | Ser_Type + | Ser_Kind + | Ser_Symb of sym_serializable + | Ser_Prod of term_serializable * binder_serializable + | Ser_Abst of term_serializable * binder_serializable + | Ser_Appl of term_serializable * term_serializable + | Ser_Meta of meta_serializable * term_serializable array + | Ser_Patt of int option * string * term_serializable array + | Ser_Wild + | Ser_Plac of bool + | Ser_TRef of term_serializable option + | Ser_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 = + { ser_meta_key : int + ; ser_meta_type : term_serializable (**Timed.ref. *) + ; ser_meta_arity : int + ; ser_meta_value : mbinder_serializable option (** Timed.ref. *) } [@@deriving yojson] + +and mbinder_serializable = mbinder_info * term_serializable * term_serializable array [@@deriving yojson] + +and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t ; ser_sym_name : string - (* ; ser_sym_type : term Timed.ref *) + ; ser_sym_type : term_serializable (* ; ser_sym_impl : bool list *) (* ; ser_sym_prop : prop *) (* ; ser_sym_nota : float notation Timed.ref *) @@ -1007,18 +1019,77 @@ type sym_serializable = (* ; ser_sym_decl_pos : Pos.popt *) } [@@deriving yojson] - let to_sym_serializable s = +let rec to_term_serializable t = match t with + | Vari x -> Ser_Vari x + | Bvar x -> Ser_Bvar x + | Type -> Ser_Type + | Kind -> Ser_Kind + | Symb x -> Ser_Symb (to_sym_serializable x) + | Prod (x, y) -> Ser_Prod (to_term_serializable x, to_binder_serializable y) + | Abst (x, y) -> Ser_Abst (to_term_serializable x, to_binder_serializable y) + | Appl (x, y) -> Ser_Appl (to_term_serializable x, to_term_serializable y) + | Meta (x, y) -> Ser_Meta ((to_meta_serializable x), Array.map to_term_serializable y) + | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) + | Wild -> Ser_Wild + | Plac x -> Ser_Plac x + | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x) ) + (* | TRef x -> Ser_TRef (match Timed.(!) x with None -> None | Some x -> Some (to_term_serializable x)) *) + | LLet (x, y, z) -> Ser_LLet (to_term_serializable x, to_term_serializable y, to_binder_serializable z) +and to_binder_serializable (x, y, z) = + (x, to_term_serializable y, Array.map to_term_serializable z) + +and to_meta_serializable t = + { ser_meta_key = t.meta_key + ; ser_meta_type = to_term_serializable (Timed.(!) t.meta_type) + ; ser_meta_arity = t.meta_arity + ; ser_meta_value = (Option.map to_mbinder_serializable (Timed.(!)t.meta_value))} + +and to_mbinder_serializable (x, y ,z) = + (x, to_term_serializable y, Array.map to_term_serializable z) + + + +and to_sym_serializable s = { ser_sym_expo = s.sym_expo ; ser_sym_path = s.sym_path ; ser_sym_name = s.sym_name + ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) } - let of_sym_serializable s = +let rec of_term_serializable t = match t with + | Ser_Vari x -> Vari x + | Ser_Bvar x -> Bvar x + | Ser_Type -> Type + | Ser_Kind -> Kind + | Ser_Symb x -> Symb (of_sym_serializable x) + | Ser_Prod (x, y) -> Prod (of_term_serializable x, of_binder_serializable y) + | Ser_Abst (x, y) -> Abst (of_term_serializable x, of_binder_serializable y) + | Ser_Appl (x, y) -> Appl (of_term_serializable x, of_term_serializable y) + | Ser_Meta (x, y) -> Meta ((of_meta_serializable x), Array.map of_term_serializable y) + | Ser_Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) + | Ser_Wild -> Wild + | Ser_Plac x -> Plac x + | Ser_TRef x -> TRef (Timed.ref (Option.map of_term_serializable x)) + | Ser_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_meta_serializable t = + { meta_key = t.ser_meta_key + ; meta_type = Timed.ref (of_term_serializable t.ser_meta_type) + ; meta_arity = t.ser_meta_arity + ; meta_value = Timed.ref (Option.map of_mbinder_serializable t.ser_meta_value)} + +and of_mbinder_serializable (x, y ,z) = + (x, of_term_serializable y, Array.map of_term_serializable z) + + +and of_sym_serializable s = { sym_expo = s.ser_sym_expo ; sym_path = s.ser_sym_path ; sym_name = s.ser_sym_name - ; sym_type = Timed.ref Type (*FIX ME*) + ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) ; sym_impl = [] (*FIX ME*) ; sym_prop = Defin (*FIX ME*) ; sym_nota = Timed.ref NoNotation (*FIX ME*) @@ -1038,8 +1109,7 @@ type sym_serializable = match (sym_serializable_of_yojson j) with | Ok j -> Ok (of_sym_serializable j) | Error s -> Error s - -let sym_dump = + let sym_dump = { sym_expo = Privat ; sym_path = [] diff --git a/src/core/term.ml.back b/src/core/term.ml.back new file mode 100644 index 000000000..43fe81b4e --- /dev/null +++ b/src/core/term.ml.back @@ -0,0 +1,1114 @@ +(** Internal representation of terms. + + This module contains the definition of the internal representation of + terms, together with smart constructors and low level operation. *) + +open Lplib open Base open Extra +open Common open Debug + +let log = Logger.make 'm' "term" "term building" +let log = log.pp + +(** {3 Term (and symbol) representation} *) + +(** Representation of a possibly qualified identifier. *) +type qident = Path.t * string + +(** Pattern-matching strategy modifiers. *) +type match_strat = + | Sequen + (** Rules are processed sequentially: a rule can be applied only if the + previous ones (in the order of declaration) cannot be. *) + | 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. *) + +(** 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. *) + | Const (** Constant. *) + | Injec (** Injective. *) + | Commu (** Commutative. *) + | Assoc of bool (** Associative left if [true], right if [false]. *) + | AC of bool (** Associative and commutative. *) + +(** Data of a binder. *) +type binder_info = {binder_name : string; binder_bound : bool} [@@deriving yojson] +type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} + +let pr_bound = D.array (fun ppf b -> if b then out ppf "*" else out ppf "_") + +(** Type for free variables. *) +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]. *) +let compare_vars : var -> var -> int = fun (i,_) (j,_) -> Stdlib.compare i j + +(** [eq_vars x y] safely computes the equality of [x] and [y]. Note that it is + unsafe to compare variables with the polymorphic equality function. *) +let eq_vars : var -> var -> bool = fun x y -> compare_vars x y = 0 + +(** [new_var name] creates a new unique variable of name [name]. *) +let new_var : string -> var = + let n = Stdlib.ref 0 in fun name -> incr n; !n, name + +(** [new_var_ind s i] creates a new [var] of name [s ^ string_of_int i]. *) +let new_var_ind : string -> int -> var = fun s i -> + new_var (Escape.add_prefix s (string_of_int i)) + +(** [base_name x] returns the base name of variable [x]. Note that this name + is not unique: two distinct variables may have the same name. *) +let base_name : var -> string = fun (_i,n) -> n + +(** [uniq_name x] returns a string uniquely identifying the variable [x]. *) +let uniq_name : var -> string = fun (i,_) -> "v" ^ string_of_int i + +(** Sets and maps of variables. *) +module Var = struct + type t = var + let compare = compare_vars +end + +module VarSet = Set.Make(Var) +module VarMap = Map.Make(Var) + +(* Type for bound variables. [InSub i] refers to the i-th slot in the + 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 [@@deriving yojson] + +(** The priority of an infix operator is a floating-point number. *) +type priority = float + +(** Notations. *) +type 'a notation = + | NoNotation + | Prefix of 'a + | Postfix of 'a + | Infix of Pratter.associativity * 'a + | Zero + | Succ of 'a notation (* NoNotation, Prefix or Postfix only *) + | Quant + | PosOne + | PosDouble + | PosSuccDouble + | IntZero + | IntPos + | IntNeg + +(** 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 + are considered invalid in unrelated code. + + Bound variables [Bvar] never appear outside of the current module. They + correspond to the variables bound by a binder above. They are replaced by + [Vari] whenever the binder is destructed (via unbind and the like) + *) +type term = + | Vari of var (** Free variable. *) + | Bvar of bvar (** Bound variables. Only used internally. *) + | Type (** "TYPE" constant. *) + | Kind (** "KIND" constant. *) + | Symb of sym (** User-defined symbol. *) + | Prod of term * binder (** Dependent product. *) + | Abst of term * binder (** Abstraction. *) + | Appl of term * term (** Term application. *) + | Meta of meta * term array (** Metavariable application. *) + | Patt of int option * string * term array + (** Pattern variable application (only used in rewriting rules). *) + | Wild (** Wildcard (only used for surface matching, never in LHS). *) + | Plac of bool + (** [Plac b] is a placeholder, or hole, for not given terms. Boolean [b] is + true if the placeholder stands for a type. *) + | TRef of term option Timed.ref + (** Reference cell (used in surface matching, and evaluation with + sharing). *) + | LLet of term * term * binder + (** [LLet(a, t, u)] is [let x : a ≔ t in u] (with [x] bound in [u]). *) + +(* and term_serializable = string + | Ser_Vari of var + | Ser_Bvar of bvar + | Ser_Type + | Ser_Kind + | Ser_Symb of sym + | Ser_Prod of term_serializable * binder_serializable + | Ser_Abst of term_serializable * binder_serializable + | Ser_Appl of term_serializable * term_serializable + | Ser_Meta of meta * term_serializable array + | Ser_Patt of int option * string * term_serializable array + | Ser_Wild + | Ser_Plac of bool + | Ser_TRef of term_serializable option + | Ser_LLet of term_serializable * term_serializable * binder_serializable +[@@deriving yojson] *) + +(** 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 binder_serializable = binder_info * term_serializable * term_serializable [@@deriving yojson] *) +and mbinder = mbinder_info * term * term array + +(** {b NOTE} that a wildcard "_" of the concrete (source code) syntax may have + a different representation depending on the context. For instance, the + {!constructor:Wild} constructor is only used when matching patterns (e.g., + with the "rewrite" tactic). In the LHS of a rewriting {!type:rule}, we use + the {!constructor:Patt} constructor to represend wildcards of the concrete + syntax. They are thus considered to be fresh, unused pattern variables. *) + +(** Representation of a decision tree (used for rewriting). *) +and dtree = rule Tree_type.dtree + +(** Representation of a user-defined symbol. *) +and sym = + { sym_expo : expo (** Visibility. *) + ; sym_path : Path.t (** Module in which the symbol is defined. *) + ; sym_name : string (** Name. *) + ; sym_type : term Timed.ref (** Type. *) + ; sym_impl : bool list (** Implicit arguments ([true] meaning implicit). *) + ; sym_prop : prop (** Property. *) + ; sym_nota : float notation Timed.ref (** Notation. *) + ; sym_def : term option Timed.ref (** Definition with ≔. *) + ; sym_opaq : bool Timed.ref (** Opacity. *) + ; sym_rules : rule list Timed.ref (** Rewriting rules. *) + ; sym_mstrat: match_strat (** Matching strategy. *) + ; sym_dtree : dtree Timed.ref (** Decision tree used for matching. *) + ; sym_pos : Pos.popt (** Position in source file of symbol name. *) + ; sym_decl_pos : Pos.popt (** Position in source file of symbol declaration + without its definition. *) } + +(** {b NOTE} {!field:sym_type} holds a (timed) reference for a technical + reason related to the writing of signatures as binary files (in relation + to {!val:Sign.link} and {!val:Sign.unlink}). This is necessary to + ensure that two identical symbols are always physically equal, even across + signatures. It should NOT be otherwise mutated. *) + +(** {b NOTE} We maintain the invariant that {!field:sym_impl} never ends with + [false]. Indeed, this information would be redundant. If a symbol has more + arguments than there are booleans in the list then the extra arguments are + all explicit. Finally, note that {!field:sym_impl} is empty if and only if + the symbol has no implicit parameters. *) + +(** {b NOTE} {!field:sym_prop} restricts the possible + values of {!field:sym_def} and {!field:sym_rules} fields. A symbol is + not allowed to be given rewriting rules (or a definition) when its mode is + set to {!constructor:Constant}. Moreover, a symbol should not be given at + the same time a definition (i.e., {!field:sym_def} different from [None]) + and rewriting rules (i.e., {!field:sym_rules} is non-empty). *) + +(** {b NOTE} For generated symbols (recursors, axioms), {!field:sym_pos} may + not be valid positions in the source. These virtual positions are however + important for exporting lambdapi files to other formats. *) + +(** {3 Representation of rewriting rules} *) + +(** Representation of a rewriting rule. A rewriting rule is mainly formed of a + LHS (left hand side), which is the pattern that should be matched for the + rule to apply, and a RHS (right hand side) giving the action to perform if + the rule applies. More explanations are given below. *) + and rule = + { lhs : term list (** Left hand side (LHS). *) + ; names : string array (** Names of pattern variables. *) + ; rhs : term (** Right hand side (RHS). *) + ; arity : int (** Required number of arguments to be applicable. *) + ; arities : int array + (** Arities of the pattern variables bound in the RHS. *) + ; vars_nb : int (** Number of variables in [lhs]. *) + ; xvars_nb : int (** Number of variables in [rhs] but not in [lhs]. *) + ; rule_pos : Pos.popt (** Position of the rule in the source file. *) } + +(** {b NOTE} {!field:arity} gives the number of arguments contained in the + LHS. It is always equal to [List.length r.lhs] and gives the minimal number + of arguments required to match the LHS. *) + +(** {b NOTE} For generated rules, {!field:rule_pos} may not be valid positions + in the source. These virtual positions are however important for exporting + lambdapi files to other formats. *) + +(** All variables of rewriting rules that appear in the RHS must appear in the + LHS. In the case of unification rules, we allow variables to appear only in + the RHS. In that case, these variables are replaced by fresh meta-variables + each time the rule is used. *) + +(** During evaluation, we only try to apply rewriting rules when we reduce the + application of a symbol [s] to a list of argument [ts]. At this point, the + symbol [s] contains every rule [r] that can potentially be applied in its + {!field:sym_rules} field. To check if a rule [r] applies, we match the + elements of [r.lhs] with those of [ts] while building an environment [env]. + During this process, a pattern of + the form {!constructor:Patt}[(Some i,_,_)] matched against a term [u] will + results in [env.(i)] being set to [u]. If all terms of [ts] can be matched + against corresponding patterns, then environment [env] is fully constructed + and it can hence be substituted in [r.rhs] with [subst_patt env r.rhs] + to get the result of the application of the rule. *) + +(** {3 Metavariables and related functions} *) + +(** Representation of a metavariable, which corresponds to a yet unknown + term typable in some context. The substitution of the free variables + of the context is suspended until the metavariable is instantiated + (i.e., set to a particular term). When a metavariable [m] is + instantiated, the suspended substitution is unlocked and terms of + the form {!constructor:Meta}[(m,env)] can be unfolded. *) +and meta = + { meta_key : int (** Unique key. *) + ; meta_type : term Timed.ref (** Type. *) + ; meta_arity : int (** Arity (environment size). *) + ; meta_value : mbinder option Timed.ref (** Definition. *) } + +let binder_name : binder -> string = fun (bi,_,_) -> bi.binder_name +let mbinder_names : mbinder -> string array = fun (bi,_,_) -> bi.mbinder_name + +(** [mbinder_arity b] gives the arity of the [mbinder]. *) +let mbinder_arity : mbinder -> int = + fun (i,_,_) -> Array.length i.mbinder_name + +(** [binder_occur b] tests whether the bound variable occurs in [b]. *) +let binder_occur : binder -> bool = fun (bi,_,_) -> bi.binder_bound +let mbinder_occur : mbinder -> int -> bool = + fun (bi,_,_) i -> assert (i < Array.length bi.mbinder_name); + bi.mbinder_bound.(i) + +(** Minimize [impl] to enforce our invariant (see {!type:Terms.sym}). *) +let minimize_impl : bool list -> bool list = + let rec rem_false l = match l with false::l -> rem_false l | _ -> l in + fun l -> List.rev (rem_false (List.rev l)) + +(** [create_sym path expo prop mstrat opaq name pos typ impl] creates a new + symbol with path [path], exposition [expo], property [prop], opacity + [opaq], matching strategy [mstrat], name [name.elt], type [typ], implicit + arguments [impl], position [name.pos], declaration position [pos], no + definition and no rules. *) +let create_sym : Path.t -> expo -> prop -> match_strat -> bool -> + Pos.strloc -> Pos.popt -> term -> bool list -> sym = + fun sym_path sym_expo sym_prop sym_mstrat sym_opaq + { elt = sym_name; pos = sym_pos } sym_decl_pos typ sym_impl -> + let open Timed in + {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None; + sym_opaq = ref sym_opaq; sym_rules = ref []; sym_nota = ref NoNotation; + sym_dtree = ref Tree_type.empty_dtree; + sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos } + +(** [is_constant s] tells whether [s] is a constant. *) +let is_constant : sym -> bool = fun s -> s.sym_prop = Const + +(** [is_injective s] tells whether [s] is injective, which is in partiular the + case if [s] is constant. *) +let is_injective : sym -> bool = fun s -> + match s.sym_prop with Const | Injec -> true | _ -> Timed.(!(s.sym_opaq)) + +(** [is_private s] tells whether the symbol [s] is private. *) +let is_private : sym -> bool = fun s -> s.sym_expo = Privat + +(** [is_modulo s] tells whether the symbol [s] is modulo some equations. *) +let is_modulo : sym -> bool = fun s -> + match s.sym_prop with Assoc _ | Commu | AC _ -> true | _ -> false + +(** Sets and maps of symbols. *) +module Sym = struct + type t = sym + let compare s1 s2 = + if s1 == s2 then 0 else + match Stdlib.compare s1.sym_name s2.sym_name with + | 0 -> Stdlib.compare s1.sym_path s2.sym_path + | n -> n +end + +module SymSet = Set.Make(Sym) +module SymMap = Map.Make(Sym) + +(** [is_unset m] returns [true] if [m] is not instantiated. *) +let is_unset : meta -> bool = fun m -> Timed.(!(m.meta_value)) = None + +(** Sets and maps of metavariables. *) +module Meta = struct + type t = meta + let compare m1 m2 = m2.meta_key - m1.meta_key +end + +module MetaSet = Set.Make(Meta) +module MetaMap = Map.Make(Meta) + +(** Dealing with AC-normalization of terms *) +let mk_bin s t1 t2 = Appl(Appl(Symb s, t1), t2) + +(** [mk_left_comb s t ts] builds a left comb of applications of [s] from + [t::ts] so that [mk_left_comb s t1 [t2; t3] = mk_bin s (mk_bin s t1 t2) + t3]. *) +let mk_left_comb : sym -> term -> term list -> term = fun s -> + List.fold_left (mk_bin s) + +(** [mk_right_comb s ts t] builds a right comb of applications of [s] to + [ts@[t]] so that [mk_right_comb s [t1; t2] t3 = mk_bin s t1 (mk_bin s t2 + t3)]. *) +let mk_right_comb : sym -> term list -> term -> term = fun s -> + List.fold_right (mk_bin s) + +(** Printing functions for debug. *) +let rec term : term pp = fun ppf t -> + match unfold t with + | Bvar (InSub k) -> out ppf "`%d" k + | Bvar (InEnv k) -> out ppf "~%d" k + | Vari v -> var ppf v + | Type -> out ppf "TYPE" + | Kind -> out ppf "KIND" + | Symb s -> sym ppf s + | Prod(a,(n,b,e)) -> + out ppf "(Π %s:%a, %a#(%a))" n.binder_name term a clos_env e term b + | Abst(a,(n,b,e)) -> + out ppf "(λ %s:%a, %a#(%a))" n.binder_name term a clos_env e term b + | Appl(a,b) -> out ppf "(%a %a)" term a term b + | Meta(m,ts) -> out ppf "?%d%a" m.meta_key terms ts + | Patt(i,s,ts) -> out ppf "$%a_%s%a" (D.option D.int) i s terms ts + | Plac(_) -> out ppf "_" + | Wild -> out ppf "_" + | TRef r -> out ppf "&%a" (Option.pp term) Timed.(!r) + | LLet(a,t,(n,b,e)) -> + out ppf "let %s:%a ≔ %a in %a#(%a)" + n.binder_name term a term t clos_env e term b +and var : var pp = fun ppf (i,n) -> out ppf "%s%d" n i +and sym : sym pp = fun ppf s -> string ppf s.sym_name +and terms : term array pp = fun ppf ts -> + if Array.length ts > 0 then D.array term ppf ts +and clos_env : term array pp = fun ppf env -> D.array term ppf env + +(** [unfold t] repeatedly unfolds the definition of the surface constructor + of [t], until a significant {!type:term} constructor is found. The term + that is returned can be neither an instantiated metavariable + nor a reference cell ({!constructor:TRef} constructor). Note + that the returned value is physically equal to [t] if no unfolding was + performed. {b NOTE} that {!val:unfold} must (almost) always be called + before matching over a value of type {!type:term}. *) +and unfold : term -> term = fun t -> + let open Timed in + match t with + | Meta(m, ts) -> + begin + match !(m.meta_value) with + | None -> t + | Some(b) -> unfold (msubst b ts) + end + | TRef(r) -> + begin + match !r with + | None -> t + | Some(v) -> unfold v + end + | _ -> t + +(** [msubst b vs] substitutes the variables bound by [b] with the values + [vs]. Note that the length of the [vs] array should match the arity of + the multiple binder [b]. *) +and msubst : mbinder -> term array -> term = fun (bi,tm,env) vs -> + let n = Array.length bi.mbinder_name in + assert (Array.length vs = n); + let rec msubst t = +(* if Logger.log_enabled() then + log "msubst %a %a" (D.array term) vs term t;*) + match unfold t with + | Bvar (InSub p) -> assert bi.mbinder_bound.(p); vs.(p) + | Bvar (InEnv p) -> env.(p) + | Appl(a,b) -> mk_Appl(msubst a, msubst b) + (* No need to substitute in the closure term: all bound variables appear + in the closure environment *) + | Abst(a,(n,u,e)) -> Abst(msubst a, (n, u, Array.map msubst e)) + | Prod(a,(n,u,e)) -> Prod(msubst a, (n, u, Array.map msubst e)) + | LLet(a,t,(n,u,e)) -> + LLet(msubst a, msubst t, (n, u, Array.map msubst e)) + | Meta(m,ts) -> Meta(m, Array.map msubst ts) + | Patt(j,n,ts) -> Patt(j,n, Array.map msubst ts) + | Type | Kind | Vari _ | Wild | Symb _ | Plac _ | TRef _ -> t + in + let r = + if Array.for_all ((=) false) bi.mbinder_bound && Array.length env = 0 + then tm + else msubst tm in + if Logger.log_enabled() then + log "msubst %a#%a %a = %a" clos_env env term tm (D.array term) vs term r; + r + +(** Total order on terms. *) +and cmp : term cmp = fun t t' -> + match unfold t, unfold t' with + | Vari x, Vari x' -> compare_vars x x' + | Type, Type + | Kind, Kind + | Wild, Wild -> 0 + | Symb s, Symb s' -> Sym.compare s s' + | Prod(t,u), Prod(t',u') + | Abst(t,u), Abst(t',u') -> lex cmp cmp_binder (t,u) (t',u') + | Appl(t,u), Appl(t',u') -> lex cmp cmp (u,t) (u',t') + | Meta(m,ts), Meta(m',ts') -> + lex Meta.compare (Array.cmp cmp) (m,ts) (m',ts') + | Patt(i,s,ts), Patt(i',s',ts') -> + lex3 Stdlib.compare Stdlib.compare (Array.cmp cmp) + (i,s,ts) (i',s',ts') + | Bvar i, Bvar j -> Stdlib.compare i j + | TRef r, TRef r' -> Stdlib.compare r r' + | LLet(a,t,u), LLet(a',t',u') -> + lex3 cmp cmp cmp_binder (a,t,u) (a',t',u') + | t, t' -> cmp_tag t t' + +and cmp_binder : binder cmp = +(* fun ({binder_name;binder_bound},u,e) (bi',u',e') -> + let mbi = {mbinder_name=[|binder_name|];mbinder_bound=[|binder_bound|]} in + let var = Vari(new_var binder_name) in + cmp (msubst (mbi,u,e)[|var|]) + (msubst({mbi with mbinder_bound=[|bi'.binder_bound|]},u',e')[|var|])*) + fun (_,u,e) (_,u',e') -> + lex cmp (Array.cmp cmp) (u,e) (u',e') + +(** [get_args t] decomposes the {!type:term} [t] into a pair [(h,args)], where + [h] is the head term of [t] and [args] is the list of arguments applied to + [h] in [t]. The returned [h] cannot be an [Appl] node. *) +and get_args : term -> term * term list = fun t -> + let rec get_args t acc = + match unfold t with + | Appl(t,u) -> get_args t (u::acc) + | t -> t, acc + in get_args t [] + +(** [get_args_len t] is similar to [get_args t] but it also returns the length + of the list of arguments. *) +and get_args_len : term -> term * term list * int = fun t -> + let rec get_args_len acc len t = + match unfold t with + | Appl(t, u) -> get_args_len (u::acc) (len + 1) t + | t -> (t, acc, len) + in + get_args_len [] 0 t + +(** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *) +and is_symb : sym -> term -> bool = fun s t -> + match unfold t with Symb(r) -> r == s | _ -> false + +(* We make the equality of terms modulo commutative and + associative-commutative symbols syntactic by always ordering arguments in + increasing order and by putting them in a comb form. + + The term [t1 + t2 + t3] is represented by the left comb [(t1 + t2) + t3] if + + is left associative and [t1 + (t2 + t3)] if + is right associative. *) + +(** [left_aliens s t] returns the list of the biggest subterms of [t] not + headed by [s], assuming that [s] is left associative and [t] is in + canonical form. This is the reverse of [mk_left_comb]. *) +and left_aliens : sym -> term -> term list = fun s -> + let rec aliens acc = function + | [] -> acc + | u::us -> + let h, ts = get_args u in + if is_symb s h then + match ts with + | t1 :: t2 :: _ -> aliens (t2 :: acc) (t1 :: us) + | _ -> aliens (u :: acc) us + else aliens (u :: acc) us + in fun t -> aliens [] [t] + +(** [right_aliens s t] returns the list of the biggest subterms of [t] not + headed by [s], assuming that [s] is right associative and [t] is in + canonical form. This is the reverse of [mk_right_comb]. *) +and right_aliens : sym -> term -> term list = fun s -> + let rec aliens acc = function + | [] -> acc + | u::us -> + let h, ts = get_args u in + if is_symb s h then + match ts with + | t1 :: t2 :: _ -> aliens (t1 :: acc) (t2 :: us) + | _ -> aliens (u :: acc) us + else aliens (u :: acc) us + in fun t -> let r = aliens [] [t] in + if Logger.log_enabled () then + log "right_aliens %a %a = %a" sym s term t (D.list term) r; + r + +(** [mk_Appl t u] puts the application of [t] to [u] in canonical form wrt C + or AC symbols. *) +and mk_Appl : term * term -> term = fun (t, u) -> + (* if Logger.log_enabled () then + log "mk_Appl(%a, %a)" term t term u; + let r = *) + match get_args t with + | Symb s, [t1] -> + begin + match s.sym_prop with + | Commu when cmp t1 u > 0 -> mk_bin s u t1 + | AC true -> (* left associative symbol *) + let ts = left_aliens s t1 and us = left_aliens s u in + begin + match List.sort cmp (ts @ us) with + | v::vs -> mk_left_comb s v vs + | _ -> assert false + end + | AC false -> (* right associative symbol *) + let ts = right_aliens s t1 and us = right_aliens s u in + let vs, v = List.split_last (List.sort cmp (ts @ us)) + in mk_right_comb s vs v + | _ -> Appl (t, u) + end + | _ -> Appl (t, u) + (* in + if Logger.log_enabled () then + log "mk_Appl(%a, %a) = %a" term t term u term r; + r *) + +(* unit test *) +let _ = + let s = + create_sym [] Privat (AC true) Eager false (Pos.none "+") None Kind [] in + let t1 = Vari (new_var "x1") in + let t2 = Vari (new_var "x2") in + let t3 = Vari (new_var "x3") in + let left = mk_bin s (mk_bin s t1 t2) t3 in + let right = mk_bin s t1 (mk_bin s t2 t3) in + let eq = eq_of_cmp cmp in + assert (eq (mk_left_comb s t1 [t2; t3]) left); + assert (eq (mk_right_comb s [t1; t2] t3) right); + let eq = eq_of_cmp (List.cmp cmp) in + assert (eq (left_aliens s left) [t1; t2; t3]); + assert (eq (right_aliens s right) [t3; t2; t1]) + +(** [is_abst t] returns [true] iff [t] is of the form [Abst _]. *) +let is_abst t = match unfold t with Abst _ -> true | _ -> false + +(** [is_prod t] returns [true] iff [t] is of the form [Prod _]. *) +let is_prod t = match unfold t with Prod _ -> true | _ -> false + +(** [is_tref t] returns [true] iff [t] is of the form [TRef _]. *) +let is_TRef t = match unfold t with TRef _ -> true | _ -> false + +(** [iter_atoms db f g t] applies f to every occurrence of a variable in t, + g to every occurrence of a symbol, and db to every occurrence of a + bound variable. + We have to be careful with binders since in the current implementation + closure environment may contain slots for variables that don't actually + appear. This is done by first checking the closure term, recording which + bound variables actually occur, and then check the elements of the + closure environment which occur. + *) +let rec iter_atoms : + (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> term -> unit = + fun db f g t -> + let rec check db t = + match unfold t with + | Vari x -> f x + | Symb s -> g s + | Bvar i -> db i + | Appl(a,b) -> check db a; check db b + | Abst(a,b) + | Prod(a,b) -> check db a; check_binder db b + | LLet(a,t,b) -> check db a; check db t; check_binder db b + | Meta(_,ts) + | Patt(_,_,ts) -> Array.iter (check db) ts + | _ -> () + and check_binder db (_bi,u,env) = + iter_atoms_closure db f g u env in + check db t + +and iter_atoms_closure : + (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> term -> term array + -> unit = + fun db f g u env -> + (* env positions occuring in [u] *) + let u_pos = ref IntSet.empty in + let db_u db = + match db with + | InEnv p -> u_pos := IntSet.add p !u_pos + | _ -> () in + (* We iterate on u, recording which env positions occur *) + iter_atoms db_u f g u; + (* We then iterate on the members of [e] that *actually* occur in u *) + Array.iteri (fun i t -> + if IntSet.mem i !u_pos then iter_atoms db f g t + (*else if t <> Wild then env.(i) <- Wild*) ) + env + +let iter_atoms_mbinder + : (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> mbinder -> unit = + fun db f g (_bi,u,env) -> iter_atoms_closure db f g u env + +(** [occur x t] tells whether variable [x] occurs in [t]. *) +let occur : var -> term -> bool = + fun x t -> + try iter_atoms + (fun _ -> ()) + (fun y -> if x==y then raise Exit) + (fun _-> ()) t; + false + with Exit -> true + +let occur_mbinder : var -> mbinder -> bool = + fun x b -> + try iter_atoms_mbinder + (fun _ -> ()) + (fun y -> if x==y then raise Exit) + (fun _-> ()) b; + false + with Exit -> true + +(** [is_closed t] checks whether [t] is closed (w.r.t. variables). We have to + be careful with binders since in the current implementation closure + environment may contain slots for variables that don't actually appear *) +let is_closed : term -> bool = + fun t -> + try iter_atoms (fun _ -> ()) (fun _ -> raise Exit) (fun _ -> ()) t; true + with Exit -> false + +let is_closed_mbinder : mbinder -> bool = + fun b -> + try iter_atoms_mbinder + (fun _ -> ()) (fun _ -> raise Exit) (fun _ -> ()) b; true + with Exit -> false + +(** [subst b v] substitutes the variable bound by [b] with the value [v]. + Assumes v is closed (since only called from outside the term library. *) +let subst : binder -> term -> term = fun (bi,tm,env) v -> + let rec subst t = + match unfold t with + | Bvar (InSub _) -> assert bi.binder_bound; v + | Bvar (InEnv p) -> env.(p) + | Appl(a,b) -> mk_Appl(subst a, subst b) + | Abst(a,(n,u,e)) -> Abst(subst a, (n, u, Array.map subst e)) + | Prod(a,(n,u,e)) -> Prod(subst a, (n ,u, Array.map subst e)) + | LLet(a,t,(n,u,e)) -> LLet(subst a, subst t, (n, u, Array.map subst e)) + | Meta(m,ts) -> Meta(m, Array.map subst ts) + | Patt(j,n,ts) -> Patt(j,n, Array.map subst ts) + | _ -> t + in + let r = + if bi.binder_bound = false && Array.length env = 0 then tm + else subst tm in + if Logger.log_enabled() then + log "subst %a#%a [%a] = %a" clos_env env term tm term v term r; + r + +(** [unbind b] substitutes the binder [b] by a fresh variable of name [name] + if given, or the binder name otherwise. The variable and the result of the + substitution are returned. *) +let unbind : ?name:string -> binder -> var * term = + fun ?(name="") ((bn,_,_) as b) -> + let n = if name="" then bn.binder_name else name in + let x = new_var n in x, subst b (Vari x) + +(** [unbind2 f g] is similar to [unbind f], but it substitutes two binders [f] + and [g] at once using the same fresh variable. *) +let unbind2 : ?name:string -> binder -> binder -> var * term * term = + fun ?(name="") ((bn1,_,_) as b1) b2 -> + let n = if name="" then bn1.binder_name else name in + let x = new_var n in x, subst b1 (Vari x), subst b2 (Vari x) + +(** [unmbind b] substitutes the multiple binder [b] with fresh variables. This + function is analogous to [unbind] for binders. Note that the names used to + create the fresh variables are based on those of the multiple binder. *) +let unmbind : mbinder -> var array * term = + fun (({mbinder_name=names;_},_,_) as b) -> + let xs = Array.init (Array.length names) (fun i -> new_var names.(i)) in + xs, msubst b (Array.map (fun x -> Vari x) xs) + +(** [bind_var x t] binds the variable [x] in [t], producing a binder. *) +let bind_var : var -> term -> binder = fun ((_,n) as x) t -> + let bound = Stdlib.ref false in + (* Replace variables [x] by de Bruijn index [i] *) + let rec bind i t = + (*if Logger.log_enabled() then log "bind_var %d %a" i term t;*) + match unfold t with + | Vari y when y == x -> bound := true; Bvar i + | Appl(a,b) -> + let a' = bind i a in + let b' = bind i b in + if a==a' && b==b' then t else Appl(a', b') + (* No need to call mk_Appl here as we only replace free variables by de + Bruijn indices. *) + | Abst(a,b) -> + let a' = bind i a in + let b' = bind_binder i b in + if a==a' && b==b' then t else Abst(a', b') + | Prod(a,b) -> + let a' = bind i a in + let b' = bind_binder i b in + if a==a' && b==b' then t else Prod(a', b') + | LLet(a,m,b) -> + let a' = bind i a in + let m' = bind i m in + let b' = bind_binder i b in + if a==a' && m==m' && b==b' then t else LLet(a', m', b') + | Meta(m,ts) -> + let ts' = Array.map (bind i) ts in + if Array.for_all2 (==) ts ts' then t else Meta(m, ts') + | Patt(j,n,ts) -> + let ts' = Array.map (bind i) ts in + if Array.for_all2 (==) ts ts' then t else Patt(j,n,ts') + | _ -> t + + and bind_binder i (bi,u,env as b) = + let env' = Array.map (bind i) env in + let j = InEnv (Array.length env') in + let u' = bind j u in + if u==u' then (* If [u==u'] then x does not occur in u *) + if Array.for_all2 (==) env env' then b + else (bi, u', env') + else (* x occurs, it has been replaced by [Bvar(j)], + corresponding to the head of [e] *) + (bi, u', Array.append env' [|Bvar i|]) in + + let b = bind (InSub 0) t in + if Logger.log_enabled() then + log "bind_var %a %a = %a" var x term t term b; + {binder_name=n; binder_bound= !bound}, b, [||] + +(** [binder f b] applies f inside [b]. *) +let binder : (term -> term) -> binder -> binder = fun f b -> + let x,t = unbind b in bind_var x (f t) + +(** [bind_mvar xs t] binds the variables of [xs] in [t] to get a binder. + It is the equivalent of [bind_var] for multiple variables. *) +let bind_mvar : var array -> term -> mbinder = + let empty = {mbinder_name=[||]; mbinder_bound=[||]} in + fun xs tm -> + if Array.length xs = 0 then empty, tm, [||] else begin + (*if Logger.log_enabled() then + log "bind_mvar %a" (D.array var) xs;*) + let top_map = Stdlib.ref IntMap.empty + and mbinder_bound = Array.make (Array.length xs) false in + Array.iteri + (fun i (ki,_) -> Stdlib.(top_map := IntMap.add ki i !top_map)) xs; + let top_fvar key = + let p = Stdlib.(IntMap.find key !top_map) in + mbinder_bound.(p) <- true; Bvar (InSub p) in + (* Replace variables [x] in [xs] by de Bruijn index [fvar x] *) + let rec bind fvar t = + (*if Logger.log_enabled() then log "bind_mvar %d %a" i term t;*) + match unfold t with + | Vari (key,_) -> + if Stdlib.(IntMap.mem key !top_map) then fvar key else t + | Appl(a,b) -> + let a' = bind fvar a in + let b' = bind fvar b in + if a==a' && b==b' then t else Appl(a', b') + (* No need to call mk_Appl here as we only replace free variables by de + Bruijn indices. *) + | Abst(a,b) -> + let a' = bind fvar a in + let b' = bind_binder fvar b in + if a==a' && b==b' then t else Abst(a', b') + | Prod(a,b) -> + let a' = bind fvar a in + let b' = bind_binder fvar b in + if a==a' && b==b' then t else Prod(a', b') + | LLet(a,m,b) -> + let a' = bind fvar a in + let m' = bind fvar m in + let b' = bind_binder fvar b in + if a==a' && m==m' && b==b' then t else LLet(a', m', b') + | Meta(m,ts) -> + let ts' = Array.map (bind fvar) ts in + if Array.for_all2 (==) ts ts' then t else Meta(m, ts') + | Patt(j,n,ts) -> + let ts' = Array.map (bind fvar) ts in + if Array.for_all2 (==) ts ts' then t else Patt(j,n,ts') + | _ -> t + + and bind_binder fvar (bi,u,u_env as b) = + let open Stdlib in + let u_env' = Array.map (bind fvar) u_env in + let u_n = ref 0 in + let u_map = ref IntMap.empty in + let fvar' key = + match IntMap.find_opt key !u_map with + | Some p -> Bvar (InEnv p) + | None -> + let p' = Array.length u_env' + !u_n in + incr u_n; + u_map := IntMap.add key p' !u_map; + Bvar (InEnv p') in + let u' = bind fvar' u in + if u==u' && !u_n = 0 && Lplib.Array.for_all2 (==) u_env u_env' then b + else (* some vars of [xs] occur in u *) + let u_env' = Array.append u_env' (Array.make !u_n Wild) in + IntMap.iter (fun key p -> u_env'.(p) <- fvar key) !u_map; + (bi, u', u_env') in + + let b = bind top_fvar tm in + if Logger.log_enabled() then + log "bind_mvar %a %a = %a %a" + (D.array var) xs term tm pr_bound mbinder_bound term b; + let bi = { mbinder_name = Array.map base_name xs; mbinder_bound } in + bi, b, [||] + end + +(** Construction functions of the private type [term]. They ensure some + invariants: + +- In a commutative function symbol application, the first argument is smaller + than the second one wrt [cmp]. + +- In an associative and commutative function symbol application, the + application is built as a left or right comb depending on the associativity + of the symbol, and arguments are ordered in increasing order wrt [cmp]. + +- In [LLet(_,_,b)], [binder_occur b = true] (useless let's are erased). *) +let mk_Vari x = Vari x +let mk_Type = Type +let mk_Kind = Kind +let mk_Symb x = Symb x +let mk_Prod (a,b) = Prod (a,b) +let mk_Arro (a,b) = let x = new_var "_" in Prod(a, bind_var x b) +let mk_Abst (a,b) = Abst (a,b) +let mk_Meta (m,ts) = (*assert (m.meta_arity = Array.length ts);*) Meta (m,ts) +let mk_Patt (i,s,ts) = Patt (i,s,ts) +let mk_Wild = Wild +let mk_Plac b = Plac b +let mk_TRef x = TRef x +let mk_LLet (a,t,b) = LLet (a,t,b) + +(** [mk_Appl_not_canonical t u] builds the non-canonical (wrt. C and AC + symbols) application of [t] to [u]. WARNING: to use only in Sign.link. *) +let mk_Appl_not_canonical : term * term -> term = fun (t, u) -> Appl(t, u) + +(** [add_args t args] builds the application of the {!type:term} [t] to a list + arguments [args]. When [args] is empty, the returned value is (physically) + equal to [t]. *) +let add_args : term -> term list -> term = fun t ts -> + match get_args t with + | Symb s, _ when is_modulo s -> + List.fold_left (fun t u -> mk_Appl(t,u)) t ts + | _ -> List.fold_left (fun t u -> Appl(t,u)) t ts + +(** [add_args_map t f ts] is equivalent to [add_args t (List.map f ts)] but + more efficient. *) +let add_args_map : term -> (term -> term) -> term list -> term = fun t f ts -> + match get_args t with + | Symb s, _ when is_modulo s -> + List.fold_left (fun t u -> mk_Appl(t, f u)) t ts + | _ -> List.fold_left (fun t u -> Appl(t, f u)) t ts + +(** Patt substitution. *) +let subst_patt : mbinder option array -> term -> term = fun env -> + let rec subst_patt t = + match unfold t with + | Patt(Some i,n,ts) when 0 <= i && i < Array.length env -> + begin match env.(i) with + | Some b -> msubst b (Array.map subst_patt ts) + | None -> mk_Patt(Some i,n,Array.map subst_patt ts) + end + | Patt(i,n,ts) -> mk_Patt(i, n, Array.map subst_patt ts) + | Prod(a,(n,b,e)) -> + mk_Prod(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) + | Abst(a,(n,b,e)) -> + mk_Abst(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) + | Appl(a,b) -> mk_Appl(subst_patt a, subst_patt b) + | Meta(m,ts) -> mk_Meta(m, Array.map subst_patt ts) + | LLet(a,t,(n,b,e)) -> + mk_LLet(subst_patt a, subst_patt t, + (n, subst_patt b, Array.map subst_patt e)) + | Wild + | Plac _ + | TRef _ + | Bvar _ + | Vari _ + | Type + | Kind + | Symb _ -> t + in subst_patt + +(** [cleanup t] unfold all metas and TRef's in [t]. *) +let rec cleanup : term -> term = fun t -> + match unfold t with + | Patt(i,n,ts) -> mk_Patt(i, n, Array.map cleanup ts) + | Prod(a,b) -> mk_Prod(cleanup a, binder cleanup b) + | Abst(a,b) -> mk_Abst(cleanup a, binder cleanup b) + | Appl(a,b) -> mk_Appl(cleanup a, cleanup b) + | Meta(m,ts) -> mk_Meta(m, Array.map cleanup ts) + | LLet(a,t,b) -> mk_LLet(cleanup a, cleanup t, binder cleanup b) + | Wild -> assert false + | Plac _ -> assert false + | TRef _ -> assert false + | Bvar _ -> assert false + | Vari _ + | Type + | Kind + | Symb _ -> t + +(** Type of a symbol and a rule. *) +type sym_rule = sym * rule + +let lhs : sym_rule -> term = fun (s, r) -> add_args (mk_Symb s) r.lhs +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 + +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 + first). *) +type ctxt = (var * term * term option) list + +let decl ppf (v,a,d) = + out ppf "%a: %a" var v term a; + match d with + | None -> () + | Some d -> out ppf " ≔ %a" term d + +let ctxt : ctxt pp = fun ppf c -> List.pp decl ", " ppf (List.rev c) + +(** Type of unification constraints. *) +type constr = ctxt * term * term + +(** Representation of unification problems. *) +type problem_aux = + { to_solve : constr list + (** List of unification problems to solve. *) + ; unsolved : constr list + (** List of unification problems that could not be solved. *) + ; recompute : bool + (** Indicates whether unsolved problems should be rechecked. *) + ; metas : MetaSet.t + (** Set of unsolved metas. *) } + +type problem = problem_aux Timed.ref + +(** Create a new empty problem. *) +let new_problem : unit -> problem = fun () -> + Timed.ref + {to_solve = []; unsolved = []; recompute = false; metas = MetaSet.empty} + +(** Printing functions for debug. *) +module Raw = struct + let sym = sym let _ = sym + let term = term let _ = term + let ctxt = ctxt let _ = ctxt +end +(* +let rec to_term_serializable t = match t with + | Vari x -> Ser_Vari x + | Bvar x -> Ser_Bvar x + | Type -> Ser_Type + | Kind -> Ser_Kind + | Symb x -> Ser_Symb x + | Prod (x, y) -> Ser_Prod (to_term_serializable x, to_binder_serializable y) + | Abst (x, y) -> Ser_Abst (to_term_serializable x, to_binder_serializable y) + | Appl (x, y) -> Ser_Appl (to_term_serializable x, to_term_serializable y) + | Meta (x, y) -> Ser_Meta (x, Array.map to_term_serializable y) + | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) + | Wild -> Ser_Wild + | Plac x -> Ser_Plac x + | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x) ) + (* | TRef x -> Ser_TRef (match Timed.(!) x with None -> None | Some x -> Some (to_term_serializable x)) *) + | LLet (x, y, z) -> Ser_LLet (to_term_serializable x, to_term_serializable y, to_binder_serializable z) +and to_binder_serializable (x, y, z) = + (x, to_term_serializable y, Array.map to_term_serializable z) +let rec of_term_serializable t = match t with + | Ser_Vari x -> Vari x + | Ser_Bvar x -> Bvar x + | Ser_Type -> Type + | Ser_Kind -> Kind + | Ser_Symb x -> Symb x + | Ser_Prod (x, y) -> Prod (of_term_serializable x, of_binder_serializable y) + | Ser_Abst (x, y) -> Abst (of_term_serializable x, of_binder_serializable y) + | Ser_Appl (x, y) -> Appl (of_term_serializable x, of_term_serializable y) + | Ser_Meta (x, y) -> Meta (x, Array.map of_term_serializable y) + | Ser_Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) + | Ser_Wild -> Wild + | Ser_Plac x -> Plac x + | Ser_TRef x -> TRef (Timed.ref (Option.map of_term_serializable x)) + | Ser_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) + *) + +type sym_serializable = + { ser_sym_expo : expo + ; ser_sym_path : Path.t + ; ser_sym_name : string + (* ; ser_sym_type : term_serializable *) + (* ; ser_sym_impl : bool list *) + (* ; ser_sym_prop : prop *) + (* ; ser_sym_nota : float notation Timed.ref *) + (* ; ser_sym_def : term option Timed.ref *) + (* ; ser_sym_opaq : bool Timed.ref *) + (* ; ser_sym_rules : rule list Timed.ref *) + (* ; ser_sym_mstrat: match_strat *) + (* ; ser_sym_dtree : dtree Timed.ref *) + (* ; ser_sym_pos : Pos.popt *) + (* ; ser_sym_decl_pos : Pos.popt *) + } [@@deriving yojson] + + let to_sym_serializable s = + { + ser_sym_expo = s.sym_expo + ; ser_sym_path = s.sym_path + ; ser_sym_name = s.sym_name + (* ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) *) + } + let of_sym_serializable s = + { + sym_expo = s.ser_sym_expo + ; sym_path = s.ser_sym_path + ; sym_name = s.ser_sym_name + ; sym_type = Timed.ref Type + (* ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) *) + ; sym_impl = [] (*FIX ME*) + ; sym_prop = Defin (*FIX ME*) + ; sym_nota = Timed.ref NoNotation (*FIX ME*) + ; sym_def = Timed.ref None (*FIX ME*) + ; sym_opaq = Timed.ref true (*FIX ME*) + ; sym_rules = Timed.ref [] (*FIX ME*) + ; sym_mstrat = Sequen (*FIX ME*) + ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) + ; sym_pos = None (*FIX ME*) + ; sym_decl_pos = None (*FIX ME*) + } + + let sym_to_yojson s = + sym_serializable_to_yojson (to_sym_serializable s) + + let sym_of_yojson j = + match (sym_serializable_of_yojson j) with + | Ok j -> Ok (of_sym_serializable j) + | Error s -> Error s + let sym_dump = + { + sym_expo = Privat + ; sym_path = [] + ; sym_name = "" + ; sym_type = Timed.ref Type + ; sym_impl = [] + ; sym_prop = Defin + ; sym_nota = Timed.ref NoNotation + ; sym_def = Timed.ref None + ; sym_opaq = Timed.ref true + ; sym_rules = Timed.ref [] + ; sym_mstrat = Sequen + ; sym_dtree = Timed.ref Tree_type.empty_dtree + ; sym_pos = None + ; sym_decl_pos = None + } \ No newline at end of file diff --git a/src/core/term.mli b/src/core/term.mli index 2489fd8dc..8c7a54a50 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -466,11 +466,41 @@ module Raw : sig val ctxt : ctxt pp end -type sym_serializable = + +type term_serializable = + | Ser_Vari of var + | Ser_Bvar of bvar + | Ser_Type + | Ser_Kind + | Ser_Symb of sym_serializable + | Ser_Prod of term_serializable * binder_serializable + | Ser_Abst of term_serializable * binder_serializable + | Ser_Appl of term_serializable * term_serializable + | Ser_Meta of meta_serializable * term_serializable array + | Ser_Patt of int option * string * term_serializable array + | Ser_Wild + | Ser_Plac of bool + | Ser_TRef of term_serializable option + | Ser_LLet of term_serializable * term_serializable * binder_serializable + +and mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} + +and binder_info = {binder_name : string; binder_bound : bool} +and binder_serializable = binder_info * term_serializable * term_serializable array + +and meta_serializable = + { ser_meta_key : int + ; ser_meta_type : term_serializable (**Timed.ref. *) + ; ser_meta_arity : int + ; ser_meta_value : mbinder_serializable option (** Timed.ref. *) } + +and mbinder_serializable = mbinder_info * term_serializable * term_serializable array + +and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t ; ser_sym_name : string - (* ; ser_sym_type : term Timed.ref *) + ; ser_sym_type : term_serializable (* ; ser_sym_impl : bool list *) (* ; ser_sym_prop : prop *) (* ; ser_sym_nota : float notation Timed.ref *) From a2ae95e5e77b731b9933eff396b32f3f59210ef5 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 7 Apr 2026 16:25:53 +0200 Subject: [PATCH 06/26] with sym_impl and sym_prop --- src/core/term.ml | 11 +++++++---- src/core/term.mli | 4 ++-- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index 7a5120c16..1fde3d28b 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -37,6 +37,7 @@ 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} [@@deriving yojson] @@ -1007,8 +1008,8 @@ and sym_serializable = ; ser_sym_path : Path.t ; ser_sym_name : string ; ser_sym_type : term_serializable - (* ; ser_sym_impl : bool list *) - (* ; ser_sym_prop : prop *) + ; ser_sym_impl : bool list + ; ser_sym_prop : prop (* ; ser_sym_nota : float notation Timed.ref *) (* ; ser_sym_def : term option Timed.ref *) (* ; ser_sym_opaq : bool Timed.ref *) @@ -1055,6 +1056,8 @@ and to_sym_serializable s = ; ser_sym_path = s.sym_path ; ser_sym_name = s.sym_name ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) + ; ser_sym_impl = s.sym_impl + ; ser_sym_prop = s.sym_prop } let rec of_term_serializable t = match t with | Ser_Vari x -> Vari x @@ -1090,8 +1093,8 @@ and of_sym_serializable s = ; sym_path = s.ser_sym_path ; sym_name = s.ser_sym_name ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) - ; sym_impl = [] (*FIX ME*) - ; sym_prop = Defin (*FIX ME*) + ; sym_impl = s.ser_sym_impl + ; sym_prop = s.ser_sym_prop ; sym_nota = Timed.ref NoNotation (*FIX ME*) ; sym_def = Timed.ref None (*FIX ME*) ; sym_opaq = Timed.ref true (*FIX ME*) diff --git a/src/core/term.mli b/src/core/term.mli index 8c7a54a50..f5baa8287 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -501,8 +501,8 @@ and sym_serializable = ; ser_sym_path : Path.t ; ser_sym_name : string ; ser_sym_type : term_serializable - (* ; ser_sym_impl : bool list *) - (* ; ser_sym_prop : prop *) + ; ser_sym_impl : bool list + ; ser_sym_prop : prop (* ; ser_sym_nota : float notation Timed.ref *) (* ; ser_sym_def : term option Timed.ref *) (* ; ser_sym_opaq : bool Timed.ref *) From edc18e1f6a5ec48addddef6ca89d83ca3df6cc45 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 7 Apr 2026 16:56:38 +0200 Subject: [PATCH 07/26] with sym_nota in in sym in sign --- src/core/term.ml | 21 +++++++++++++++------ src/core/term.mli | 2 +- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index 1fde3d28b..58c543198 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -89,12 +89,22 @@ 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 @@ -104,7 +114,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 @@ -1010,7 +1020,7 @@ and sym_serializable = ; ser_sym_type : term_serializable ; ser_sym_impl : bool list ; ser_sym_prop : prop - (* ; ser_sym_nota : float notation Timed.ref *) + ; ser_sym_nota : float notation (*Timed.ref*) (* ; ser_sym_def : term option Timed.ref *) (* ; ser_sym_opaq : bool Timed.ref *) (* ; ser_sym_rules : rule list Timed.ref *) @@ -1048,8 +1058,6 @@ and to_meta_serializable t = and to_mbinder_serializable (x, y ,z) = (x, to_term_serializable y, Array.map to_term_serializable z) - - and to_sym_serializable s = { ser_sym_expo = s.sym_expo @@ -1058,6 +1066,7 @@ and to_sym_serializable s = ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) ; ser_sym_impl = s.sym_impl ; ser_sym_prop = s.sym_prop + ; ser_sym_nota = Timed.(!)s.sym_nota } let rec of_term_serializable t = match t with | Ser_Vari x -> Vari x @@ -1095,7 +1104,7 @@ and of_sym_serializable s = ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) ; sym_impl = s.ser_sym_impl ; sym_prop = s.ser_sym_prop - ; sym_nota = Timed.ref NoNotation (*FIX ME*) + ; sym_nota = Timed.ref s.ser_sym_nota (*FIX ME*) ; sym_def = Timed.ref None (*FIX ME*) ; sym_opaq = Timed.ref true (*FIX ME*) ; sym_rules = Timed.ref [] (*FIX ME*) diff --git a/src/core/term.mli b/src/core/term.mli index f5baa8287..f10db372d 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -503,7 +503,7 @@ and sym_serializable = ; ser_sym_type : term_serializable ; ser_sym_impl : bool list ; ser_sym_prop : prop - (* ; ser_sym_nota : float notation Timed.ref *) + ; ser_sym_nota : float notation (*Timed.ref*) (* ; ser_sym_def : term option Timed.ref *) (* ; ser_sym_opaq : bool Timed.ref *) (* ; ser_sym_rules : rule list Timed.ref *) From 2ec32a27ec86b239acae4fd2d9dad0985484f10a Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 7 Apr 2026 17:51:37 +0200 Subject: [PATCH 08/26] with sym_rule in in sym in sign --- src/common/pos.ml | 4 ++-- src/core/term.ml | 53 ++++++++++++++++++++++++++++++++++++++++------- src/core/term.mli | 17 ++++++++++++--- 3 files changed, 61 insertions(+), 13 deletions(-) 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/term.ml b/src/core/term.ml index 58c543198..d6aa59f3c 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -1013,6 +1013,17 @@ and meta_serializable = and mbinder_serializable = mbinder_info * term_serializable * term_serializable array [@@deriving yojson] +and rule_serializable = + { ser_lhs : term_serializable list + ; ser_names : string array + ; ser_rhs : term_serializable + ; ser_arity : int + ; ser_arities : int array + ; ser_vars_nb : int + ; ser_xvars_nb : int + ; ser_rule_pos : Pos.popt + }[@@deriving yojson] + and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t @@ -1021,9 +1032,9 @@ and sym_serializable = ; ser_sym_impl : bool list ; ser_sym_prop : prop ; ser_sym_nota : float notation (*Timed.ref*) - (* ; ser_sym_def : term option Timed.ref *) - (* ; ser_sym_opaq : bool Timed.ref *) - (* ; ser_sym_rules : rule list Timed.ref *) + ; ser_sym_def : term_serializable option (*Timed.ref*) + ; ser_sym_opaq : bool (*Timed.ref*) + ; ser_sym_rules : rule_serializable list (* Timed.ref *) (* ; ser_sym_mstrat: match_strat *) (* ; ser_sym_dtree : dtree Timed.ref *) (* ; ser_sym_pos : Pos.popt *) @@ -1067,6 +1078,21 @@ and to_sym_serializable s = ; ser_sym_impl = s.sym_impl ; ser_sym_prop = s.sym_prop ; ser_sym_nota = Timed.(!)s.sym_nota + ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) + ; ser_sym_opaq = Timed.(!)s.sym_opaq + ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + } + +and to_rule_serializable (r : rule) : rule_serializable = + { + ser_lhs = List.map to_term_serializable r.lhs; + ser_names = r.names; + ser_rhs = to_term_serializable r.rhs; + ser_arity = r.arity; + ser_arities = r.arities; + ser_vars_nb = r.vars_nb; + ser_xvars_nb = r.xvars_nb; + ser_rule_pos = r.rule_pos; } let rec of_term_serializable t = match t with | Ser_Vari x -> Vari x @@ -1095,7 +1121,6 @@ and of_meta_serializable t = and of_mbinder_serializable (x, y ,z) = (x, of_term_serializable y, Array.map of_term_serializable z) - and of_sym_serializable s = { sym_expo = s.ser_sym_expo @@ -1104,16 +1129,28 @@ and of_sym_serializable s = ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) ; sym_impl = s.ser_sym_impl ; sym_prop = s.ser_sym_prop - ; sym_nota = Timed.ref s.ser_sym_nota (*FIX ME*) - ; sym_def = Timed.ref None (*FIX ME*) - ; sym_opaq = Timed.ref true (*FIX ME*) - ; sym_rules = Timed.ref [] (*FIX ME*) + ; sym_nota = Timed.ref s.ser_sym_nota + ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) + ; sym_opaq = Timed.ref s.ser_sym_opaq + ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) ; sym_mstrat = Sequen (*FIX ME*) ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) ; sym_pos = None (*FIX ME*) ; sym_decl_pos = None (*FIX ME*) } + and of_rule_serializable (r : rule_serializable) : rule = + { + lhs = List.map of_term_serializable r.ser_lhs; + names = r.ser_names; + rhs = of_term_serializable r.ser_rhs; + arity = r.ser_arity; + arities = r.ser_arities; + vars_nb = r.ser_vars_nb; + xvars_nb = r.ser_xvars_nb; + rule_pos = r.ser_rule_pos; + } + let sym_to_yojson s = sym_serializable_to_yojson (to_sym_serializable s) diff --git a/src/core/term.mli b/src/core/term.mli index f10db372d..aa3a94a29 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -496,6 +496,17 @@ and meta_serializable = and mbinder_serializable = mbinder_info * term_serializable * term_serializable array +and rule_serializable = + { ser_lhs : term_serializable list + ; ser_names : string array + ; ser_rhs : term_serializable + ; ser_arity : int + ; ser_arities : int array + ; ser_vars_nb : int + ; ser_xvars_nb : int + ; ser_rule_pos : Pos.popt + } + and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t @@ -504,9 +515,9 @@ and sym_serializable = ; ser_sym_impl : bool list ; ser_sym_prop : prop ; ser_sym_nota : float notation (*Timed.ref*) - (* ; ser_sym_def : term option Timed.ref *) - (* ; ser_sym_opaq : bool Timed.ref *) - (* ; ser_sym_rules : rule list Timed.ref *) + ; ser_sym_def : term_serializable option (* Timed.ref *) + ; ser_sym_opaq : bool (* Timed.ref *) + ; ser_sym_rules : rule_serializable list (* Timed.ref*) (* ; ser_sym_mstrat: match_strat *) (* ; ser_sym_dtree : dtree Timed.ref *) (* ; ser_sym_pos : Pos.popt *) From ad22779995369d731fec21132cac8b26aecf0eea Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 8 Apr 2026 10:25:17 +0200 Subject: [PATCH 09/26] with ser_sym_mstrat in in sym in sign --- src/core/term.ml | 6 ++++-- src/core/term.mli | 4 ++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index d6aa59f3c..b76ecd447 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -22,6 +22,7 @@ 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 = @@ -1035,7 +1036,7 @@ and sym_serializable = ; ser_sym_def : term_serializable option (*Timed.ref*) ; ser_sym_opaq : bool (*Timed.ref*) ; ser_sym_rules : rule_serializable list (* Timed.ref *) - (* ; ser_sym_mstrat: match_strat *) + ; ser_sym_mstrat: match_strat (* ; ser_sym_dtree : dtree Timed.ref *) (* ; ser_sym_pos : Pos.popt *) (* ; ser_sym_decl_pos : Pos.popt *) @@ -1081,6 +1082,7 @@ and to_sym_serializable s = ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) ; ser_sym_opaq = Timed.(!)s.sym_opaq ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + ; ser_sym_mstrat = s.sym_mstrat } and to_rule_serializable (r : rule) : rule_serializable = @@ -1133,7 +1135,7 @@ and of_sym_serializable s = ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) ; sym_opaq = Timed.ref s.ser_sym_opaq ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) - ; sym_mstrat = Sequen (*FIX ME*) + ; sym_mstrat = s.ser_sym_mstrat ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) ; sym_pos = None (*FIX ME*) ; sym_decl_pos = None (*FIX ME*) diff --git a/src/core/term.mli b/src/core/term.mli index aa3a94a29..093e6b0e4 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -506,7 +506,7 @@ and rule_serializable = ; ser_xvars_nb : int ; ser_rule_pos : Pos.popt } - + and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t @@ -518,7 +518,7 @@ and sym_serializable = ; ser_sym_def : term_serializable option (* Timed.ref *) ; ser_sym_opaq : bool (* Timed.ref *) ; ser_sym_rules : rule_serializable list (* Timed.ref*) - (* ; ser_sym_mstrat: match_strat *) + ; ser_sym_mstrat: match_strat (* ; ser_sym_dtree : dtree Timed.ref *) (* ; ser_sym_pos : Pos.popt *) (* ; ser_sym_decl_pos : Pos.popt *) From d4eaa717275d9879131a2fcf6d9e005d99dbde3c Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Thu, 9 Apr 2026 10:43:53 +0200 Subject: [PATCH 10/26] with sym_dtree in in sym in sign --- src/core/term.ml | 34 +++++++----- src/core/term.mli | 5 +- src/core/tree_type.ml | 122 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 146 insertions(+), 15 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index b76ecd447..2cac3a7f8 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -1025,6 +1025,8 @@ and rule_serializable = ; ser_rule_pos : Pos.popt }[@@deriving yojson] +and dtree_serializable = rule_serializable Tree_type.dtree_serializable [@@deriving yojson] + and sym_serializable = { ser_sym_expo : expo ; ser_sym_path : Path.t @@ -1037,7 +1039,7 @@ and sym_serializable = ; ser_sym_opaq : bool (*Timed.ref*) ; ser_sym_rules : rule_serializable list (* Timed.ref *) ; ser_sym_mstrat: match_strat - (* ; ser_sym_dtree : dtree Timed.ref *) + ; ser_sym_dtree : dtree_serializable (* Timed.ref *) (* ; ser_sym_pos : Pos.popt *) (* ; ser_sym_decl_pos : Pos.popt *) } [@@deriving yojson] @@ -1058,6 +1060,8 @@ let rec to_term_serializable t = match t with | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x) ) (* | TRef x -> Ser_TRef (match Timed.(!) x with None -> None | Some x -> Some (to_term_serializable x)) *) | LLet (x, y, z) -> Ser_LLet (to_term_serializable x, to_term_serializable y, to_binder_serializable z) + +and to_dtree_serializable d = Tree_type.to_dtree_serializable (fun x -> to_rule_serializable x) d and to_binder_serializable (x, y, z) = (x, to_term_serializable y, Array.map to_term_serializable z) @@ -1072,17 +1076,18 @@ and to_mbinder_serializable (x, y ,z) = and to_sym_serializable s = { - ser_sym_expo = s.sym_expo - ; ser_sym_path = s.sym_path - ; ser_sym_name = s.sym_name - ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) - ; ser_sym_impl = s.sym_impl - ; ser_sym_prop = s.sym_prop - ; ser_sym_nota = Timed.(!)s.sym_nota - ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) - ; ser_sym_opaq = Timed.(!)s.sym_opaq - ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) - ; ser_sym_mstrat = s.sym_mstrat + ser_sym_expo = s.sym_expo + ; ser_sym_path = s.sym_path + ; ser_sym_name = s.sym_name + ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) + ; ser_sym_impl = s.sym_impl + ; ser_sym_prop = s.sym_prop + ; ser_sym_nota = Timed.(!)s.sym_nota + ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) + ; ser_sym_opaq = Timed.(!)s.sym_opaq + ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + ; ser_sym_mstrat = s.sym_mstrat + ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) } and to_rule_serializable (r : rule) : rule_serializable = @@ -1111,6 +1116,9 @@ let rec of_term_serializable t = match t with | Ser_Plac x -> Plac x | Ser_TRef x -> TRef (Timed.ref (Option.map of_term_serializable x)) | Ser_LLet (x, y, z) -> LLet (of_term_serializable x, of_term_serializable y, of_binder_serializable z) + +and of_dtree_serializable d = Tree_type.of_dtree_serializable of_rule_serializable d + and of_binder_serializable (x, y, z) = (x, of_term_serializable y, Array.map of_term_serializable z) @@ -1136,7 +1144,7 @@ and of_sym_serializable s = ; sym_opaq = Timed.ref s.ser_sym_opaq ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) ; sym_mstrat = s.ser_sym_mstrat - ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) + ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) ; sym_pos = None (*FIX ME*) ; sym_decl_pos = None (*FIX ME*) } diff --git a/src/core/term.mli b/src/core/term.mli index 093e6b0e4..c5a39d1ef 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -519,11 +519,14 @@ and sym_serializable = ; ser_sym_opaq : bool (* Timed.ref *) ; ser_sym_rules : rule_serializable list (* Timed.ref*) ; ser_sym_mstrat: match_strat - (* ; ser_sym_dtree : dtree Timed.ref *) + ; ser_sym_dtree : dtree_serializable (* ; ser_sym_pos : Pos.popt *) (* ; ser_sym_decl_pos : Pos.popt *) } +and dtree_serializable = rule_serializable Tree_type.dtree_serializable + + val sym_dump : sym val sym_to_yojson : sym -> Yojson.Safe.t val sym_of_yojson : Yojson.Safe.t -> (sym, string) result \ No newline at end of file diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index 5b8a439ee..3286a2544 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,124 @@ 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) From edcbb355dab880f77c6c1ddd3b6a56a2c980eb3b Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Thu, 9 Apr 2026 11:00:46 +0200 Subject: [PATCH 11/26] with sym_symbols serialised in sign --- src/core/sign.ml | 14 +- src/core/term.ml | 81 +-- src/core/term.ml.back | 1114 ----------------------------------------- src/core/term.mli | 4 +- 4 files changed, 54 insertions(+), 1159 deletions(-) delete mode 100644 src/core/term.ml.back diff --git a/src/core/sign.ml b/src/core/sign.ml index 6b961e703..360ac301d 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -478,17 +478,8 @@ let rec dependencies : t -> (Path.t * t) list = fun sign -> in List.concat (minimize [] deps) -let dump = - { - sign_symbols = ref StrMap.empty - ; sign_path = ["/tmp/test_sign_read_write.lpo"] - ; sign_deps = ref Path.Map.empty - ; sign_builtins = ref StrMap.empty - ; sign_ind = ref SymMap.empty - ; sign_cp_pos = ref SymMap.empty } - let%test "rev" = - let sign = dump in + let sign = Ghost.sign in let symbols = Timed.(!) sign.sign_symbols in let symbols = StrMap.add "" { @@ -506,8 +497,7 @@ let%test "rev" = (fun a b -> (Sym.compare a b) = 0 (* Should compare : *) - (* a.sym_name = b.sym_name - && a.sym_expo = b.sym_expo + (* a.sym_expo = b.sym_expo && (Path.compare a.sym_path b.sym_path = 0) && (a.sym_name = b.sym_name) *) ) diff --git a/src/core/term.ml b/src/core/term.ml index 2cac3a7f8..e3feef9c8 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -1040,8 +1040,8 @@ and sym_serializable = ; ser_sym_rules : rule_serializable list (* Timed.ref *) ; ser_sym_mstrat: match_strat ; ser_sym_dtree : dtree_serializable (* Timed.ref *) - (* ; ser_sym_pos : Pos.popt *) - (* ; ser_sym_decl_pos : Pos.popt *) + ; ser_sym_pos : Pos.popt + ; ser_sym_decl_pos : Pos.popt } [@@deriving yojson] let rec to_term_serializable t = match t with @@ -1076,18 +1076,20 @@ and to_mbinder_serializable (x, y ,z) = and to_sym_serializable s = { - ser_sym_expo = s.sym_expo - ; ser_sym_path = s.sym_path - ; ser_sym_name = s.sym_name - ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) - ; ser_sym_impl = s.sym_impl - ; ser_sym_prop = s.sym_prop - ; ser_sym_nota = Timed.(!)s.sym_nota - ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) - ; ser_sym_opaq = Timed.(!)s.sym_opaq - ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) - ; ser_sym_mstrat = s.sym_mstrat - ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) + ser_sym_expo = s.sym_expo + ; ser_sym_path = s.sym_path + ; ser_sym_name = s.sym_name + ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) + ; ser_sym_impl = s.sym_impl + ; ser_sym_prop = s.sym_prop + ; ser_sym_nota = Timed.(!)s.sym_nota + ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) + ; ser_sym_opaq = Timed.(!)s.sym_opaq + ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + ; ser_sym_mstrat = s.sym_mstrat + ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) + ; ser_sym_pos = s.sym_pos + ; ser_sym_decl_pos = s.sym_decl_pos } and to_rule_serializable (r : rule) : rule_serializable = @@ -1134,19 +1136,19 @@ and of_mbinder_serializable (x, y ,z) = and of_sym_serializable s = { sym_expo = s.ser_sym_expo - ; sym_path = s.ser_sym_path - ; sym_name = s.ser_sym_name - ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) - ; sym_impl = s.ser_sym_impl - ; sym_prop = s.ser_sym_prop - ; sym_nota = Timed.ref s.ser_sym_nota - ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) - ; sym_opaq = Timed.ref s.ser_sym_opaq - ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) - ; sym_mstrat = s.ser_sym_mstrat - ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) - ; sym_pos = None (*FIX ME*) - ; sym_decl_pos = None (*FIX ME*) + ; sym_path = s.ser_sym_path + ; sym_name = s.ser_sym_name + ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) + ; sym_impl = s.ser_sym_impl + ; sym_prop = s.ser_sym_prop + ; sym_nota = Timed.ref s.ser_sym_nota + ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) + ; sym_opaq = Timed.ref s.ser_sym_opaq + ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) + ; sym_mstrat = s.ser_sym_mstrat + ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) + ; sym_pos = s.ser_sym_pos + ; sym_decl_pos = s.ser_sym_decl_pos } and of_rule_serializable (r : rule_serializable) : rule = @@ -1174,14 +1176,31 @@ and of_sym_serializable s = ; sym_path = [] ; sym_name = "" ; sym_type = Timed.ref Type - ; sym_impl = [] + ; sym_impl = [true; false] ; sym_prop = Defin ; sym_nota = Timed.ref NoNotation - ; sym_def = Timed.ref None + ; 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 = None - ; sym_decl_pos = None + ; 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 + } + } \ No newline at end of file diff --git a/src/core/term.ml.back b/src/core/term.ml.back deleted file mode 100644 index 43fe81b4e..000000000 --- a/src/core/term.ml.back +++ /dev/null @@ -1,1114 +0,0 @@ -(** Internal representation of terms. - - This module contains the definition of the internal representation of - terms, together with smart constructors and low level operation. *) - -open Lplib open Base open Extra -open Common open Debug - -let log = Logger.make 'm' "term" "term building" -let log = log.pp - -(** {3 Term (and symbol) representation} *) - -(** Representation of a possibly qualified identifier. *) -type qident = Path.t * string - -(** Pattern-matching strategy modifiers. *) -type match_strat = - | Sequen - (** Rules are processed sequentially: a rule can be applied only if the - previous ones (in the order of declaration) cannot be. *) - | 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. *) - -(** 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. *) - | Const (** Constant. *) - | Injec (** Injective. *) - | Commu (** Commutative. *) - | Assoc of bool (** Associative left if [true], right if [false]. *) - | AC of bool (** Associative and commutative. *) - -(** Data of a binder. *) -type binder_info = {binder_name : string; binder_bound : bool} [@@deriving yojson] -type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} - -let pr_bound = D.array (fun ppf b -> if b then out ppf "*" else out ppf "_") - -(** Type for free variables. *) -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]. *) -let compare_vars : var -> var -> int = fun (i,_) (j,_) -> Stdlib.compare i j - -(** [eq_vars x y] safely computes the equality of [x] and [y]. Note that it is - unsafe to compare variables with the polymorphic equality function. *) -let eq_vars : var -> var -> bool = fun x y -> compare_vars x y = 0 - -(** [new_var name] creates a new unique variable of name [name]. *) -let new_var : string -> var = - let n = Stdlib.ref 0 in fun name -> incr n; !n, name - -(** [new_var_ind s i] creates a new [var] of name [s ^ string_of_int i]. *) -let new_var_ind : string -> int -> var = fun s i -> - new_var (Escape.add_prefix s (string_of_int i)) - -(** [base_name x] returns the base name of variable [x]. Note that this name - is not unique: two distinct variables may have the same name. *) -let base_name : var -> string = fun (_i,n) -> n - -(** [uniq_name x] returns a string uniquely identifying the variable [x]. *) -let uniq_name : var -> string = fun (i,_) -> "v" ^ string_of_int i - -(** Sets and maps of variables. *) -module Var = struct - type t = var - let compare = compare_vars -end - -module VarSet = Set.Make(Var) -module VarMap = Map.Make(Var) - -(* Type for bound variables. [InSub i] refers to the i-th slot in the - 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 [@@deriving yojson] - -(** The priority of an infix operator is a floating-point number. *) -type priority = float - -(** Notations. *) -type 'a notation = - | NoNotation - | Prefix of 'a - | Postfix of 'a - | Infix of Pratter.associativity * 'a - | Zero - | Succ of 'a notation (* NoNotation, Prefix or Postfix only *) - | Quant - | PosOne - | PosDouble - | PosSuccDouble - | IntZero - | IntPos - | IntNeg - -(** 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 - are considered invalid in unrelated code. - - Bound variables [Bvar] never appear outside of the current module. They - correspond to the variables bound by a binder above. They are replaced by - [Vari] whenever the binder is destructed (via unbind and the like) - *) -type term = - | Vari of var (** Free variable. *) - | Bvar of bvar (** Bound variables. Only used internally. *) - | Type (** "TYPE" constant. *) - | Kind (** "KIND" constant. *) - | Symb of sym (** User-defined symbol. *) - | Prod of term * binder (** Dependent product. *) - | Abst of term * binder (** Abstraction. *) - | Appl of term * term (** Term application. *) - | Meta of meta * term array (** Metavariable application. *) - | Patt of int option * string * term array - (** Pattern variable application (only used in rewriting rules). *) - | Wild (** Wildcard (only used for surface matching, never in LHS). *) - | Plac of bool - (** [Plac b] is a placeholder, or hole, for not given terms. Boolean [b] is - true if the placeholder stands for a type. *) - | TRef of term option Timed.ref - (** Reference cell (used in surface matching, and evaluation with - sharing). *) - | LLet of term * term * binder - (** [LLet(a, t, u)] is [let x : a ≔ t in u] (with [x] bound in [u]). *) - -(* and term_serializable = string - | Ser_Vari of var - | Ser_Bvar of bvar - | Ser_Type - | Ser_Kind - | Ser_Symb of sym - | Ser_Prod of term_serializable * binder_serializable - | Ser_Abst of term_serializable * binder_serializable - | Ser_Appl of term_serializable * term_serializable - | Ser_Meta of meta * term_serializable array - | Ser_Patt of int option * string * term_serializable array - | Ser_Wild - | Ser_Plac of bool - | Ser_TRef of term_serializable option - | Ser_LLet of term_serializable * term_serializable * binder_serializable -[@@deriving yojson] *) - -(** 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 binder_serializable = binder_info * term_serializable * term_serializable [@@deriving yojson] *) -and mbinder = mbinder_info * term * term array - -(** {b NOTE} that a wildcard "_" of the concrete (source code) syntax may have - a different representation depending on the context. For instance, the - {!constructor:Wild} constructor is only used when matching patterns (e.g., - with the "rewrite" tactic). In the LHS of a rewriting {!type:rule}, we use - the {!constructor:Patt} constructor to represend wildcards of the concrete - syntax. They are thus considered to be fresh, unused pattern variables. *) - -(** Representation of a decision tree (used for rewriting). *) -and dtree = rule Tree_type.dtree - -(** Representation of a user-defined symbol. *) -and sym = - { sym_expo : expo (** Visibility. *) - ; sym_path : Path.t (** Module in which the symbol is defined. *) - ; sym_name : string (** Name. *) - ; sym_type : term Timed.ref (** Type. *) - ; sym_impl : bool list (** Implicit arguments ([true] meaning implicit). *) - ; sym_prop : prop (** Property. *) - ; sym_nota : float notation Timed.ref (** Notation. *) - ; sym_def : term option Timed.ref (** Definition with ≔. *) - ; sym_opaq : bool Timed.ref (** Opacity. *) - ; sym_rules : rule list Timed.ref (** Rewriting rules. *) - ; sym_mstrat: match_strat (** Matching strategy. *) - ; sym_dtree : dtree Timed.ref (** Decision tree used for matching. *) - ; sym_pos : Pos.popt (** Position in source file of symbol name. *) - ; sym_decl_pos : Pos.popt (** Position in source file of symbol declaration - without its definition. *) } - -(** {b NOTE} {!field:sym_type} holds a (timed) reference for a technical - reason related to the writing of signatures as binary files (in relation - to {!val:Sign.link} and {!val:Sign.unlink}). This is necessary to - ensure that two identical symbols are always physically equal, even across - signatures. It should NOT be otherwise mutated. *) - -(** {b NOTE} We maintain the invariant that {!field:sym_impl} never ends with - [false]. Indeed, this information would be redundant. If a symbol has more - arguments than there are booleans in the list then the extra arguments are - all explicit. Finally, note that {!field:sym_impl} is empty if and only if - the symbol has no implicit parameters. *) - -(** {b NOTE} {!field:sym_prop} restricts the possible - values of {!field:sym_def} and {!field:sym_rules} fields. A symbol is - not allowed to be given rewriting rules (or a definition) when its mode is - set to {!constructor:Constant}. Moreover, a symbol should not be given at - the same time a definition (i.e., {!field:sym_def} different from [None]) - and rewriting rules (i.e., {!field:sym_rules} is non-empty). *) - -(** {b NOTE} For generated symbols (recursors, axioms), {!field:sym_pos} may - not be valid positions in the source. These virtual positions are however - important for exporting lambdapi files to other formats. *) - -(** {3 Representation of rewriting rules} *) - -(** Representation of a rewriting rule. A rewriting rule is mainly formed of a - LHS (left hand side), which is the pattern that should be matched for the - rule to apply, and a RHS (right hand side) giving the action to perform if - the rule applies. More explanations are given below. *) - and rule = - { lhs : term list (** Left hand side (LHS). *) - ; names : string array (** Names of pattern variables. *) - ; rhs : term (** Right hand side (RHS). *) - ; arity : int (** Required number of arguments to be applicable. *) - ; arities : int array - (** Arities of the pattern variables bound in the RHS. *) - ; vars_nb : int (** Number of variables in [lhs]. *) - ; xvars_nb : int (** Number of variables in [rhs] but not in [lhs]. *) - ; rule_pos : Pos.popt (** Position of the rule in the source file. *) } - -(** {b NOTE} {!field:arity} gives the number of arguments contained in the - LHS. It is always equal to [List.length r.lhs] and gives the minimal number - of arguments required to match the LHS. *) - -(** {b NOTE} For generated rules, {!field:rule_pos} may not be valid positions - in the source. These virtual positions are however important for exporting - lambdapi files to other formats. *) - -(** All variables of rewriting rules that appear in the RHS must appear in the - LHS. In the case of unification rules, we allow variables to appear only in - the RHS. In that case, these variables are replaced by fresh meta-variables - each time the rule is used. *) - -(** During evaluation, we only try to apply rewriting rules when we reduce the - application of a symbol [s] to a list of argument [ts]. At this point, the - symbol [s] contains every rule [r] that can potentially be applied in its - {!field:sym_rules} field. To check if a rule [r] applies, we match the - elements of [r.lhs] with those of [ts] while building an environment [env]. - During this process, a pattern of - the form {!constructor:Patt}[(Some i,_,_)] matched against a term [u] will - results in [env.(i)] being set to [u]. If all terms of [ts] can be matched - against corresponding patterns, then environment [env] is fully constructed - and it can hence be substituted in [r.rhs] with [subst_patt env r.rhs] - to get the result of the application of the rule. *) - -(** {3 Metavariables and related functions} *) - -(** Representation of a metavariable, which corresponds to a yet unknown - term typable in some context. The substitution of the free variables - of the context is suspended until the metavariable is instantiated - (i.e., set to a particular term). When a metavariable [m] is - instantiated, the suspended substitution is unlocked and terms of - the form {!constructor:Meta}[(m,env)] can be unfolded. *) -and meta = - { meta_key : int (** Unique key. *) - ; meta_type : term Timed.ref (** Type. *) - ; meta_arity : int (** Arity (environment size). *) - ; meta_value : mbinder option Timed.ref (** Definition. *) } - -let binder_name : binder -> string = fun (bi,_,_) -> bi.binder_name -let mbinder_names : mbinder -> string array = fun (bi,_,_) -> bi.mbinder_name - -(** [mbinder_arity b] gives the arity of the [mbinder]. *) -let mbinder_arity : mbinder -> int = - fun (i,_,_) -> Array.length i.mbinder_name - -(** [binder_occur b] tests whether the bound variable occurs in [b]. *) -let binder_occur : binder -> bool = fun (bi,_,_) -> bi.binder_bound -let mbinder_occur : mbinder -> int -> bool = - fun (bi,_,_) i -> assert (i < Array.length bi.mbinder_name); - bi.mbinder_bound.(i) - -(** Minimize [impl] to enforce our invariant (see {!type:Terms.sym}). *) -let minimize_impl : bool list -> bool list = - let rec rem_false l = match l with false::l -> rem_false l | _ -> l in - fun l -> List.rev (rem_false (List.rev l)) - -(** [create_sym path expo prop mstrat opaq name pos typ impl] creates a new - symbol with path [path], exposition [expo], property [prop], opacity - [opaq], matching strategy [mstrat], name [name.elt], type [typ], implicit - arguments [impl], position [name.pos], declaration position [pos], no - definition and no rules. *) -let create_sym : Path.t -> expo -> prop -> match_strat -> bool -> - Pos.strloc -> Pos.popt -> term -> bool list -> sym = - fun sym_path sym_expo sym_prop sym_mstrat sym_opaq - { elt = sym_name; pos = sym_pos } sym_decl_pos typ sym_impl -> - let open Timed in - {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None; - sym_opaq = ref sym_opaq; sym_rules = ref []; sym_nota = ref NoNotation; - sym_dtree = ref Tree_type.empty_dtree; - sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos } - -(** [is_constant s] tells whether [s] is a constant. *) -let is_constant : sym -> bool = fun s -> s.sym_prop = Const - -(** [is_injective s] tells whether [s] is injective, which is in partiular the - case if [s] is constant. *) -let is_injective : sym -> bool = fun s -> - match s.sym_prop with Const | Injec -> true | _ -> Timed.(!(s.sym_opaq)) - -(** [is_private s] tells whether the symbol [s] is private. *) -let is_private : sym -> bool = fun s -> s.sym_expo = Privat - -(** [is_modulo s] tells whether the symbol [s] is modulo some equations. *) -let is_modulo : sym -> bool = fun s -> - match s.sym_prop with Assoc _ | Commu | AC _ -> true | _ -> false - -(** Sets and maps of symbols. *) -module Sym = struct - type t = sym - let compare s1 s2 = - if s1 == s2 then 0 else - match Stdlib.compare s1.sym_name s2.sym_name with - | 0 -> Stdlib.compare s1.sym_path s2.sym_path - | n -> n -end - -module SymSet = Set.Make(Sym) -module SymMap = Map.Make(Sym) - -(** [is_unset m] returns [true] if [m] is not instantiated. *) -let is_unset : meta -> bool = fun m -> Timed.(!(m.meta_value)) = None - -(** Sets and maps of metavariables. *) -module Meta = struct - type t = meta - let compare m1 m2 = m2.meta_key - m1.meta_key -end - -module MetaSet = Set.Make(Meta) -module MetaMap = Map.Make(Meta) - -(** Dealing with AC-normalization of terms *) -let mk_bin s t1 t2 = Appl(Appl(Symb s, t1), t2) - -(** [mk_left_comb s t ts] builds a left comb of applications of [s] from - [t::ts] so that [mk_left_comb s t1 [t2; t3] = mk_bin s (mk_bin s t1 t2) - t3]. *) -let mk_left_comb : sym -> term -> term list -> term = fun s -> - List.fold_left (mk_bin s) - -(** [mk_right_comb s ts t] builds a right comb of applications of [s] to - [ts@[t]] so that [mk_right_comb s [t1; t2] t3 = mk_bin s t1 (mk_bin s t2 - t3)]. *) -let mk_right_comb : sym -> term list -> term -> term = fun s -> - List.fold_right (mk_bin s) - -(** Printing functions for debug. *) -let rec term : term pp = fun ppf t -> - match unfold t with - | Bvar (InSub k) -> out ppf "`%d" k - | Bvar (InEnv k) -> out ppf "~%d" k - | Vari v -> var ppf v - | Type -> out ppf "TYPE" - | Kind -> out ppf "KIND" - | Symb s -> sym ppf s - | Prod(a,(n,b,e)) -> - out ppf "(Π %s:%a, %a#(%a))" n.binder_name term a clos_env e term b - | Abst(a,(n,b,e)) -> - out ppf "(λ %s:%a, %a#(%a))" n.binder_name term a clos_env e term b - | Appl(a,b) -> out ppf "(%a %a)" term a term b - | Meta(m,ts) -> out ppf "?%d%a" m.meta_key terms ts - | Patt(i,s,ts) -> out ppf "$%a_%s%a" (D.option D.int) i s terms ts - | Plac(_) -> out ppf "_" - | Wild -> out ppf "_" - | TRef r -> out ppf "&%a" (Option.pp term) Timed.(!r) - | LLet(a,t,(n,b,e)) -> - out ppf "let %s:%a ≔ %a in %a#(%a)" - n.binder_name term a term t clos_env e term b -and var : var pp = fun ppf (i,n) -> out ppf "%s%d" n i -and sym : sym pp = fun ppf s -> string ppf s.sym_name -and terms : term array pp = fun ppf ts -> - if Array.length ts > 0 then D.array term ppf ts -and clos_env : term array pp = fun ppf env -> D.array term ppf env - -(** [unfold t] repeatedly unfolds the definition of the surface constructor - of [t], until a significant {!type:term} constructor is found. The term - that is returned can be neither an instantiated metavariable - nor a reference cell ({!constructor:TRef} constructor). Note - that the returned value is physically equal to [t] if no unfolding was - performed. {b NOTE} that {!val:unfold} must (almost) always be called - before matching over a value of type {!type:term}. *) -and unfold : term -> term = fun t -> - let open Timed in - match t with - | Meta(m, ts) -> - begin - match !(m.meta_value) with - | None -> t - | Some(b) -> unfold (msubst b ts) - end - | TRef(r) -> - begin - match !r with - | None -> t - | Some(v) -> unfold v - end - | _ -> t - -(** [msubst b vs] substitutes the variables bound by [b] with the values - [vs]. Note that the length of the [vs] array should match the arity of - the multiple binder [b]. *) -and msubst : mbinder -> term array -> term = fun (bi,tm,env) vs -> - let n = Array.length bi.mbinder_name in - assert (Array.length vs = n); - let rec msubst t = -(* if Logger.log_enabled() then - log "msubst %a %a" (D.array term) vs term t;*) - match unfold t with - | Bvar (InSub p) -> assert bi.mbinder_bound.(p); vs.(p) - | Bvar (InEnv p) -> env.(p) - | Appl(a,b) -> mk_Appl(msubst a, msubst b) - (* No need to substitute in the closure term: all bound variables appear - in the closure environment *) - | Abst(a,(n,u,e)) -> Abst(msubst a, (n, u, Array.map msubst e)) - | Prod(a,(n,u,e)) -> Prod(msubst a, (n, u, Array.map msubst e)) - | LLet(a,t,(n,u,e)) -> - LLet(msubst a, msubst t, (n, u, Array.map msubst e)) - | Meta(m,ts) -> Meta(m, Array.map msubst ts) - | Patt(j,n,ts) -> Patt(j,n, Array.map msubst ts) - | Type | Kind | Vari _ | Wild | Symb _ | Plac _ | TRef _ -> t - in - let r = - if Array.for_all ((=) false) bi.mbinder_bound && Array.length env = 0 - then tm - else msubst tm in - if Logger.log_enabled() then - log "msubst %a#%a %a = %a" clos_env env term tm (D.array term) vs term r; - r - -(** Total order on terms. *) -and cmp : term cmp = fun t t' -> - match unfold t, unfold t' with - | Vari x, Vari x' -> compare_vars x x' - | Type, Type - | Kind, Kind - | Wild, Wild -> 0 - | Symb s, Symb s' -> Sym.compare s s' - | Prod(t,u), Prod(t',u') - | Abst(t,u), Abst(t',u') -> lex cmp cmp_binder (t,u) (t',u') - | Appl(t,u), Appl(t',u') -> lex cmp cmp (u,t) (u',t') - | Meta(m,ts), Meta(m',ts') -> - lex Meta.compare (Array.cmp cmp) (m,ts) (m',ts') - | Patt(i,s,ts), Patt(i',s',ts') -> - lex3 Stdlib.compare Stdlib.compare (Array.cmp cmp) - (i,s,ts) (i',s',ts') - | Bvar i, Bvar j -> Stdlib.compare i j - | TRef r, TRef r' -> Stdlib.compare r r' - | LLet(a,t,u), LLet(a',t',u') -> - lex3 cmp cmp cmp_binder (a,t,u) (a',t',u') - | t, t' -> cmp_tag t t' - -and cmp_binder : binder cmp = -(* fun ({binder_name;binder_bound},u,e) (bi',u',e') -> - let mbi = {mbinder_name=[|binder_name|];mbinder_bound=[|binder_bound|]} in - let var = Vari(new_var binder_name) in - cmp (msubst (mbi,u,e)[|var|]) - (msubst({mbi with mbinder_bound=[|bi'.binder_bound|]},u',e')[|var|])*) - fun (_,u,e) (_,u',e') -> - lex cmp (Array.cmp cmp) (u,e) (u',e') - -(** [get_args t] decomposes the {!type:term} [t] into a pair [(h,args)], where - [h] is the head term of [t] and [args] is the list of arguments applied to - [h] in [t]. The returned [h] cannot be an [Appl] node. *) -and get_args : term -> term * term list = fun t -> - let rec get_args t acc = - match unfold t with - | Appl(t,u) -> get_args t (u::acc) - | t -> t, acc - in get_args t [] - -(** [get_args_len t] is similar to [get_args t] but it also returns the length - of the list of arguments. *) -and get_args_len : term -> term * term list * int = fun t -> - let rec get_args_len acc len t = - match unfold t with - | Appl(t, u) -> get_args_len (u::acc) (len + 1) t - | t -> (t, acc, len) - in - get_args_len [] 0 t - -(** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *) -and is_symb : sym -> term -> bool = fun s t -> - match unfold t with Symb(r) -> r == s | _ -> false - -(* We make the equality of terms modulo commutative and - associative-commutative symbols syntactic by always ordering arguments in - increasing order and by putting them in a comb form. - - The term [t1 + t2 + t3] is represented by the left comb [(t1 + t2) + t3] if - + is left associative and [t1 + (t2 + t3)] if + is right associative. *) - -(** [left_aliens s t] returns the list of the biggest subterms of [t] not - headed by [s], assuming that [s] is left associative and [t] is in - canonical form. This is the reverse of [mk_left_comb]. *) -and left_aliens : sym -> term -> term list = fun s -> - let rec aliens acc = function - | [] -> acc - | u::us -> - let h, ts = get_args u in - if is_symb s h then - match ts with - | t1 :: t2 :: _ -> aliens (t2 :: acc) (t1 :: us) - | _ -> aliens (u :: acc) us - else aliens (u :: acc) us - in fun t -> aliens [] [t] - -(** [right_aliens s t] returns the list of the biggest subterms of [t] not - headed by [s], assuming that [s] is right associative and [t] is in - canonical form. This is the reverse of [mk_right_comb]. *) -and right_aliens : sym -> term -> term list = fun s -> - let rec aliens acc = function - | [] -> acc - | u::us -> - let h, ts = get_args u in - if is_symb s h then - match ts with - | t1 :: t2 :: _ -> aliens (t1 :: acc) (t2 :: us) - | _ -> aliens (u :: acc) us - else aliens (u :: acc) us - in fun t -> let r = aliens [] [t] in - if Logger.log_enabled () then - log "right_aliens %a %a = %a" sym s term t (D.list term) r; - r - -(** [mk_Appl t u] puts the application of [t] to [u] in canonical form wrt C - or AC symbols. *) -and mk_Appl : term * term -> term = fun (t, u) -> - (* if Logger.log_enabled () then - log "mk_Appl(%a, %a)" term t term u; - let r = *) - match get_args t with - | Symb s, [t1] -> - begin - match s.sym_prop with - | Commu when cmp t1 u > 0 -> mk_bin s u t1 - | AC true -> (* left associative symbol *) - let ts = left_aliens s t1 and us = left_aliens s u in - begin - match List.sort cmp (ts @ us) with - | v::vs -> mk_left_comb s v vs - | _ -> assert false - end - | AC false -> (* right associative symbol *) - let ts = right_aliens s t1 and us = right_aliens s u in - let vs, v = List.split_last (List.sort cmp (ts @ us)) - in mk_right_comb s vs v - | _ -> Appl (t, u) - end - | _ -> Appl (t, u) - (* in - if Logger.log_enabled () then - log "mk_Appl(%a, %a) = %a" term t term u term r; - r *) - -(* unit test *) -let _ = - let s = - create_sym [] Privat (AC true) Eager false (Pos.none "+") None Kind [] in - let t1 = Vari (new_var "x1") in - let t2 = Vari (new_var "x2") in - let t3 = Vari (new_var "x3") in - let left = mk_bin s (mk_bin s t1 t2) t3 in - let right = mk_bin s t1 (mk_bin s t2 t3) in - let eq = eq_of_cmp cmp in - assert (eq (mk_left_comb s t1 [t2; t3]) left); - assert (eq (mk_right_comb s [t1; t2] t3) right); - let eq = eq_of_cmp (List.cmp cmp) in - assert (eq (left_aliens s left) [t1; t2; t3]); - assert (eq (right_aliens s right) [t3; t2; t1]) - -(** [is_abst t] returns [true] iff [t] is of the form [Abst _]. *) -let is_abst t = match unfold t with Abst _ -> true | _ -> false - -(** [is_prod t] returns [true] iff [t] is of the form [Prod _]. *) -let is_prod t = match unfold t with Prod _ -> true | _ -> false - -(** [is_tref t] returns [true] iff [t] is of the form [TRef _]. *) -let is_TRef t = match unfold t with TRef _ -> true | _ -> false - -(** [iter_atoms db f g t] applies f to every occurrence of a variable in t, - g to every occurrence of a symbol, and db to every occurrence of a - bound variable. - We have to be careful with binders since in the current implementation - closure environment may contain slots for variables that don't actually - appear. This is done by first checking the closure term, recording which - bound variables actually occur, and then check the elements of the - closure environment which occur. - *) -let rec iter_atoms : - (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> term -> unit = - fun db f g t -> - let rec check db t = - match unfold t with - | Vari x -> f x - | Symb s -> g s - | Bvar i -> db i - | Appl(a,b) -> check db a; check db b - | Abst(a,b) - | Prod(a,b) -> check db a; check_binder db b - | LLet(a,t,b) -> check db a; check db t; check_binder db b - | Meta(_,ts) - | Patt(_,_,ts) -> Array.iter (check db) ts - | _ -> () - and check_binder db (_bi,u,env) = - iter_atoms_closure db f g u env in - check db t - -and iter_atoms_closure : - (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> term -> term array - -> unit = - fun db f g u env -> - (* env positions occuring in [u] *) - let u_pos = ref IntSet.empty in - let db_u db = - match db with - | InEnv p -> u_pos := IntSet.add p !u_pos - | _ -> () in - (* We iterate on u, recording which env positions occur *) - iter_atoms db_u f g u; - (* We then iterate on the members of [e] that *actually* occur in u *) - Array.iteri (fun i t -> - if IntSet.mem i !u_pos then iter_atoms db f g t - (*else if t <> Wild then env.(i) <- Wild*) ) - env - -let iter_atoms_mbinder - : (bvar -> unit) -> (var -> unit) -> (sym -> unit) -> mbinder -> unit = - fun db f g (_bi,u,env) -> iter_atoms_closure db f g u env - -(** [occur x t] tells whether variable [x] occurs in [t]. *) -let occur : var -> term -> bool = - fun x t -> - try iter_atoms - (fun _ -> ()) - (fun y -> if x==y then raise Exit) - (fun _-> ()) t; - false - with Exit -> true - -let occur_mbinder : var -> mbinder -> bool = - fun x b -> - try iter_atoms_mbinder - (fun _ -> ()) - (fun y -> if x==y then raise Exit) - (fun _-> ()) b; - false - with Exit -> true - -(** [is_closed t] checks whether [t] is closed (w.r.t. variables). We have to - be careful with binders since in the current implementation closure - environment may contain slots for variables that don't actually appear *) -let is_closed : term -> bool = - fun t -> - try iter_atoms (fun _ -> ()) (fun _ -> raise Exit) (fun _ -> ()) t; true - with Exit -> false - -let is_closed_mbinder : mbinder -> bool = - fun b -> - try iter_atoms_mbinder - (fun _ -> ()) (fun _ -> raise Exit) (fun _ -> ()) b; true - with Exit -> false - -(** [subst b v] substitutes the variable bound by [b] with the value [v]. - Assumes v is closed (since only called from outside the term library. *) -let subst : binder -> term -> term = fun (bi,tm,env) v -> - let rec subst t = - match unfold t with - | Bvar (InSub _) -> assert bi.binder_bound; v - | Bvar (InEnv p) -> env.(p) - | Appl(a,b) -> mk_Appl(subst a, subst b) - | Abst(a,(n,u,e)) -> Abst(subst a, (n, u, Array.map subst e)) - | Prod(a,(n,u,e)) -> Prod(subst a, (n ,u, Array.map subst e)) - | LLet(a,t,(n,u,e)) -> LLet(subst a, subst t, (n, u, Array.map subst e)) - | Meta(m,ts) -> Meta(m, Array.map subst ts) - | Patt(j,n,ts) -> Patt(j,n, Array.map subst ts) - | _ -> t - in - let r = - if bi.binder_bound = false && Array.length env = 0 then tm - else subst tm in - if Logger.log_enabled() then - log "subst %a#%a [%a] = %a" clos_env env term tm term v term r; - r - -(** [unbind b] substitutes the binder [b] by a fresh variable of name [name] - if given, or the binder name otherwise. The variable and the result of the - substitution are returned. *) -let unbind : ?name:string -> binder -> var * term = - fun ?(name="") ((bn,_,_) as b) -> - let n = if name="" then bn.binder_name else name in - let x = new_var n in x, subst b (Vari x) - -(** [unbind2 f g] is similar to [unbind f], but it substitutes two binders [f] - and [g] at once using the same fresh variable. *) -let unbind2 : ?name:string -> binder -> binder -> var * term * term = - fun ?(name="") ((bn1,_,_) as b1) b2 -> - let n = if name="" then bn1.binder_name else name in - let x = new_var n in x, subst b1 (Vari x), subst b2 (Vari x) - -(** [unmbind b] substitutes the multiple binder [b] with fresh variables. This - function is analogous to [unbind] for binders. Note that the names used to - create the fresh variables are based on those of the multiple binder. *) -let unmbind : mbinder -> var array * term = - fun (({mbinder_name=names;_},_,_) as b) -> - let xs = Array.init (Array.length names) (fun i -> new_var names.(i)) in - xs, msubst b (Array.map (fun x -> Vari x) xs) - -(** [bind_var x t] binds the variable [x] in [t], producing a binder. *) -let bind_var : var -> term -> binder = fun ((_,n) as x) t -> - let bound = Stdlib.ref false in - (* Replace variables [x] by de Bruijn index [i] *) - let rec bind i t = - (*if Logger.log_enabled() then log "bind_var %d %a" i term t;*) - match unfold t with - | Vari y when y == x -> bound := true; Bvar i - | Appl(a,b) -> - let a' = bind i a in - let b' = bind i b in - if a==a' && b==b' then t else Appl(a', b') - (* No need to call mk_Appl here as we only replace free variables by de - Bruijn indices. *) - | Abst(a,b) -> - let a' = bind i a in - let b' = bind_binder i b in - if a==a' && b==b' then t else Abst(a', b') - | Prod(a,b) -> - let a' = bind i a in - let b' = bind_binder i b in - if a==a' && b==b' then t else Prod(a', b') - | LLet(a,m,b) -> - let a' = bind i a in - let m' = bind i m in - let b' = bind_binder i b in - if a==a' && m==m' && b==b' then t else LLet(a', m', b') - | Meta(m,ts) -> - let ts' = Array.map (bind i) ts in - if Array.for_all2 (==) ts ts' then t else Meta(m, ts') - | Patt(j,n,ts) -> - let ts' = Array.map (bind i) ts in - if Array.for_all2 (==) ts ts' then t else Patt(j,n,ts') - | _ -> t - - and bind_binder i (bi,u,env as b) = - let env' = Array.map (bind i) env in - let j = InEnv (Array.length env') in - let u' = bind j u in - if u==u' then (* If [u==u'] then x does not occur in u *) - if Array.for_all2 (==) env env' then b - else (bi, u', env') - else (* x occurs, it has been replaced by [Bvar(j)], - corresponding to the head of [e] *) - (bi, u', Array.append env' [|Bvar i|]) in - - let b = bind (InSub 0) t in - if Logger.log_enabled() then - log "bind_var %a %a = %a" var x term t term b; - {binder_name=n; binder_bound= !bound}, b, [||] - -(** [binder f b] applies f inside [b]. *) -let binder : (term -> term) -> binder -> binder = fun f b -> - let x,t = unbind b in bind_var x (f t) - -(** [bind_mvar xs t] binds the variables of [xs] in [t] to get a binder. - It is the equivalent of [bind_var] for multiple variables. *) -let bind_mvar : var array -> term -> mbinder = - let empty = {mbinder_name=[||]; mbinder_bound=[||]} in - fun xs tm -> - if Array.length xs = 0 then empty, tm, [||] else begin - (*if Logger.log_enabled() then - log "bind_mvar %a" (D.array var) xs;*) - let top_map = Stdlib.ref IntMap.empty - and mbinder_bound = Array.make (Array.length xs) false in - Array.iteri - (fun i (ki,_) -> Stdlib.(top_map := IntMap.add ki i !top_map)) xs; - let top_fvar key = - let p = Stdlib.(IntMap.find key !top_map) in - mbinder_bound.(p) <- true; Bvar (InSub p) in - (* Replace variables [x] in [xs] by de Bruijn index [fvar x] *) - let rec bind fvar t = - (*if Logger.log_enabled() then log "bind_mvar %d %a" i term t;*) - match unfold t with - | Vari (key,_) -> - if Stdlib.(IntMap.mem key !top_map) then fvar key else t - | Appl(a,b) -> - let a' = bind fvar a in - let b' = bind fvar b in - if a==a' && b==b' then t else Appl(a', b') - (* No need to call mk_Appl here as we only replace free variables by de - Bruijn indices. *) - | Abst(a,b) -> - let a' = bind fvar a in - let b' = bind_binder fvar b in - if a==a' && b==b' then t else Abst(a', b') - | Prod(a,b) -> - let a' = bind fvar a in - let b' = bind_binder fvar b in - if a==a' && b==b' then t else Prod(a', b') - | LLet(a,m,b) -> - let a' = bind fvar a in - let m' = bind fvar m in - let b' = bind_binder fvar b in - if a==a' && m==m' && b==b' then t else LLet(a', m', b') - | Meta(m,ts) -> - let ts' = Array.map (bind fvar) ts in - if Array.for_all2 (==) ts ts' then t else Meta(m, ts') - | Patt(j,n,ts) -> - let ts' = Array.map (bind fvar) ts in - if Array.for_all2 (==) ts ts' then t else Patt(j,n,ts') - | _ -> t - - and bind_binder fvar (bi,u,u_env as b) = - let open Stdlib in - let u_env' = Array.map (bind fvar) u_env in - let u_n = ref 0 in - let u_map = ref IntMap.empty in - let fvar' key = - match IntMap.find_opt key !u_map with - | Some p -> Bvar (InEnv p) - | None -> - let p' = Array.length u_env' + !u_n in - incr u_n; - u_map := IntMap.add key p' !u_map; - Bvar (InEnv p') in - let u' = bind fvar' u in - if u==u' && !u_n = 0 && Lplib.Array.for_all2 (==) u_env u_env' then b - else (* some vars of [xs] occur in u *) - let u_env' = Array.append u_env' (Array.make !u_n Wild) in - IntMap.iter (fun key p -> u_env'.(p) <- fvar key) !u_map; - (bi, u', u_env') in - - let b = bind top_fvar tm in - if Logger.log_enabled() then - log "bind_mvar %a %a = %a %a" - (D.array var) xs term tm pr_bound mbinder_bound term b; - let bi = { mbinder_name = Array.map base_name xs; mbinder_bound } in - bi, b, [||] - end - -(** Construction functions of the private type [term]. They ensure some - invariants: - -- In a commutative function symbol application, the first argument is smaller - than the second one wrt [cmp]. - -- In an associative and commutative function symbol application, the - application is built as a left or right comb depending on the associativity - of the symbol, and arguments are ordered in increasing order wrt [cmp]. - -- In [LLet(_,_,b)], [binder_occur b = true] (useless let's are erased). *) -let mk_Vari x = Vari x -let mk_Type = Type -let mk_Kind = Kind -let mk_Symb x = Symb x -let mk_Prod (a,b) = Prod (a,b) -let mk_Arro (a,b) = let x = new_var "_" in Prod(a, bind_var x b) -let mk_Abst (a,b) = Abst (a,b) -let mk_Meta (m,ts) = (*assert (m.meta_arity = Array.length ts);*) Meta (m,ts) -let mk_Patt (i,s,ts) = Patt (i,s,ts) -let mk_Wild = Wild -let mk_Plac b = Plac b -let mk_TRef x = TRef x -let mk_LLet (a,t,b) = LLet (a,t,b) - -(** [mk_Appl_not_canonical t u] builds the non-canonical (wrt. C and AC - symbols) application of [t] to [u]. WARNING: to use only in Sign.link. *) -let mk_Appl_not_canonical : term * term -> term = fun (t, u) -> Appl(t, u) - -(** [add_args t args] builds the application of the {!type:term} [t] to a list - arguments [args]. When [args] is empty, the returned value is (physically) - equal to [t]. *) -let add_args : term -> term list -> term = fun t ts -> - match get_args t with - | Symb s, _ when is_modulo s -> - List.fold_left (fun t u -> mk_Appl(t,u)) t ts - | _ -> List.fold_left (fun t u -> Appl(t,u)) t ts - -(** [add_args_map t f ts] is equivalent to [add_args t (List.map f ts)] but - more efficient. *) -let add_args_map : term -> (term -> term) -> term list -> term = fun t f ts -> - match get_args t with - | Symb s, _ when is_modulo s -> - List.fold_left (fun t u -> mk_Appl(t, f u)) t ts - | _ -> List.fold_left (fun t u -> Appl(t, f u)) t ts - -(** Patt substitution. *) -let subst_patt : mbinder option array -> term -> term = fun env -> - let rec subst_patt t = - match unfold t with - | Patt(Some i,n,ts) when 0 <= i && i < Array.length env -> - begin match env.(i) with - | Some b -> msubst b (Array.map subst_patt ts) - | None -> mk_Patt(Some i,n,Array.map subst_patt ts) - end - | Patt(i,n,ts) -> mk_Patt(i, n, Array.map subst_patt ts) - | Prod(a,(n,b,e)) -> - mk_Prod(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) - | Abst(a,(n,b,e)) -> - mk_Abst(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) - | Appl(a,b) -> mk_Appl(subst_patt a, subst_patt b) - | Meta(m,ts) -> mk_Meta(m, Array.map subst_patt ts) - | LLet(a,t,(n,b,e)) -> - mk_LLet(subst_patt a, subst_patt t, - (n, subst_patt b, Array.map subst_patt e)) - | Wild - | Plac _ - | TRef _ - | Bvar _ - | Vari _ - | Type - | Kind - | Symb _ -> t - in subst_patt - -(** [cleanup t] unfold all metas and TRef's in [t]. *) -let rec cleanup : term -> term = fun t -> - match unfold t with - | Patt(i,n,ts) -> mk_Patt(i, n, Array.map cleanup ts) - | Prod(a,b) -> mk_Prod(cleanup a, binder cleanup b) - | Abst(a,b) -> mk_Abst(cleanup a, binder cleanup b) - | Appl(a,b) -> mk_Appl(cleanup a, cleanup b) - | Meta(m,ts) -> mk_Meta(m, Array.map cleanup ts) - | LLet(a,t,b) -> mk_LLet(cleanup a, cleanup t, binder cleanup b) - | Wild -> assert false - | Plac _ -> assert false - | TRef _ -> assert false - | Bvar _ -> assert false - | Vari _ - | Type - | Kind - | Symb _ -> t - -(** Type of a symbol and a rule. *) -type sym_rule = sym * rule - -let lhs : sym_rule -> term = fun (s, r) -> add_args (mk_Symb s) r.lhs -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 - -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 - first). *) -type ctxt = (var * term * term option) list - -let decl ppf (v,a,d) = - out ppf "%a: %a" var v term a; - match d with - | None -> () - | Some d -> out ppf " ≔ %a" term d - -let ctxt : ctxt pp = fun ppf c -> List.pp decl ", " ppf (List.rev c) - -(** Type of unification constraints. *) -type constr = ctxt * term * term - -(** Representation of unification problems. *) -type problem_aux = - { to_solve : constr list - (** List of unification problems to solve. *) - ; unsolved : constr list - (** List of unification problems that could not be solved. *) - ; recompute : bool - (** Indicates whether unsolved problems should be rechecked. *) - ; metas : MetaSet.t - (** Set of unsolved metas. *) } - -type problem = problem_aux Timed.ref - -(** Create a new empty problem. *) -let new_problem : unit -> problem = fun () -> - Timed.ref - {to_solve = []; unsolved = []; recompute = false; metas = MetaSet.empty} - -(** Printing functions for debug. *) -module Raw = struct - let sym = sym let _ = sym - let term = term let _ = term - let ctxt = ctxt let _ = ctxt -end -(* -let rec to_term_serializable t = match t with - | Vari x -> Ser_Vari x - | Bvar x -> Ser_Bvar x - | Type -> Ser_Type - | Kind -> Ser_Kind - | Symb x -> Ser_Symb x - | Prod (x, y) -> Ser_Prod (to_term_serializable x, to_binder_serializable y) - | Abst (x, y) -> Ser_Abst (to_term_serializable x, to_binder_serializable y) - | Appl (x, y) -> Ser_Appl (to_term_serializable x, to_term_serializable y) - | Meta (x, y) -> Ser_Meta (x, Array.map to_term_serializable y) - | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) - | Wild -> Ser_Wild - | Plac x -> Ser_Plac x - | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x) ) - (* | TRef x -> Ser_TRef (match Timed.(!) x with None -> None | Some x -> Some (to_term_serializable x)) *) - | LLet (x, y, z) -> Ser_LLet (to_term_serializable x, to_term_serializable y, to_binder_serializable z) -and to_binder_serializable (x, y, z) = - (x, to_term_serializable y, Array.map to_term_serializable z) -let rec of_term_serializable t = match t with - | Ser_Vari x -> Vari x - | Ser_Bvar x -> Bvar x - | Ser_Type -> Type - | Ser_Kind -> Kind - | Ser_Symb x -> Symb x - | Ser_Prod (x, y) -> Prod (of_term_serializable x, of_binder_serializable y) - | Ser_Abst (x, y) -> Abst (of_term_serializable x, of_binder_serializable y) - | Ser_Appl (x, y) -> Appl (of_term_serializable x, of_term_serializable y) - | Ser_Meta (x, y) -> Meta (x, Array.map of_term_serializable y) - | Ser_Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) - | Ser_Wild -> Wild - | Ser_Plac x -> Plac x - | Ser_TRef x -> TRef (Timed.ref (Option.map of_term_serializable x)) - | Ser_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) - *) - -type sym_serializable = - { ser_sym_expo : expo - ; ser_sym_path : Path.t - ; ser_sym_name : string - (* ; ser_sym_type : term_serializable *) - (* ; ser_sym_impl : bool list *) - (* ; ser_sym_prop : prop *) - (* ; ser_sym_nota : float notation Timed.ref *) - (* ; ser_sym_def : term option Timed.ref *) - (* ; ser_sym_opaq : bool Timed.ref *) - (* ; ser_sym_rules : rule list Timed.ref *) - (* ; ser_sym_mstrat: match_strat *) - (* ; ser_sym_dtree : dtree Timed.ref *) - (* ; ser_sym_pos : Pos.popt *) - (* ; ser_sym_decl_pos : Pos.popt *) - } [@@deriving yojson] - - let to_sym_serializable s = - { - ser_sym_expo = s.sym_expo - ; ser_sym_path = s.sym_path - ; ser_sym_name = s.sym_name - (* ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) *) - } - let of_sym_serializable s = - { - sym_expo = s.ser_sym_expo - ; sym_path = s.ser_sym_path - ; sym_name = s.ser_sym_name - ; sym_type = Timed.ref Type - (* ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) *) - ; sym_impl = [] (*FIX ME*) - ; sym_prop = Defin (*FIX ME*) - ; sym_nota = Timed.ref NoNotation (*FIX ME*) - ; sym_def = Timed.ref None (*FIX ME*) - ; sym_opaq = Timed.ref true (*FIX ME*) - ; sym_rules = Timed.ref [] (*FIX ME*) - ; sym_mstrat = Sequen (*FIX ME*) - ; sym_dtree = Timed.ref Tree_type.empty_dtree (*FIX ME*) - ; sym_pos = None (*FIX ME*) - ; sym_decl_pos = None (*FIX ME*) - } - - let sym_to_yojson s = - sym_serializable_to_yojson (to_sym_serializable s) - - let sym_of_yojson j = - match (sym_serializable_of_yojson j) with - | Ok j -> Ok (of_sym_serializable j) - | Error s -> Error s - let sym_dump = - { - sym_expo = Privat - ; sym_path = [] - ; sym_name = "" - ; sym_type = Timed.ref Type - ; sym_impl = [] - ; sym_prop = Defin - ; sym_nota = Timed.ref NoNotation - ; sym_def = Timed.ref None - ; sym_opaq = Timed.ref true - ; sym_rules = Timed.ref [] - ; sym_mstrat = Sequen - ; sym_dtree = Timed.ref Tree_type.empty_dtree - ; sym_pos = None - ; sym_decl_pos = None - } \ No newline at end of file diff --git a/src/core/term.mli b/src/core/term.mli index c5a39d1ef..faaa3c462 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -520,8 +520,8 @@ and sym_serializable = ; ser_sym_rules : rule_serializable list (* Timed.ref*) ; ser_sym_mstrat: match_strat ; ser_sym_dtree : dtree_serializable - (* ; ser_sym_pos : Pos.popt *) - (* ; ser_sym_decl_pos : Pos.popt *) + ; ser_sym_pos : Pos.popt + ; ser_sym_decl_pos : Pos.popt } and dtree_serializable = rule_serializable Tree_type.dtree_serializable From 90a187356a001f5f91c93d0b9729f071d0b8fbf7 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Thu, 9 Apr 2026 13:44:34 +0200 Subject: [PATCH 12/26] with sign_deps in sign --- src/core/sign.ml | 86 +++++++++++++++++++++++++++++++++++++++++++---- src/core/term.ml | 2 ++ src/core/term.mli | 11 ++++-- 3 files changed, 90 insertions(+), 9 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index 360ac301d..7cb8b6cc1 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -14,23 +14,69 @@ 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 } + [@to_yojson fun l -> + `List (List.map + (fun r -> rule_serializable_to_yojson (to_rule_serializable r)) + l)] + [@of_yojson fun j -> + match j with + | `List lst -> + let rec aux acc = function + | [] -> Ok (List.rev acc) + | x :: xs -> + begin match rule_serializable_of_yojson x with + | Ok r_ser -> + aux (of_rule_serializable r_ser :: acc) xs + | Error e -> Error e + end + in + aux [] lst + | _ -> Error "rules: expected list"] + ; nota : float notation option }[@@deriving yojson] + + +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" (** Data associated to a dependency. *) type dep_data = { dep_symbols : sym_data StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_data_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_data_of_yojson j] ; dep_open : bool } + [@@deriving yojson] (** Representation of a signature, that is, what is introduced by a module/file. Signatures must be created with the functions [create] or [read] below only.*) type t = - { sign_symbols : sym StrMap.t ref - ; sign_path : Path.t - ; sign_deps : dep_data Path.Map.t ref + { sign_symbols : sym StrMap.t ref (*OK*) + ; sign_path : Path.t (*OK*) + ; 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 } @@ -255,10 +301,14 @@ let toJson sign : Yojson.Safe.t = StrMap.bindings (Timed.(!)sign.sign_symbols) |> List.map (fun (k, v) -> (k, sym_to_yojson v)) in + let dep_data_assoc = + Path.Map.bindings (Timed.(!) sign.sign_deps) + |>List.map (fun (k, v) -> (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) in `Assoc [ "version" , `String Version.version ; "sign_path" , `List (List.map (fun s -> `String s) sign.sign_path) ; ("sign_symbols", `Assoc rules_assoc) + ; ("sign_deps", `Assoc dep_data_assoc) ] (** [write sign file] writes the signature [sign] to the file [fname]. *) @@ -479,6 +529,27 @@ let rec dependencies : t -> (Path.t * t) list = fun sign -> List.concat (minimize [] deps) let%test "rev" = + let rule = + {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 = {rules=[rule]; nota=None} in + let 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 "" @@ -488,7 +559,10 @@ let%test "rev" = sym_path = ["rep"; "file"] } symbols in - let sign = {sign with sign_symbols = Timed.ref 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) + } in write sign "/tmp/test_sign_read_write.json"; let r_sign = read "/tmp/test_sign_read_write.json" in diff --git a/src/core/term.ml b/src/core/term.ml index e3feef9c8..48c6390d9 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -1170,6 +1170,8 @@ and of_sym_serializable s = match (sym_serializable_of_yojson j) with | Ok j -> Ok (of_sym_serializable j) | Error s -> Error s + + let dump_term = Type let sym_dump = { sym_expo = Privat diff --git a/src/core/term.mli b/src/core/term.mli index faaa3c462..e1d97c3f1 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 @@ -152,7 +153,7 @@ and rule = ; vars_nb : int (** Number of variables in [lhs]. *) ; xvars_nb : int (** Number of variables in [rhs] but not in [lhs]. *) ; rule_pos : Pos.popt (** Position of the rule in the source file. *) } - + (** The LHS (or pattern) of a rewriting rule is always formed of a head symbol (on which the rule is defined) applied to a list of pattern arguments. The list of arguments is given in [lhs], but the head symbol itself is @@ -505,7 +506,7 @@ and rule_serializable = ; ser_vars_nb : int ; ser_xvars_nb : int ; ser_rule_pos : Pos.popt - } + } [@@deriving yojson] and sym_serializable = { ser_sym_expo : expo @@ -529,4 +530,8 @@ and dtree_serializable = rule_serializable Tree_type.dtree_serializable val sym_dump : sym val sym_to_yojson : sym -> Yojson.Safe.t -val sym_of_yojson : Yojson.Safe.t -> (sym, string) result \ No newline at end of file +val sym_of_yojson : Yojson.Safe.t -> (sym, string) result + +val to_rule_serializable : rule -> rule_serializable +val of_rule_serializable : rule_serializable -> rule +val dump_term : term \ No newline at end of file From 70fc2120df36fe7f31af868e4be82ac89da4d10d Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Thu, 9 Apr 2026 13:58:01 +0200 Subject: [PATCH 13/26] with sign_builtins in sign --- src/core/sign.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index 7cb8b6cc1..c886f1786 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -303,12 +303,18 @@ let toJson sign : Yojson.Safe.t = in let dep_data_assoc = Path.Map.bindings (Timed.(!) sign.sign_deps) - |>List.map (fun (k, v) -> (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) in + |>List.map (fun (k, v) -> (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) + in + let sign_builtins = + StrMap.bindings (Timed.(!)sign.sign_builtins) + |> List.map (fun (k, v) -> (k, sym_to_yojson v)) + in `Assoc [ "version" , `String Version.version ; "sign_path" , `List (List.map (fun s -> `String s) sign.sign_path) ; ("sign_symbols", `Assoc rules_assoc) ; ("sign_deps", `Assoc dep_data_assoc) + ; ("sign_builtins", `Assoc sign_builtins) ] (** [write sign file] writes the signature [sign] to the file [fname]. *) @@ -562,6 +568,7 @@ let%test "rev" = 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 From 8de35863539757560f2772517405c9a8c805353e Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Thu, 9 Apr 2026 16:54:41 +0200 Subject: [PATCH 14/26] run sanity check --- src/core/sign.ml | 29 +++---- src/core/term.ml | 171 +++++++++++++++++++++++++----------------- src/core/term.mli | 10 ++- src/core/tree_type.ml | 15 ++-- 4 files changed, 133 insertions(+), 92 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index c886f1786..46f6df173 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -35,9 +35,8 @@ type sym_data = aux [] lst | _ -> Error "rules: expected list"] ; nota : float notation option }[@@deriving yojson] - -let strmap_to_yojson to_elt (m : 'a StrMap.t) : Yojson.Safe.t = + let strmap_to_yojson to_elt (m : 'a StrMap.t) : Yojson.Safe.t = `List ( StrMap.bindings m |> List.map (fun (k, v) -> @@ -76,7 +75,7 @@ type dep_data = type t = { sign_symbols : sym StrMap.t ref (*OK*) ; sign_path : Path.t (*OK*) - ; sign_deps : dep_data Path.Map.t ref + ; 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 } @@ -303,7 +302,8 @@ let toJson sign : Yojson.Safe.t = in let dep_data_assoc = Path.Map.bindings (Timed.(!) sign.sign_deps) - |>List.map (fun (k, v) -> (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) + |>List.map (fun (k, v) -> + (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) in let sign_builtins = StrMap.bindings (Timed.(!)sign.sign_builtins) @@ -350,7 +350,9 @@ let read : string -> t = fun fname -> |> Yojson.Safe.Util.member "version" |> Yojson.Safe.Util.to_string in if version <> Version.version then - raise (Failure ("Version " ^ version ^ " found but " ^ Version.version ^ "expected (current)")); + raise (Failure + ("Version " ^ version ^ " found but " ^ + Version.version ^ "expected (current)")); let sign_path = json_sign |> Yojson.Safe.Util.member "sign_path" @@ -370,14 +372,14 @@ let read : string -> t = fun fname -> let sign = create (sign_path) in let sign = {sign with sign_symbols = Timed.ref sign_symbols} in - (* READ sign_symbols and update sign *) (* let sign = Marshal.from_channel ic in *) close_in ic; sign with Failure msg -> close_in ic; - fatal_no_pos "File \"%s\" is incompatible with current binary. %s" fname msg + 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; @@ -535,7 +537,7 @@ let rec dependencies : t -> (Path.t * t) list = fun sign -> List.concat (minimize [] deps) let%test "rev" = - let rule = + let rule = {lhs = [Term.dump_term] ; names = [|"rule1"|] ; rhs = Term.dump_term @@ -543,7 +545,7 @@ let%test "rev" = ; arities = [|1; 2|] ; vars_nb = 5 ; xvars_nb = 9 - ; rule_pos = Some { fname = Some "file" + ; rule_pos = Some { fname = Some "file" ; start_line = 0 ; start_col = 0 ; start_offset = 0 @@ -560,22 +562,23 @@ let%test "rev" = let symbols = Timed.(!) sign.sign_symbols in let symbols = StrMap.add "" { - sym_dump + 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_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 && + sign.sign_path = r_sign.sign_path && (StrMap.equal - (fun a b -> + (fun a b -> (Sym.compare a b) = 0 (* Should compare : *) (* a.sym_expo = b.sym_expo diff --git a/src/core/term.ml b/src/core/term.ml index 48c6390d9..2c0fdf654 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -41,8 +41,11 @@ type prop = [@@deriving yojson] (** Data of a binder. *) -type binder_info = {binder_name : string; binder_bound : bool} [@@deriving yojson] -type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} [@@deriving yojson] +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 "_") @@ -105,7 +108,10 @@ type 'a notation = | NoNotation | Prefix of 'a | Postfix of 'a - | Infix of (Pratter.associativity [@to_yojson associativity_to_yojson] [@of_yojson associativity_of_yojson]) * '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 @@ -1004,15 +1010,24 @@ type term_serializable = | Ser_LLet of term_serializable * term_serializable * binder_serializable [@@deriving yojson] -and binder_serializable = binder_info * term_serializable * term_serializable array [@@deriving yojson] +and binder_serializable = + binder_info + * term_serializable + * term_serializable array + [@@deriving yojson] and meta_serializable = { ser_meta_key : int - ; ser_meta_type : term_serializable (**Timed.ref. *) - ; ser_meta_arity : int - ; ser_meta_value : mbinder_serializable option (** Timed.ref. *) } [@@deriving yojson] + ; ser_meta_type : term_serializable + ; ser_meta_arity : int + ; ser_meta_value : mbinder_serializable option + } [@@deriving yojson] -and mbinder_serializable = mbinder_info * term_serializable * term_serializable array [@@deriving yojson] +and mbinder_serializable = + mbinder_info + * term_serializable + * term_serializable array + [@@deriving yojson] and rule_serializable = { ser_lhs : term_serializable list @@ -1025,7 +1040,8 @@ and rule_serializable = ; ser_rule_pos : Pos.popt }[@@deriving yojson] -and dtree_serializable = rule_serializable Tree_type.dtree_serializable [@@deriving yojson] +and dtree_serializable = + rule_serializable Tree_type.dtree_serializable [@@deriving yojson] and sym_serializable = { ser_sym_expo : expo @@ -1045,23 +1061,29 @@ and sym_serializable = } [@@deriving yojson] let rec to_term_serializable t = match t with - | Vari x -> Ser_Vari x - | Bvar x -> Ser_Bvar x - | Type -> Ser_Type - | Kind -> Ser_Kind - | Symb x -> Ser_Symb (to_sym_serializable x) - | Prod (x, y) -> Ser_Prod (to_term_serializable x, to_binder_serializable y) - | Abst (x, y) -> Ser_Abst (to_term_serializable x, to_binder_serializable y) - | Appl (x, y) -> Ser_Appl (to_term_serializable x, to_term_serializable y) - | Meta (x, y) -> Ser_Meta ((to_meta_serializable x), Array.map to_term_serializable y) - | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) - | Wild -> Ser_Wild - | Plac x -> Ser_Plac x - | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x) ) - (* | TRef x -> Ser_TRef (match Timed.(!) x with None -> None | Some x -> Some (to_term_serializable x)) *) - | LLet (x, y, z) -> Ser_LLet (to_term_serializable x, to_term_serializable y, to_binder_serializable z) - -and to_dtree_serializable d = Tree_type.to_dtree_serializable (fun x -> to_rule_serializable x) d + | Vari x -> Ser_Vari x + | Bvar x -> Ser_Bvar x + | Type -> Ser_Type + | Kind -> Ser_Kind + | Symb x -> Ser_Symb (to_sym_serializable x) + | Prod (x, y) ->Ser_Prod + (to_term_serializable x, to_binder_serializable y) + | Abst (x, y) ->Ser_Abst + (to_term_serializable x, to_binder_serializable y) + | Appl (x, y) ->Ser_Appl + (to_term_serializable x, to_term_serializable y) + | Meta (x, y) ->Ser_Meta + ((to_meta_serializable x), Array.map to_term_serializable y) + | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) + | Wild -> Ser_Wild + | Plac x -> Ser_Plac x + | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x)) + | LLet (x, y, z) -> Ser_LLet (to_term_serializable x + , to_term_serializable y + , to_binder_serializable z) + +and to_dtree_serializable d = + Tree_type.to_dtree_serializable (fun x -> to_rule_serializable x) d and to_binder_serializable (x, y, z) = (x, to_term_serializable y, Array.map to_term_serializable z) @@ -1069,27 +1091,28 @@ and to_meta_serializable t = { ser_meta_key = t.meta_key ; ser_meta_type = to_term_serializable (Timed.(!) t.meta_type) ; ser_meta_arity = t.meta_arity - ; ser_meta_value = (Option.map to_mbinder_serializable (Timed.(!)t.meta_value))} + ; ser_meta_value = + (Option.map to_mbinder_serializable (Timed.(!)t.meta_value))} and to_mbinder_serializable (x, y ,z) = (x, to_term_serializable y, Array.map to_term_serializable z) and to_sym_serializable s = { - ser_sym_expo = s.sym_expo - ; ser_sym_path = s.sym_path - ; ser_sym_name = s.sym_name - ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) - ; ser_sym_impl = s.sym_impl - ; ser_sym_prop = s.sym_prop - ; ser_sym_nota = Timed.(!)s.sym_nota - ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) - ; ser_sym_opaq = Timed.(!)s.sym_opaq - ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) - ; ser_sym_mstrat = s.sym_mstrat - ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) - ; ser_sym_pos = s.sym_pos - ; ser_sym_decl_pos = s.sym_decl_pos + ser_sym_expo = s.sym_expo + ; ser_sym_path = s.sym_path + ; ser_sym_name = s.sym_name + ; ser_sym_type = (to_term_serializable (Timed.(!) s.sym_type)) + ; ser_sym_impl = s.sym_impl + ; ser_sym_prop = s.sym_prop + ; ser_sym_nota = Timed.(!)s.sym_nota + ; ser_sym_def = Option.map to_term_serializable (Timed.(!) s.sym_def) + ; ser_sym_opaq = Timed.(!)s.sym_opaq + ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) + ; ser_sym_mstrat = s.sym_mstrat + ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) + ; ser_sym_pos = s.sym_pos + ; ser_sym_decl_pos = s.sym_decl_pos } and to_rule_serializable (r : rule) : rule_serializable = @@ -1106,29 +1129,39 @@ and to_rule_serializable (r : rule) : rule_serializable = let rec of_term_serializable t = match t with | Ser_Vari x -> Vari x | Ser_Bvar x -> Bvar x - | Ser_Type -> Type - | Ser_Kind -> Kind + | Ser_Type -> Type + | Ser_Kind -> Kind | Ser_Symb x -> Symb (of_sym_serializable x) - | Ser_Prod (x, y) -> Prod (of_term_serializable x, of_binder_serializable y) - | Ser_Abst (x, y) -> Abst (of_term_serializable x, of_binder_serializable y) - | Ser_Appl (x, y) -> Appl (of_term_serializable x, of_term_serializable y) - | Ser_Meta (x, y) -> Meta ((of_meta_serializable x), Array.map of_term_serializable y) + | Ser_Prod (x, y) -> Prod + (of_term_serializable x, of_binder_serializable y) + | Ser_Abst (x, y) -> Abst + (of_term_serializable x, of_binder_serializable y) + | Ser_Appl (x, y) -> Appl + (of_term_serializable x, of_term_serializable y) + | Ser_Meta (x, y) -> Meta + ((of_meta_serializable x) + , Array.map of_term_serializable y) | Ser_Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) - | Ser_Wild -> Wild + | Ser_Wild -> Wild | Ser_Plac x -> Plac x - | Ser_TRef x -> TRef (Timed.ref (Option.map of_term_serializable x)) - | Ser_LLet (x, y, z) -> LLet (of_term_serializable x, of_term_serializable y, of_binder_serializable z) + | Ser_TRef x -> TRef(Timed.ref (Option.map of_term_serializable x)) + | Ser_LLet (x, y, z) -> LLet + (of_term_serializable x + , of_term_serializable y + , of_binder_serializable z) -and of_dtree_serializable d = Tree_type.of_dtree_serializable of_rule_serializable d +and of_dtree_serializable d = + Tree_type.of_dtree_serializable of_rule_serializable d and of_binder_serializable (x, y, z) = (x, of_term_serializable y, Array.map of_term_serializable z) and of_meta_serializable t = { meta_key = t.ser_meta_key - ; meta_type = Timed.ref (of_term_serializable t.ser_meta_type) + ; meta_type = Timed.ref (of_term_serializable t.ser_meta_type) ; meta_arity = t.ser_meta_arity - ; meta_value = Timed.ref (Option.map of_mbinder_serializable t.ser_meta_value)} + ; meta_value = + Timed.ref (Option.map of_mbinder_serializable t.ser_meta_value)} and of_mbinder_serializable (x, y ,z) = (x, of_term_serializable y, Array.map of_term_serializable z) @@ -1136,19 +1169,19 @@ and of_mbinder_serializable (x, y ,z) = and of_sym_serializable s = { sym_expo = s.ser_sym_expo - ; sym_path = s.ser_sym_path - ; sym_name = s.ser_sym_name - ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) - ; sym_impl = s.ser_sym_impl - ; sym_prop = s.ser_sym_prop - ; sym_nota = Timed.ref s.ser_sym_nota - ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) - ; sym_opaq = Timed.ref s.ser_sym_opaq - ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) - ; sym_mstrat = s.ser_sym_mstrat - ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) - ; sym_pos = s.ser_sym_pos - ; sym_decl_pos = s.ser_sym_decl_pos + ; sym_path = s.ser_sym_path + ; sym_name = s.ser_sym_name + ; sym_type = Timed.ref (of_term_serializable s.ser_sym_type) + ; sym_impl = s.ser_sym_impl + ; sym_prop = s.ser_sym_prop + ; sym_nota = Timed.ref s.ser_sym_nota + ; sym_def = Timed.ref (Option.map of_term_serializable s.ser_sym_def) + ; sym_opaq = Timed.ref s.ser_sym_opaq + ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) + ; sym_mstrat = s.ser_sym_mstrat + ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) + ; sym_pos = s.ser_sym_pos + ; sym_decl_pos = s.ser_sym_decl_pos } and of_rule_serializable (r : rule_serializable) : rule = @@ -1186,8 +1219,8 @@ and of_sym_serializable s = ; sym_rules = Timed.ref [] ; sym_mstrat = Sequen ; sym_dtree = Timed.ref Tree_type.empty_dtree - ; sym_pos = - Some { fname = Some "file" + ; sym_pos = + Some { fname = Some "file" ; start_line = 0 ; start_col = 0 ; start_offset = 0 @@ -1196,7 +1229,7 @@ and of_sym_serializable s = ; end_offset = 1 } ; sym_decl_pos = - Some { fname = Some "Another/file" + Some { fname = Some "Another/file" ; start_line = 2 ; start_col = 2 ; start_offset = 2 diff --git a/src/core/term.mli b/src/core/term.mli index e1d97c3f1..9c6f99417 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -153,7 +153,7 @@ and rule = ; vars_nb : int (** Number of variables in [lhs]. *) ; xvars_nb : int (** Number of variables in [rhs] but not in [lhs]. *) ; rule_pos : Pos.popt (** Position of the rule in the source file. *) } - + (** The LHS (or pattern) of a rewriting rule is always formed of a head symbol (on which the rule is defined) applied to a list of pattern arguments. The list of arguments is given in [lhs], but the head symbol itself is @@ -487,15 +487,17 @@ type term_serializable = and mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} and binder_info = {binder_name : string; binder_bound : bool} -and binder_serializable = binder_info * term_serializable * term_serializable array +and binder_serializable = + binder_info * term_serializable * term_serializable array and meta_serializable = { ser_meta_key : int ; ser_meta_type : term_serializable (**Timed.ref. *) - ; ser_meta_arity : int + ; ser_meta_arity : int ; ser_meta_value : mbinder_serializable option (** Timed.ref. *) } -and mbinder_serializable = mbinder_info * term_serializable * term_serializable array +and mbinder_serializable = + mbinder_info * term_serializable * term_serializable array and rule_serializable = { ser_lhs : term_serializable list diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index 3286a2544..b19225851 100644 --- a/src/core/tree_type.ml +++ b/src/core/tree_type.ml @@ -217,8 +217,9 @@ let rec to_tree_serializable (f : 'a -> 'b) (t : 'a tree) Option.map (to_tree_serializable f) default } -let rec of_tree_serializable (f : 'a -> 'a_serializable) (t : 'a tree_serializable) - : 'a_serializabe tree = +let rec of_tree_serializable + (f : 'a -> 'a_serializable) (t : 'a tree_serializable) + : 'a_serializabe tree = match t with | Fail_s -> Fail @@ -261,15 +262,17 @@ 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 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 = +let of_dtree_serializable ((f : 'a_serialisable -> 'a)) + ((n, t) :'a_serialisable dtree_serializable) + : 'a dtree = ( lazy n , lazy (of_tree_serializable f t) ) From 4e16dc852dd2d3cfb55f5caff0ab54b375474872 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Fri, 10 Apr 2026 12:41:37 +0200 Subject: [PATCH 15/26] read sign_deps in json file --- src/common/path.ml | 6 ++++++ src/core/sign.ml | 39 +++++++++++++++++++++++++++++++-------- 2 files changed, 37 insertions(+), 8 deletions(-) diff --git a/src/common/path.ml b/src/common/path.ml index e2fd3acdc..00db7c1d3 100644 --- a/src/common/path.ml +++ b/src/common/path.ml @@ -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/core/sign.ml b/src/core/sign.ml index 46f6df173..e0c2b31a4 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -363,14 +363,37 @@ let read : string -> t = fun fname -> json_sign |> Yojson.Safe.Util.member "sign_symbols" |> Yojson.Safe.Util.to_assoc - |> List.fold_left (fun acc (k, v) -> - match sym_of_yojson v with - | Ok sym -> StrMap.add k sym acc - | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) - ) StrMap.empty - in - let sign = create (sign_path) in - let sign = {sign with sign_symbols = Timed.ref sign_symbols} in + |> List.fold_left + (fun acc (k, v) -> + match sym_of_yojson v with + | Ok sym -> StrMap.add k sym acc + | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) + ) StrMap.empty + in + + let sign_deps = + json_sign + |> Yojson.Safe.Util.member "sign_deps" + |> Yojson.Safe.Util.to_assoc + |> List.fold_left (fun acc (s,j) -> + let p = Path.Path.make s in + match dep_data_of_yojson j with + | Ok dep_data -> Path.Map.add p dep_data acc + | Error e -> failwith ("Erreur sur " ^ s ^ ": " ^ e) + ) + Path.Map.empty + (* (fun acc (_, _v) -> + (* match dep_data_of_yojson v with + | Ok d -> Path.Map.add "k" d acc + | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) *) + ) Path.Map.empty *) + + in + + let sign = create (sign_path) in + let sign = + {sign with sign_symbols = Timed.ref sign_symbols + ; sign_deps = Timed.ref sign_deps } in (* READ sign_symbols and update sign *) From 24498c5b01de548729e7be54fbbe4c7c422e2a47 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Fri, 10 Apr 2026 12:46:41 +0200 Subject: [PATCH 16/26] read sign_builtins from json file --- src/core/sign.ml | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index e0c2b31a4..decb88420 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -75,7 +75,7 @@ type dep_data = type t = { sign_symbols : sym StrMap.t ref (*OK*) ; sign_path : Path.t (*OK*) - ; sign_deps : dep_data Path.Map.t ref + ; sign_deps : dep_data Path.Map.t ref (*OK*) ; sign_builtins : sym StrMap.t ref ; sign_ind : ind_data SymMap.t ref ; sign_cp_pos : cp_pos list SymMap.t ref } @@ -382,18 +382,26 @@ let read : string -> t = fun fname -> | Error e -> failwith ("Erreur sur " ^ s ^ ": " ^ e) ) Path.Map.empty - (* (fun acc (_, _v) -> - (* match dep_data_of_yojson v with - | Ok d -> Path.Map.add "k" d acc - | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) *) - ) Path.Map.empty *) + in + let sign_builtins = + json_sign + |> Yojson.Safe.Util.member "sign_builtins" + |> Yojson.Safe.Util.to_assoc + |> List.fold_left + (fun acc (k, v) -> + match sym_of_yojson v with + | Ok sym -> StrMap.add k sym acc + | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) + ) StrMap.empty in + let sign = create (sign_path) in let sign = {sign with sign_symbols = Timed.ref sign_symbols - ; sign_deps = Timed.ref sign_deps } in + ; sign_deps = Timed.ref sign_deps + ; sign_builtins = Timed.ref sign_builtins } in (* READ sign_symbols and update sign *) From 5fcb20d3c38e2d4e2af4c9c244db0d2d374677eb Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Mon, 13 Apr 2026 11:10:46 +0200 Subject: [PATCH 17/26] wip : t_serializable in sign.ml --- src/core/sign.ml | 109 ++++++++++++++++++- src/core/term.ml | 266 ++++++++++++++++++++++++++-------------------- src/core/term.mli | 11 +- 3 files changed, 270 insertions(+), 116 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index decb88420..98f813e5b 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -59,6 +59,64 @@ let strmap_of_yojson of_elt (json : Yojson.Safe.t) 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 Symdata_StrMap_serializable = struct +include StrMap +let strMap_serializable_to_yojson m = + strmap_to_yojson sym_data_to_yojson m +let strMap_serializable_to_yojson m = + strmap_of_yojson sym_data_of_yojson m +end *) + (** Data associated to a dependency. *) type dep_data = { dep_symbols : sym_data StrMap.t @@ -69,6 +127,50 @@ type dep_data = ; dep_open : bool } [@@deriving yojson] +type t_serializable = + { ser_sign_symbols : sym_serializable StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_serializable_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_serializable_of_yojson j] + ; ser_sign_path : Path.t + ; ser_sign_deps : dep_data Path.Map.t + [@to_yojson fun m -> + pathmap_to_yojson dep_data_to_yojson m] + [@of_yojson fun m -> + pathmap_of_yojson dep_data_of_yojson m] + ; ser_sign_builtins : sym_serializable StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_serializable_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_serializable_of_yojson j] + (* ; ser_sign_ind : ind_data SymMap.t *) + ; ser_sign_cp_pos : cp_pos list SymMap.t + [@to_yojson fun m -> + symmap_to_yojson (fun lst -> + `List (List.map (fun elt -> cp_pos_to_yojson elt) lst) + ) m + ] + [@of_yojson fun json -> + symmap_of_yojson + (fun j -> + match j with + | `List lst -> + let rec aux acc = function + | [] -> Ok (List.rev acc) + | x :: xs -> + (match cp_pos_of_yojson x with + | Ok v -> aux (v :: acc) xs + | Error e -> Error e) + in + aux [] lst + | _ -> Error "Expected list for cp_pos list" + ) + json + ] + } + [@@deriving yojson] + (** Representation of a signature, that is, what is introduced by a module/file. Signatures must be created with the functions [create] or [read] below only.*) @@ -76,9 +178,12 @@ type t = { sign_symbols : sym StrMap.t ref (*OK*) ; sign_path : Path.t (*OK*) ; sign_deps : dep_data Path.Map.t ref (*OK*) - ; sign_builtins : sym StrMap.t ref + ; sign_builtins : sym StrMap.t ref (*OK*) ; 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 + } + (* [@@deriving yojson] *) + (** [mem sign name] checks whether a symbol named [name] exists in [sign]. *) let mem : t -> string -> bool = fun sign name -> diff --git a/src/core/term.ml b/src/core/term.ml index 2c0fdf654..cdddc9714 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -263,6 +263,75 @@ and meta = ; meta_arity : int (** Arity (environment size). *) ; meta_value : mbinder option Timed.ref (** Definition. *) } + +type term_serializable = + | Ser_Vari of var + | Ser_Bvar of bvar + | Ser_Type + | Ser_Kind + | Ser_Symb of sym_serializable + | Ser_Prod of term_serializable * binder_serializable + | Ser_Abst of term_serializable * binder_serializable + | Ser_Appl of term_serializable * term_serializable + | Ser_Meta of meta_serializable * term_serializable array + | Ser_Patt of int option * string * term_serializable array + | Ser_Wild + | Ser_Plac of bool + | Ser_TRef of term_serializable option + | Ser_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 = + { ser_meta_key : int + ; ser_meta_type : term_serializable + ; ser_meta_arity : int + ; ser_meta_value : mbinder_serializable option + } [@@deriving yojson] + +and mbinder_serializable = + mbinder_info + * term_serializable + * term_serializable array + [@@deriving yojson] + +and rule_serializable = + { ser_lhs : term_serializable list + ; ser_names : string array + ; ser_rhs : term_serializable + ; ser_arity : int + ; ser_arities : int array + ; ser_vars_nb : int + ; ser_xvars_nb : int + ; ser_rule_pos : Pos.popt + }[@@deriving yojson] + +and dtree_serializable = + rule_serializable Tree_type.dtree_serializable [@@deriving yojson] + +and sym_serializable = + { ser_sym_expo : expo + ; ser_sym_path : Path.t + ; ser_sym_name : string + ; ser_sym_type : term_serializable + ; ser_sym_impl : bool list + ; ser_sym_prop : prop + ; ser_sym_nota : float notation (*Timed.ref*) + ; ser_sym_def : term_serializable option (*Timed.ref*) + ; ser_sym_opaq : bool (*Timed.ref*) + ; ser_sym_rules : rule_serializable list (* Timed.ref *) + ; ser_sym_mstrat: match_strat + ; ser_sym_dtree : dtree_serializable (* Timed.ref *) + ; ser_sym_pos : Pos.popt + ; ser_sym_decl_pos : Pos.popt + } [@@deriving yojson] + + let binder_name : binder -> string = fun (bi,_,_) -> bi.binder_name let mbinder_names : mbinder -> string array = fun (bi,_,_) -> bi.mbinder_name @@ -942,123 +1011,11 @@ type sym_rule = sym * rule let lhs : sym_rule -> term = fun (s, r) -> add_args (mk_Symb s) r.lhs 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 - -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 - first). *) -type ctxt = (var * term * term option) list - -let decl ppf (v,a,d) = - out ppf "%a: %a" var v term a; - match d with - | None -> () - | Some d -> out ppf " ≔ %a" term d - -let ctxt : ctxt pp = fun ppf c -> List.pp decl ", " ppf (List.rev c) -(** Type of unification constraints. *) -type constr = ctxt * term * term -(** Representation of unification problems. *) -type problem_aux = - { to_solve : constr list - (** List of unification problems to solve. *) - ; unsolved : constr list - (** List of unification problems that could not be solved. *) - ; recompute : bool - (** Indicates whether unsolved problems should be rechecked. *) - ; metas : MetaSet.t - (** Set of unsolved metas. *) } -type problem = problem_aux Timed.ref -(** Create a new empty problem. *) -let new_problem : unit -> problem = fun () -> - Timed.ref - {to_solve = []; unsolved = []; recompute = false; metas = MetaSet.empty} -(** Printing functions for debug. *) -module Raw = struct - let sym = sym let _ = sym - let term = term let _ = term - let ctxt = ctxt let _ = ctxt -end - -type term_serializable = - | Ser_Vari of var - | Ser_Bvar of bvar - | Ser_Type - | Ser_Kind - | Ser_Symb of sym_serializable - | Ser_Prod of term_serializable * binder_serializable - | Ser_Abst of term_serializable * binder_serializable - | Ser_Appl of term_serializable * term_serializable - | Ser_Meta of meta_serializable * term_serializable array - | Ser_Patt of int option * string * term_serializable array - | Ser_Wild - | Ser_Plac of bool - | Ser_TRef of term_serializable option - | Ser_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 = - { ser_meta_key : int - ; ser_meta_type : term_serializable - ; ser_meta_arity : int - ; ser_meta_value : mbinder_serializable option - } [@@deriving yojson] - -and mbinder_serializable = - mbinder_info - * term_serializable - * term_serializable array - [@@deriving yojson] - -and rule_serializable = - { ser_lhs : term_serializable list - ; ser_names : string array - ; ser_rhs : term_serializable - ; ser_arity : int - ; ser_arities : int array - ; ser_vars_nb : int - ; ser_xvars_nb : int - ; ser_rule_pos : Pos.popt - }[@@deriving yojson] - -and dtree_serializable = - rule_serializable Tree_type.dtree_serializable [@@deriving yojson] - -and sym_serializable = - { ser_sym_expo : expo - ; ser_sym_path : Path.t - ; ser_sym_name : string - ; ser_sym_type : term_serializable - ; ser_sym_impl : bool list - ; ser_sym_prop : prop - ; ser_sym_nota : float notation (*Timed.ref*) - ; ser_sym_def : term_serializable option (*Timed.ref*) - ; ser_sym_opaq : bool (*Timed.ref*) - ; ser_sym_rules : rule_serializable list (* Timed.ref *) - ; ser_sym_mstrat: match_strat - ; ser_sym_dtree : dtree_serializable (* Timed.ref *) - ; ser_sym_pos : Pos.popt - ; ser_sym_decl_pos : Pos.popt - } [@@deriving yojson] let rec to_term_serializable t = match t with | Vari x -> Ser_Vari x @@ -1199,11 +1156,94 @@ and of_sym_serializable s = let sym_to_yojson s = sym_serializable_to_yojson (to_sym_serializable s) - let sym_of_yojson j = + 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 + + + + + + + + + + + + + + + + + + + + + + + +(** 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 + [@@deriving yojson] + +(** 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 + first). *) +type ctxt = (var * term * term option) list + +let decl ppf (v,a,d) = + out ppf "%a: %a" var v term a; + match d with + | None -> () + | Some d -> out ppf " ≔ %a" term d + +let ctxt : ctxt pp = fun ppf c -> List.pp decl ", " ppf (List.rev c) + +(** Type of unification constraints. *) +type constr = ctxt * term * term + +(** Representation of unification problems. *) +type problem_aux = + { to_solve : constr list + (** List of unification problems to solve. *) + ; unsolved : constr list + (** List of unification problems that could not be solved. *) + ; recompute : bool + (** Indicates whether unsolved problems should be rechecked. *) + ; metas : MetaSet.t + (** Set of unsolved metas. *) } + +type problem = problem_aux Timed.ref + +(** Create a new empty problem. *) +let new_problem : unit -> problem = fun () -> + Timed.ref + {to_solve = []; unsolved = []; recompute = false; metas = MetaSet.empty} + +(** Printing functions for debug. *) +module Raw = struct + let sym = sym let _ = sym + let term = term let _ = term + let ctxt = ctxt let _ = ctxt +end + let dump_term = Type let sym_dump = { diff --git a/src/core/term.mli b/src/core/term.mli index 9c6f99417..ea79319cf 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -448,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 @@ -534,6 +536,13 @@ val sym_dump : sym 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 + val dump_term : term \ No newline at end of file From 9e930c80c175470ca082e5b4b29ed7e95e105e97 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 14 Apr 2026 11:21:20 +0200 Subject: [PATCH 18/26] use ppx-deriving to import/export sign.t --- src/core/sign.ml | 183 +++++++++++++++++++++++++---------------------- 1 file changed, 96 insertions(+), 87 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index 98f813e5b..42abe0c2e 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -9,10 +9,31 @@ module J = Yojson.Basic (** Data associated to inductive types. *) type ind_data = { ind_cons : sym list (** Constructors. *) + [@to_yojson fun m -> `List (List.map sym_to_yojson m)] + [@of_yojson fun j -> + match j with + |`List l -> + let rec aux acc l = + begin match l with + | [] -> Ok acc + | el :: lt -> begin match sym_of_yojson el with + | Ok x -> aux (x :: acc) lt + | Error e -> Error e + end + end + in + aux [] l + |_ -> Error "Expected list of sym_json" + ] ; ind_prop : sym (** Induction principle. *) + [@to_yojson fun m -> + sym_to_yojson m] + [@of_yojson fun j -> + sym_of_yojson j] ; 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] type sym_data = { rules : rule list @@ -127,32 +148,61 @@ type dep_data = ; dep_open : bool } [@@deriving yojson] -type t_serializable = - { ser_sign_symbols : sym_serializable StrMap.t +(** Representation of a signature, that is, what is introduced by a + module/file. Signatures must be created with the functions [create] or + [read] below only.*) +(* type t = + { sign_symbols : sym StrMap.t ref (*OK*) + ; sign_path : Path.t (*OK*) + ; sign_deps : dep_data Path.Map.t ref (*OK*) + ; sign_builtins : sym StrMap.t ref (*OK*) + ; sign_ind : ind_data SymMap.t ref + ; sign_cp_pos : cp_pos list SymMap.t ref + } *) + + type t = + { sign_symbols : sym StrMap.t ref [@to_yojson fun m -> - strmap_to_yojson sym_serializable_to_yojson m] + strmap_to_yojson sym_to_yojson (Timed.(!)m)] [@of_yojson fun j -> - strmap_of_yojson sym_serializable_of_yojson j] - ; ser_sign_path : Path.t - ; ser_sign_deps : dep_data Path.Map.t + match (strmap_of_yojson sym_of_yojson j) with + |Ok x -> Ok (Timed.ref x) + | Error e -> Error e + ] + ; sign_path : Path.t + ; sign_deps : dep_data Path.Map.t ref [@to_yojson fun m -> - pathmap_to_yojson dep_data_to_yojson m] + pathmap_to_yojson dep_data_to_yojson (Timed.(!)m)] [@of_yojson fun m -> - pathmap_of_yojson dep_data_of_yojson m] - ; ser_sign_builtins : sym_serializable StrMap.t + match pathmap_of_yojson dep_data_of_yojson m with + | Ok x -> Ok (ref x) + | Error e -> Error e ] + ; sign_builtins : sym StrMap.t ref [@to_yojson fun m -> - strmap_to_yojson sym_serializable_to_yojson m] + strmap_to_yojson sym_to_yojson !m] [@of_yojson fun j -> - strmap_of_yojson sym_serializable_of_yojson j] - (* ; ser_sign_ind : ind_data SymMap.t *) - ; ser_sign_cp_pos : cp_pos list SymMap.t + match strmap_of_yojson sym_of_yojson j with + | Ok x -> Ok (ref x) + | Error e -> Error e ] + ; sign_ind : ind_data SymMap.t ref + [@to_yojson fun m -> + symmap_to_yojson ind_data_to_yojson !m + ] + [@of_yojson fun json -> + match symmap_of_yojson + (ind_data_of_yojson + ) json with + | Ok x -> Ok (ref x) + | Error e -> Error e + ] + ; sign_cp_pos : cp_pos list SymMap.t ref [@to_yojson fun m -> symmap_to_yojson (fun lst -> `List (List.map (fun elt -> cp_pos_to_yojson elt) lst) - ) m + ) !m ] [@of_yojson fun json -> - symmap_of_yojson + match symmap_of_yojson (fun j -> match j with | `List lst -> @@ -166,24 +216,36 @@ type t_serializable = aux [] lst | _ -> Error "Expected list for cp_pos list" ) - json + json with + | Ok x -> Ok (ref x) + | Error e -> Error e ] } [@@deriving yojson] -(** Representation of a signature, that is, what is introduced by a - module/file. Signatures must be created with the functions [create] or - [read] below only.*) -type t = - { sign_symbols : sym StrMap.t ref (*OK*) - ; sign_path : Path.t (*OK*) - ; sign_deps : dep_data Path.Map.t ref (*OK*) - ; sign_builtins : sym StrMap.t ref (*OK*) - ; sign_ind : ind_data SymMap.t ref - ; sign_cp_pos : cp_pos list SymMap.t ref - } - (* [@@deriving yojson] *) +let to_yojson_with_version (t : t) (version : string) = + match to_yojson 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 -> + of_yojson (`Assoc (List.remove_assoc "version" fields)) + |_ -> raise (Failure "Unknown po format. + Field version missing or corrupted file") (** [mem sign name] checks whether a symbol named [name] exists in [sign]. *) let mem : t -> string -> bool = fun sign name -> @@ -430,7 +492,7 @@ let write : t -> string -> unit = fun sign fname -> match Unix.fork () with | 0 -> let oc = open_out fname in unlink sign; - let sign_json = toJson sign in + let sign_json = to_yojson sign 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]; *) @@ -450,68 +512,15 @@ let read : string -> t = fun fname -> let sign = try let json_sign = Yojson.Safe.from_channel ic in - let version = - json_sign - |> Yojson.Safe.Util.member "version" - |> Yojson.Safe.Util.to_string in - if version <> Version.version then - raise (Failure - ("Version " ^ version ^ " found but " ^ - Version.version ^ "expected (current)")); - let sign_path = - json_sign - |> Yojson.Safe.Util.member "sign_path" - |> Yojson.Safe.Util.to_list - |> List.map Yojson.Safe.Util.to_string in - - let sign_symbols = - json_sign - |> Yojson.Safe.Util.member "sign_symbols" - |> Yojson.Safe.Util.to_assoc - |> List.fold_left - (fun acc (k, v) -> - match sym_of_yojson v with - | Ok sym -> StrMap.add k sym acc - | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) - ) StrMap.empty - in - - let sign_deps = - json_sign - |> Yojson.Safe.Util.member "sign_deps" - |> Yojson.Safe.Util.to_assoc - |> List.fold_left (fun acc (s,j) -> - let p = Path.Path.make s in - match dep_data_of_yojson j with - | Ok dep_data -> Path.Map.add p dep_data acc - | Error e -> failwith ("Erreur sur " ^ s ^ ": " ^ e) - ) - Path.Map.empty - in - - let sign_builtins = - json_sign - |> Yojson.Safe.Util.member "sign_builtins" - |> Yojson.Safe.Util.to_assoc - |> List.fold_left - (fun acc (k, v) -> - match sym_of_yojson v with - | Ok sym -> StrMap.add k sym acc - | Error e -> failwith ("Erreur sur " ^ k ^ ": " ^ e) - ) StrMap.empty - in - - - let sign = create (sign_path) in - let sign = - {sign with sign_symbols = Timed.ref sign_symbols - ; sign_deps = Timed.ref sign_deps - ; sign_builtins = Timed.ref sign_builtins } in + let sign = of_yojson json_sign in (* READ sign_symbols and update sign *) (* let sign = Marshal.from_channel ic in *) - close_in ic; sign + close_in ic; + match sign with + | Ok sign -> sign + | Error e -> raise (Failure e) with Failure msg -> close_in ic; fatal_no_pos From 7cb2c831d653f9e7f07e8253a9323e844bf03b94 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 14 Apr 2026 12:00:24 +0200 Subject: [PATCH 19/26] sumplify term.t by removing unliked fields --- src/core/term.ml | 45 ++++----------------------------------------- src/core/term.mli | 5 ----- 2 files changed, 4 insertions(+), 46 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index cdddc9714..55882a00c 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -266,18 +266,13 @@ and meta = type term_serializable = | Ser_Vari of var - | Ser_Bvar of bvar | Ser_Type | Ser_Kind | Ser_Symb of sym_serializable | Ser_Prod of term_serializable * binder_serializable | Ser_Abst of term_serializable * binder_serializable | Ser_Appl of term_serializable * term_serializable - | Ser_Meta of meta_serializable * term_serializable array | Ser_Patt of int option * string * term_serializable array - | Ser_Wild - | Ser_Plac of bool - | Ser_TRef of term_serializable option | Ser_LLet of term_serializable * term_serializable * binder_serializable [@@deriving yojson] @@ -1019,7 +1014,6 @@ let rhs : sym_rule -> term = fun (_, r) -> r.rhs let rec to_term_serializable t = match t with | Vari x -> Ser_Vari x - | Bvar x -> Ser_Bvar x | Type -> Ser_Type | Kind -> Ser_Kind | Symb x -> Ser_Symb (to_sym_serializable x) @@ -1029,31 +1023,17 @@ let rec to_term_serializable t = match t with (to_term_serializable x, to_binder_serializable y) | Appl (x, y) ->Ser_Appl (to_term_serializable x, to_term_serializable y) - | Meta (x, y) ->Ser_Meta - ((to_meta_serializable x), Array.map to_term_serializable y) | Patt (x, y, z) -> Ser_Patt (x, y, Array.map to_term_serializable z) - | Wild -> Ser_Wild - | Plac x -> Ser_Plac x - | TRef x -> Ser_TRef (Option.map to_term_serializable (Timed.(!) x)) | LLet (x, y, z) -> Ser_LLet (to_term_serializable x , to_term_serializable y , to_binder_serializable z) + | _ -> assert false and to_dtree_serializable d = Tree_type.to_dtree_serializable (fun x -> to_rule_serializable x) d and to_binder_serializable (x, y, z) = (x, to_term_serializable y, Array.map to_term_serializable z) -and to_meta_serializable t = - { ser_meta_key = t.meta_key - ; ser_meta_type = to_term_serializable (Timed.(!) t.meta_type) - ; ser_meta_arity = t.meta_arity - ; ser_meta_value = - (Option.map to_mbinder_serializable (Timed.(!)t.meta_value))} - -and to_mbinder_serializable (x, y ,z) = - (x, to_term_serializable y, Array.map to_term_serializable z) - and to_sym_serializable s = { ser_sym_expo = s.sym_expo @@ -1085,23 +1065,16 @@ and to_rule_serializable (r : rule) : rule_serializable = } let rec of_term_serializable t = match t with | Ser_Vari x -> Vari x - | Ser_Bvar x -> Bvar x | Ser_Type -> Type | Ser_Kind -> Kind | Ser_Symb x -> Symb (of_sym_serializable x) | Ser_Prod (x, y) -> Prod - (of_term_serializable x, of_binder_serializable y) + (of_term_serializable x, of_binder_serializable y) | Ser_Abst (x, y) -> Abst - (of_term_serializable x, of_binder_serializable y) + (of_term_serializable x, of_binder_serializable y) | Ser_Appl (x, y) -> Appl - (of_term_serializable x, of_term_serializable y) - | Ser_Meta (x, y) -> Meta - ((of_meta_serializable x) - , Array.map of_term_serializable y) + (of_term_serializable x, of_term_serializable y) | Ser_Patt (x, y, z) -> Patt (x, y, Array.map of_term_serializable z) - | Ser_Wild -> Wild - | Ser_Plac x -> Plac x - | Ser_TRef x -> TRef(Timed.ref (Option.map of_term_serializable x)) | Ser_LLet (x, y, z) -> LLet (of_term_serializable x , of_term_serializable y @@ -1113,16 +1086,6 @@ and of_dtree_serializable d = and of_binder_serializable (x, y, z) = (x, of_term_serializable y, Array.map of_term_serializable z) -and of_meta_serializable t = - { meta_key = t.ser_meta_key - ; meta_type = Timed.ref (of_term_serializable t.ser_meta_type) - ; meta_arity = t.ser_meta_arity - ; meta_value = - Timed.ref (Option.map of_mbinder_serializable t.ser_meta_value)} - -and of_mbinder_serializable (x, y ,z) = - (x, of_term_serializable y, Array.map of_term_serializable z) - and of_sym_serializable s = { sym_expo = s.ser_sym_expo diff --git a/src/core/term.mli b/src/core/term.mli index ea79319cf..6692edb44 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -472,18 +472,13 @@ end type term_serializable = | Ser_Vari of var - | Ser_Bvar of bvar | Ser_Type | Ser_Kind | Ser_Symb of sym_serializable | Ser_Prod of term_serializable * binder_serializable | Ser_Abst of term_serializable * binder_serializable | Ser_Appl of term_serializable * term_serializable - | Ser_Meta of meta_serializable * term_serializable array | Ser_Patt of int option * string * term_serializable array - | Ser_Wild - | Ser_Plac of bool - | Ser_TRef of term_serializable option | Ser_LLet of term_serializable * term_serializable * binder_serializable and mbinder_info = {mbinder_name : string array; mbinder_bound : bool array} From fbd2f076cbf3e26cc17e41787788b547270501ff Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 14 Apr 2026 12:07:06 +0200 Subject: [PATCH 20/26] remove ser_sym_dtree from sym serialisable --- src/core/term.ml | 9 +-------- src/core/term.mli | 1 - 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index 55882a00c..30e2fcf22 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -321,7 +321,6 @@ and sym_serializable = ; ser_sym_opaq : bool (*Timed.ref*) ; ser_sym_rules : rule_serializable list (* Timed.ref *) ; ser_sym_mstrat: match_strat - ; ser_sym_dtree : dtree_serializable (* Timed.ref *) ; ser_sym_pos : Pos.popt ; ser_sym_decl_pos : Pos.popt } [@@deriving yojson] @@ -1029,8 +1028,6 @@ let rec to_term_serializable t = match t with , to_binder_serializable z) | _ -> assert false -and to_dtree_serializable d = - Tree_type.to_dtree_serializable (fun x -> to_rule_serializable x) d and to_binder_serializable (x, y, z) = (x, to_term_serializable y, Array.map to_term_serializable z) @@ -1047,7 +1044,6 @@ and to_sym_serializable s = ; ser_sym_opaq = Timed.(!)s.sym_opaq ; ser_sym_rules = List.map to_rule_serializable (Timed.(!)s.sym_rules) ; ser_sym_mstrat = s.sym_mstrat - ; ser_sym_dtree = to_dtree_serializable (Timed.(!)s.sym_dtree) ; ser_sym_pos = s.sym_pos ; ser_sym_decl_pos = s.sym_decl_pos } @@ -1080,9 +1076,6 @@ let rec of_term_serializable t = match t with , of_term_serializable y , of_binder_serializable z) -and of_dtree_serializable d = - Tree_type.of_dtree_serializable of_rule_serializable d - and of_binder_serializable (x, y, z) = (x, of_term_serializable y, Array.map of_term_serializable z) @@ -1099,7 +1092,7 @@ and of_sym_serializable s = ; sym_opaq = Timed.ref s.ser_sym_opaq ; sym_rules = Timed.ref (List.map of_rule_serializable s.ser_sym_rules) ; sym_mstrat = s.ser_sym_mstrat - ; sym_dtree = Timed.ref (of_dtree_serializable s.ser_sym_dtree) + ; sym_dtree = Timed.ref (Tree_type.empty_dtree) ; sym_pos = s.ser_sym_pos ; sym_decl_pos = s.ser_sym_decl_pos } diff --git a/src/core/term.mli b/src/core/term.mli index 6692edb44..837878f24 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -519,7 +519,6 @@ and sym_serializable = ; ser_sym_opaq : bool (* Timed.ref *) ; ser_sym_rules : rule_serializable list (* Timed.ref*) ; ser_sym_mstrat: match_strat - ; ser_sym_dtree : dtree_serializable ; ser_sym_pos : Pos.popt ; ser_sym_decl_pos : Pos.popt } From ba5841bbf3e8ba58752506ee086df41570e82d2d Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 14 Apr 2026 12:11:47 +0200 Subject: [PATCH 21/26] use json with version --- src/core/sign.ml | 28 +++------------------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/src/core/sign.ml b/src/core/sign.ml index 42abe0c2e..160ad0872 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -224,7 +224,7 @@ type dep_data = [@@deriving yojson] -let to_yojson_with_version (t : t) (version : string) = +let to_yojson_with_version (t : t) (version : string) : Yojson.Safe.t = match to_yojson t with | `Assoc fields -> `Assoc (("version", `String version) :: fields) @@ -462,28 +462,6 @@ let strip_private : t -> unit = fun sign -> sign.sign_symbols := StrMap.filter (fun _ s -> not_prv s) !(sign.sign_symbols) -let toJson sign : Yojson.Safe.t = - let rules_assoc = - StrMap.bindings (Timed.(!)sign.sign_symbols) - |> List.map (fun (k, v) -> (k, sym_to_yojson v)) - in - let dep_data_assoc = - Path.Map.bindings (Timed.(!) sign.sign_deps) - |>List.map (fun (k, v) -> - (Format.asprintf "%a" Path.Path.pp k, dep_data_to_yojson v)) - in - let sign_builtins = - StrMap.bindings (Timed.(!)sign.sign_builtins) - |> List.map (fun (k, v) -> (k, sym_to_yojson v)) - in - `Assoc [ - "version" , `String Version.version - ; "sign_path" , `List (List.map (fun s -> `String s) sign.sign_path) - ; ("sign_symbols", `Assoc rules_assoc) - ; ("sign_deps", `Assoc dep_data_assoc) - ; ("sign_builtins", `Assoc sign_builtins) - ] - (** [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 @@ -492,7 +470,7 @@ let write : t -> string -> unit = fun sign fname -> match Unix.fork () with | 0 -> let oc = open_out fname in unlink sign; - let sign_json = to_yojson sign in + 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]; *) @@ -512,7 +490,7 @@ let read : string -> t = fun fname -> let sign = try let json_sign = Yojson.Safe.from_channel ic in - let sign = of_yojson json_sign in + let sign = of_yojson_with_version json_sign in (* READ sign_symbols and update sign *) From 5e8e9605a43c5503d22c91c63d153ea9f71a73ea Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 15 Apr 2026 08:27:58 +0200 Subject: [PATCH 22/26] wip: move serialization code to dedicated file --- src/core/sig_serialize.ml | 161 ++++++++++++++++++++++++++++++++++++++ src/core/sign.ml | 155 +----------------------------------- src/handle/compile.ml | 5 +- 3 files changed, 165 insertions(+), 156 deletions(-) create mode 100644 src/core/sig_serialize.ml diff --git a/src/core/sig_serialize.ml b/src/core/sig_serialize.ml new file mode 100644 index 000000000..fb225f43d --- /dev/null +++ b/src/core/sig_serialize.ml @@ -0,0 +1,161 @@ +open Sign +open Term +open Lplib.Extra +open Common +open Error +open Timed + + +(** [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; + 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 -> t = fun fname -> + let ic = open_in fname in + let sign = + 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 = + 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 + + +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 = {rules=[rule]; nota=None} in + let 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 160ad0872..8976a4e92 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 module J = Yojson.Basic @@ -462,106 +462,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; - 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 -> t = fun fname -> - let ic = open_in fname in - let sign = - 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 = - 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 @@ -658,56 +558,3 @@ let rec dependencies : t -> (Path.t * t) list = fun sign -> | d::deps -> minimize ((List.filter not_here d) :: acc) deps in List.concat (minimize [] deps) - -let%test "rev" = - let rule = - {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 = {rules=[rule]; nota=None} in - let 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/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); From 17ed6bb9a6b9ecd4b95c0b24fca6f1b829278e03 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 15 Apr 2026 10:53:19 +0200 Subject: [PATCH 23/26] with sin_serializable --- src/core/sig_serialize.ml | 78 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 75 insertions(+), 3 deletions(-) diff --git a/src/core/sig_serialize.ml b/src/core/sig_serialize.ml index fb225f43d..797b63a7c 100644 --- a/src/core/sig_serialize.ml +++ b/src/core/sig_serialize.ml @@ -6,8 +6,80 @@ open Error open Timed + type t = + { sign_symbols : sym StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_of_yojson j] + ; sign_path : Path.t + ; sign_deps : dep_data Path.Map.t + [@to_yojson fun m -> + pathmap_to_yojson dep_data_to_yojson m] + [@of_yojson fun m -> + pathmap_of_yojson dep_data_of_yojson m ] + ; sign_builtins : sym StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_of_yojson j ] + ; sign_ind : ind_data SymMap.t + [@to_yojson fun m -> + symmap_to_yojson ind_data_to_yojson m + ] + [@of_yojson fun json -> + symmap_of_yojson + (ind_data_of_yojson + ) json + ] + ; sign_cp_pos : cp_pos list SymMap.t + [@to_yojson fun m -> + symmap_to_yojson (fun lst -> + `List (List.map (fun elt -> cp_pos_to_yojson elt) lst) + ) m + ] + [@of_yojson fun json -> + symmap_of_yojson + (fun j -> + match j with + | `List lst -> + let rec aux acc = function + | [] -> Ok (List.rev acc) + | x :: xs -> + (match cp_pos_of_yojson x with + | Ok v -> aux (v :: acc) xs + | Error e -> Error e) + in + aux [] lst + | _ -> Error "Expected list for cp_pos list" + ) + json + ] + } + [@@deriving yojson] + +let to_sign_serializable (s:Sign.t) : t = + { sign_symbols = Timed.(!)s.sign_symbols + ; sign_path = s.sign_path + ; sign_deps = Timed.(!)s.sign_deps + ; sign_builtins = Timed.(!)s.sign_builtins + ; sign_ind = 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 s.sign_deps + ; sign_builtins = Timed.ref s.sign_builtins + ; sign_ind = Timed.ref s.sign_ind + ; sign_cp_pos = Timed.ref s.sign_cp_pos + } + + + (** [write sign file] writes the signature [sign] to the file [fname]. *) -let write : t -> string -> unit = fun sign 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. *) @@ -29,9 +101,9 @@ let write s n = Debug.(record_time Writing (fun () -> write s n)) 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 read : string -> Sign.t = fun fname -> let ic = open_in fname in - let sign = + let sign:Sign.t = try let json_sign = Yojson.Safe.from_channel ic in let sign = of_yojson_with_version json_sign in From 1ac15e5c906988de7373d0ab09fbd5178f328267 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 15 Apr 2026 11:00:11 +0200 Subject: [PATCH 24/26] wip : move to/of_yojson --- src/core/sig_serialize.ml | 27 ++++++++++++ src/core/sign.ml | 89 +-------------------------------------- 2 files changed, 28 insertions(+), 88 deletions(-) diff --git a/src/core/sig_serialize.ml b/src/core/sig_serialize.ml index 797b63a7c..f0732d88e 100644 --- a/src/core/sig_serialize.ml +++ b/src/core/sig_serialize.ml @@ -77,6 +77,33 @@ let of_sign_serializable (s:t) : Sign.t = } +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 -> diff --git a/src/core/sign.ml b/src/core/sign.ml index 8976a4e92..8cdac4b39 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -151,101 +151,14 @@ type dep_data = (** Representation of a signature, that is, what is introduced by a module/file. Signatures must be created with the functions [create] or [read] below only.*) -(* type t = - { sign_symbols : sym StrMap.t ref (*OK*) - ; sign_path : Path.t (*OK*) - ; sign_deps : dep_data Path.Map.t ref (*OK*) - ; sign_builtins : sym StrMap.t ref (*OK*) - ; sign_ind : ind_data SymMap.t ref - ; sign_cp_pos : cp_pos list SymMap.t ref - } *) - - type t = +type t = { sign_symbols : sym StrMap.t ref - [@to_yojson fun m -> - strmap_to_yojson sym_to_yojson (Timed.(!)m)] - [@of_yojson fun j -> - match (strmap_of_yojson sym_of_yojson j) with - |Ok x -> Ok (Timed.ref x) - | Error e -> Error e - ] ; sign_path : Path.t ; sign_deps : dep_data Path.Map.t ref - [@to_yojson fun m -> - pathmap_to_yojson dep_data_to_yojson (Timed.(!)m)] - [@of_yojson fun m -> - match pathmap_of_yojson dep_data_of_yojson m with - | Ok x -> Ok (ref x) - | Error e -> Error e ] ; sign_builtins : sym StrMap.t ref - [@to_yojson fun m -> - strmap_to_yojson sym_to_yojson !m] - [@of_yojson fun j -> - match strmap_of_yojson sym_of_yojson j with - | Ok x -> Ok (ref x) - | Error e -> Error e ] ; sign_ind : ind_data SymMap.t ref - [@to_yojson fun m -> - symmap_to_yojson ind_data_to_yojson !m - ] - [@of_yojson fun json -> - match symmap_of_yojson - (ind_data_of_yojson - ) json with - | Ok x -> Ok (ref x) - | Error e -> Error e - ] ; sign_cp_pos : cp_pos list SymMap.t ref - [@to_yojson fun m -> - symmap_to_yojson (fun lst -> - `List (List.map (fun elt -> cp_pos_to_yojson elt) lst) - ) !m - ] - [@of_yojson fun json -> - match symmap_of_yojson - (fun j -> - match j with - | `List lst -> - let rec aux acc = function - | [] -> Ok (List.rev acc) - | x :: xs -> - (match cp_pos_of_yojson x with - | Ok v -> aux (v :: acc) xs - | Error e -> Error e) - in - aux [] lst - | _ -> Error "Expected list for cp_pos list" - ) - json with - | Ok x -> Ok (ref x) - | Error e -> Error e - ] } - [@@deriving yojson] - - -let to_yojson_with_version (t : t) (version : string) : Yojson.Safe.t = - match to_yojson 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 -> - of_yojson (`Assoc (List.remove_assoc "version" fields)) - |_ -> raise (Failure "Unknown po format. - Field version missing or corrupted file") (** [mem sign name] checks whether a symbol named [name] exists in [sign]. *) let mem : t -> string -> bool = fun sign name -> From d08a0bd68643f35cb120a2be7f7f400477e0347b Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 15 Apr 2026 14:48:30 +0200 Subject: [PATCH 25/26] move ind_data and sym_data to serilizer --- src/core/sig_serialize.ml | 124 ++++++++++++++++++++++++++++++++++---- src/core/sign.ml | 47 +-------------- 2 files changed, 114 insertions(+), 57 deletions(-) diff --git a/src/core/sig_serialize.ml b/src/core/sig_serialize.ml index f0732d88e..559b56744 100644 --- a/src/core/sig_serialize.ml +++ b/src/core/sig_serialize.ml @@ -6,7 +6,100 @@ open Error open Timed - type t = +type ind_data = + { ind_cons : sym list (** Constructors. *) + [@to_yojson fun m -> `List (List.map sym_to_yojson m)] + [@of_yojson fun j -> + match j with + |`List l -> + let rec aux acc l = + begin match l with + | [] -> Ok acc + | el :: lt -> begin match sym_of_yojson el with + | Ok x -> aux (x :: acc) lt + | Error e -> Error e + end + end + in + aux [] l + |_ -> Error "Expected list of sym_json" + ] + ; ind_prop : sym (** Induction principle. *) + [@to_yojson fun m -> + sym_to_yojson m] + [@of_yojson fun j -> + sym_of_yojson j] + ; 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] + +type sym_data = + { rules : rule list + [@to_yojson fun l -> + `List (List.map + (fun r -> rule_serializable_to_yojson (to_rule_serializable r)) + l)] + [@of_yojson fun j -> + match j with + | `List lst -> + let rec aux acc = function + | [] -> Ok (List.rev acc) + | x :: xs -> + begin match rule_serializable_of_yojson x with + | Ok r_ser -> + aux (of_rule_serializable r_ser :: acc) xs + | Error e -> Error e + end + in + aux [] lst + | _ -> Error "rules: expected list"] + ; nota : float notation option }[@@deriving yojson] + +type dep_data = + { dep_symbols : sym_data StrMap.t + [@to_yojson fun m -> + strmap_to_yojson sym_data_to_yojson m] + [@of_yojson fun j -> + strmap_of_yojson sym_data_of_yojson j] + ; 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 [@to_yojson fun m -> strmap_to_yojson sym_to_yojson m] @@ -61,18 +154,24 @@ open Timed let to_sign_serializable (s:Sign.t) : t = { sign_symbols = Timed.(!)s.sign_symbols ; sign_path = s.sign_path - ; sign_deps = Timed.(!)s.sign_deps + ; sign_deps = (Path.Map.map + (fun d -> to_dep_data_serializable d) + (Timed.(!)s.sign_deps)) ; sign_builtins = Timed.(!)s.sign_builtins - ; sign_ind = Timed.(!)s.sign_ind + ; 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 s.sign_deps + ; 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 s.sign_ind + ; 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 } @@ -188,12 +287,14 @@ let read : string -> Sign.t = fun fname -> 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 + 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 = + 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 = shallow_reset_sym s; reset_ind i 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 @@ -224,8 +325,9 @@ let%test "rev" = ; end_offset = 1 } } in - let sym_data = {rules=[rule]; nota=None} in - let dep_data = {dep_symbols = (StrMap. add "key1" sym_data StrMap.empty) + 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 diff --git a/src/core/sign.ml b/src/core/sign.ml index 8cdac4b39..a23b6d32f 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -9,54 +9,14 @@ module J = Yojson.Basic (** Data associated to inductive types. *) type ind_data = { ind_cons : sym list (** Constructors. *) - [@to_yojson fun m -> `List (List.map sym_to_yojson m)] - [@of_yojson fun j -> - match j with - |`List l -> - let rec aux acc l = - begin match l with - | [] -> Ok acc - | el :: lt -> begin match sym_of_yojson el with - | Ok x -> aux (x :: acc) lt - | Error e -> Error e - end - end - in - aux [] l - |_ -> Error "Expected list of sym_json" - ] ; ind_prop : sym (** Induction principle. *) - [@to_yojson fun m -> - sym_to_yojson m] - [@of_yojson fun j -> - sym_of_yojson j] ; 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] type sym_data = { rules : rule list - [@to_yojson fun l -> - `List (List.map - (fun r -> rule_serializable_to_yojson (to_rule_serializable r)) - l)] - [@of_yojson fun j -> - match j with - | `List lst -> - let rec aux acc = function - | [] -> Ok (List.rev acc) - | x :: xs -> - begin match rule_serializable_of_yojson x with - | Ok r_ser -> - aux (of_rule_serializable r_ser :: acc) xs - | Error e -> Error e - end - in - aux [] lst - | _ -> Error "rules: expected list"] - ; nota : float notation option }[@@deriving yojson] - + ; nota : float notation option } let strmap_to_yojson to_elt (m : 'a StrMap.t) : Yojson.Safe.t = `List ( StrMap.bindings m @@ -141,12 +101,7 @@ end *) (** Data associated to a dependency. *) type dep_data = { dep_symbols : sym_data StrMap.t - [@to_yojson fun m -> - strmap_to_yojson sym_data_to_yojson m] - [@of_yojson fun j -> - strmap_of_yojson sym_data_of_yojson j] ; dep_open : bool } - [@@deriving yojson] (** Representation of a signature, that is, what is introduced by a module/file. Signatures must be created with the functions [create] or From d944d89c5f6d5b0fbba8c56805a4e81f8249201b Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Wed, 15 Apr 2026 16:41:14 +0200 Subject: [PATCH 26/26] add ppx_deriving_yojson to lambdapi dependencies --- lambdapi.opam | 1 + 1 file changed, 1 insertion(+) 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}