Replace Bindlib by de Bruijn indices

doc/terms.rst

@@ -16,10 +16,6 @@ An identifier can be:
 **Remark:** for any regular identifier ``i``, ``{|i|}`` and ``i`` are
 identified.
 
-**Remark:** Escaped identifiers or regular identifiers ending with a
-non-negative integer with leading zeros cannot be used for bound
-variable names.
-
 **Convention:** identifiers starting with an uppercase letter denote
 types (e.g.  ``Nat``, ``List``), and identifiers starting with a
 lowercase letter denote constructors, functions and proofs

dune-project

@@ -31,6 +31,7 @@ systems: Dedukti, Coq, HRS, CPF.")
   (menhir (>= 20200624))
   (sedlex (>= 3.2))
   (alcotest :with-test)
+  (alt-ergo :with-test)
   (dedukti (and :with-test (>= 2.7)))
   (bindlib (>= 5.0.1))
   (timed (>= 1.0))

lambdapi.opam

@@ -24,6 +24,7 @@ depends: [
   "menhir" {>= "20200624"}
   "sedlex" {>= "3.2"}
   "alcotest" {with-test}
+  "alt-ergo" {with-test}
   "dedukti" {with-test & >= "2.7"}
   "bindlib" {>= "6.0.0"}
   "timed" {>= "1.0"}

src/cli/init.ml

@@ -3,6 +3,8 @@ open Common open Error
 open Format
 open Parsing
 
+module CLT = Cmdliner.Term
+
 let write_file : string -> (formatter -> unit) -> unit = fun fn pp ->
   let oc = open_out fn in
   let ppf = formatter_of_out_channel oc in
@@ -54,7 +56,7 @@ let run : Path.t -> unit = fun root_path ->
   in
   Error.handle_exceptions run
 
-let root_path : Path.t Term.t =
+let root_path : Path.t CLT.t =
   let doc =
     "Defines the root path of the package. It is the module path under which \
      the package will be registered and installed (if desired), and it will \

src/cli/install.ml

@@ -2,6 +2,8 @@ open Cmdliner
 open Common open Library open Error
 open Parsing
 
+module CLT = Cmdliner.Term
+
 let run_command : bool -> string -> unit = fun dry_run cmd ->
   if dry_run then Console.out 1 "%s" cmd else
   match Sys.command cmd with
@@ -88,22 +90,22 @@ let run_uninstall : Config.t -> bool -> string -> unit =
   in
   Error.handle_exceptions run
 
-let dry_run : bool Term.t =
+let dry_run : bool CLT.t =
   let doc =
     "Do not install anything, only print the command that would be executed \
      if the option was not given."
   in
   Arg.(value & flag & info ["dry-run"] ~doc)
 
-let pkg_file : string Term.t =
+let pkg_file : string CLT.t =
   let doc =
     Printf.sprintf
       "Path to the package configuration file $(b,%s) corresponding to the \
        package that should be uninstalled." Package.pkg_file
   in
   Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"FILE" ~doc)
 
-let files : string list Term.t =
+let files : string list CLT.t =
   let doc =
     Printf.sprintf
       "Source file with the [%s] extension (or with the [%s] extension when \

src/common/debug.ml

@@ -46,6 +46,10 @@ module D = struct
       out ppf "]"
     end
 
+  let hashtbl : 'a pp -> 'b pp -> ('a, 'b) Hashtbl.t pp = fun key elt ->
+    let tbl ppf = Hashtbl.iter (fun k v -> out ppf "%a,%a; " key k elt v) in
+    fun ppf -> out ppf "[%a]" tbl
+
   let map : (('key -> 'elt -> unit) -> 'map -> unit)
     -> 'key pp -> string -> 'elt pp -> string -> 'map pp =
     fun iter key sep1 elt sep2 ppf m ->

src/common/logger.ml

@@ -105,3 +105,11 @@ let reset_loggers ?(default=Stdlib.(! default_loggers)) () =
 (** [log_summary ()] gives the keys and descriptions for logging options. *)
 let log_summary () =
   List.map (fun d -> (d.logger_key, d.logger_desc)) Stdlib.(!loggers)
+
+(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *)
+let set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b = fun b c f x ->
+  let is_activated = String.contains (get_activated_loggers()) in
+  let v = is_activated c in
+  let s = String.make 1 c in
+  set_debug b s;
+  try let r = f x in set_debug v s; r with e -> set_debug v s; raise e

src/common/logger.mli

@@ -31,3 +31,6 @@ val reset_loggers : ?default:string -> unit -> unit
 
 (** [log_summary ()] gives the keys and descriptions for logging options. *)
 val log_summary : unit -> (char * string) list
+
+(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *)
+val set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b

src/core/coercion.ml

@@ -11,16 +11,9 @@ let _ =
   (* Add the rule [coerce $A $A $t ↪ $t] (but we don't have access to
      the parser here) *)
   let rule =
-    let lhs =
-      [ mk_Patt (Some 0, "A", [||])
-      ; mk_Patt (Some 0, "A", [||])
-      ; mk_Patt (Some 1, "t", [||]) ]
-    in
-    let vars = [|new_tevar "A"; new_tevar "t"|] in
-    let rhs = _TEnv (_TE_Vari vars.(1)) [||] in
-    let rhs = Bindlib.(bind_mvar vars rhs |> unbox) in
-    let arity = 3 in
-    let arities = [|0; 0|] in
-    { lhs; rhs; arity; arities; vars; xvars_nb = 0; rule_pos = None }
+    let a = mk_Patt (Some 0, "A", [||])
+    and t = mk_Patt (Some 1, "t", [||]) in
+    let lhs = [a; a; t] and arities = [|0; 0|] in
+    { lhs; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0; rule_pos = None }
   in
-  Sign.add_rule Ghost.sign coerce rule
+  Sign.add_rule Ghost.sign (coerce, rule)

src/core/ctxt.ml

@@ -7,65 +7,50 @@ open Timed
 (** [type_of x ctx] returns the type of [x] in the context [ctx] when it
     appears in it, and
 @raise [Not_found] otherwise. *)
-let type_of : tvar -> ctxt -> term = fun x ctx ->
-  let (_,a,_) = List.find (fun (y,_,_) -> Bindlib.eq_vars x y) ctx in a
+let type_of : var -> ctxt -> term = fun x ctx ->
+  let (_,a,_) = List.find (fun (y,_,_) -> eq_vars x y) ctx in a
 
 (** [def_of x ctx] returns the definition of [x] in the context [ctx] if it
     appears, and [None] otherwise *)
-let rec def_of : tvar -> ctxt -> ctxt * term option = fun x c ->
+let rec def_of : var -> ctxt -> ctxt * term option = fun x c ->
   match c with
   | []         -> [], None
-  | (y,_,d)::c -> if Bindlib.eq_vars x y then c,d else def_of x c
+  | (y,_,d)::c -> if eq_vars x y then c,d else def_of x c
 
 (** [mem x ctx] tells whether variable [x] is mapped in the context [ctx]. *)
-let mem : tvar -> ctxt -> bool = fun x ->
-  List.exists (fun (y,_,_) -> Bindlib.eq_vars x y)
+let mem : var -> ctxt -> bool = fun x ->
+  List.exists (fun (y,_,_) -> eq_vars x y)
 
 (** [to_prod ctx t] builds a product by abstracting over the context [ctx], in
     the term [t]. It returns the number of products as well. *)
 let to_prod : ctxt -> term -> term * int = fun ctx t ->
   let f (t,c) (x,a,v) =
-    let b = Bindlib.bind_var x t in
+    let b = bind_var x t in
     match v with
-    | None -> _Prod (lift a) b, c + 1
-    | Some v -> _LLet (lift a) (lift v) b, c
+    | None -> mk_Prod (a, b), c + 1
+    | Some v -> mk_LLet (a, v, b), c
   in
-  let t, c = List.fold_left f (lift t, 0) ctx in
-  Bindlib.unbox t, c
-
-(** [to_prod_box bctx t] is similar to [to_prod bctx t] but operates on boxed
-    contexts and terms. *)
-let to_prod_box : bctxt -> tbox -> tbox * int = fun bctx t ->
-  let f (t, c) (x, a) =
-    let b = Bindlib.bind_var x t in
-    (_Prod a b, c + 1)
-  in
-  List.fold_left f (t, 0) bctx
-
-(** [box_context ctx] lifts context [ctx] to a boxed context. *)
-let box_context : ctxt -> bctxt =
-  List.filter_map
-    (fun (x, t, u) -> if u = None then Some (x, lift t) else None)
+  List.fold_left f (t, 0) ctx
 
 (** [to_abst ctx t] builds a sequence of abstractions over the context [ctx],
     in the term [t]. *)
 let to_abst : ctxt -> term -> term = fun ctx t ->
-  let f t (x, a, _) = _Abst (lift a) (Bindlib.bind_var x t) in
-  Bindlib.unbox (List.fold_left f (lift t) ctx)
+  let f t (x, a, _) = mk_Abst (a, bind_var x t) in
+  List.fold_left f t ctx
 
 (** [to_let ctx t] adds the defined variables of [ctx] on top of [t]. *)
 let to_let : ctxt -> term -> term = fun ctx t ->
   let f t = function
     | _, _, None -> t
-    | x, a, Some u -> _LLet (lift a) (lift u) (Bindlib.bind_var x t)
+    | x, a, Some u -> mk_LLet (a, u, bind_var x t)
   in
-  Bindlib.unbox (List.fold_left f (lift t) ctx)
+  List.fold_left f t ctx
 
 (** [sub ctx vs] returns the sub-context of [ctx] made of the variables of
     [vs]. *)
-let sub : ctxt -> tvar array -> ctxt = fun ctx vs ->
+let sub : ctxt -> var array -> ctxt = fun ctx vs ->
   let f ((x,_,_) as hyp) ctx =
-    if Array.exists (Bindlib.eq_vars x) vs then hyp::ctx else ctx
+    if Array.exists (eq_vars x) vs then hyp::ctx else ctx
   in
   List.fold_right f ctx []
 
@@ -79,9 +64,8 @@ let rec unfold : ctxt -> term -> term = fun ctx t ->
       begin
         match !(m.meta_value) with
         | None    -> t
-        | Some(b) -> unfold ctx (Bindlib.msubst b ts)
+        | Some(b) -> unfold ctx (msubst b ts)
       end
-  | TEnv(TE_Some(b), ts) -> unfold ctx (Bindlib.msubst b ts)
   | TRef(r) ->
       begin
         match !r with

src/core/dune

@@ -10,4 +10,4 @@
  (public_name lambdapi.core)
  (synopsis "LambdaPi interactive theorem prover [core]")
  (modules :standard)
- (libraries lambdapi.common lambdapi.lplib pratter bindlib why3 unix))
+ (libraries lambdapi.common lambdapi.lplib pratter why3 unix))