open UriManager
module Ast = CicNotationPt
+module NRef = NReference
let debug_print _ = ();;
-let refine_term metasenv context uri term ugraph ~localization_tbl =
-(* if benchmark then incr actual_refinements; *)
+let cic_name_of_name = function
+ | Ast.Ident (n, None) -> n
+ | _ -> assert false
+;;
+
+let refine_term metasenv subst context uri term _ ~localization_tbl =
assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
- try
- let term', _, metasenv',ugraph1 =
- NCicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
- (Disambiguate.Ok (term', metasenv')),ugraph1
- with
- exn ->
- let rec process_exn loc =
- function
- HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Disambiguate.Uncertain (loc,msg),ugraph
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- Disambiguate.Ko (loc,msg),ugraph
- | exn -> raise exn
- in
- process_exn None exn
+ debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
+ (NCicPp.ppterm ~metasenv ~subst ~context term)));
+ try
+ let localise t =
+ try NCicUntrusted.NCicHash.find localization_tbl t
+ with Not_found -> assert false
+ in
+ let metasenv, subst, term, _ =
+ NCicRefiner.typeof metasenv subst context term None ~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)) ;
+ 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))));
+ Disambiguate.Ko loc_msg
+;;
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
+ ignore (env,item,num,args);
+ assert false
+ (*
try
snd (Environment.find item env) env num args
with Not_found ->
failwith ("Domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item))
+*)
(* TODO move it to Cic *)
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | Cic.Name hd :: tl when hd = name -> acc
+ | hd :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term
+ ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
+
let rec aux ~localize loc context = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
let res = aux ~localize loc context term in
- if localize then Cic.CicHash.add localization_tbl res loc;
+ if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
| CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
resolve env (Symbol (symb, i)) ~args:cic_args ()
| CicNotationPt.Appl terms ->
- Cic.Appl (List.map (aux ~localize loc context) terms)
+ NCic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
- let cic_type = aux_option ~localize loc context (Some `Type) typ in
- let cic_name = CicNotationUtil.cic_name_of_name var in
+ let cic_type = aux_option ~localize loc context `Type typ in
+ let cic_name = cic_name_of_name var in
let cic_body = aux ~localize loc (cic_name :: context) body in
(match binder_kind with
- | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
+ | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
| `Pi
- | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
+ | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
resolve env (Symbol ("exists", 0))
- ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
+ ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
- let cic_outtype = aux_option ~localize loc context None outtype in
- let do_branch ((head, _, args), term) =
+ let cic_outtype = aux_option ~localize loc context `Term outtype in
+ let do_branch ((_, _, args), term) =
let rec do_branch' context = function
| [] -> aux ~localize loc context term
| (name, typ) :: tl ->
- let cic_name = CicNotationUtil.cic_name_of_name name in
+ let cic_name = cic_name_of_name name in
let cic_body = do_branch' (cic_name :: context) tl in
let typ =
match typ with
- | None -> Cic.Implicit (Some `Type)
+ | None -> NCic.Implicit `Type
| Some typ -> aux ~localize loc context typ
in
- Cic.Lambda (cic_name, typ, cic_body)
+ NCic.Lambda (cic_name, typ, cic_body)
in
do_branch' context args
in
- let indtype_uri, indtype_no =
- if create_dummy_ids then
- (UriManager.uri_of_string "cic:/fake_indty.con", 0)
- else
+ if create_dummy_ids then
+ let branches =
+ List.map
+ (function
+ Ast.Wildcard,term -> ("wildcard",None,[]), term
+ | Ast.Pattern _,_ ->
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc, "Syntax error: the left hand side of a "^
+ "branch pattern must be \"_\"")))
+ ) branches
+ in
+ (*
+ NCic.MutCase (ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
+ *) ignore branches; assert false (* patterns not implemented yet *)
+ else
+ let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
- | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
- | Cic.Implicit _ ->
- raise (Disambiguate.Try_again (lazy "The type of the term to be matched
- is still unknown"))
+ | NCic.Const r -> r
+ | NCic.Implicit _ ->
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| _ ->
- raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc,"The type of the term to be matched "^
+ "is not (co)inductive!"))))
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (Some loc, lazy "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"))
+ | [] -> raise (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")))
in
(match resolve env (Id (fst_constructor branches)) () with
- | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
- (indtype_uri, indtype_no)
- | Cic.Implicit _ ->
- raise (Disambiguate.Try_again (lazy "The type of the term to be matched
- is still unknown"))
+ | NCic.Const r -> r
+ | NCic.Implicit _ ->
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| _ ->
- raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
- in
- let branches =
- if create_dummy_ids then
- List.map
- (function
- Ast.Wildcard,term -> ("wildcard",None,[]), term
- | Ast.Pattern _,_ ->
- raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
- ) branches
- else
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
- Cic.InductiveDefinition (il,_,leftsno,_) ->
- let _,_,_,cl =
- try
- List.nth il indtype_no
- with _ -> assert false
- in
- let rec count_prod t =
- match CicReduction.whd [] t with
- Cic.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
- in
- let rec sort branches cl =
- match cl with
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc,
+ "The type of the term to be matched is not (co)inductive!"))))
+ in
+ let _,leftsno,itl,_,indtyp_no =
+ NCicEnvironment.get_checked_indtys indtype_ref in
+ let _,_,_,cl =
+ try
+ List.nth itl indtyp_no
+ with _ -> assert false in
+ let rec count_prod t =
+ match NCicReduction.whd [] t with
+ NCic.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0
+ in
+ let rec sort branches cl =
+ match cl with
+ [] ->
+ let rec analyze unused unrecognized useless =
+ function
[] ->
- let rec analyze unused unrecognized useless =
- function
- [] ->
- if unrecognized != [] then
- raise (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy
- ("Unrecognized constructors: " ^
- String.concat " " unrecognized)))
- else if useless > 0 then
- raise (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy
- ("The last " ^ string_of_int useless ^
- "case" ^ if useless > 1 then "s are" else " is" ^
- " unused")))
- else
- []
- | (Ast.Wildcard,_)::tl when not unused ->
- analyze true unrecognized useless tl
- | (Ast.Pattern (head,_,_),_)::tl when not unused ->
- analyze unused (head::unrecognized) useless tl
- | _::tl -> analyze unused unrecognized (useless + 1) tl
- in
- analyze false [] 0 branches
- | (name,ty)::cltl ->
- let rec find_and_remove =
+ if unrecognized != [] then
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy
+ (loc,"Unrecognized constructors: " ^
+ String.concat " " unrecognized)))
+ else if useless > 0 then
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy
+ (loc,"The last " ^ string_of_int useless ^
+ "case" ^ if useless > 1 then "s are" else " is" ^
+ " unused")))
+ else
+ []
+ | (Ast.Wildcard,_)::tl when not unused ->
+ analyze true unrecognized useless tl
+ | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+ analyze unused (head::unrecognized) useless tl
+ | _::tl -> analyze unused unrecognized (useless + 1) tl
+ in
+ analyze false [] 0 branches
+ | (_,name,ty)::cltl ->
+ let rec find_and_remove =
+ function
+ [] ->
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc, "Missing case: " ^ name)))
+ | ((Ast.Wildcard, _) as branch :: _) as branches ->
+ branch, branches
+ | (Ast.Pattern (name',_,_),_) as branch :: tl
+ when name = name' ->
+ branch,tl
+ | branch::tl ->
+ let found,rest = find_and_remove tl in
+ found, branch::rest
+ in
+ let branch,tl = find_and_remove branches in
+ 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
+ else
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc,"Wrong number of arguments for " ^ name)))
+ | Ast.Wildcard,term ->
+ let rec mk_lambdas =
function
- [] ->
- raise
- (DisambiguateTypes.Invalid_choice
- (Some loc, lazy ("Missing case: " ^ name)))
- | ((Ast.Wildcard, _) as branch :: _) as branches ->
- branch, branches
- | (Ast.Pattern (name',_,_),_) as branch :: tl
- when name = name' ->
- branch,tl
- | branch::tl ->
- let found,rest = find_and_remove tl in
- found, branch::rest
+ 0 -> term
+ | n ->
+ CicNotationPt.Binder
+ (`Lambda, (CicNotationPt.Ident ("_", None), None),
+ mk_lambdas (n - 1))
in
- let branch,tl = find_and_remove branches in
- 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
- else
- raise
- (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy ("Wrong number of arguments for " ^ name)))
- | Ast.Wildcard,term ->
- let rec mk_lambdas =
- function
- 0 -> term
- | n ->
- CicNotationPt.Binder
- (`Lambda, (CicNotationPt.Ident ("_", None), None),
- mk_lambdas (n - 1))
- in
- (("wildcard",None,[]),
- mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
- in
- sort branches cl
- | _ -> assert false
- in
- Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
- (List.map do_branch branches))
+ (("wildcard",None,[]),
+ mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+ in
+ let branches = sort branches cl in
+ NCic.Match (indtype_ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
| CicNotationPt.Cast (t1, t2) ->
let cic_t1 = aux ~localize loc context t1 in
let cic_t2 = aux ~localize loc context t2 in
- Cic.Cast (cic_t1, cic_t2)
+ NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1)
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
- let cic_name = CicNotationUtil.cic_name_of_name name in
+ let cic_name = cic_name_of_name name in
let cic_typ =
match typ with
- | None -> Cic.Implicit (Some `Type)
+ | None -> NCic.Implicit `Type
| Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
- Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
- | CicNotationPt.LetRec (kind, defs, body) ->
+ NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
+ | CicNotationPt.LetRec (_kind, _defs, _body) ->
+ assert false (*
let context' =
List.fold_left
(fun acc (_, (name, _), _, _) ->
- CicNotationUtil.cic_name_of_name name :: acc)
+ cic_name_of_name name :: acc)
context defs
in
let cic_body =
let unlocalized_body = aux ~localize:false loc context' body in
match unlocalized_body with
- Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
- | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
+ NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
+ | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
(try
let l' =
List.map
aux_option ~localize loc context (Some `Type)
(HExtlib.map_option (add_binders `Pi) typ) in
let name =
- match CicNotationUtil.cic_name_of_name name with
- | Cic.Anonymous ->
+ match cic_name_of_name name with
+ | NCic.Anonymous ->
CicNotationPt.fail loc
"Recursive functions cannot be anonymous"
- | Cic.Name name -> name
+ | NCic.Name name -> name
in
(name, decr_idx, cic_type, cic_body))
defs
in
let fix_or_cofix n =
match kind with
- `Inductive -> Cic.Fix (n,inductiveFuns)
+ `Inductive -> NCic.Fix (n,inductiveFuns)
| `CoInductive ->
let coinductiveFuns =
List.map
(fun (name, _, typ, body) -> name, typ, body)
inductiveFuns
in
- Cic.CoFix (n,coinductiveFuns)
+ NCic.CoFix (n,coinductiveFuns)
in
let counter = ref ~-1 in
- let build_term funs (var,_,ty,_) t =
+ let build_term _ (var,_,ty,_) t =
incr counter;
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
+ NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
in
(match cic_body with
`AvoidLetInNoAppl n ->
fix_or_cofix n'
| `AvoidLetIn (n,l) ->
let n' = List.length inductiveFuns - n in
- Cic.Appl (fix_or_cofix n'::l)
+ NCic.Appl (fix_or_cofix n'::l)
| `AddLetIn cic_body ->
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
+*)
| CicNotationPt.Ident _
| CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
- | 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";
- Cic.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, Cic.Implicit None) uris)
- in
- (try
- match cic with
- | Cic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.Const (uri, mk_subst uris)
- | Cic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.Var (uri, mk_subst uris)
- | Cic.MutInd (uri, i, []) ->
- (try
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.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 *)
- Cic.MutInd (uri,i,[]))
- | Cic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_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 ->
-(*
- 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 -> Cic.Implicit None
- | CicNotationPt.UserInput -> Cic.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 *)
| CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
- List.map
- (function
- None -> None
- | Some term -> Some (aux ~localize loc context term))
- subst
+ List.map
+ (function None -> assert false| Some t -> aux ~localize loc context t)
+ subst
in
- Cic.Meta (index, cic_subst)
- | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
- | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
- | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
+ NCic.Meta (index, (0, NCic.Ctx cic_subst))
+ | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
+ | CicNotationPt.Sort `Set -> assert false
+ | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
+ [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+ | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
+ [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
- | None -> Cic.Implicit annotation
+ | None -> NCic.Implicit annotation
| Some term -> aux ~localize loc context term
in
aux ~localize:true HExtlib.dummy_floc context ast
let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
~localization_tbl
=
- assert false
-(*
- let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+ let context = List.map fst context in
interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
~localization_tbl
-*)
;;
let domain_of_term ~context =
- let context = List.map (fun x -> Cic.Name (fst x)) context in
+ let context = List.map (fun name,_ -> Cic.Name name) context in
Disambiguate.domain_of_ast_term ~context
;;
module Make (C : DisambiguateTypes.Callbacks) = struct
module Disambiguator = Disambiguate.Make(C)
- let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- (text,prefix_len,term) =
- let term =
- if fresh_instances then CicNotationUtil.freshen_term term else term
- in
- let localization_tbl = Cic.CicHash.create 503 in
- Disambiguator.disambiguate_thing
- ~dbd ~context ~metasenv ~initial_ugraph ~aliases
- ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing:domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
- ~refine_thing:refine_term (text,prefix_len,term)
- ~localization_tbl
+ let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ~subst
+ ~aliases ~universe ?goal (text,prefix_len,term)
+ =
+ let term =
+ if fresh_instances then CicNotationUtil.freshen_term term else term
+ in
+ let localization_tbl = NCicUntrusted.NCicHash.create 503 in
+ let hint =
+ match goal with
+ None -> (fun _ y -> y),(fun x -> x)
+ | Some n ->
+ (fun metasenv y ->
+ let _,_,ty = NCicUtils.lookup_meta n metasenv in
+ NCic.LetIn ("_",ty,y,NCic.Rel 1)),
+ (function
+ | Disambiguate.Ok (t,m,s,ug) ->
+ (match t with
+ | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug)
+ | _ -> assert false)
+ | k -> k)
+ in
+ let res,b =
+ Disambiguator.disambiguate_thing
+ ~dbd ~context ~metasenv ~initial_ugraph:() ~aliases
+ ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~domain_of_thing:domain_of_term
+ ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
+ ~refine_thing:refine_term (text,prefix_len,term)
+ ~localization_tbl ~hint ~subst
+ in
+ List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
end
projects / helm.git / blobdiff