module Ast = NotationPt
module NRef = NReference
-let debug_print s = prerr_endline (Lazy.force s);;
+(*let debug_print s = prerr_endline (Lazy.force s);;*)
let debug_print _ = ();;
let cic_name_of_name = function
- | Ast.Ident (n, None) -> n
+ | Ast.Ident (n,_) -> n
| _ -> assert false
;;
aux 1 context
let interpretate_term_and_interpretate_term_option (status: #NCic.status)
- ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+ ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~universe ~uri ~is_path
~localization_tbl
=
+ let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term
+ DisambiguateTypes.codomain_item) in
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
(NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
aux ~localize loc context
(NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
- | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
+ | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args)
+ | NotationPt.Appl
+ (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) ->
+ NCic.Implicit `Term
+ | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args)
+ | NotationPt.Appl (NotationPt.AttributedTerm
+ (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
+ (try
+ prerr_endline ("interpr Appl/Sym: " ^ symb);
+ let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in
+ Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*))
+ interpr (`Args cic_args)
+ with Failure err ->
+ prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err);
+ assert false)
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
| `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
- | `Exists ->
- Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
- (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
+ | `Exists -> assert false)
+ (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None))
+ (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])*)
| NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context `Term outtype in
else
let indtype_ref =
match indty_ident with
- | Some (indty_ident, _) ->
- (match Disambiguate.resolve ~env ~mk_choice
- (Id indty_ident) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
- | NCic.Implicit _ ->
- raise (Disambiguate.Try_again
- (lazy "The type of the term to be matched is still unknown"))
- | t ->
- raise (DisambiguateTypes.Invalid_choice
- (lazy (loc,"The type of the term to be matched "^
- "is not (co)inductive: " ^ status#ppterm
- ~metasenv:[] ~subst:[] ~context:[] t))))
+ | Some (_,Some r) -> r
+ | Some (_, None) ->
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| None ->
- let rec fst_constructor =
+ let rec fst_constructor concrete_pat_found =
function
- (Ast.Pattern (head, _, _), _) :: _ -> head
- | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+ | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl
+ | (Ast.Pattern (head, Some href, _), _) :: _ ->
+ head, href
+ | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl
+ | [] when concrete_pat_found -> raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| [] -> raise (Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
(DisambiguateTypes.string_of_domain_item k ^ " => " ^
description_of_alias v)) env;
*)
- (match Disambiguate.resolve ~env ~mk_choice
- (Id (fst_constructor branches)) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
- let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
- NReference.mk_indty b r
- | NCic.Implicit _ ->
- raise (Disambiguate.Try_again
- (lazy "The type of the term to be matched is still unknown"))
- | t ->
- raise (DisambiguateTypes.Invalid_choice
- (lazy (loc,
- "The type of the term to be matched is not (co)inductive: "
- ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
+ let kname,href = fst_constructor false branches in
+ let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href
+ in
+ NReference.mk_indty b href
in
let _,leftsno,itl,_,indtyp_no =
NCicEnvironment.get_checked_indtys status indtype_ref in
NCic.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0
in
- let rec sort branches cl =
+ let rec sort cno branches cl =
match cl with
[] ->
let rec analyze unused unrecognized useless =
(lazy (loc, "Missing case: " ^ name)))
| ((Ast.Wildcard, _) as branch :: _) as branches ->
branch, branches
+ | (Ast.Pattern (name',Some href,_),_) as branch :: tl ->
+ prerr_endline
+ (Printf.sprintf "analysis of %s and %s" name name');
+ (match href with
+ | NReference.Ref (curi, (NReference.Con (n,cno',_))) ->
+ (* check che la curi corrisponda alla uri del tipo induttivo *)
+ let this_indty = NReference.mk_indty true href in
+ if indtype_ref <> this_indty then
+ (prerr_endline "fail1";
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc, Printf.sprintf
+ "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s."
+ (NReference.string_of_reference indtype_ref)
+ (NReference.string_of_reference href)
+ (NReference.string_of_reference this_indty)))))
+ else
+ if cno = cno' then (prerr_endline "ok";branch, tl)
+ else
+ (prerr_endline (Printf.sprintf "skip %d %d" cno cno');
+ let found,rest = find_and_remove tl in
+ found, branch::rest)
+ | _ ->
+ (prerr_endline "fail2";
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc,"Malformed pattern: found " ^
+ (NReference.string_of_reference href) ^
+ " which is not a type constructor.")))))
| (Ast.Pattern (name',_,_),_) as branch :: tl
when name = name' ->
branch,tl
match branch with
Ast.Pattern (name,y,args),term ->
if List.length args = count_prod ty - leftsno then
- ((name,y,args),term)::sort tl cltl
+ ((name,y,args),term)::sort (cno+1) tl cltl
else
raise
(DisambiguateTypes.Invalid_choice
0 -> term
| n ->
NotationPt.Binder
- (`Lambda, (NotationPt.Ident ("_", None), None),
+ (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None),
mk_lambdas (n - 1))
in
(("wildcard",None,[]),
- mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+ mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl
in
- let branches = sort branches cl in
+ let branches = sort 1 branches cl in
NCic.Match (indtype_ref, cic_outtype, cic_term,
(List.map do_branch branches))
| NotationPt.Cast (t1, t2) ->
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
| NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
| NotationPt.Ident _
- | NotationPt.Uri _
| NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
- | NotationPt.Ident (name, subst) ->
- assert (subst = None);
- (try
- NCic.Rel (find_in_context name context)
- with Not_found ->
- try NCic.Const (List.assoc name obj_context)
- with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
- | NotationPt.Uri (uri, subst) ->
- assert (subst = None);
+ | NotationPt.Ident (name, `Rel) ->
+ (try NCic.Rel (find_in_context name context)
+ with Not_found ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> assert false)) (* bug in initialize_ast *)
+ | NotationPt.Ident (name, `Ambiguous) ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> NCic.Implicit `Closed)
+ (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *)
+ | NotationPt.Ident (name, `Uri uri) ->
(try
NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
| NotationPt.Implicit `JustOne -> NCic.Implicit `Term
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
- | NotationPt.Num (num, i) ->
- Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
+ | NotationPt.Num (num, i) ->
+ let i = HExtlib.map_option
+ (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in
+ Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num)
| NotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
- Disambiguate.resolve ~env ~mk_choice
- (Symbol (symbol, instance)) (`Args [])
+ let instance = HExtlib.map_option
+ (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc))
+ instance
+ in
+ Disambiguate.resolve ~env ~universe ~mk_choice
+ (loc (*,Symbol symbol*)) instance (`Args [])
| NotationPt.Variable _
| NotationPt.Magic _
| NotationPt.Layout _
(fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
;;
-let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
+let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri
~is_path ast ~obj_context ~localization_tbl ~mk_choice
=
let context = List.map fst context in
fst
(interpretate_term_and_interpretate_term_option status
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
~localization_tbl)
~context ast
;;
-let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri
- ~is_path ~localization_tbl ~mk_choice ~obj_context
+let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env
+ ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context
=
let context = List.map fst context in
snd
(interpretate_term_and_interpretate_term_option status
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
~localization_tbl)
~context
;;
fst
(interpretate_term_and_interpretate_term_option status
~obj_context:[] ~mk_choice:(fun _ -> assert false)
- ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+ ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty
+ ~universe:DisambiguateTypes.Environment.empty
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
let ncic_name_of_ident = function
- | Ast.Ident (name, None) -> name
+ | Ast.Ident (name,_) -> name
| _ -> assert false
;;
let interpretate_obj status
(* ?(create_dummy_ids=false) *)
- ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice
+ ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice
=
assert (context = []);
assert (is_path = false);
| NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
interpretate_term status
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
+ ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty
in
let height = (* XXX calculate *) 0 in
uri, height, [], [],
in
let cic_body =
interpretate_term status
- ~obj_context ~context ~env ~uri:None ~is_path:false
+ ~obj_context ~context ~env ~universe ~uri:None ~is_path:false
(add_binders `Lambda body)
in
let cic_type =
interpretate_term_option status
~obj_context:[]
- ~context ~env ~uri:None ~is_path:false `Type
+ ~context ~env ~universe ~uri:None ~is_path:false `Type
(HExtlib.map_option (add_binders `Pi) typ)
in
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
| bo ->
let bo =
interpretate_term status
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+ ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo
in
let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
~is_path:false t
in
(name,NCic.Decl t)::context,(name,t)::res
(fun (name,_,ty,cl) ->
let ty' =
add_params
- (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
~is_path:false ty) in
let cl' =
List.map
(fun (name,ty) ->
let ty' =
add_params
- (interpretate_term status ~obj_context ~context ~env ~uri:None
+ (interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
~is_path:false ty) in
let relevance = [] in
relevance,name,ty'
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
~is_path:false t
in
(name,NCic.Decl t)::context,(name,t)::res
let leftno = List.length params in
let ty' =
add_params
- (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
~is_path:false ty) in
let nref =
NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
List.fold_left
(fun (context,res) (name,ty,_coercion,_arity) ->
let ty =
- interpretate_term status ~obj_context ~context ~env ~uri:None
+ interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
~is_path:false ty in
let context' = (name,NCic.Decl ty)::context in
context',(name,ty)::res
NCic.Inductive (true,leftno,tyl,attrs)
;;
+let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
+ (* ast_of_alias_spec is duplicate in Disambiguate *)
+ let ast_of_alias_spec t alias = match (t,alias) with
+ | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try
+ let res = Environment.find item universe in
+ let id = match item with
+ | DisambiguateTypes.Id id -> id
+ | DisambiguateTypes.Symbol _ -> "SYM"
+ | DisambiguateTypes.Num _ -> "NUM"
+ in
+ debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
+ (List.length res)));
+ res
+ with Not_found -> [])
+ in
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ (*
+ List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])
+ *)
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ in
+ let init_pattern ~local_names = function
+ | Ast.Wildcard as t -> local_names,t
+ | Ast.Pattern (c,uri,vars) ->
+ let ln',vars' = init_vars ~local_names vars in
+ let uri' = match uri with
+ | Some _ -> uri
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id c) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ in
+ ln',Ast.Pattern (c,uri',vars')
+ in
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id id
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
+ | Ast.Num _ -> DisambiguateTypes.Num
+ | _ -> assert false
+ in
+ match t with
+ | Ast.Ident (id,(`Ambiguous|`Rel))
+ when List.mem id local_names -> Ast.Ident (id,`Rel)
+ | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else ast_of_alias_spec t (List.hd choices)
+ | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
+ | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
+ | Ast.Binder (k,(n,ty),body) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let body' = init ~local_names:(n'::local_names) body in
+ Ast.Binder (k,(n,ty'),body')
+ | Ast.Case (t,ity,oty,pl) ->
+ let t' = init ~local_names t in
+ let oty' = HExtlib.map_option (init ~local_names) oty in
+ let pl' =
+ List.map (fun (p,u) ->
+ let ns,p' = init_pattern ~local_names p in
+ p',init ~local_names:ns u) pl in
+ let ity' = HExtlib.map_option
+ (fun (ity_id,href) ->
+ let href' = match href with
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id ity_id) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ | Some _ -> href
+ in (ity_id,href')) ity
+ in Ast.Case (t',ity',oty',pl')
+ | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
+ | Ast.LetIn ((n,ty),u,v) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let u' = init ~local_names u in
+ let v' = init ~local_names:(n'::local_names) v in
+ Ast.LetIn ((n,ty'),u',v')
+ | Ast.LetRec (ik,l,t) ->
+ let recfuns =
+ List.fold_right (fun (_,(n,_),_,_) acc ->
+ cic_name_of_name n::acc) l [] in
+ let l' = List.map (fun (vl,(n,ty),u,m) ->
+ let ln',vl' = init_vars ~local_names vl in
+ let ty' = HExtlib.map_option (init ~local_names:ln') ty in
+ let ln'' = recfuns@ln' in
+ let u' = init ~local_names:ln'' u in
+ vl',(n,ty'),u',m) l in
+ let t' = init ~local_names:(recfuns@local_names) t in
+ Ast.LetRec (ik,l',t') (* XXX: t??? *)
+ | t -> t
+;;
+
+let initialize_obj ~universe ~lookup_in_library o =
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])*)
+ in
+
+ match o with
+ | Ast.Inductive (ls,itl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let indtys =
+ List.fold_right
+ (fun (name,_,_,_) acc -> name::acc) itl [] in
+ let itl' = List.map
+ (fun (name,isind,ty,cl) ->
+ let ty' = init ~local_names:ln ty in
+ let cl' =
+ List.map (fun (cname,cty) ->
+ cname, init ~local_names:(indtys@ln) cty) cl
+ in
+ name,isind,ty',cl') itl
+ in
+ Ast.Inductive (ls',itl')
+ | Ast.Theorem (flav,n,ty,bo,p) ->
+ let ty' = init ~local_names:[] ty in
+ let bo' = HExtlib.map_option (init ~local_names:[]) bo in
+ Ast.Theorem (flav,n,ty',bo',p)
+ | Ast.Record (ls,n,ty,fl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let ty' = init ~local_names:ln ty in
+ let _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) ->
+ (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl
+ in
+ let fl' = List.rev fl' in
+ Ast.Record (ls',n,ty',fl')
+;;
+
let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
+ let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
+ let local_names = List.map (fun (n,_) -> n) context in
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_term
- ~context ~metasenv ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ Disambiguate.disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+ ~initial_ugraph:() ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term status) (text,prefix_len,term)
- ~mk_localization_tbl ~expty ~subst
- in
- List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+ ~refine_thing:(refine_term status)
+ (text,prefix_len,
+ (initialize_ast ~universe ~lookup_in_library ~local_names term))
+ ~visit:Disambiguate.bfvisit
+ ~mk_localization_tbl
;;
let disambiguate_obj (status: #NCicCoercion.status)
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_obj
- ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ let obj' = initialize_obj ~universe ~lookup_in_library obj in
+ Disambiguate.disambiguate_thing
+ ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe
- ~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+ ~initial_ugraph:() ~expty:None
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+ ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
- (text,prefix_len,obj)
- ~mk_localization_tbl ~expty:None
- in
- List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+ (text,prefix_len,obj')
+ ~visit:Disambiguate.bfvisit_obj
+ ~mk_localization_tbl
;;
(*
let _ =