- | [] -> raise (ParsingError "manca dopo variabile lambda")\r
- | c::cs -> (if c = '.' then (match read_smt vars' cs with\r
- | None, _, _ -> raise (ParsingError "manca corpo lambda")\r
- | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)\r
- | Some _, _, _ -> raise (ParsingError "???")\r
- ) else raise (ParsingError "manca . nel lambda")\r
- ))\r
+ | [] -> raise (ParsingError "Lambda expression incomplete")\r
+ | '.' :: cs -> (match read_smt (bound', free) cs with\r
+ | None, _, _ -> raise (ParsingError "Lambda body expected")\r
+ | Some [t], cs, (_, free) ->\r
+ let g, cs, free = read_garbage (bound', free) (strip_spaces cs) in\r
+ Some [mk_lam t g], cs, (bound, free)\r
+ | Some _, _, _ -> assert false\r
+ )\r
+ | _::_ -> raise (ParsingError "Expected `.` after variable in lambda"))\r