;;
let refine_term metasenv subst context uri ~use_coercions
- term ugraph ~localization_tbl =
+ term expty ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
let saved_use_coercions = !CicRefine.insert_coercions in
try
CicRefine.insert_coercions := use_coercions;
+ let term =
+ match expty with
+ | None -> term
+ | Some ty -> Cic.Cast(term,ty)
+ in
let term', _, metasenv',ugraph1 =
CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
+ in
+ let term' =
+ match expty, term' with
+ | None,_ -> term'
+ | Some _,Cic.Cast (term',_) -> term'
+ | _ -> assert false
in
CicRefine.insert_coercions := saved_use_coercions;
(Disambiguate.Ok (term', metasenv',[],ugraph1))
in
process_exn Stdpp.dummy_loc exn
-let refine_obj metasenv subst context uri ~use_coercions obj ugraph
+let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
~localization_tbl =
assert (context = []);
assert (metasenv = []);
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 _
+ | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.NRef _ -> assert false
+ | CicNotationPt.Ident (name,subst)
| CicNotationPt.Uri (name, subst) as ast ->
let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
(try
| 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 (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+ | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
| CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~mk_choice ~env
(DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
- | _ -> assert false (* god bless Bologna *)
+ | CicNotationPt.Variable _
+ | CicNotationPt.Magic _
+ | CicNotationPt.Layout _
+ | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term
List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
(Cic.Anonymous,_) -> Some "_");;
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let disambiguate_term ~context ~metasenv ~subst ~expty
?(initial_ugraph = CicUniv.oblivion_ugraph)
~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
- let hint = match goal with
- | None -> (fun _ x -> x), fun k -> k
- | Some i ->
- (fun metasenv t ->
- let _,c,ty = CicUtil.lookup_meta i metasenv in
- assert(c=context);
- Cic.Cast(t,ty)),
- function
- | Disambiguate.Ok (t,m,s,ug) ->
- (match t with
- | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
- | _ -> assert false)
- | k -> k
- in
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
~initial_ugraph ~aliases ~string_context_of_context
~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~refine_thing:refine_term (text,prefix_len,term)
~mk_localization_tbl
- ~hint
+ ~expty
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
- let hint = (fun _ x -> x), fun k -> k in
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
~aliases ~universe ~uri ~string_context_of_context
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj
~mk_localization_tbl
- ~hint
+ ~expty:None
~passes:(MultiPassDisambiguator.passes ())
~freshen_thing:CicNotationUtil.freshen_obj
(text,prefix_len,obj)