- let input_or_locate_uri ~title ?id () =
- match id with
- | Some id -> raise (Unbound_identifier id)
- | None -> assert false
- end
- in
- let module Disambiguate' = Disambiguate.Make(Chat) in
- let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
- let (id_to_uris, metasenv, term) =
- match
- Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
- with
- | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
- | _ -> assert false
- in
- let uris =
- match req#path with
- | "/match" -> MetadataQuery.match_term ~dbh term
- | "/hint" ->
- let status = ProofEngineTypes.initial_status term metasenv in
- let intros = PrimitiveTactics.intros_tac () in
- let subgoals = ProofEngineTypes.apply_tactic intros status in
- (match subgoals with
- | proof, [goal] ->
- let (uri,metasenv,bo,ty) = proof in
- List.map fst (MetadataQuery.hint ~dbh (proof, goal))
- | _ -> assert false)
- | "/elim" ->
- let uri =
- match term with
- | Cic.MutInd (uri, typeno, _) ->
- UriManager.string_of_uriref (uri, [typeno])
- | _ -> assert false
- in
- MetadataQuery.elim ~dbh uri
- | _ -> assert false
- in
- send_results ~id_to_uris (`Results uris) req outchan
+ let input_or_locate_uri ~title ?id () =
+ match id with
+ | Some id -> raise (Unbound_identifier id)
+ | None -> assert false
+ end
+ in
+ let module Disambiguate' = Disambiguate.Make(Chat) in
+ let ast = Grammar.Entry.parse CicNotationParser.term (Stream.of_string term_str) in
+ let (id_to_uris, metasenv, term) =
+ match
+ Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+ ~aliases:id_to_uris ast
+ with
+ | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
+ | _ -> assert false
+ in
+ let uris =
+ match req#path with
+ | "/match" -> MetadataQuery.match_term ~dbd term
+ | "/instance" -> MetadataQuery.instance ~dbd term
+ | "/hint" ->
+ let status = ProofEngineTypes.initial_status term metasenv in
+ let intros = PrimitiveTactics.intros_tac () in
+ let subgoals = ProofEngineTypes.apply_tactic intros status in
+ (match subgoals with
+ | proof, [goal] ->
+ let (uri,metasenv,bo,ty) = proof in
+ List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
+ | _ -> assert false)
+ | "/elim" ->
+ let uri =
+ match term with
+ | Cic.MutInd (uri, typeno, _) ->
+ UriManager.uri_of_uriref uri typeno None
+ | _ -> raise Not_a_MutInd
+ in
+ MetadataQuery.elim ~dbd uri
+ | _ -> assert false
+ in
+ let uris = List.map UriManager.string_of_uri uris in
+ send_results ~id_to_uris (`Results uris) req outchan
+ with
+ | Not_a_MutInd ->
+ send_results (`Error (MooglePp.pp_error "Not an inductive type"
+ ("elim requires as input an identifier corresponding to an inductive"
+ ^ " type")))
+ req outchan