add tactic set (#1101)

CHANGES.md

@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Added
 
+- Add tactic `set`.
 - Add export format `raw_dk`.
 - Fix of the color of the text in command line when console.out is used.
 - Use black text instead of red when diplaying query answers.

doc/Makefile.bnf

@@ -59,6 +59,7 @@ lambdapi.bnf: Makefile.bnf ../src/parsing/lpParser.mly
 	-e 's/REQUIRE/"require"/g' \
         -e 's/RESOLVE/"resolve"/g' \
 	-e 's/REWRITE/"rewrite"/g' \
+        -e 's/SET/"set"/g' \
 	-e 's/UNIF_RULE/"unif_rule"/g' \
 	-e 's/RULE/"rule"/g' \
 	-e 's/SIDE/<side>/g' \

doc/lambdapi.bnf

@@ -146,6 +146,7 @@ QID ::= [UID "."]+ UID
            | "fail"
            | "generalize" <uid>
            | "have" <uid> ":" <term>
+           | "set" <uid> "≔" <term>
            | "induction"
            | "refine" <term>
            | "reflexivity"

doc/tactics.rst

@@ -133,6 +133,13 @@ unification algorithms will then try to instantiate some of the
 metavariables. The new metavariables that cannot be solved are added
 as new goals.
 
+.. _set:
+
+``set``
+-------
+
+``set x ≔ t`` extends the current context with ``x ≔ t``.
+
 .. _simplify:
 
 ``simplify``

editors/emacs/lambdapi-smie.el

@@ -20,6 +20,7 @@
     "reflexivity"
     "remove"
     "rewrite"
+    "set"
     "simplify"
     "solve"
     "symmetry"
@@ -98,12 +99,13 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
               ("fail")
               ("focus" ident)
               ("generalize" ident)
-              ("have" sterm)
+              ("have" ident ":" sterm)
               ("induction")
               ("refine" sterm)
               ("reflexivity")
               ("remove" ident)
               ("rewrite" "[" rw-patt "]")
+              ("set" ident "≔" sterm)
               ("simplify")
               ("simplify" ident)
               ("solve")
@@ -197,6 +199,7 @@ The default lexer is used because the syntax is primarily made of sexps."
     (`(:before . "reflexivity") `(column . ,lambdapi-indent-basic))
     (`(:before . "remove") `(column . ,lambdapi-indent-basic))
     (`(:before . "rewrite") `(column . ,lambdapi-indent-basic))
+    (`(:before . "set") `(column . ,lambdapi-indent-basic))
     (`(:before . "simplify") `(column . ,lambdapi-indent-basic))
     (`(:before . "solve") `(column . ,lambdapi-indent-basic))
     (`(:before . "symmetry") `(column . ,lambdapi-indent-basic))
@@ -222,7 +225,7 @@ The default lexer is used because the syntax is primarily made of sexps."
     (`(:after . ,(or "symbol" "inductive")) lambdapi-indent-basic)
     (`(:after . ,(or "apply" "assume" "fail" "focus" "generalize" "have"
                      "induction" "refine" "reflexivity" "remove" "rewrite"
-                     "simplify" "solve" "symmetry" "why3"))
+                     "set" "simplify" "solve" "symmetry" "why3"))
      lambdapi-indent-basic)
 
     ;; Toplevel

editors/emacs/lambdapi-vars.el

@@ -15,6 +15,7 @@
     "reflexivity"
     "remove"
     "rewrite"
+    "set"
     "simplify"
     "solve"
     "symmetry"

editors/vim/syntax/lambdapi.vim

@@ -49,8 +49,8 @@ syntax keyword KeywordOK contained end
 syntax keyword KeywordOK contained fail
 syntax keyword KeywordOK contained flag
 syntax keyword KeywordOK contained focus
-syntax keyword KeywordOK contained have
 syntax keyword KeywordOK contained generalize
+syntax keyword KeywordOK contained have
 syntax keyword KeywordOK contained in
 syntax keyword KeywordOK contained induction
 syntax keyword KeywordOK contained inductive
@@ -82,6 +82,7 @@ syntax keyword KeywordOK contained rule
 syntax keyword KeywordOK contained search
 syntax keyword KeywordOK contained search-query
 syntax keyword KeywordOK contained sequential
+syntax keyword KeywordOK contained set
 syntax keyword KeywordOK contained simplify
 syntax keyword KeywordOK contained solve
 syntax keyword KeywordOK contained symbol
@@ -116,8 +117,8 @@ syntax keyword KeywordKO contained end
 syntax keyword KeywordKO contained fail
 syntax keyword KeywordKO contained flag
 syntax keyword KeywordKO contained focus
-syntax keyword KeywordKO contained have
 syntax keyword KeywordKO contained generalize
+syntax keyword KeywordKO contained have
 syntax keyword KeywordKO contained in
 syntax keyword KeywordKO contained induction
 syntax keyword KeywordKO contained inductive
@@ -149,6 +150,7 @@ syntax keyword KeywordKO contained rule
 syntax keyword KeywordKO contained search
 syntax keyword KeywordKO contained search-query
 syntax keyword KeywordKO contained sequential
+syntax keyword KeywordKO contained set
 syntax keyword KeywordKO contained simplify
 syntax keyword KeywordKO contained solve
 syntax keyword KeywordKO contained symbol

editors/vscode/syntaxes/lp.tmLanguage.json

@@ -25,7 +25,7 @@
   ],
   "repository": {
     "commands": {
-      "match": "\\b(abort|admit|admitted|apply|as|assert|assertnot|associative|assume|begin|builtin|coerce_rule|commutative|compute|constant|debug|end|fail|flag|focus|generalize|have|in|induction|inductive|infix|injective|left|let|notation|off|on|open|opaque|postfix|prefix|print|private|proofterm|protected|prover|prover_timeout|quantifier|refine|reflexivity|remove|require|rewrite|rule|search|sequential|simplify|symbol|symmetry|try|type|TYPE|unif_rule|why3|with)\\b",
+      "match": "\\b(abort|admit|admitted|apply|as|assert|assertnot|associative|assume|begin|builtin|coerce_rule|commutative|compute|constant|debug|end|fail|flag|focus|generalize|have|in|induction|inductive|infix|injective|left|let|notation|off|on|open|opaque|postfix|prefix|print|private|proofterm|protected|prover|prover_timeout|quantifier|refine|reflexivity|remove|require|rewrite|rule|search|sequential|set|simplify|symbol|symmetry|try|type|TYPE|unif_rule|why3|with)\\b",
       "name": "keyword.control.lp"
     },
     "comments": {
@@ -44,7 +44,7 @@
     },
 
     "tactics": {
-      "match": "\\b(apply|assume|fail|focus|generalize|have|induction|refine|reflexivity|remove|rewrite|simplify|solve|symmetry|try|why3)\\b",
+      "match": "\\b(apply|assume|fail|focus|generalize|have|induction|refine|reflexivity|remove|rewrite|set|simplify|solve|symmetry|try|why3)\\b",
       "name": "keyword.control.tactics.lp"
     },
 

misc/lambdapi.tex

@@ -9,7 +9,7 @@
   tabsize=2,
   basicstyle={\ttfamily\small\upshape},
   backgroundcolor=\color{lightgrey},
-  keywords={abort,admit,admitted,apply,as,assert,assertnot,associative,assume,begin,builtin,commutative,compute,constant,debug,end,fail,flag,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,require,rewrite,right,rule,sequential,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
+  keywords={abort,admit,admitted,apply,as,assert,assertnot,associative,assume,begin,builtin,commutative,compute,constant,debug,end,fail,flag,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
   sensitive=true,
   keywordstyle=\color{blue},
   morecomment=[l]{//},

src/core/ctxt.ml

@@ -28,24 +28,25 @@ let to_prod : ctxt -> term -> term * int = fun ctx t ->
     let b = Bindlib.bind_var x t in
     match v with
     | None -> _Prod (lift a) b, c + 1
-    | Some v -> _LLet (lift a) (lift v) b, c
+    | Some v -> _LLet (lift a) (lift v) b, c + 1
   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 f (t,c) (x,a,v) =
     let b = Bindlib.bind_var x t in
-    (_Prod a b, c + 1)
+    match v with
+    | None -> _Prod a b, c + 1
+    | Some v -> _LLet a v 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.map (fun (x,t,u) -> (x,lift t,Option.map lift u))
 
 (** [to_abst ctx t] builds a sequence of abstractions over the context [ctx],
     in the term [t]. *)

src/core/env.ml

@@ -20,7 +20,7 @@ let empty : env = []
 (** [add v a t env] extends the environment [env] by mapping the string
     [Bindlib.name_of v] to [(v,a,t)]. *)
 let add : tvar -> tbox -> tbox option -> env -> env = fun v a t env ->
-  (Bindlib.name_of v, (v, a, t)) :: env
+  (Bindlib.name_of v, (v,a,t)) :: env
 
 (** [find n env] returns the Bindlib variable associated to the variable  name
     [n] in the environment [env]. If none is found, [Not_found] is raised. *)
@@ -30,16 +30,15 @@ let find : string -> env -> tvar = fun n env ->
 (** [mem n env] returns [true] iff [n] is mapped to a variable in [env]. *)
 let mem : string -> env -> bool = List.mem_assoc
 
-(** [to_prod env t] builds a sequence of products / let-bindings whose domains
-    are the variables of the environment [env] (from left to right), and whose
-    body is the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t]
-    you obtain a term of the form [Πx1:a1,..,Πxn:an,t]. *)
+(** [to_prod env t] builds a sequence of products/lets whose domains are the
+    variables of the environment [env] (from left to right), and whose body is
+    the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t] you
+    obtain a term of the form [Πx1:a1,..,Πxn:an,t]. *)
 let to_prod_box : env -> tbox -> tbox = fun env t ->
-  let add_prod t (_,(x,a,u)) =
-    let b = Bindlib.bind_var x t in
-    match u with
-    | Some u -> _LLet a u b
-    | None -> _Prod a b
+  let add_prod t (_,(x,a,d)) =
+    match d with
+    | None -> _Prod a (Bindlib.bind_var x t)
+    | Some d -> _LLet a d (Bindlib.bind_var x t)
   in
   List.fold_left add_prod t env
 
@@ -61,24 +60,21 @@ let to_abst : env -> tbox -> term = fun env t ->
   in
   Bindlib.unbox (List.fold_left add_abst t env)
 
-(** [vars env] extracts the array of the {e not defined} Bindlib variables in
-    [env]. Note that the order is reversed: [vars [(xn,an);..;(x1,a1)] =
-    [|x1;..;xn|]]. *)
+(** [vars env] extracts the array of the Bindlib variables in [env]. Note that
+    the order is reversed: [vars [(xn,an);..;(x1,a1)] = [|x1;..;xn|]]. *)
 let vars : env -> tvar array = fun env ->
-  let f (_, (x, _, u)) = if u = None then Some(x) else None in
-  Array.of_list (List.filter_rev_map f env)
+  Array.of_list (List.rev_map (fun (_,(x,_,_)) -> x) env)
 
 (** [appl t env] applies [t] to the variables of [env]. *)
 let appl : tbox -> env -> tbox = fun t env ->
   List.fold_right (fun (_,(x,_,_)) t -> _Appl t (_Vari x)) env t
 
-(** [to_tbox env] extracts the array of the {e not defined} variables in [env]
-   and injects them in the [tbox] type.  This is the same as [Array.map _Vari
-   (vars env)]. Note that the order is reversed: [to_tbox [(xn,an);..;(x1,a1)]
-   = [|x1;..;xn|]]. *)
+(** [to_tbox env] extracts the array of the variables in [env] and injects
+    them in [tbox]. This is the same as [Array.map _Vari (vars env)]. Note
+    that the order is reversed: [to_tbox [(xn,an);..;(x1,a1)] =
+    [|x1;..;xn|]]. *)
 let to_tbox : env -> tbox array = fun env ->
-  let f (_, (x, _, u)) = if u = None then Some(_Vari x) else None in
-  Array.of_list (List.filter_rev_map f env)
+  Array.of_list (List.rev_map (fun (_,(x,_,_)) -> _Vari x) env)
 
 (** [to_ctxt e] converts an environment into a context. *)
 let to_ctxt : env -> ctxt =
@@ -88,12 +84,14 @@ let to_ctxt : env -> ctxt =
 (** [match_prod c t f] returns [f a b] if [t] matches [Prod(a,b)] possibly
    after reduction.
 @raise [Invalid_argument] if [t] is not a product. *)
-let match_prod : ctxt -> term -> (term -> tbinder -> 'a) -> 'a = fun c t f ->
+let match_prod : ctxt -> term -> (term -> term option -> tbinder -> 'a) -> 'a
+  = fun c t f ->
   match unfold t with
-  | Prod(a,b) -> f a b
+  | Prod(a,b) -> f a None b
+  | LLet(a,d,b) -> f a (Some d) b
   | _ ->
       match Eval.whnf c t with
-      | Prod(a,b) -> f a b
+      | Prod(a,b) -> f a None b
       | _ -> invalid_arg __LOC__
 
 (** [of_prod c s t] returns a tuple [(env,b)] where [b] is constructed from
@@ -105,10 +103,11 @@ let match_prod : ctxt -> term -> (term -> tbinder -> 'a) -> 'a = fun c t f ->
 let of_prod : ctxt -> string -> term -> env * term = fun c s t ->
   let i = Stdlib.ref (-1) in
   let rec build_env env t =
-    try match_prod c t (fun a b ->
+    try match_prod c t (fun a d b ->
             let name = Stdlib.(incr i; s ^ string_of_int !i) in
             let x, b = LibTerm.unbind_name name b in
-            build_env (add x (lift a) None env) b)
+            build_env (add x (lift a) (Option.map lift d) env) b
+          )
     with Invalid_argument _ -> env, t
   in build_env [] t
 
@@ -123,9 +122,10 @@ let of_prod : ctxt -> string -> term -> env * term = fun c s t ->
 let of_prod_nth : ctxt -> int -> term -> env * term = fun c n t ->
   let rec build_env i env t =
     if i >= n then env, t
-    else match_prod c t (fun a b ->
+    else match_prod c t (fun a d b ->
              let x, b = Bindlib.unbind b in
-             build_env (i+1) (add x (lift a) None env) b)
+             build_env (i+1) (add x (lift a) (Option.map lift d) env) b
+           )
   in build_env 0 [] t
 
 (** [of_prod_using c xs t] is similar to [of_prod s c n t] where [n =
@@ -137,7 +137,8 @@ let of_prod_using : ctxt -> tvar array -> term -> env * term = fun c xs t ->
   let n = Array.length xs in
   let rec build_env i env t =
     if i >= n then env, t
-    else match_prod c t (fun a b ->
-             let env = add xs.(i) (lift a) None env in
-             build_env (i+1) env (Bindlib.subst b (mk_Vari(xs.(i)))))
+    else match_prod c t (fun a d b ->
+             let env = add xs.(i) (lift a) (Option.map lift d) env in
+             build_env (i+1) env (Bindlib.subst b (mk_Vari(xs.(i))))
+           )
   in build_env 0 [] t

src/core/eval.ml

@@ -122,9 +122,12 @@ let eq_modulo : (config -> term -> term) -> config -> term -> term -> bool =
     | [] -> ()
     | (a,b)::l ->
     if Logger.log_enabled () then log_conv "eq: %a ≡ %a" term a term b;
-    let a = Config.unfold cfg a and b = Config.unfold cfg b in
     if a == b then eq cfg l else
     match a, b with
+    | Vari x, Vari y when Bindlib.eq_vars x y -> eq cfg l
+    | _ ->
+    let a = Config.unfold cfg a and b = Config.unfold cfg b in
+    match a, b with
     | LLet(_,t,u), _ ->
       let x,u = Bindlib.unbind u in
       eq {cfg with varmap = VarMap.add x t cfg.varmap} ((u,b)::l)
@@ -526,20 +529,21 @@ let whnf : reducer = fun ?tags c t ->
 
 let whnf = time_reducer whnf
 
-(** [simplify t] computes a beta whnf of [t] belonging to the set S such that:
-- terms of S are in beta whnf normal format
-- if [t] is a product, then both its domain and codomain are in S. *)
-let rec simplify : term -> term = fun t ->
+(** [simplify c t] computes a beta whnf of [t] in context [c] belonging to the
+    set S such that (1) terms of S are in beta whnf normal format, (2) if [t]
+    is a product, then both its domain and codomain are in S. *)
+let simplify : ctxt -> term -> term = fun c ->
   let tags = [`NoRw; `NoExpand ] in
-  match get_args (whnf ~tags [] t) with
-  | Prod(a,b), _ ->
-     let x, b = Bindlib.unbind b in
-     mk_Prod (simplify a, bind x lift (simplify b))
-  | h, ts -> add_args_map h (whnf ~tags []) ts
+  let rec simp t =
+    match get_args (whnf ~tags c t) with
+    | Prod(a,b), _ ->
+        let x, b = Bindlib.unbind b in mk_Prod (simp a, bind x lift (simp b))
+    | h, ts -> add_args_map h (whnf ~tags c) ts
+  in simp
 
 let simplify =
-  let open Stdlib in let r = ref mk_Kind in fun t ->
-  Debug.(record_time Rewriting (fun () -> r := simplify t)); !r
+  let open Stdlib in let r = ref mk_Kind in fun c t ->
+  Debug.(record_time Rewriting (fun () -> r := simplify c t)); !r
 
 (** If [s] is a non-opaque symbol having a definition, [unfold_sym s t]
    replaces in [t] all the occurrences of [s] by its definition. *)

src/core/eval.mli

@@ -65,10 +65,10 @@ val snf : ?dtree:(sym -> dtree) -> ?tags:rw_tag list -> ctxt -> term -> term
     context [c]. *)
 val hnf : ?tags:rw_tag list -> ctxt -> term -> term
 
-(** [simplify t] computes a beta whnf of [t] belonging to the set S such that:
-    - terms of S are in beta whnf normal format
-    - if [t] is a product, then both its domain and codomain are in S. *)
-val simplify : term -> term
+(** [simplify c t] computes a beta whnf of [t] in context [c] belonging to the
+    set S such that (1) terms of S are in beta whnf normal format, (2) if [t]
+    is a product, then both its domain and codomain are in S. *)
+val simplify : ctxt -> term -> term
 
 (** If [s] is a non-opaque symbol having a definition, [unfold_sym s t]
    replaces in [t] all the occurrences of [s] by its definition. *)