- if Domain.is_empty todo_dom then
- match test_env current_env Domain.empty with
- | Ok (term, metasenv) -> [ current_env, term, metasenv ]
- | Ko | Uncertain -> []
- else
- let item = Domain.choose todo_dom in
- let remaining_dom = Domain.remove item todo_dom in
- debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
- let choices = lookup_choices item in
- let rec filter = function
- | [] -> []
- | codomain_item :: tl ->
- debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
- let new_env = Environment.add item codomain_item current_env in
- (match test_env new_env remaining_dom with
- | Ok (term, metasenv) ->
- (if Domain.is_empty remaining_dom then
- [ new_env, term, metasenv ]
- else
- aux new_env remaining_dom)
- @ filter tl
- | Uncertain ->
- (if Domain.is_empty remaining_dom then
- []
- else
- aux new_env remaining_dom)
- @ filter tl
- | Ko -> filter tl)
- in
- filter choices
+ match todo_dom with
+ | [] ->
+ (match test_env current_env [] with
+ | Ok (term, metasenv) -> [ current_env, term, metasenv ]
+ | Ko | Uncertain -> [])
+ | item :: remaining_dom ->
+ debug_print (sprintf "CHOOSED ITEM: %s"
+ (string_of_domain_item item));
+ let choices = lookup_choices item in
+ let rec filter = function
+ | [] -> []
+ | codomain_item :: tl ->
+ debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
+ let new_env =
+ Environment.add item codomain_item current_env
+ in
+ (match test_env new_env remaining_dom with
+ | Ok (term, metasenv) ->
+ (match remaining_dom with
+ | [] -> [ new_env, term, metasenv ]
+ | _ -> aux new_env remaining_dom) @ filter tl
+ | Uncertain ->
+ (match remaining_dom with
+ | [] -> []
+ | _ -> aux new_env remaining_dom) @ filter tl
+ | Ko -> filter tl)
+ in
+ filter choices