let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-let refine_term metasenv subst context uri term ugraph ~localization_tbl =
+let rec string_context_of_context =
+ List.map
+ (function
+ | Cic.Name n -> Some n
+ | Cic.Anonymous -> Some "_")
+;;
+
+let refine_term metasenv subst context uri ~use_coercions
+ term expty ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
- try
- let term', _, metasenv',ugraph1 =
- CicRefine.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 loc exn
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- Disambiguate.Ko (lazy (loc,Lazy.force msg))
- | exn -> raise exn
- in
- process_exn Stdpp.dummy_loc exn
+ 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))
+ with
+ exn ->
+ CicRefine.insert_coercions := saved_use_coercions;
+ let rec process_exn loc =
+ function
+ HExtlib.Localized (loc,exn) -> process_exn loc exn
+ | CicRefine.Uncertain msg ->
+ debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
+ Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
+ | CicRefine.RefineFailure msg ->
+ debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) (Lazy.force msg)));
+ Disambiguate.Ko (lazy (loc,Lazy.force msg))
+ | exn -> raise exn
+ in
+ process_exn Stdpp.dummy_loc exn
-let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
+let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
+ ~localization_tbl =
assert (context = []);
assert (metasenv = []);
assert (subst = []);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
+ let saved_use_coercions = !CicRefine.insert_coercions in
try
+ CicRefine.insert_coercions := use_coercions;
let obj', metasenv,ugraph =
CicRefine.typecheck metasenv uri obj ~localization_tbl
in
- (Disambiguate.Ok (obj', metasenv,[],ugraph))
+ CicRefine.insert_coercions := saved_use_coercions;
+ (Disambiguate.Ok (obj', metasenv,[],ugraph))
with
exn ->
+ CicRefine.insert_coercions := saved_use_coercions;
let rec process_exn loc =
function
HExtlib.Localized (loc,exn) -> process_exn loc exn
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
if is_uri ast then raise Not_found;(* don't search the env for URIs *)
- let index = Disambiguate.find_in_context name context in
+ let index =
+ Disambiguate.find_in_context name (string_context_of_context context)
+ in
if subst <> None then
CicNotationPt.fail loc "Explicit substitutions not allowed here";
Cic.Rel index
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 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 ~expty
+ ?(initial_ugraph = CicUniv.oblivion_ugraph)
+ ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
+=
+ let mk_localization_tbl x = Cic.CicHash.create x in
+ MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
+ ~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) ~mk_choice)
+ ~refine_thing:refine_term (text,prefix_len,term)
+ ~mk_localization_tbl
+ ~expty
+ ~freshen_thing:CicNotationUtil.freshen_term
+ ~passes:(MultiPassDisambiguator.passes ())
-
-module type CicDisambiguator =
-sig
- val disambiguate_term :
- ?fresh_instances:bool ->
- context:Cic.context ->
- metasenv:Cic.metasenv ->
- subst:Cic.substitution ->
- ?goal:int ->
- ?initial_ugraph:CicUniv.universe_graph ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list *
- bool
-
- val disambiguate_obj :
- ?fresh_instances:bool ->
- aliases:Cic.term DisambiguateTypes.environment ->
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list *
- bool
-end
-
-module Make (C: DisambiguateTypes.Callbacks) =
- struct
- module Disambiguator = Disambiguate.Make(C)
-
- let mk_implicit =
- function true -> Cic.Implicit (Some `Closed)
- | _ -> Cic.Implicit None
- ;;
-
- let disambiguate_term ?(fresh_instances=false) ~context ~metasenv
- ~subst ?goal
- ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
- ~lookup_in_library
- (text,prefix_len,term)
- =
- let term =
- if fresh_instances then CicNotationUtil.freshen_term term else term
- in
- 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
- Disambiguator.disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~mk_implicit
- ~universe ~lookup_in_library
- ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
- ~refine_thing:refine_term (text,prefix_len,term)
- ~localization_tbl
- ~hint
-
- let disambiguate_obj
- ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library
- (text,prefix_len,obj)
- =
- let obj =
- if fresh_instances then CicNotationUtil.freshen_obj obj else obj
- in
- let hint =
- (fun _ x -> x),
- fun k -> k
- in
- let localization_tbl = Cic.CicHash.create 503 in
- Disambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~mk_implicit
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
- ~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library
- ~initial_ugraph:CicUniv.empty_ugraph
- ~interpretate_thing:interpretate_obj
- ~refine_thing:refine_obj
- ~localization_tbl
- ~hint
- (text,prefix_len,obj)
-end
+let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
+=
+ let mk_localization_tbl x = Cic.CicHash.create x in
+ MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
+ ~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 ~mk_implicit ~description_of_alias
+ ~initial_ugraph:CicUniv.empty_ugraph
+ ~interpretate_thing:(interpretate_obj ~mk_choice)
+ ~refine_thing:refine_obj
+ ~mk_localization_tbl
+ ~expty:None
+ ~passes:(MultiPassDisambiguator.passes ())
+ ~freshen_thing:CicNotationUtil.freshen_obj
+ (text,prefix_len,obj)
projects / helm.git / blobdiff