@@ -21,6 +21,9 @@ open Ident
2121open Zelus
2222open Deftypes
2323
24+ let unbound x =
25+ Misc. internal_error " A-normal form" Ident. fprint_t x
26+
2427type 'a tree = | Leaf of 'a | Lpar of 'a tree list
2528
2629(* the type of the accumulator *)
@@ -40,7 +43,7 @@ let rec matching eq_list ({ pat_desc } as p) ({ e_desc } as e) =
4043 | _ -> (Aux. eq_make p e) :: eq_list
4144
4245let find { renaming; subst } id =
43- try Env. find id renaming with | Not_found -> assert false
46+ try Env. find id renaming with | Not_found -> unbound id
4447
4548let rec make_pat t =
4649 match t with
@@ -94,7 +97,7 @@ let pattern funs ({ renaming; subst } as acc) ({ pat_desc } as p) =
9497 | Not_found ->
9598 try
9699 make_pat (Env. find x subst)
97- with | Not_found -> assert false in
100+ with | Not_found -> unbound x in
98101 p, acc
99102 | _ -> raise Mapfold. Fallback
100103
@@ -107,12 +110,12 @@ let expression funs ({ renaming; subst } as acc) ({ e_desc } as e) =
107110 | Not_found ->
108111 try
109112 make_exp (Env. find x subst)
110- with | Not_found -> assert false in
113+ with | Not_found -> unbound x in
111114 e, acc
112115 | _ -> raise Mapfold. Fallback
113116
114117let equation funs acc eq =
115- let ({ eq_desc } as eq), acc = Mapfold. equation_it funs acc eq in
118+ let ({ eq_desc } as eq), acc = Mapfold. equation funs acc eq in
116119 let eq = match eq_desc with
117120 | EQeq (p , e ) ->
118121 Aux. par (matching [] p e)
@@ -124,9 +127,12 @@ let vardec_list funs ({ renaming; subst } as acc) v_list =
124127 (* default value of combine function, it is not split into a tuple *)
125128 (* but a single name. The code below makes this assumption. *)
126129 let vardec v_list ({ var_name } as v ) =
127- let t = Env. find var_name subst in
130+ let n_list =
131+ try [Env. find var_name renaming]
132+ with Not_found ->
133+ try names [] (Env. find var_name subst) with Not_found -> unbound var_name in
128134 List. fold_left
129- (fun v_list n -> { v with var_name = n } :: v_list) v_list (names [] t) in
135+ (fun v_list n -> { v with var_name = n } :: v_list) v_list n_list in
130136 List. fold_left vardec [] v_list, acc
131137
132138let set_index funs acc n =
0 commit comments