- let t_magic = [p_base, 0; p_rec, 1] in
- let compiled = compiler t_magic in
+ let compiled_base = compiler [p_base, 0]
+ and compiled_rec = compiler [p_rec, 0] in
+ (fun term env ->
+ let aux_base term =
+ match compiled_base term with
+ | None -> None
+ | Some (env', _) -> Some (env', [])
+ in
+ let rec aux term =
+ match compiled_rec term with
+ | None -> aux_base term
+ | Some (env', _) ->
+ begin
+ let acc = Env.lookup_term env' acc_name in
+ let env'' = Env.remove_name env' acc_name in
+ match aux acc with
+ | None -> aux_base term
+ | Some (base_env, rec_envl) ->
+ Some (base_env, env'' :: rec_envl)
+ end
+ in
+ match aux term with
+ | None -> None
+ | Some (base_env, rec_envl) ->
+ Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *)
+
+ | Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
+ let p_some_decls = Env.declarations_of_term p_some in
+ let none_env = List.map Env.opt_binding_of_name p_some_decls in
+ let compiled = compiler [p_some, 0] in