(Ok (term', metasenv')),ugraph1
with
| CicRefine.Uncertain _ ->
- debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
Uncertain,ugraph
- | CicRefine.RefineFailure _ ->
- debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.RefineFailure msg ->
+ debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) msg);
Ko,ugraph
| CicUnification.UnificationFailure s ->
prerr_endline ("PASSADI QUI: " ^ s);
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
- with Not_found -> assert false
+ with Not_found ->
+ failwith ("Domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
let find_in_environment name context =
Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
- | CicAst.Ident (name, subst) ->
+ | CicAst.Ident (name, subst)
+ | CicAst.Uri (name, subst) as ast ->
+ let is_uri = function CicAst.Uri _ -> true | _ -> false in
(try
+ if is_uri ast then raise Not_found;(* don't search the env for URIs *)
let index = find_in_environment name context in
if subst <> None then
CicTextualParser2.fail loc
"Explicit substitutions not allowed here";
Cic.Rel index
with Not_found ->
- let cic = resolve env (Id name) () in
+ let cic =
+ if is_uri ast then (* we have the URI, build the term out of it *)
+ try
+ CicUtil.term_of_uri name
+ with UriManager.IllFormedUri _ ->
+ CicTextualParser2.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
subst
| None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
in
- (* the try is for CicTypeChecker.typecheck *)
(try
match cic with
| Cic.Const (uri, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.Constant (_, _, _, uris) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.Variable (_, _, _, uris) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
| Cic.MutConstruct (uri, i, j, []) ->
- let uris =
- let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
- match o with
- (*match CicTypeChecker.typecheck uri with*)
- | Cic.InductiveDefinition (_, uris, _) -> uris
- | _ -> assert false
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
(*
let dom' = aux loc context term in
dom' @ dom)
[Id name] subst))
+ | CicAst.Uri _ -> []
| CicAst.Implicit -> []
| CicAst.Num (num, i) -> [ Num i ]
| CicAst.Meta (index, local_context) ->
uris
let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+ ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
res
with
CicEnvironment.CircularDependency s ->
- raise (Failure "e chi la becca sta CircularDependency?");
+ failwith "Disambiguate: circular dependency"
end