- | CicNotationPt.Ident (name, subst)
- | CicNotationPt.Uri (name, subst) as ast ->
- let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
- (try
- if is_uri ast then raise Not_found;(* don't search the env for URIs *)
- let index = find_in_context name context in
- if subst <> None then
- CicNotationPt.fail loc "Explicit substitutions not allowed here";
- NCic.Rel index
- with Not_found ->
- let cic =
- if is_uri ast then (* we have the URI, build the term out of it *)
- try
- CicUtil.term_of_uri (UriManager.uri_of_string name)
- with UriManager.IllFormedUri _ ->
- CicNotationPt.fail loc "Ill formed URI"
- else
- resolve env (Id name) ()
- in
- let mk_subst uris =
- let ids_to_uris =
- List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
- in
- (match subst with
- | Some subst ->
- List.map
- (fun (s, term) ->
- (try
- List.assoc s ids_to_uris, aux ~localize loc context term
- with Not_found ->
- raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
- subst
- | None -> List.map (fun uri -> uri, NCic.Implicit None) uris)
- in
- (try
- match cic with
- | NCic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.Const (uri, mk_subst uris)
- | NCic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.Var (uri, mk_subst uris)
- | NCic.MutInd (uri, i, []) ->
- (try
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.MutInd (uri, i, mk_subst uris)
- with
- CicEnvironment.Object_not_found _ ->
- (* if we are here it is probably the case that during the
- definition of a mutual inductive type we have met an
- occurrence of the type in one of its constructors.
- However, the inductive type is not yet in the environment
- *)
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- NCic.MutInd (uri,i,[]))
- | NCic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.MutConstruct (uri, i, j, mk_subst uris)
- | NCic.Meta _ | NCic.Implicit _ as t ->
-(*
- debug_print (lazy (sprintf
- "Warning: %s must be instantiated with _[%s] but we do not enforce it"
- (CicPp.ppterm t)
- (String.concat "; "
- (List.map
- (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
- subst))));
-*)
- t
- | _ ->
- raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
- with
- CicEnvironment.CircularDependency _ ->
- raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
- | CicNotationPt.Implicit -> NCic.Implicit None
- | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
+ | CicNotationPt.Ident (name, subst) ->
+ assert (subst = None);
+ (try
+ NCic.Rel (find_in_context name context)
+ with Not_found -> resolve env (Id name) ())
+ | CicNotationPt.Uri (name, subst) ->
+ assert (subst = None);
+ (try
+ NCic.Const (NRef.reference_of_string name)
+ with NRef.IllFormedReference _ ->
+ CicNotationPt.fail loc "Ill formed reference")
+ | CicNotationPt.Implicit -> NCic.Implicit `Term
+ | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
+patterns not implemented *)