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.043s
details
Expand
smt_stats
rlimit count28
num allocs737155
time0.018000
memory5.330000
max memory5.330000
Expand
  • start[0.043s]
      let (_x_0 : Reflect.Term.t) = Reflect.Term.Const (Reflect.Term.Const_z 1)
      in
      not
      (Reflect.Term.Apply
       (Reflect.Term.Ident
        {Reflect.Uid.name = "+";
         Reflect.Uid.payload =
         "\\\\u{ffffff84}\\\\u{ffffff95}\\\\u{ffffffa6}\\\\u{ffffffbe}"},
        [_x_0; _x_0])
       = Reflect.Term.Const (Reflect.Term.Const_z 2))
  • simplify

    into
    true
    expansions
    []
    rewrite_steps
      forward_chaining
      • Unsat

      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 * int * Reflect.Term.t
        | Construct of Reflect.Uid.t * Reflect.Term.t list
        | Destruct of Reflect.Uid.t * int * int * Reflect.Uid.t option *
            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
        | Case of Reflect.Term.t * Reflect.Term.case list * Reflect.Term.t option
        | Let_tuple of Reflect.Var.t list * Reflect.Term.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.018s
      details
      Expand
      smt_stats
      rlimit count58
      num allocs3676628
      time0.008000
      memory5.890000
      max memory5.890000
      Expand
      • start[0.018s] true
      • simplify

        into
        true
        expansions
        []
        rewrite_steps
          forward_chaining
          • Unsat

          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 count58
          num allocs8643632
          time0.008000
          memory6.460000
          max memory6.460000
          Expand
          • start[0.018s] true
          • simplify

            into
            true
            expansions
            []
            rewrite_steps
              forward_chaining
              • Unsat

              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 -> int -> 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\000.\000\000\000\004\000\000\000\020\000\000\000\015\192@'prelude@\144\t pI\214\240Q\016\130\246\248H\141\156^\141\210V\255]\001w\134\016\133\129*\130\246\015meX/"},
                 [Reflect.Term.Apply
                  (Reflect.Term.Ident
                   {Reflect.Uid.name = "+";
                    Reflect.Uid.payload =
                    "\132\149\166\190\000\000\000.\000\000\000\004\000\000\000\020\000\000\000\015\192@'prelude@\144\t pI\214\240Q\016\130\246\248H\141\156^\141\210V\255]\001w\134\016\133\129*\130\246\015meX/"},
                   [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
              def-depth2
              def-ty-depth6
              call signaturemk_plus_0 (x : Int.t) (y : Int.t)
              validatedin 0.001s
              locationjupyter cell 6:1,0--69
              hashes
              mk_plus_0kLdFinGgImontBeWI2wadDPABEcHGPuDdTAscGguM5M

              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) ->
               begin match (_x : Reflect.Term.t) with
                 | Reflect.Term.Bool (_pat_87 : bool) ->
                   if _pat_87 then Reflect.Term.Bool false else Reflect.Term.Bool true
                 | Reflect.Term.Apply
                    ((_pat_85 : Reflect.Term.t), (_pat_86 : Reflect.Term.t list)) ->
                   begin match (_pat_86 : Reflect.Term.t list) with
                     | ( :: ) ((t : Reflect.Term.t), (_pat_89 : Reflect.Term.t list)) ->
                       begin match (_pat_85 : Reflect.Term.t) with
                         | Reflect.Term.Ident (_pat_90 : Reflect.Uid.t) ->
                           begin match (_pat_89 : Reflect.Term.t list) with
                             | [] ->
                               if "not" = _pat_90.Reflect.Uid.name
                               then
                                 if "\132\149\166\190\000\000\000/\000\000\000\004\000\000\000\020\000\000\000\015\192\000M'prelude@\144\t \028\185\t\162\137\187\005\184\174\178S\141\249e\015\148S\142Gk\214\244\199\228\206\007\209\025\030eu\244"
                                    = _pat_90.Reflect.Uid.payload
                                 then t
                                 else let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
                               else let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
                             | _ -> let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
                           end
                         | _ -> let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
                       end
                     | _ -> let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
                   end
                 | _ -> let (_uu__var_5 : Reflect.Term.t) = _x in _uu__var_5
               end
              def
              namemk_not
              typeReflect.Term.t -> Reflect.Term.t
              recursivefalse
              def-depth3
              def-ty-depth6
              call signaturemk_not (_x : Reflect.Term.t)
              validatedin 0.004s
              locationjupyter cell 11:2,0--127
              hashes
              mk_notoz7Zgpv5OzD9N93iSeIAMlY/lw7RX0fkNwZVGWdStVw
              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))