let rec gen_bindings_of_string_sexpr ({ expr_of_string_sexpr } as conv) b accum = function (* All bindings consumed: return accumulator in original order *) | [] -> List.rev accum (* Take first binding *) | HStringSExpr.List [HStringSExpr.Atom var; expr] :: tl -> (* Convert to an expression *) let expr = expr_of_string_sexpr conv b expr in (* Get the type of the expression *) let expr_type = Term.type_of_term expr in (* Create a variable of the identifier and the type of the expression *) let tvar = Var.mk_free_var var expr_type in (* Add bound expresssion to accumulator *) gen_bindings_of_string_sexpr conv b ((tvar, expr) :: accum) tl (* Expression must be a pair *) | e :: _ -> failwith ("Invalid expression in let binding: " ^ (string_of_t HStringSExpr.pp_print_sexpr e))