(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 =
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 ->
(*
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