(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-open Printf
-
-open DisambiguateTypes
-open UriManager
-
+module P = Printf
+module DT = DisambiguateTypes
module Ast = NotationPt
module NRef = NReference
-let debug_print s = prerr_endline (Lazy.force s);;
-let debug_print _ = ();;
-
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
+let debug = ref false;;
+let debug_print s = if !debug then prerr_endline (Lazy.force s);;
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
| _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
;;
-let refine_term
- metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl=
+let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_coercions term expty _
+ ~localization_tbl
+=
assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
- (NCicPp.ppterm ~metasenv ~subst ~context term)));
+ debug_print (lazy (P.sprintf "TEST_INTERPRETATION: %s"
+ (status#ppterm ~metasenv ~subst ~context term)));
try
let localise t =
try NCicUntrusted.NCicHash.find localization_tbl t
with Not_found ->
- prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+ prerr_endline ("NOT LOCALISED" ^ status#ppterm ~metasenv ~subst ~context t);
(*assert false*) HExtlib.dummy_floc
in
let metasenv, subst, term, _ =
NCicRefiner.typeof
- (rdb#set_coerc_db
- (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
+ (status#set_coerc_db
+ (if use_coercions then status#coerc_db else NCicCoercion.empty_db))
metasenv subst context term expty ~localise
in
Disambiguate.Ok (term, metasenv, subst, ())
with
| NCicRefiner.Uncertain loc_msg ->
debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
- NCicPp.ppterm ~metasenv ~subst ~context term)) ;
+ status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
- debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
- (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
+ debug_print (lazy (P.sprintf "PRUNED:\nterm%s\nmessage:%s"
+ (status#ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
-let refine_obj
- ~rdb metasenv subst _context _uri
- ~use_coercions obj _ _ugraph ~localization_tbl
+let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
+ ~localization_tbl
=
+ (*prerr_endline ((P.sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
assert (metasenv=[]);
assert (subst=[]);
let localise t =
try
let obj =
NCicRefiner.typeof_obj
- (rdb#set_coerc_db
- (if use_coercions then rdb#coerc_db
+ (status#set_coerc_db
+ (if use_coercions then status#coerc_db
else NCicCoercion.empty_db))
obj ~localise
in
with
| NCicRefiner.Uncertain loc_msg ->
debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
- NCicPp.ppobj obj)) ;
+ status#ppobj obj)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
- debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
- (NCicPp.ppobj obj) (snd(Lazy.force loc_msg))));
+ debug_print (lazy (P.sprintf "PRUNED:\nobj: %s\nmessage: %s"
+ (status#ppobj obj) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
in
aux 1 context
-let interpretate_term_and_interpretate_term_option
- ?(create_dummy_ids=false)
- ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl
+let interpretate_term_and_interpretate_term_option (status: #NCic.status)
+ ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
+ ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- | NotationPt.Appl (NotationPt.Appl inner :: args) ->
- aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl
- (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
+ (NotationPt.AttributedTerm (att, inner)::args)->
aux ~localize loc context
- (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+ (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args)))
+ | NotationPt.Appl (NotationPt.Appl inner :: args) ->
+ aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
+ Disambiguate.resolve ~mk_choice ~env (DT.Symbol (symb, i)) (`Args cic_args)
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
+ Disambiguate.resolve ~env ~mk_choice (DT.Symbol ("exists", 0))
(`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
raise (DisambiguateTypes.Invalid_choice
(lazy (loc, "Syntax error: the left hand side of a "^
"branch pattern must be \"_\"")))
- ) branches
+ ) branches in
+ let indtype_ref =
+ let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in
+ NRef.reference_of_spec uri (NRef.Ind (true,1,1))
in
- (*
- NCic.MutCase (ref, cic_outtype, cic_term,
- (List.map do_branch branches))
- *) ignore branches; assert false (* patterns not implemented yet *)
+ NCic.Match (indtype_ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
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
+ (DT.Id indty_ident) (`Args []) with
+ | NCic.Const (NRef.Ref (_,NRef.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: " ^ NCicPp.ppterm
+ "is not (co)inductive: " ^ status#ppterm
~metasenv:[] ~subst:[] ~context:[] t))))
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (lazy (loc,"The type "^
+ | [] -> raise (DT.Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
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 r in
- NReference.mk_indty b r
+ (DT.Id (fst_constructor branches)) (`Args []) with
+ | NCic.Const (NRef.Ref (_,NRef.Con _) as r) ->
+ let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
+ NRef.mk_indty b r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
raise (DisambiguateTypes.Invalid_choice
(lazy (loc,
"The type of the term to be matched is not (co)inductive: "
- ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
+ ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
in
let _,leftsno,itl,_,indtyp_no =
- NCicEnvironment.get_checked_indtys indtype_ref in
+ NCicEnvironment.get_checked_indtys status indtype_ref in
let _,_,_,cl =
try
List.nth itl indtyp_no
with _ -> assert false in
let rec count_prod t =
- match NCicReduction.whd ~subst:[] [] t with
+ match NCicReduction.whd status ~subst:[] [] t with
NCic.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0
in
in
let cic_body = aux ~localize loc (cic_name :: context) body in
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
with Not_found ->
try NCic.Const (List.assoc name obj_context)
with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+ Disambiguate.resolve ~env ~mk_choice (DT.Id name) (`Args []))
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
+ NCic.Const (NRef.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
- | NotationPt.NCic t ->
- let context = (* to make metas_of_term happy *)
- List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
- assert(NCicUntrusted.metas_of_term [] context t = []); t
+ | NotationPt.NCic t -> t
| NotationPt.Implicit `Vector -> NCic.Implicit `Vector
| 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)
+ Disambiguate.resolve ~env ~mk_choice (DT.Num i) (`Num_arg num)
| NotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| NotationPt.Sort `Set -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
- | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
- [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
| NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
- | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
- [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
- (Symbol (symbol, instance)) (`Args [])
+ (DT.Symbol (symbol, instance)) (`Args [])
| NotationPt.Variable _
| NotationPt.Magic _
| NotationPt.Layout _
(fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~obj_context ~localization_tbl ~mk_choice
+let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~obj_context ~localization_tbl ~mk_choice
=
let context = List.map fst context in
fst
- (interpretate_term_and_interpretate_term_option
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ (interpretate_term_and_interpretate_term_option status
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~localization_tbl)
~context ast
;;
-let interpretate_term_option
- ?(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 ~uri
+ ~is_path ~localization_tbl ~mk_choice ~obj_context
=
let context = List.map fst context in
snd
- (interpretate_term_and_interpretate_term_option
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ (interpretate_term_and_interpretate_term_option status
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~localization_tbl)
~context
;;
-let disambiguate_path path =
+let disambiguate_path status path =
let localization_tbl = NCicUntrusted.NCicHash.create 23 in
fst
- (interpretate_term_and_interpretate_term_option
+ (interpretate_term_and_interpretate_term_option status
~obj_context:[] ~mk_choice:(fun _ -> assert false)
~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
-let new_flavour_of_flavour = function
- | `Definition -> `Definition
- | `MutualDefinition -> `Definition
- | `Fact -> `Fact
- | `Lemma -> `Lemma
- | `Remark -> `Example
- | `Theorem -> `Theorem
- | `Variant -> `Corollary
- | `Axiom -> `Fact
-;;
-
let ncic_name_of_ident = function
| Ast.Ident (name, None) -> name
| _ -> assert false
;;
-let interpretate_obj
+let interpretate_obj status
(* ?(create_dummy_ids=false) *)
~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice
=
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
+ | NotationPt.Theorem (name, ty, bo, attrs) ->
+ let _, flavour, _ = attrs in
let ty' =
- interpretate_term
+ interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
in
let height = (* XXX calculate *) 0 in
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
- (match bo with
- | NotationPt.LetRec (kind, defs, _) ->
- let inductive = kind = `Inductive in
- let _,obj_context =
- List.fold_left
- (fun (i,acc) (_,(name,_),_,k) ->
- (i+1,
- (ncic_name_of_ident name, NReference.reference_of_spec uri
- (if inductive then NReference.Fix (i,k,0)
- else NReference.CoFix i)) :: acc))
- (0,[]) defs
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t ->
- NotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- interpretate_term
- ~obj_context ~context ~env ~uri:None ~is_path:false
- (add_binders `Lambda body)
- in
- let cic_type =
- interpretate_term_option
- ~obj_context:[]
- ~context ~env ~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))
- defs
- in
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
- NCic.Fixpoint (inductive,inductiveFuns,attrs)
- | bo ->
- let bo =
- interpretate_term
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
- in
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
- NCic.Constant ([],name,Some bo,ty',attrs)))
- | NotationPt.Inductive (params,tyl) ->
+ let bo =
+ interpretate_term status
+ ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+ in
+ NCic.Constant ([],name,Some bo,ty',attrs))
+ | NotationPt.Inductive (params,tyl,source) ->
let context,params =
let context,res =
List.fold_left
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false t
in
(name,NCic.Decl t)::context,(name,t)::res
List.fold_left
(fun (i,res) (name,_,_,_) ->
let nref =
- NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+ NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno))
in
i+1,(name,nref)::res)
(0,[]) tyl) in
(fun (name,_,ty,cl) ->
let ty' =
add_params
- (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false ty) in
let cl' =
List.map
(fun (name,ty) ->
let ty' =
add_params
- (interpretate_term ~obj_context ~context ~env ~uri:None
+ (interpretate_term status ~obj_context ~context ~env ~uri:None
~is_path:false ty) in
let relevance = [] in
relevance,name,ty'
) tyl
in
let height = (* XXX calculate *) 0 in
- let attrs = `Provided, `Regular in
+ let attrs = source, `Regular in
uri, height, [], [],
NCic.Inductive (inductive,leftno,tyl,attrs)
- | NotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields,source) ->
let context,params =
let context,res =
List.fold_left
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~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 ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false ty) in
let nref =
- NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+ NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in
let obj_context = [name,nref] in
let fields' =
snd (
List.fold_left
(fun (context,res) (name,ty,_coercion,_arity) ->
let ty =
- interpretate_term ~obj_context ~context ~env ~uri:None
+ interpretate_term status ~obj_context ~context ~env ~uri:None
~is_path:false ty in
let context' = (name,NCic.Decl ty)::context in
context',(name,ty)::res
let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
let height = (* XXX calculate *) 0 in
- let attrs = `Provided, `Record field_names in
+ let attrs = source, `Record field_names in
uri, height, [], [],
NCic.Inductive (true,leftno,tyl,attrs)
+ | NotationPt.LetRec (kind, defs, attrs) ->
+ let inductive = kind = `Inductive in
+ let _,obj_context =
+ List.fold_left
+ (fun (i,acc) (_,(name,_),_,k) ->
+ (i+1,
+ (ncic_name_of_ident name, NRef.reference_of_spec uri
+ (if inductive then NRef.Fix (i,k,0)
+ else NRef.CoFix i)) :: acc))
+ (0,[]) defs
+ in
+ let inductiveFuns =
+ List.map
+ (fun (params, (name, typ), body, decr_idx) ->
+ let add_binders kind t =
+ List.fold_right
+ (fun var t ->
+ NotationPt.Binder (kind, var, t)) params t
+ in
+ let cic_body =
+ interpretate_term status
+ ~obj_context ~context ~env ~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
+ (HExtlib.map_option (add_binders `Pi) typ)
+ in
+ ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
+ defs
+ in
+ let height = (* XXX calculate *) 0 in
+ uri, height, [], [],
+ NCic.Fixpoint (inductive,inductiveFuns,attrs)
;;
-let disambiguate_term ~context ~metasenv ~subst ~expty
- ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~rdb ~lookup_in_library
- (text,prefix_len,term)
- =
+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 mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
MultiPassDisambiguator.disambiguate_thing
~context ~metasenv ~initial_ugraph:() ~aliases
~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:NotationPp.pp_term
+ ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term ~rdb) (text,prefix_len,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
;;
-let disambiguate_obj
+let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~rdb ~lookup_in_library ~uri
- (text,prefix_len,obj)
+ ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj NotationPp.pp_term)
+ ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
- ~interpretate_thing:(interpretate_obj ~mk_choice)
- ~refine_thing:(refine_obj ~rdb)
+ ~interpretate_thing:(interpretate_obj status ~mk_choice)
+ ~refine_thing:(refine_obj status)
(text,prefix_len,obj)
- ~mk_localization_tbl ~expty:None
+ ~mk_localization_tbl ~expty:`XTNone
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
projects / helm.git / blobdiff