;;
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 = []);
process_exn Stdpp.dummy_loc exn
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~localization_tbl ~obj_context
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
| 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
- Disambiguate.resolve env
- (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args ()
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args)
| CicNotationPt.Appl terms ->
Cic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- Disambiguate.resolve env (DisambiguateTypes.Symbol ("exists", 0))
- ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol ("exists", 0))
+ (`Args [ cic_type; Cic.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
match indty_ident with
| Some (indty_ident, _) ->
(match
- Disambiguate.resolve env
- (DisambiguateTypes.Id indty_ident) ()
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id indty_ident) (`Args [])
with
| Cic.MutInd (uri, tyno, _) -> (uri, tyno)
| Cic.Implicit _ ->
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
| [] -> raise (DisambiguateTypes.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 Disambiguate.resolve env
- (DisambiguateTypes.Id (fst_constructor branches)) () with
+ (match Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id (fst_constructor branches))
+ (`Args []) with
| Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
(indtype_uri, indtype_no)
| Cic.Implicit _ ->
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
with UriManager.IllFormedUri _ ->
CicNotationPt.fail loc "Ill formed URI"
else
- Disambiguate.resolve env (DisambiguateTypes.Id name) ()
+ try
+ List.assoc name obj_context
+ with
+ Not_found ->
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Id name) (`Args [])
in
let mk_subst uris =
let ids_to_uris =
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
| CicNotationPt.Implicit -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
- | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num ()
+ | CicNotationPt.Num (num, i) ->
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Num i) (`Num_arg num)
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| 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 env (DisambiguateTypes.Symbol (symbol, instance)) ()
- | _ -> assert false (* god bless Bologna *)
+ Disambiguate.resolve ~mk_choice ~env
+ (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
+ | 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
let localization_tbl = Cic.CicHash.create 23 in
(* here we are throwing away useful localization informations!!! *)
fst (
- interpretate_term ~create_dummy_ids:true
+ interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
- path ~localization_tbl, localization_tbl)
+ path ~localization_tbl ~obj_context:[], localization_tbl)
-let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
+let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
+ ~localization_tbl
+=
assert (context = []);
assert (is_path = false);
- let interpretate_term = interpretate_term ~localization_tbl in
+ let interpretate_term ?(obj_context=[]) =
+ interpretate_term ~mk_choice ~localization_tbl ~obj_context in
match obj with
| CicNotationPt.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
context,List.rev res in
let add_params =
List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
- let name_to_uris =
+ let obj_context =
snd (
List.fold_left
(*here the explicit_named_substituion is assumed to be of length 0 *)
- (fun (i,res) (name,_,_,_) ->
- i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
- ) (0,[]) tyl) in
- let con_env = DisambiguateTypes.env_of_list name_to_uris env in
+ (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
+ (0,[]) tyl) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
List.map
(fun (name,ty) ->
let ty' =
- add_params (interpretate_term context con_env None false ty)
+ add_params
+ (interpretate_term ~obj_context ~context ~env ~uri:None
+ ~is_path:false ty)
in
name,ty'
) cl
Cic.Constant (name,bo',ty',[],attrs))
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~localization_tbl
=
- let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
-interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
-~localization_tbl
-;;
-
-let mk_implicit =
- function true -> Cic.Implicit (Some `Closed)
- | _ -> Cic.Implicit None
+ let context =
+ List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
+ in
+ interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
+ ast ~localization_tbl ~obj_context:[]
;;
let string_context_of_context =
List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
(Cic.Anonymous,_) -> Some "_");;
-let disambiguate_term ~context ~metasenv ~subst ?goal
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- ~lookup_in_library
- (text,prefix_len,term)
+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 localization_tbl = Cic.CicHash.create 503 in
+ let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context
- ~universe ~lookup_in_library
+ ~initial_ugraph ~aliases ~string_context_of_context
+ ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
+ ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~refine_thing:refine_term (text,prefix_len,term)
- ~localization_tbl
- ~hint
+ ~mk_localization_tbl
+ ~expty
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
-let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library
- (text,prefix_len,obj)
+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 localization_tbl = Cic.CicHash.create 503 in
+ let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~aliases ~universe ~uri ~string_context_of_context
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library
+ ~lookup_in_library ~mk_implicit ~description_of_alias
~initial_ugraph:CicUniv.empty_ugraph
- ~interpretate_thing:interpretate_obj
+ ~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj
- ~localization_tbl
- ~hint
+ ~mk_localization_tbl
+ ~expty:None
~passes:(MultiPassDisambiguator.passes ())
~freshen_thing:CicNotationUtil.freshen_obj
(text,prefix_len,obj)
projects / helm.git / blobdiff