Commit 8db81520 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

the code is compiling, still not done

parent 9d2d9af5
Pipeline #1654 failed with stage
in 1 minute and 47 seconds
This diff is collapsed.
......@@ -240,75 +240,49 @@ let add_binding : type a. formula -> variable_string -> a term -> formula =
fun formula s t ->
let env' = env_add_binding formula.env s t in
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T ( collect_var u s t,
collect_var v s t ))
| B (bu,bv) ->
update_term_pair entry (B ( collect_var bu s t,
collect_var bv s t )))
formula.formula_element_list in
{ formula_element_list = f';
env = env' }
{ formula with env = env' }
(* remove_binding formula s: Remove the binding associated with s in formula. *)
let remove_binding formula s =
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T (expand_var formula.env u s,
expand_var formula.env v s))
let env' = env_remove_binding formula.env s in
| B (bu,bv) ->
update_term_pair entry (B (expand_var formula.env bu s,
expand_var formula.env bv s)))
formula.formula_element_list in
let env' = env_remove_binding formula.env s in
{ formula_element_list = f';
env = env' }
{ formula with env = env' }
(* clean_bindings formula : Remove all bindings that are unused. *)
let clean_bindings formula =
(* (\* clean_bindings formula : Remove all bindings that are unused. *\) *)
(* let clean_bindings formula = *)
let clean_bindings_aux : type a. a sort -> formula -> formula =
fun sort formula ->
(* let clean_bindings_aux : type a. a sort -> formula -> formula = *)
(* fun sort formula -> *)
let appears : type a. a sort -> variable_string -> bool = fun sort var ->
List.exists (fun el -> match el.term_pair with
| B (b,b') -> (subterm formula.env (t_var var sort) b)
|| (subterm formula.env (t_var var sort) b')
(* let appears : type a. a sort -> variable_string -> bool = fun sort var -> *)
(* List.exists (fun el -> match el.term_pair with *)
(* | B (b,b') -> (subterm formula.env (t_var var sort) b) *)
(* || (subterm formula.env (t_var var sort) b') *)
| T (u,u') -> (subterm formula.env (t_var var sort) u)
|| (subterm formula.env (t_var var sort) u'))
formula.formula_element_list in
(* | T (u,u') -> (subterm formula.env (t_var var sort) u) *)
(* || (subterm formula.env (t_var var sort) u')) *)
(* formula.formula_element_list in *)
let f_fold : type a. variable_string list -> (variable_string * a term) ->
variable_string list =
fun acc (var, t) ->
if appears (get_sort t) var then
acc
else
var :: acc in
(* let f_fold : type a. variable_string list -> (variable_string * a term) -> *)
(* variable_string list = *)
(* fun acc (var, t) -> *)
(* if appears (get_sort t) var then *)
(* acc *)
(* else *)
(* var :: acc in *)
let to_remove = match sort with
| Msg ->
List.fold_left f_fold [] (get_bindings formula.env Msg)
(* let to_remove = match sort with *)
(* | Msg -> *)
(* List.fold_left f_fold [] (get_bindings formula.env Msg) *)
| Bool ->
List.fold_left f_fold [] (get_bindings formula.env Bool) in
(* | Bool -> *)
(* List.fold_left f_fold [] (get_bindings formula.env Bool) in *)
List.fold_left remove_binding formula to_remove in
(* List.fold_left remove_binding formula to_remove in *)
clean_bindings_aux Msg formula
|> (clean_bindings_aux Bool)
(* clean_bindings_aux Msg formula *)
(* |> (clean_bindings_aux Bool) *)
......
......@@ -88,8 +88,8 @@ val add_binding : formula -> variable_string -> 'a term -> formula
(* remove_binding formula s: Remove the binding associated with s in formula. *)
val remove_binding : formula -> variable_string -> formula
(* clean_bindings formula : Remove all bindings that are unused. *)
val clean_bindings : formula -> formula
(* (\* clean_bindings formula : Remove all bindings that are unused. *\) *)
(* val clean_bindings : formula -> formula *)
(*******************)
......
......@@ -364,7 +364,6 @@ type alg = | AT of msg term | AB of boole term
(* Try to automatically apply the IfThen axiom, relying on heuristics. *)
let auto_ift state =
let goal = state.c_proof.goal in
let env = goal.env in
let new_ift side u v = match side with
| Left -> IFT (Left,u,v,[])
......@@ -390,7 +389,6 @@ let auto_ift state =
and term_auto_ift_msg side alg_list acc t =
match t.content with
| Name _ -> term_auto_ift side alg_list acc
| Var _ -> assert (false)
| Fun (s,l) ->
let new_alg_list =
......@@ -408,7 +406,6 @@ let auto_ift state =
| True -> term_auto_ift side alg_list acc
| False -> term_auto_ift side alg_list acc
| Name _ -> term_auto_ift side alg_list acc
| Var _ -> assert (false)
| EQ (u,v) ->
let acc' = (extend_ift_list side u v) @ acc in
......@@ -477,12 +474,9 @@ let weakly_normalize_proof ?collect:(c=false) state =
let w_l_t = weak_normalize env left_term
and w_r_t = weak_normalize env right_term in
let w_l_t' = if c then collect_all env w_l_t else w_l_t
and w_r_t' = if c then collect_all env w_r_t else w_r_t in
let new_rule_list =
(R (Left,left_term, w_l_t', []),i)
:: (R (Right,right_term, w_r_t', []),i)
(R (Left,left_term, w_l_t, []),i)
:: (R (Right,right_term, w_r_t, []),i)
:: rule_list in
(i+1, new_rule_list))
(0,[])
......@@ -490,15 +484,17 @@ let weakly_normalize_proof ?collect:(c=false) state =
let state' = unary_aux state rewrite_simplification_rule_list in
if c then
begin
let new_formula = clean_bindings state'.c_proof.goal in
state'
state'.c_proof.goal <- new_formula;
state'
end
else
state'
(* if c then *)
(* begin *)
(* let new_formula = clean_bindings state'.c_proof.goal in *)
(* state'.c_proof.goal <- new_formula; *)
(* state' *)
(* end *)
(* else *)
(* state' *)
(* We apply FA everywhere we can, except for the following function symbols:
......@@ -729,8 +725,11 @@ let create_guard_data_side goal encs t =
(* We add a new term binding for the guarded decryption *)
let g_t_name_suffix = match t.content with
| Var (s,Msg) -> s
| Fun("dec",[Fun (s,_);_]) -> s
(* | Var (s,Msg) -> s *)
| Fun("dec",[u;_]) ->
begin match u.content with
| Fun (s,_) -> s
| _ -> "" end
| _ -> "" in
(* We add a new term binding for the guarded decryption *)
......@@ -742,7 +741,7 @@ let create_guard_data_side goal encs t =
{ dec_term = t;
dec_term_content = m;
guard_enc_list = encs;
guarded_dec = t_var g_t_name Msg } in
guarded_dec = guarded_t } in
let new_goal = add_binding goal g_t_name guarded_t in
......@@ -760,7 +759,7 @@ let create_guard_data_side goal encs t =
|> weak_normalize c_goal.env in
match g_u.content with
| Var _ -> c_goal
(* | Var _ -> c_goal *)
| _ ->
let new_c_goal = add_binding c_goal var_fresh g_u in
......@@ -924,7 +923,10 @@ let auto_guard state sk fk =
(* Return true if t is a decryption. *)
let is_dec t = match t.content with
| Fun("dec",[_;Fun("sk",[_])]) -> true
| Fun("dec",[_;k]) ->
begin match k.content with
| Fun("sk",[_]) -> true
| _ -> false end
| _ -> false in
let (l_g_decs,r_g_decs) = List.split constr.decryptions in
......@@ -1438,13 +1440,15 @@ add_c_action
match Formula.nth state.c_proof.goal index with
| B _ -> raise Bad_argument
| T (If (b,_,_), If (b',_,_)) ->
let rule = (CS (b,b')) in
let (l_prem, r_prem) = cs_apply rule state.c_proof.goal in
| T (u, u') ->
begin match u.content, u'.content with
| If (b,_,_), If (b',_,_) ->
let rule = (CS (b,b')) in
let (l_prem, r_prem) = cs_apply rule state.c_proof.goal in
binary_aux state rule l_prem r_prem sk sk fk
binary_aux state rule l_prem r_prem sk sk fk
| _ -> raise Bad_argument)
| _ -> raise Bad_argument end)
with
| Bad_argument ->
add_error_fun rule_short_help state
......
......@@ -102,7 +102,7 @@ let rec inject : abstract process -> concrete process = function
let print_term_par ppf t =
let open Fmt in
match t with
match t.content with
| (Name (s,Msg)) -> print_term ppf t
| _ -> pf ppf "(%a)" print_term t
......@@ -238,6 +238,19 @@ let rec print_process_decl ppf decl =
(* Miscellaneous *)
(*****************)
(* var_subst s t u : Substitute s by t in u. *)
let rec var_subst : type a. name_string -> msg term -> a term -> a term =
fun s t u -> match u.content with
| Name (s',Msg) -> if s = s' then t else u
| Name (s',Bool) -> u
| Fun (s,l) -> t_fun s (List.map (var_subst s t) l)
| EQ (v,w) -> t_eq (var_subst s t v) (var_subst s t w)
| If (b,v,w) -> t_ite (var_subst s t b)
(var_subst s t v)
( var_subst s t w)
| True -> u
| False -> u
(* Substitute Var s by t in the process p.
Be careful, this does not apply the substitution in the environment! *)
let rec process_subst s t p = match p with
......@@ -415,16 +428,15 @@ let ireduce conf side =
let (l_args,env',map_fresh') =
List.fold_left2 (fun (acc_args,env,map_fresh) t arg_name ->
match t with
| Var _ -> (t :: acc_args, env, map_fresh)
| _ ->
if term_is_binded env t then
(t :: acc_args, env, map_fresh)
else
let (var, map_fresh') =
fresh_name env map_fresh side arg_name in
let env' = env_add_binding env var t in
(t_var var Msg) :: acc_args, env', map_fresh')
(t :: acc_args, env', map_fresh'))
([],env,map_fresh) l l_arg_names in
(List.rev l_args,env',map_fresh')
......@@ -469,15 +481,14 @@ let ireduce conf side =
map_fresh
acc_gp_list'
| g, Let (s, t, p') -> match collect_all env t with
| Var _ ->
| g, Let (s, t, p') ->
if term_is_binded env t then
aux_ireduce
reduced_gp_list
env
map_fresh
((g, process_subst s t p') :: acc_gp_list')
| _ ->
else
let (var, map_fresh') = fresh_name env map_fresh side s in
let env' = env_add_binding env var t in
......@@ -486,7 +497,7 @@ let ireduce conf side =
reduced_gp_list
env'
map_fresh'
((g, process_subst s (t_var var Msg) p') :: acc_gp_list') in
((g, process_subst s t p') :: acc_gp_list') in
let (gp_list',env',map_fresh') =
aux_ireduce [] conf.env conf.map_fresh conf.procs in
......@@ -877,12 +888,10 @@ let get_adv_term conf frame phi side s =
let env'' = env_add_binding env' var adv_term in
let adv_term_var = t_var var Msg in
let new_conf = { conf with env = env'';
map_fresh = map_fresh' } in
(adv_term_var, new_conf)
(adv_term, new_conf)
(* A f_conf is a configuration, the current frame (in reverse order)
and the variable term phi mapped to the current frame. *)
......@@ -995,11 +1004,9 @@ let apply_action action side f_conf =
let env' = env_add_binding env var_phi' term_phi' in
let phi' = t_var var_phi' Msg in
let f_conf_side' = { f_procs = red_new_conf.procs;
frame = norm_outputed_term :: frame;
phi = phi' } in
phi = term_phi' } in
let f_conf' = { f_conf with f_env = env';
f_map_fresh = map_fresh' } in
......
......@@ -96,12 +96,9 @@ let new_formula_element ancestor term_pair =
(******************)
(* Auxilliary functions used by fa_apply *)
let rec fa_get_s env (t : msg term) = match t with
let rec fa_get_s env (t : msg term) = match t.content with
| Name (_,Msg) -> (false, None)
| Var (s,Msg) ->
fa_get_s env (eiv env t)
| Fun (s,l) -> (true, Some (s,List.length l))
| If (_,u,v) ->
......@@ -115,7 +112,7 @@ let rec fa_get_s env (t : msg term) = match t with
let fa_apply env t t' =
let rec fa_aux (s_leave,i_leave) t = match t with
let rec fa_aux (s_leave,i_leave) t = match t.content with
| Fun (s,l) ->
if (s = s_leave) && (List.length l = i_leave) then
......@@ -137,9 +134,6 @@ let fa_apply env t t' =
"FA: all branches should start by a function or bottom" in
raise (Bad_rule (error_message,FA))
| Var (s,Msg) ->
fa_aux (s_leave,i_leave) (eiv env t)
| _ -> assert false in
match fa_get_s env t, fa_get_s env t' with
......@@ -155,11 +149,7 @@ let fa_apply env t t' =
same function or bottom" in
raise (Bad_rule (error_message,FA))
let rec b_fa_apply env b b' =
let bb = eiv env b in
let bb' = eiv env b' in
match bb,bb' with
let rec b_fa_apply env b b' = match b.content,b'.content with
| EQ(u,v), EQ(u',v') ->
bt_combine [] ((u,u') :: [(v,v')])
......@@ -171,11 +161,7 @@ let rec b_fa_apply env b b' =
raise (Bad_rule ("FA: both terms should start by the same function",FA))
let fab_apply env t t' =
let tt = eiv env t in
let tt' = eiv env t' in
match tt,tt' with
let fab_apply env t t' = match t.content,t'.content with
| If (b,u,v), If (b',u',v') ->
bt_combine [(b,b')] ((u,u') :: [(v,v')])
......@@ -207,12 +193,10 @@ let rewrite : type a b. environment -> a term -> a term -> b term
| _ -> aux_rec m
and aux_rec : type a. a term -> a term = fun m ->
match m with
and aux_rec : type a. a term -> a term = fun m -> match m.content with
| Name _ -> m
| True -> m
| False -> m
| Var _ -> ein env m aux
| Fun (s,l) ->
t_fun s (List.map aux l)
......@@ -231,10 +215,12 @@ let rewrite : type a b. environment -> a term -> a term -> b term
end
| If (b,tl,tr) ->
match aux b with
let r_b = aux b in
match r_b.content with
| True -> aux tl
| False -> aux tr
| _ as r_b -> t_ite r_b (aux tl) (aux tr) in
| _ -> t_ite r_b (aux tl) (aux tr) in
aux term
......@@ -245,9 +231,8 @@ let rewrite : type a b. environment -> a term -> a term -> b term
If is simplified by keeping only the then branch. *)
let ift_apply env u v t encs =
let rec down t = match t with
let rec down t = match t.content with
| Name (_,Msg) -> rewrite env u v t encs
| Var (_,Msg) -> ein env t down
| Fun ("enc",l) ->
if List.exists (fun x -> syntactic_equal env x t) encs then
......@@ -272,22 +257,12 @@ let ift_apply env u v t encs =
t_ite b (rewrite env u v tl encs) (down tr)
else
begin try
let exp_b = eiv env b in
match exp_b with
| EQ (bl,br) ->
let b_res = t_eq (down bl) (down br) in
if syntactic_equal env b_res exp_b then
t_ite b (down tl) (down tr)
else
t_ite b_res (down tl) (down tr)
begin match b.content with
| EQ (bl,br) ->
let b_res = t_eq (down bl) (down br) in
t_ite b_res (down tl) (down tr)
| _ -> t_ite b (down tl) (down tr)
with
| Unexpandable _ -> t_ite b (down tl) (down tr)
end
| _ -> t_ite b (down tl) (down tr) end
| _ -> assert false in
down t
......@@ -304,11 +279,10 @@ let b_ift_rule_apply env side u v b b' encs =
| Left -> b
| Right -> b' in
let next_cond = ein env apply_on (fun b ->
match b with
| EQ(tl,tr) ->
t_eq (ift_apply env u v tl encs) (ift_apply env u v tr encs )
| _ -> b) in
let next_cond = match apply_on.content with
| EQ(tl,tr) ->
t_eq (ift_apply env u v tl encs) (ift_apply env u v tr encs )
| _ -> apply_on in
match side with
| Left -> bt_combine [next_cond , b'] []
......@@ -328,16 +302,16 @@ let r_apply : type a b. environment -> a term -> a term -> side -> b term
match side, get_sort t with
| Left, Msg ->
bt_combine [] [collect_all env (rewrite env u v t encs), t']
bt_combine [] [rewrite env u v t encs, t']
| Right, Msg ->
bt_combine [] [t, collect_all env (rewrite env u v t' encs)]
bt_combine [] [t, rewrite env u v t' encs]
| Left, Bool ->
bt_combine [collect_all env (rewrite env u v t encs), t'] []
bt_combine [rewrite env u v t encs, t'] []
| Right, Bool ->
bt_combine [t, collect_all env (rewrite env u v t' encs)] []
bt_combine [t, rewrite env u v t' encs] []
else
let string_error = "R_EQU: terms are not R-equal" in
......@@ -346,11 +320,9 @@ let r_apply : type a b. environment -> a term -> a term -> side -> b term
let if_intro_apply env t t' (b,b') =
let intro_apply t b =
try match eiv env b with
| EQ (u,v) -> t_ite b (rewrite env u v t []) t
| _ -> t_ite b t t
with
| Unexpandable _ -> t_ite b t t in
match b.content with
| EQ (u,v) -> t_ite b (rewrite env u v t []) t
| _ -> t_ite b t t in
bt_combine [] [intro_apply t b, intro_apply t' b']
......@@ -445,16 +417,17 @@ let cs_apply r formula =
(fun x -> match x.term_pair with
| Formula.B _ -> (x,x)
| Formula.T (If (b,u,v), If (b',u',v')) ->
if (syntactic_equal formula.env rule_b b)
&& (syntactic_equal formula.env rule_b' b') then
( new_formula_element x (Formula.T (u,u')),
new_formula_element x (Formula.T (v,v')) )
| Formula.T (t,t') -> match t.content, t'.content with
| If (b,u,v), If (b',u',v') ->
if (syntactic_equal formula.env rule_b b)
&& (syntactic_equal formula.env rule_b' b') then
( new_formula_element x (Formula.T (u,u')),
new_formula_element x (Formula.T (v,v')) )
else
(x,x)
| Formula.T _ -> (x,x))
| _ -> (x,x))
formula.formula_element_list)
| _ -> failwith "cs_apply bad rule argument"
......@@ -465,30 +438,28 @@ let cs_apply r formula =
rewrite the If application into its else branch. *)
let rec rewrite_cond_false
: type a. environment -> boole term -> a term -> a term =
fun env b s ->
ein env s (fun t -> match t with
| False -> t
| True -> t
| Name _ -> t
| Var _ -> assert (false)
| EQ (u,v) ->
if syntactic_equal env b t then
t_false ()
else
t_eq (rewrite_cond_false env b u)
(rewrite_cond_false env b v)
fun env b t -> match t.content with
| False -> t
| True -> t
| Name _ -> t
| EQ (u,v) ->
if syntactic_equal env b t then
t_false ()
else
t_eq (rewrite_cond_false env b u)
(rewrite_cond_false env b v)
| Fun (f_s,l) -> t_fun f_s (List.map (rewrite_cond_false env b) l)
| Fun (f_s,l) -> t_fun f_s (List.map (rewrite_cond_false env b) l)
| If (b',u,v) ->
if syntactic_equal env b b' then
rewrite_cond_false env b v
| If (b',u,v) ->
if syntactic_equal env b b' then
rewrite_cond_false env b v
else
t_ite (rewrite_cond_false env b b')
(rewrite_cond_false env b u)
(rewrite_cond_false env b v))
else
t_ite (rewrite_cond_false env b b')
(rewrite_cond_false env b u)
(rewrite_cond_false env b v)
exception Bad_cond_fresh
......@@ -544,9 +515,7 @@ let cond_fresh_apply r formula = match r with
cond_fresh_term formula_element u1 u2)
formula.formula_element_list in
let (second_premise, env') = match eiv_i formula.env b 2 with
| EQ (Name (n, Msg), u) | EQ (u, Name (n, Msg)) ->
let build_prem n u =
let n_fresh = fresh_name formula.env (n ^ "_fresh") in
let env' = bind_new_type formula.env n_fresh TName in
......@@ -558,8 +527,14 @@ let cond_fresh_apply r formula = match r with
:: [ { term_pair = T (u, u);
hidden_status = false;
unitary_result = Unset } ],
env' )
env' ) in
let (second_premise, env') = match b.content with
| EQ (u,v) -> begin match v.content with
| Name (n, Msg) -> build_prem n u
| _ -> match u.content with
| Name (n,Msg) -> build_prem n v
| _ -> raise Bad_cond_fresh end
| _ -> raise Bad_cond_fresh in
(first_premise, second_premise, env')
......
This diff is collapsed.
......@@ -18,7 +18,6 @@ and _ term_cnt = private
| True : boole term_cnt
| False : boole term_cnt
| Name : name_string * 'a sort -> 'a term_cnt
| Var : variable_string * 'a sort -> 'a term_cnt
| Fun : function_symbol_string * msg term list -> msg term_cnt
| If : boole term * msg term * msg term -> msg term_cnt
| EQ : msg term * msg term -> boole term_cnt
......@@ -56,8 +55,6 @@ val t_eq : msg term -> msg term -> boole term
val t_name : name_string -> 'a sort -> 'a term
val t_var : variable_string -> 'a sort -> 'a term
val t_cst : function_symbol_string -> msg term
val t_true : unit -> boole term
......@@ -140,6 +137,8 @@ exception Not_type_checking of string
(* Return true iff s is binded in the environment. *)
val is_binded : environment -> string -> bool
val term_is_binded : environment -> 'a term -> bool
(* fresh_name env pre : Return a string s such that pre is a preffix of s, and
s is fresh in env. *)
val fresh_name : environment -> string -> string
......@@ -160,34 +159,6 @@ val type_check : 'a term -> environment -> environment
val type_check_all : environment -> msg term list -> boole term list
-> environment
(**********************)
(* Variable Expansion *)
(**********************)
exception Unexpandable of string
(* expand_var env t s: Expand in t every occurrence of the variable s into its
value in the environment env. *)
val expand_var : environment -> 'a term -> variable_string -> 'a term
(* expand_all env t: Expand the term t in the environment env. *)
val expand_all : environment -> 'a term -> 'a term
(* (\* eiv env t: Expand t if it is a variable, using the *)
(* environment env. Raise an Unexpandable (err_msg) if the variable *)
(* cannot be expanded. *\) *)
(* val eiv : environment -> 'a term -> 'a term *)
(* (\* Like eiv, but i steps. *\) *)
(* val eiv_i : environment -> 'a term -> int -> 'a term *)
(* (\* ein env t f: Apply f to t. If t is a variable tries to expand it *)
(* in the environment env before applying f. If f is the identity on the *)
(* expanded term then return the unexpanded variable. *\) *)
(* val ein : *)
(* environment -> 'a term -> ('a term -> 'a term) -> 'a term *)
(* get_head env term: return Some f, where f is the head function symbol of
term modulo if-homomorphism. Return None if it does not exists.
Warning: Bot is ignored and treaded as a Name *)
......@@ -198,16 +169,6 @@ val get_head : environment -> msg term -> function_symbol_string option
Raise No_such_binding is a binding does not exist. *)
val set_binded_names : environment -> 'a term -> 'a term
(***********************)
(* Variable Collection *)
(***********************)
(* collect_var t s t': Collect in t all subterms t' into a term variable s. *)
val collect_var : 'a term -> variable_string -> 'b term -> 'a term
(* collect_all env t: Collect in t all bindings in the environment env. *)
val collect_all : environment -> 'a term -> 'a term
(*************************)
(* Add New Term Bindings *)
......@@ -225,21 +186,6 @@ val env_add_binding : environment -> variable_string -> 'a term -> environment
val env_remove_binding : environment -> variable_string -> environment
(*********************)
(* Term Substitution *)
(*********************)
(* var_subst s u t: Replace Var s by u in t: t[u/s].
Be careful, this does not apply the substitution in the environment!
No type-checking is done. *)
val var_subst : variable_string -> msg term -> 'a term -> 'a term
(* var_bsubst s bu t: Replace Var s by bu in t: t[bu/s].
Be careful, this does not apply the substitution in the environment!
No type-checking is done.*)
val var_bsubst : variable_string -> boole term -> 'a term -> 'a term
(********************)
(* Subterm Checking *)
(********************)
......
......@@ -54,7 +54,7 @@ bterm:
| FALSE
{ Term.t_false () }
| n = NAME
{ Term.t_var n Term.Bool }