Reflection

Imandra is able to reflect its normal expressions into a special datatype from the prelude, called Reflect.Term.t. A Reflect.Term.t is a logic-mode (recursive) type that can be reasoned about, the same way lists, trees, records or any other logic-mode types can be.

In [1]:
let arith_term = [%quote 1 + 1];;

(* note: [%q x] is short for [%quote x] *)

let arith_term2 = [%q 2];;
Out[1]:
val arith_term : Reflect.Term.t = (+ 1 1)
val arith_term2 : Reflect.Term.t = 2

These two terms are distinct, because they are distinct ASTs.

In [2]:
verify (arith_term <> arith_term2);;
Out[2]:
- : bool = true
Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
rlimit count24
mk bool var5
num allocs2250821
memory5.900000
max memory6.210000
Expand
  • start[0.021s]
      not
      (Reflect.Term.Apply
       (Reflect.Term.Ident
        {Reflect.Uid.name = "+"; Reflect.Uid.payload = "\\x84\\x95\\xa6\\xbe"},
        [Reflect.Term.Const (Reflect.Term.Const_z 1);
         Reflect.Term.Const (Reflect.Term.Const_z 1)])
       = Reflect.Term.Const (Reflect.Term.Const_z 2))
  • simplify

    into
    true
    expansions
    []
    rewrite_steps
      forward_chaining
      • unsat

        (mp (asserted (not true)) (rewrite (= (not true) false)) false)

      The data type Reflect.Term.t closely mirrors Imandra's internal AST. It looks like this:

      In [3]:
      #show Reflect.Term.t
      
      Out[3]:
      type nonrec t =
          Bool of bool
        | Const of Reflect.Term.const
        | If of Reflect.Term.t * Reflect.Term.t * Reflect.Term.t
        | Apply of Reflect.Term.t * Reflect.Term.t list
        | Ident of Reflect.Uid.t
        | Tuple of Reflect.Term.t list
        | Let of { rec_ : bool;
            bindings : Reflect.Term.t Reflect.Term.binding list;
            body : Reflect.Term.t;
          }
        | Tuple_field of int * Reflect.Term.t
        | Construct of Reflect.Uid.t * Reflect.Term.t list
        | Destruct of Reflect.Uid.t * int * Reflect.Term.t
        | Is_a of Reflect.Uid.t * Reflect.Term.t
        | Field of Reflect.Uid.t * Reflect.Term.t
        | Record of (Reflect.Uid.t * Reflect.Term.t) list * Reflect.Term.t option
        | Fun of Reflect.Var.t * Reflect.Term.t
      
      In [4]:
      (* let's have some helpers, it's a bit subtle to get the Uid of "+" *)
      let ast_plus = [%quote (+)];;
      let ast_one = Reflect.Term.(Const (Const_z 1));;
      
      verify (arith_term = Reflect.Term.(Apply (ast_plus, [ast_one; ast_one])))
      
      Out[4]:
      val ast_plus : Reflect.Term.t = +
      val ast_one : Reflect.Term.t = 1
      - : bool = true
      
      Proved
      proof
      ground_instances0
      definitions0
      inductions0
      search_time
      0.017s
      details
      Expand
      smt_stats
      rlimit count54
      mk bool var5
      num allocs8708264
      memory6.470000
      max memory6.770000
      Expand
      • start[0.017s]
          Reflect.Term.Apply
          (Reflect.Term.Ident
           {Reflect.Uid.name = "+"; Reflect.Uid.payload = "\\x84\\x95\\xa6\\xbe"},
           [Reflect.Term.Const (Reflect.Term.Const_z 1);
            Reflect.Term.Const (Reflect.Term.Const_z 1)])
          =
          Reflect.Term.Apply
          (Reflect.Term.Ident
           {Reflect.Uid.name = "+"; Reflect.Uid.payload = "\\x84\\x95\\xa6\\xbe"},
           [Reflect.Term.Const (Reflect.Term.Const_z 1);
            Reflect.Term.Const (Reflect.Term.Const_z 1)])
      • simplify

        into
        true
        expansions
        []
        rewrite_steps
          forward_chaining
          • unsat

            (mp (asserted (not true)) (rewrite (= (not true) false)) false)

          Building new terms manually

          As demonstrated above, it is possible to build new terms with Reflect.Term.Apply and other constructors. However, applying functions is made difficult by the existence of Reflect.Uid.ts (a reflection of Imandra's internal unique IDs) that are impossible to guess.

          To remediate that, [%uid f] can be used to obtain the Reflect.Uid.t for a function f in scope:

          In [5]:
          let uid_plus = [%uid (+)];;
          
          let arith_term_manual = Reflect.Term.(Apply (Ident uid_plus, [[%q 1]; [%q 1]]));;
          
          verify (arith_term = arith_term_manual);;
          
          Out[5]:
          val uid_plus : Reflect.Uid.t = +
          val arith_term_manual : Reflect.Term.t = (+ 1 1)
          - : bool = true
          
          Proved
          proof
          ground_instances0
          definitions0
          inductions0
          search_time
          0.018s
          details
          Expand
          smt_stats
          rlimit count54
          mk bool var5
          num allocs16820140
          memory9.770000
          max memory10.080000
          Expand
          • start[0.018s]
              Reflect.Term.Apply
              (Reflect.Term.Ident
               {Reflect.Uid.name = "+"; Reflect.Uid.payload = "\\x84\\x95\\xa6\\xbe"},
               [Reflect.Term.Const (Reflect.Term.Const_z 1);
                Reflect.Term.Const (Reflect.Term.Const_z 1)])
              =
              Reflect.Term.Apply
              (Reflect.Term.Ident
               {Reflect.Uid.name = "+"; Reflect.Uid.payload = "\\x84\\x95\\xa6\\xbe"},
               [Reflect.Term.Const (Reflect.Term.Const_z 1);
                Reflect.Term.Const (Reflect.Term.Const_z 1)])
          • simplify

            into
            true
            expansions
            []
            rewrite_steps
              forward_chaining
              • unsat

                (mp (asserted (not true)) (rewrite (= (not true) false)) false)

              Unquote

              Now, it is possible to unquote values or other subterms inside a quoted expression. This way, quoted expressions can be parametrized. Here is a function that produces the AST x + y + 0:

              In [6]:
              let mk_plus_0 x y : Reflect.Term.t =
                  [%quote [%u x] + [%u y] + 0];;
              
              Out[6]:
              val mk_plus_0 : Int.t -> Int.t -> Reflect.Term.t = <fun>
              

              The expression [%u x] (short for [%unquote x]) pulls x from the outside scope and injects it, as an integer, into the reflected term (of type Reflect.Term.t).

              It is important to remark that this function takes integers, not ASTs. It is type-safe, you cannot produce a ill-typed expression this way!

              In [7]:
              mk_plus_0 10 50;;
              
              (* this doesn't typecheck:
              mk_plus_0 true "hello";;
              *)
              
              Out[7]:
              - : Reflect.Term.t = (+ (+ 10 50) 0)
              

              The actual AST produced by [%quote …] is significantly more verbose (click on "definition" below). Again note that x and y have type Int.t.

              In [8]:
              #h mk_plus_0;;
              
              Out[8]:
              
              

              Fun: mk_plus_0

              iml
              definition
              fun (x : Int.t) ->
               fun (y : Int.t) ->
                let (_unquoted_var_1 : Int.t) = y and (_unquoted_var_0 : Int.t) = x in
                Reflect.Term.Apply
                (Reflect.Term.Ident
                 {Reflect.Uid.name = "+";
                  Reflect.Uid.payload =
                  "\132\149\166\190\000\000\000N\000\000\000\004\000\000\000\028\000\000\000\019\192|'prelude@\144\t@bc310c4058cc3439a59f581eb4dd696b5e2e6eea796f68fa425d54e787b1834b"},
                 [Reflect.Term.Apply
                  (Reflect.Term.Ident
                   {Reflect.Uid.name = "+";
                    Reflect.Uid.payload =
                    "\132\149\166\190\000\000\000N\000\000\000\004\000\000\000\028\000\000\000\019\192|'prelude@\144\t@bc310c4058cc3439a59f581eb4dd696b5e2e6eea796f68fa425d54e787b1834b"},
                   [Reflect.Term.Const (Reflect.Term.Const_z _unquoted_var_0);
                    Reflect.Term.Const (Reflect.Term.Const_z _unquoted_var_1)]);
                  Reflect.Term.Const (Reflect.Term.Const_z 0)])
              def
              namemk_plus_0
              typeInt.t -> Int.t -> Reflect.Term.t
              recursivefalse
              call signaturemk_plus_0 (x : Int.t) (y : Int.t)
              validatedin 0.001s
              locationjupyter cell 6:1,0--69
              hashes
              mk_plus_00b829f927d32306fc2c5e2382724f8bc7fc6f72e00baef5541c0c25962b64a7e

              Instead of [%unquote x], which injects a well-typed value inside the AST, we can use [%uu x] or [%unquote_splice x] to inject an already reflected term. This doesn't guarantee type-safety anymore, so one should be careful not to create ill-typed ASTs.

              In [9]:
              (* ternary conjunction of arbitrary terms *)
              let mk_and3 x y z : Reflect.Term.t =
                  [%quote [%uu x] && [%uu y] && [%uu z]];;
              
              Out[9]:
              val mk_and3 :
                Reflect.Term.t -> Reflect.Term.t -> Reflect.Term.t -> Reflect.Term.t =
                <fun>
              
              In [10]:
              mk_and3 [%q true] [%q false] [%q true];;
              
              (* ill-typed!! Do not do that! *)
              mk_and3 [%q 1] [%q None] [%q ("hello", "world")];;
              
              Out[10]:
              - : Reflect.Term.t = (&& true (&& false true))
              - : Reflect.Term.t = (&& 1 (&& None ("hello", "world")))
              

              Quotations in patterns

              It is possible to use [%q …] in pattern position, as well as [%q? p] where p is a valid Imandra pattern. This is useful to build functions that operate on Reflect.Term.t:

              In [11]:
              (* build the negation of the reflected term "t", but with some simplifications *)
              let mk_not = function
                | [%q (not [%uu t])] -> t
                | [%q true] -> [%q false]
                | [%q false] -> [%q true]
                | t -> [%q [%uu t]]
                ;;
              
              #h mk_not;;
              
              Out[11]:
              val mk_not : Reflect.Term.t -> Reflect.Term.t = <fun>
              

              Fun: mk_not

              iml
              definition
              fun (_x : Reflect.Term.t) ->
               if Is_a(Reflect.Term.Apply, _x)
                  && Is_a(Reflect.Term.Ident, Destruct(Reflect.Term.Apply, 0, _x))
                     && (Destruct(Reflect.Term.Ident, 0,
                                  Destruct(Reflect.Term.Apply, 0, _x))).Reflect.Uid.name
                        = "not"
                        && (Destruct(Reflect.Term.Ident, 0,
                                     Destruct(Reflect.Term.Apply, 0, _x))).Reflect.Uid.payload
                           =
                           "\132\149\166\190\000\000\000N\000\000\000\004\000\000\000\028\000\000\000\019\192q'prelude@\144\t@83f6cfed887c57674af881eb149fdc44473a073eee1c9dc6beb6aa4748c8c40b"
                           && (Destruct(Reflect.Term.Apply, 1, _x)) <> []
                              && List.tl (Destruct(Reflect.Term.Apply, 1, _x)) = []
               then
                 let (t : Reflect.Term.t) = List.hd (Destruct(Reflect.Term.Apply, 1, _x))
                 in t
               else
               if Is_a(Reflect.Term.Bool, _x) && Destruct(Reflect.Term.Bool, 0, _x) = true
               then Reflect.Term.Bool false
               else
               if Is_a(Reflect.Term.Bool, _x) && Destruct(Reflect.Term.Bool, 0, _x) = false
               then Reflect.Term.Bool true
               else
                 let (t : Reflect.Term.t) = _x in
                 let (_uu__var_5 : Reflect.Term.t) = t in _uu__var_5
              def
              namemk_not
              typeReflect.Term.t -> Reflect.Term.t
              recursivefalse
              call signaturemk_not (_x : Reflect.Term.t)
              validatedin 0.002s
              locationjupyter cell 11:2,0--127
              hashes
              mk_nota615c557338154b8f1651c5377141aeefb030e3d1646c94f0e3a3e9ef1756060
              In [12]:
              mk_not [%q true];;
              mk_not [%q false];;
              mk_not [%q not true];;
              mk_not [%q not (not (not false))];;
              
              Out[12]:
              - : Reflect.Term.t = false
              - : Reflect.Term.t = true
              - : Reflect.Term.t = true
              - : Reflect.Term.t = (not (not false))