--- /dev/null
+requires="helm-acic_content"
+version="0.0.1"
+archive(byte)="disambiguation.cma"
+archive(native)="disambiguation.cmxa"
-requires="helm-whelp helm-acic_content helm-ng_refiner helm-cic_disambiguation"
+requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation"
version="0.0.1"
archive(byte)="ng_disambiguation.cma"
archive(native)="ng_disambiguation.cmxa"
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 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', _, metasenv',ugraph1 =
+ CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
+ 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
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
~localization_tbl
;;
+let mk_implicit =
+ function true -> Cic.Implicit (Some `Closed)
+ | _ -> Cic.Implicit None
+;;
+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 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
+ MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
+ ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context
+ ~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
+ ~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 ~aliases ~universe ~uri ~lookup_in_library
+ (text,prefix_len,obj)
+=
+ let hint = (fun _ x -> x), fun k -> k in
+ let localization_tbl = Cic.CicHash.create 503 in
+ MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
+ ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context
+ ~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
+ ~passes:(MultiPassDisambiguator.passes ())
+ ~freshen_thing:CicNotationUtil.freshen_obj
+ (text,prefix_len,obj)
val interpretate_path :
context:Cic.name list -> CicNotationPt.term -> Cic.term
-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_term :
+ 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) : CicDisambiguator
+val disambiguate_obj :
+ 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
--- /dev/null
+disambiguate.cmi: disambiguateTypes.cmi
+multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
+disambiguateTypes.cmo: disambiguateTypes.cmi
+disambiguateTypes.cmx: disambiguateTypes.cmi
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \
+ multiPassDisambiguator.cmi
+multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \
+ multiPassDisambiguator.cmi
--- /dev/null
+disambiguate.cmi: disambiguateTypes.cmi
+multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
+disambiguateTypes.cmo: disambiguateTypes.cmi
+disambiguateTypes.cmx: disambiguateTypes.cmi
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \
+ multiPassDisambiguator.cmi
+multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \
+ multiPassDisambiguator.cmi
PACKAGE = disambiguation
INTERFACE_FILES = \
disambiguateTypes.mli \
- disambiguate.mli
+ disambiguate.mli \
+ multiPassDisambiguator.mli
IMPLEMENTATION_FILES = \
- $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
- $(patsubst %,%_notation.ml,$(NOTATIONS))
+ $(patsubst %.mli, %.ml, $(INTERFACE_FILES))
all:
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | Cic.Name hd :: tl when hd = name -> acc
+ | Some hd :: tl when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
+let string_of_name =
+ function
+ | Ast.Ident (n, None) -> Some n
+ | _ -> assert false
+;;
+
let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
| Ast.AttributedTerm (`Loc loc, term) ->
domain_of_term ~loc ~context term
let type_dom = domain_of_term_option ~loc ~context typ in
let body_dom =
domain_of_term ~loc
- ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
+ ~context:(string_of_name var :: context) body in
(match kind with
| `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
| _ -> type_dom @ body_dom)
let (term_context, args_domain) =
List.fold_left
(fun (cont, dom) (name, typ) ->
- (CicNotationUtil.cic_name_of_name name :: cont,
+ (string_of_name name :: cont,
(match typ with
| None -> dom
| Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
let body_dom = domain_of_term ~loc ~context body in
let type_dom = domain_of_term_option ~loc ~context typ in
let where_dom =
- domain_of_term ~loc
- ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
+ domain_of_term ~loc ~context:(string_of_name var :: context) where in
body_dom @ type_dom @ where_dom
| Ast.LetRec (kind, defs, where) ->
let add_defs context =
List.fold_left
- (fun acc (_, (var, _), _, _) ->
- CicNotationUtil.cic_name_of_name var :: acc
+ (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
) context defs in
let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
let defs_dom =
let context' =
add_defs
(List.fold_left
- (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
+ (fun acc (var,_) -> string_of_name var :: acc)
context params)
in
List.rev
(snd
(List.fold_left
(fun (context,res) (var,ty) ->
- CicNotationUtil.cic_name_of_name var :: context,
+ string_of_name var :: context,
domain_of_term_option ~loc ~context ty @ res)
(add_defs context,[]) params))
@ dom
uniq_domain (domain_of_term ~context term)
let domain_of_obj ~context ast =
- let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
assert (context = []);
match ast with
| Ast.Theorem (_,_,ty,bo) ->
let context, dom =
List.fold_left
(fun (context, dom) (var, ty) ->
- let context' = CicNotationUtil.cic_name_of_name var :: context in
+ let context' = string_of_name var :: context in
match ty with
None -> context', dom
| Some ty -> context', dom @ domain_of_term context ty
) ([], []) params in
let context_w_types =
- List.rev_map
- (fun (var, _, _, _) -> Cic.Name var) tyl
- @ context in
+ List.rev_map (fun (var, _, _, _) -> Some var) tyl @ context in
dom
@ List.flatten (
List.map
let context, dom =
List.fold_left
(fun (context, dom) (var, ty) ->
- let context' = CicNotationUtil.cic_name_of_name var :: context in
+ let context' = string_of_name var :: context in
match ty with
None -> context', dom
| Some ty -> context', dom @ domain_of_term context ty
) ([], []) params in
- let context_w_types = Cic.Name var :: context in
+ let context_w_types = Some var :: context in
dom
@ domain_of_term context ty
@ snd
(List.fold_left
(fun (context,res) (name,ty,_,_) ->
- Cic.Name name::context, res @ domain_of_term context ty
+ Some name::context, res @ domain_of_term context ty
) (context_w_types,[]) fields)
let domain_of_obj ~context obj =
let domain_of_ast_term = domain_of_term;;
-let domain_of_term ~context term =
- let context =
- List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
- in
- domain_of_term ~context term
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
+ use_coercions:bool ->
mk_implicit:(bool -> 'refined_term) ->
+ string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
'refined_term DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
- domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
env:'refined_term DisambiguateTypes.codomain_item
localization_tbl:'cichash ->
'raw_thing) ->
refine_thing:(
- 'metasenv -> 'subst -> 'context -> 'uri ->
+ 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing
- ~context ~metasenv ~subst ~mk_implicit
+ ~context ~metasenv ~subst ~use_coercions
+ ~mk_implicit ~string_context_of_context
~initial_ugraph:base_univ ~hint
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
=
debug_print (lazy "DISAMBIGUATE INPUT");
debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
- let thing_dom = domain_of_thing ~context thing in
+ let thing_dom =
+ domain_of_thing ~context:(string_context_of_context context) thing in
debug_print
(lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
(*
let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
let k =
- refine_thing metasenv subst
- context uri cic_thing ugraph ~localization_tbl
+ refine_thing metasenv subst context uri
+ ~use_coercions cic_thing ugraph ~localization_tbl
in
let k = (snd hint) k in
k
| Uncertain _ ->
aux aliases diff lookup_in_todo_dom todo_dom []
| Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
- try
let res =
match aux' aliases [] None todo_dom with
| [],uncertain,errors ->
true
in
res
- with
- CicEnvironment.CircularDependency s ->
- failwith "Disambiguate: circular dependency"
end
-
-
DisambiguateTypes.Environment.key ->
?num:string -> ?args:'term list -> unit -> 'term
-val find_in_context: string -> Cic.name list -> int
-
-val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+val find_in_context: string -> string option list -> int
+val domain_of_ast_term: context:
+ string option list -> CicNotationPt.term -> domain
val domain_of_term: context:
- (Cic.name * 'a) option list -> CicNotationPt.term -> domain
+ string option list -> CicNotationPt.term -> domain
val domain_of_obj:
- context:(Cic.name * 'a) option list ->
- CicNotationPt.term CicNotationPt.obj -> domain
+ context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
module type Disambiguator =
sig
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
+ use_coercions:bool ->
mk_implicit:(bool -> 'refined_term) ->
+ string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
hint:
('metasenv -> 'raw_thing -> 'raw_thing) *
'refined_term DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
- domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
env:'refined_term DisambiguateTypes.codomain_item
localization_tbl:'cichash ->
'raw_thing) ->
refine_thing:(
- 'metasenv -> 'subst -> 'context -> 'uri ->
+ 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+let debug = false;;
+let debug_print s =
+ if debug then prerr_endline (Lazy.force s);;
+
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t * bool) list list
+ (** parameters are: option name, error message *)
+
+let mono_uris_callback ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+ if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
+ "matita.auto_disambiguation"
+ then
+ function l -> l
+ else
+ raise Ambiguous_input
+
+let mono_interp_callback _ _ _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+module Callbacks =
+ struct
+ let interactive_user_uri_choice = !_choose_uris_callback
+
+ let interactive_interpretation_choice interp =
+ !_choose_interp_callback interp
+
+ let input_or_locate_uri ~(title:string) ?id () = None
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ end
+
+module Disambiguator = Disambiguate.Make (Callbacks)
+
+(* implement module's API *)
+
+let only_one_pass = ref false;;
+
+let passes () = (* <fresh_instances?, aliases, coercions?> *)
+ if !only_one_pass then
+ [ (true, `Mono, false) ]
+ else
+ [ (true, `Mono, false);
+ (true, `Multi, false);
+ (true, `Mono, true);
+ (true, `Multi, true);
+ (true, `Library, false);
+ (* for demo to reduce the number of interpretations *)
+ (true, `Library, true);
+ ]
+;;
+
+let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+ let module D = DisambiguateTypes in
+ let minimize d =
+ if not minimize_instances then
+ d
+ else
+ let rec aux =
+ function
+ [] -> []
+ | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function
+ (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+ | _ -> true
+ ) d
+ then
+ (D.Symbol (s,0),ci)::(aux tl)
+ else
+ he::(aux tl)
+ | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+ then
+ (D.Num 0,ci)::(aux tl)
+ else
+ he::(aux tl)
+ | he::tl -> he::(aux tl)
+ in
+ aux d
+ in
+ (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+ user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+ (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+ user_asked
+
+let disambiguate_thing ~passes ~aliases ~universe ~f thing =
+ assert (universe <> None);
+ let library = false, DisambiguateTypes.Environment.empty, None in
+ let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+ let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+ let passes =
+ List.map
+ (function (fresh_instances,env,use_coercions) ->
+ fresh_instances,
+ (match env with `Mono -> mono_aliases | `Multi -> multi_aliases |
+ `Library -> library),
+ use_coercions) passes in
+ let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
+ f ~fresh_instances ~aliases ~universe ~use_coercions thing
+ in
+ let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+ if use_mono_aliases then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else if user_asked then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else
+ drop_aliases_and_clear_diff res
+ in
+ let rec aux i errors passes =
+ debug_print (lazy ("Pass: " ^ string_of_int i));
+ match passes with
+ [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
+ | hd :: tl ->
+ (try
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
+ aux (i+1) (errors @ [newerrors]) tl)
+ | [] -> assert false
+ in
+ aux 1 [] passes
+
+let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
+ ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases
+ ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing
+ ~interpretate_thing ~refine_thing ~localization_tbl thing
+ =
+ let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
+ let thing = if fresh_instances then freshen_thing thing else thing
+ in
+ Disambiguator.disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~mk_implicit ~string_context_of_context
+ ~initial_ugraph ~hint
+ ~aliases ~universe ~lookup_in_library
+ ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~localization_tbl (txt,len,thing)
+ in
+ disambiguate_thing ~passes ~aliases ~universe ~f thing
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+ * compiler) *)
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t * bool) list list
+ (** parameters are: option name, error message *)
+
+(** initially false; for debugging only (???) *)
+val only_one_pass: bool ref
+
+val passes : unit -> (bool * [> `Library | `Mono | `Multi ] * bool) list
+
+val set_choose_uris_callback:
+ DisambiguateTypes.interactive_user_uri_choice_type -> unit
+
+val set_choose_interp_callback:
+ DisambiguateTypes.interactive_interpretation_choice_type -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_uris_callback if not set otherwise with set_choose_uris_callback
+ * above *)
+val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_interp_callback if not set otherwise with set_choose_interp_callback
+ * above *)
+val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+
+val disambiguate_thing:
+ passes:(bool * [ `Library | `Mono | `Multi ] * bool) list ->
+ freshen_thing: ('ast_thing -> 'ast_thing) ->
+ context:'context ->
+ metasenv:'metasenv ->
+ subst:'subst ->
+ mk_implicit:(bool -> 'refined_term) ->
+ string_context_of_context:('context -> string option list) ->
+ initial_ugraph:'ugraph ->
+ hint:
+ ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result ->
+ ('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+ aliases:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ universe:'refined_term DisambiguateTypes.codomain_item list
+ DisambiguateTypes.Environment.t option ->
+ lookup_in_library:(
+ DisambiguateTypes.interactive_user_uri_choice_type ->
+ DisambiguateTypes.input_or_locate_uri_type ->
+ DisambiguateTypes.Environment.key ->
+ 'refined_term DisambiguateTypes.codomain_item list) ->
+ uri:'uri ->
+ pp_thing:('ast_thing -> string) ->
+ domain_of_thing:
+ (context: string option list -> 'ast_thing -> Disambiguate.domain) ->
+ interpretate_thing:(
+ context:'context ->
+ env:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ uri:'uri ->
+ is_path:bool ->
+ 'ast_thing ->
+ localization_tbl:'cichash ->
+ 'raw_thing) ->
+ refine_thing:(
+ 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
+ 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+ localization_tbl:'cichash ->
+ string * int * 'ast_thing ->
+ ((DisambiguateTypes.Environment.key *
+ 'refined_term DisambiguateTypes.codomain_item) list *
+ 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, subst, cic, _) =
singleton "first"
- (MultiPassDisambiguator.disambiguate_term
+ (CicDisambiguate.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~lookup_in_library
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, _, cic, ugraph) =
singleton "second"
- (MultiPassDisambiguator.disambiguate_term ~lookup_in_library
+ (CicDisambiguate.disambiguate_term ~lookup_in_library
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~context ~metasenv ~subst:[] ?goal
); *)
let (diff, metasenv, _, cic, _) =
singleton "third"
- (MultiPassDisambiguator.disambiguate_obj ~lookup_in_library
+ (CicDisambiguate.disambiguate_obj ~lookup_in_library
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
(text,prefix_len,obj)) in
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-let debug = false;;
-let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
-
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
- (** parameters are: option name, error message *)
-exception Unbound_identifier of string
-
-let mono_uris_callback ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id =
- if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
- "matita.auto_disambiguation"
- then
- function l -> l
- else
- raise Ambiguous_input
-
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
- struct
- let interactive_user_uri_choice = !_choose_uris_callback
-
- let interactive_interpretation_choice interp =
- !_choose_interp_callback interp
-
- let input_or_locate_uri ~(title:string) ?id () = None
- (* Zack: I try to avoid using this callback. I therefore assume that
- * the presence of an identifier that can't be resolved via "locate"
- * query is a syntax error *)
- end
-
-module Disambiguator = CicDisambiguate.Make (Callbacks)
-
-(* implement module's API *)
-
-let only_one_pass = ref false;;
-
-let disambiguate_thing ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
- ~(drop_aliases_and_clear_diff: 'b -> 'b)
- (thing: 'a)
-=
- assert (universe <> None);
- let library = false, DisambiguateTypes.Environment.empty, None in
- let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
- let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
- let passes = (* <fresh_instances?, aliases, coercions?> *)
- if !only_one_pass then
- [ (true, mono_aliases, false) ]
- else
- [ (true, mono_aliases, false);
- (true, multi_aliases, false);
- (true, mono_aliases, true);
- (true, multi_aliases, true);
- (true, library, false);
- (* for demo to reduce the number of interpretations *)
- (true, library, true);
- ]
- in
- let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
- CicRefine.insert_coercions := insert_coercions;
- f ~fresh_instances ~aliases ~universe thing
- in
- let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
- if use_mono_aliases then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else if user_asked then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else
- drop_aliases_and_clear_diff res
- in
- let rec aux i errors passes =
- debug_print (lazy ("Pass: " ^ string_of_int i));
- match passes with
- [ pass ] ->
- (try
- set_aliases pass (try_pass pass)
- with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, errors @ [newerrors])))
- | hd :: tl ->
- (try
- set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
- aux (i+1) (errors @ [newerrors]) tl)
- | [] -> assert false
- in
- let saved_insert_coercions = !CicRefine.insert_coercions in
- try
- let res = aux 1 [] passes in
- CicRefine.insert_coercions := saved_insert_coercions;
- res
- with exn ->
- CicRefine.insert_coercions := saved_insert_coercions;
- raise exn
-
-type disambiguator_thing =
- { do_it :
- 'a 'b 'term.
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- f:(?fresh_instances:bool ->
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b * bool) ->
- drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
- drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
- }
-
-let disambiguate_thing =
- let profiler = HExtlib.profile "disambiguate_thing" in
- { do_it =
- fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.HExtlib.profile
- (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff) thing
- }
-
-let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
- let module D = DisambiguateTypes in
- let minimize d =
- if not minimize_instances then
- d
- else
- let rec aux =
- function
- [] -> []
- | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function
- (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
- | _ -> true
- ) d
- then
- (D.Symbol (s,0),ci)::(aux tl)
- else
- he::(aux tl)
- | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
- then
- (D.Num 0,ci)::(aux tl)
- else
- he::(aux tl)
- | he::tl -> he::(aux tl)
- in
- aux d
- in
- (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
- user_asked
-
-let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
- user_asked
-
-let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
- =
- assert (fresh_instances = None);
- let f =
- Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
- in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff term
-
-let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj =
- assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff obj
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(** raised when ambiguous input is found but not expected (e.g. in the batch
- * compiler) *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
- (** parameters are: option name, error message *)
-
-(** initially false; for debugging only (???) *)
-val only_one_pass: bool ref
-
-val set_choose_uris_callback:
- DisambiguateTypes.interactive_user_uri_choice_type -> unit
-
-val set_choose_interp_callback:
- DisambiguateTypes.interactive_interpretation_choice_type -> unit
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_uris_callback if not set otherwise with set_choose_uris_callback
- * above *)
-val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_interp_callback if not set otherwise with set_choose_interp_callback
- * above *)
-val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
-
-(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
-
-include CicDisambiguate.CicDisambiguator
-nDisambiguate.cmo: nDisambiguate.cmi
-nDisambiguate.cmx: nDisambiguate.cmi
-nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi
-nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi
+nCicDisambiguate.cmo: nCicDisambiguate.cmi
+nCicDisambiguate.cmx: nCicDisambiguate.cmi
PACKAGE = ng_disambiguation
PREDICATES =
-INTERFACE_FILES = \
- nDisambiguate.mli nGrafiteDisambiguator.mli\
+INTERFACE_FILES = nCicDisambiguate.mli
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+open Printf
+
+open DisambiguateTypes
+open UriManager
+
+module Ast = CicNotationPt
+module NRef = NReference
+
+let debug_print _ = ();;
+
+let cic_name_of_name = function
+ | Ast.Ident (n, None) -> n
+ | _ -> assert false
+;;
+
+let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization_tbl =
+ assert (uri=None);
+ 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
+;;
+
+ (* TODO move it to Cic *)
+let find_in_context name context =
+ let rec aux acc = function
+ | [] -> raise Not_found
+ | 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
+=
+ (* 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 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
+ Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args ()
+ | CicNotationPt.Appl 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 `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 -> NCic.Lambda (cic_name, cic_type, cic_body)
+ | `Pi
+ | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
+ | `Exists ->
+ Disambiguate.resolve env (Symbol ("exists", 0))
+ ~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 `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 = cic_name_of_name name in
+ let cic_body = do_branch' (cic_name :: context) tl in
+ let typ =
+ match typ with
+ | None -> NCic.Implicit `Type
+ | Some typ -> aux ~localize loc context typ
+ in
+ NCic.Lambda (cic_name, typ, cic_body)
+ in
+ do_branch' context args
+ in
+ 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 Disambiguate.resolve env (Id indty_ident) () with
+ | 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
+ (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 (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 (Id (fst_constructor branches)) () with
+ | 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
+ (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
+ [] ->
+ 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
+ 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
+ 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
+ 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 = cic_name_of_name name in
+ let cic_typ =
+ match typ with
+ | None -> NCic.Implicit `Type
+ | Some t -> aux ~localize loc context t
+ in
+ let cic_body = aux ~localize loc (cic_name :: context) body in
+ 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, _), _, _) ->
+ 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
+ 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
+ (function t ->
+ let t',subst,metasenv =
+ CicMetaSubst.delift_rels [] [] (List.length defs) t
+ in
+ assert (subst=[]);
+ assert (metasenv=[]);
+ t') l
+ in
+ (* We can avoid the LetIn. But maybe we need to recompute l'
+ so that it is localized *)
+ if localize then
+ match body with
+ CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+ (* since we avoid the letin, the context has no
+ * recfuns in it *)
+ let l' = List.map (aux ~localize loc context) l in
+ `AvoidLetIn (n,l')
+ | _ -> assert false
+ else
+ `AvoidLetIn (n,l')
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ if localize then
+ `AddLetIn (aux ~localize loc context' body)
+ else
+ `AddLetIn unlocalized_body)
+ | _ ->
+ if localize then
+ `AddLetIn (aux ~localize loc context' body)
+ else
+ `AddLetIn unlocalized_body
+ in
+ let inductiveFuns =
+ List.map
+ (fun (params, (name, typ), body, decr_idx) ->
+ let add_binders kind t =
+ List.fold_right
+ (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
+ in
+ let cic_body =
+ aux ~localize loc context' (add_binders `Lambda body) in
+ let cic_type =
+ aux_option ~localize loc context (Some `Type)
+ (HExtlib.map_option (add_binders `Pi) typ) in
+ let name =
+ match cic_name_of_name name with
+ | NCic.Anonymous ->
+ CicNotationPt.fail loc
+ "Recursive functions cannot be anonymous"
+ | NCic.Name name -> name
+ in
+ (name, decr_idx, cic_type, cic_body))
+ defs
+ in
+ let fix_or_cofix n =
+ match kind with
+ `Inductive -> NCic.Fix (n,inductiveFuns)
+ | `CoInductive ->
+ let coinductiveFuns =
+ List.map
+ (fun (name, _, typ, body) -> name, typ, body)
+ inductiveFuns
+ in
+ NCic.CoFix (n,coinductiveFuns)
+ in
+ let counter = ref ~-1 in
+ let build_term _ (var,_,ty,_) t =
+ incr counter;
+ NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
+ in
+ (match cic_body with
+ `AvoidLetInNoAppl n ->
+ let n' = List.length inductiveFuns - n in
+ fix_or_cofix n'
+ | `AvoidLetIn (n,l) ->
+ let n' = List.length inductiveFuns - n in
+ 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) ->
+ assert (subst = None);
+ (try
+ NCic.Rel (find_in_context name context)
+ with Not_found -> Disambiguate.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) -> Disambiguate.resolve env (Num i) ~num ()
+ | CicNotationPt.Meta (index, subst) ->
+ let cic_subst =
+ List.map
+ (function None -> assert false| Some t -> aux ~localize loc context t)
+ subst
+ in
+ 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) ->
+ Disambiguate.resolve env (Symbol (symbol, instance)) ()
+ | _ -> assert false (* god bless Bologna *)
+ and aux_option ~localize loc context annotation = function
+ | 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
+=
+ 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 =
+ Disambiguate.domain_of_ast_term ~context
+;;
+
+let disambiguate_term ~context ~metasenv ~subst ?goal
+ ~aliases ~universe ~lookup_in_library
+ (text,prefix_len,term)
+ =
+ 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 =
+ MultiPassDisambiguator.disambiguate_thing
+ ~freshen_thing:CicNotationUtil.freshen_term
+ ~context ~metasenv ~initial_ugraph:() ~aliases
+ ~string_context_of_context:(List.map (fun (x,_) -> Some x))
+ ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~mk_implicit:(function false -> NCic.Implicit `Term
+ | true -> NCic.Implicit `Closed)
+ ~passes:(MultiPassDisambiguator.passes ())
+ ~lookup_in_library ~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
+;;
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+val disambiguate_term :
+ context:NCic.context ->
+ metasenv:NCic.metasenv ->
+ subst:NCic.substitution ->
+ ?goal:int ->
+ aliases:NCic.term DisambiguateTypes.environment ->
+ universe:NCic.term DisambiguateTypes.multiple_environment option ->
+ lookup_in_library:(
+ DisambiguateTypes.interactive_user_uri_choice_type ->
+ DisambiguateTypes.input_or_locate_uri_type ->
+ DisambiguateTypes.Environment.key ->
+ NCic.term DisambiguateTypes.codomain_item list) ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+ ((DisambiguateTypes.domain_item *
+ NCic.term DisambiguateTypes.codomain_item) list *
+ NCic.metasenv *
+ NCic.substitution *
+ NCic.term) list *
+ bool
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-open Printf
-
-open DisambiguateTypes
-open UriManager
-
-module Ast = CicNotationPt
-module NRef = NReference
-
-let debug_print _ = ();;
-
-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"
- (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
-;;
-
- (* TODO move it to Cic *)
-let find_in_context name context =
- let rec aux acc = function
- | [] -> raise Not_found
- | 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
-=
- (* 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 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
- Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args ()
- | CicNotationPt.Appl 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 `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 -> NCic.Lambda (cic_name, cic_type, cic_body)
- | `Pi
- | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
- | `Exists ->
- Disambiguate.resolve env (Symbol ("exists", 0))
- ~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 `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 = cic_name_of_name name in
- let cic_body = do_branch' (cic_name :: context) tl in
- let typ =
- match typ with
- | None -> NCic.Implicit `Type
- | Some typ -> aux ~localize loc context typ
- in
- NCic.Lambda (cic_name, typ, cic_body)
- in
- do_branch' context args
- in
- 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 Disambiguate.resolve env (Id indty_ident) () with
- | 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
- (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 (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 (Id (fst_constructor branches)) () with
- | 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
- (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
- [] ->
- 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
- 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
- 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
- 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 = cic_name_of_name name in
- let cic_typ =
- match typ with
- | None -> NCic.Implicit `Type
- | Some t -> aux ~localize loc context t
- in
- let cic_body = aux ~localize loc (cic_name :: context) body in
- 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, _), _, _) ->
- 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
- 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
- (function t ->
- let t',subst,metasenv =
- CicMetaSubst.delift_rels [] [] (List.length defs) t
- in
- assert (subst=[]);
- assert (metasenv=[]);
- t') l
- in
- (* We can avoid the LetIn. But maybe we need to recompute l'
- so that it is localized *)
- if localize then
- match body with
- CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- (* since we avoid the letin, the context has no
- * recfuns in it *)
- let l' = List.map (aux ~localize loc context) l in
- `AvoidLetIn (n,l')
- | _ -> assert false
- else
- `AvoidLetIn (n,l')
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body)
- | _ ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- aux ~localize loc context' (add_binders `Lambda body) in
- let cic_type =
- aux_option ~localize loc context (Some `Type)
- (HExtlib.map_option (add_binders `Pi) typ) in
- let name =
- match cic_name_of_name name with
- | NCic.Anonymous ->
- CicNotationPt.fail loc
- "Recursive functions cannot be anonymous"
- | NCic.Name name -> name
- in
- (name, decr_idx, cic_type, cic_body))
- defs
- in
- let fix_or_cofix n =
- match kind with
- `Inductive -> NCic.Fix (n,inductiveFuns)
- | `CoInductive ->
- let coinductiveFuns =
- List.map
- (fun (name, _, typ, body) -> name, typ, body)
- inductiveFuns
- in
- NCic.CoFix (n,coinductiveFuns)
- in
- let counter = ref ~-1 in
- let build_term _ (var,_,ty,_) t =
- incr counter;
- NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
- in
- (match cic_body with
- `AvoidLetInNoAppl n ->
- let n' = List.length inductiveFuns - n in
- fix_or_cofix n'
- | `AvoidLetIn (n,l) ->
- let n' = List.length inductiveFuns - n in
- 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) ->
- assert (subst = None);
- (try
- NCic.Rel (find_in_context name context)
- with Not_found -> Disambiguate.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) -> Disambiguate.resolve env (Num i) ~num ()
- | CicNotationPt.Meta (index, subst) ->
- let cic_subst =
- List.map
- (function None -> assert false| Some t -> aux ~localize loc context t)
- subst
- in
- 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) ->
- Disambiguate.resolve env (Symbol (symbol, instance)) ()
- | _ -> assert false (* god bless Bologna *)
- and aux_option ~localize loc context annotation = function
- | 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
-=
- 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 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) ~context ~metasenv ~subst
- ~aliases ~universe ~lookup_in_library ?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
- ~context ~metasenv ~initial_ugraph:() ~aliases
- ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~mk_implicit:(function false -> NCic.Implicit `Term
- | true -> NCic.Implicit `Closed)
- ~lookup_in_library ~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
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-module Make (C : DisambiguateTypes.Callbacks) : sig
-val disambiguate_term :
- ?fresh_instances:bool ->
- context:NCic.context ->
- metasenv:NCic.metasenv ->
- subst:NCic.substitution ->
- aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- NCic.term DisambiguateTypes.codomain_item list) ->
- ?goal: int ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list *
- NCic.metasenv * (* new metasenv *)
- NCic.substitution *
- NCic.term) list * (* disambiguated term *)
- bool
-end
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id$ *)
-
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
-
-open Printf
-
-let debug = false;;
-let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
-
-module Callbacks =
- struct
- let interactive_user_uri_choice ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- assert false
-
- let interactive_interpretation_choice interp =
- assert false
-
- let input_or_locate_uri ~(title:string) ?id () =
- assert false
- end
-
-module Disambiguator = NDisambiguate.Make (Callbacks)
-
-let only_one_pass = ref false;;
-
-let disambiguate_thing ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:NCic.term DisambiguateTypes.environment ->
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
- ~(drop_aliases_and_clear_diff: 'b -> 'b)
- (thing: 'a)
-=
- assert (universe <> None);
- let library = false, DisambiguateTypes.Environment.empty, None in
- let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
- let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
- let passes = (* <fresh_instances?, aliases, coercions?> *)
- if !only_one_pass then
- [ (true, mono_aliases, false) ]
- else
- [ (true, mono_aliases, false);
- (true, multi_aliases, false);
- (true, mono_aliases, true);
- (true, multi_aliases, true);
- (true, library, false);
- (* for demo to reduce the number of interpretations *)
- (true, library, true);
- ]
- in
- let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
- CicRefine.insert_coercions := insert_coercions;
- f ~fresh_instances ~aliases ~universe thing
- in
- let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
- if use_mono_aliases then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else if user_asked then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else
- drop_aliases_and_clear_diff res
- in
- let rec aux i errors passes =
- debug_print (lazy ("Pass: " ^ string_of_int i));
- match passes with
- [ pass ] ->
- (try
- set_aliases pass (try_pass pass)
- with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, errors @ [newerrors])))
- | hd :: tl ->
- (try
- set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
- aux (i+1) (errors @ [newerrors]) tl)
- | [] -> assert false
- in
- let saved_insert_coercions = !CicRefine.insert_coercions in
- try
- let res = aux 1 [] passes in
- CicRefine.insert_coercions := saved_insert_coercions;
- res
- with exn ->
- CicRefine.insert_coercions := saved_insert_coercions;
- raise exn
-
-type disambiguator_thing =
- { do_it :
- 'a 'b.
- aliases:NCic.term DisambiguateTypes.environment ->
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
- f:(?fresh_instances:bool ->
- aliases:NCic.term DisambiguateTypes.environment ->
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b * bool) ->
- drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
- drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
- }
-
-let disambiguate_thing =
- let profiler = HExtlib.profile "disambiguate_thing" in
- { do_it =
- fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.HExtlib.profile
- (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff) thing
- }
-
-let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
- let module D = DisambiguateTypes in
- let minimize d =
- if not minimize_instances then
- d
- else
- let rec aux =
- function
- [] -> []
- | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function
- (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
- | _ -> true
- ) d
- then
- (D.Symbol (s,0),ci)::(aux tl)
- else
- he::(aux tl)
- | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
- then
- (D.Num 0,ci)::(aux tl)
- else
- he::(aux tl)
- | he::tl -> he::(aux tl)
- in
- aux d
- in
- (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
- user_asked
-
-let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
- user_asked
-
-let disambiguate_term ~context ~metasenv ~subst ?goal
- ~aliases ~universe term
- =
- let f =
- Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal
- ~lookup_in_library:(fun _ _ -> assert false)
- in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff term
-
-let disambiguate_obj ~aliases ~universe ~uri obj =
- assert false (*
- assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff obj
- *)
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id$ *)
-
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
-
-val disambiguate_term :
- context:NCic.context ->
- metasenv:NCic.metasenv ->
- subst:NCic.substitution ->
- ?goal:int ->
- aliases:NCic.term DisambiguateTypes.environment ->
- universe:NCic.term DisambiguateTypes.multiple_environment option ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item *
- NCic.term DisambiguateTypes.codomain_item) list *
- NCic.metasenv * (* new metasenv *)
- NCic.substitution *
- NCic.term) list * (* disambiguated term *)
- bool
projects / helm.git / commitdiff