From: Enrico Tassi Date: Fri, 21 Nov 2008 15:15:43 +0000 (+0000) Subject: disambiguation now returns and takes in input the substitution X-Git-Tag: make_still_working~4522 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=424982ded255df68245241f56064202844ed1194;p=helm.git disambiguation now returns and takes in input the substitution --- diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 248baa195..45186669d 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -103,19 +103,19 @@ let descr_of_domain_item = function | Symbol (s, _) -> s | Num i -> string_of_int i -type ('a,'m) test_result = - | Ok of 'a * 'm +type ('term,'metasenv,'subst,'graph) test_result = + | Ok of 'term * 'metasenv * 'subst * 'graph | Ko of Stdpp.location option * string Lazy.t | Uncertain of Stdpp.location option * string Lazy.t -let refine_term metasenv context uri term ugraph ~localization_tbl = +let refine_term metasenv subst context uri 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 - (Ok (term', metasenv')),ugraph1 + (Ok (term', metasenv',[],ugraph1)) with exn -> let rec process_exn loc = @@ -123,35 +123,38 @@ let refine_term metasenv context uri term ugraph ~localization_tbl = HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (loc,msg),ugraph + Uncertain (loc,msg) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko (loc,msg),ugraph + Ko (loc,msg) | exn -> raise exn in process_exn None exn -let refine_obj metasenv context uri obj ugraph ~localization_tbl = - assert (context = []); +let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = + assert (context = []); + assert (metasenv = []); + assert (subst = []); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try let obj', metasenv,ugraph = - CicRefine.typecheck metasenv uri obj ~localization_tbl + CicRefine.typecheck metasenv uri obj ~localization_tbl in - (Ok (obj', metasenv)),ugraph + (Ok (obj', metasenv,[],ugraph)) with exn -> let rec process_exn loc = function HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain (loc,msg),ugraph + debug_print (lazy ("UNCERTAIN!!! [" ^ + (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (loc,msg) | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (loc,msg),ugraph + Ko (loc,msg) | exn -> raise exn in process_exn None exn @@ -934,10 +937,11 @@ sig dbd:HSql.dbd -> context:'context -> metasenv:'metasenv -> + subst:'subst -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv) test_result -> 'ugraph -> - ('refined_thing,'metasenv) test_result * 'ugraph) -> + (('refined_thing,'metasenv,'subst,'ugraph) test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> universe:DisambiguateTypes.codomain_item list DisambiguateTypes.Environment.t option -> @@ -950,28 +954,32 @@ sig uri:'uri -> is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) -> refine_thing:('metasenv -> + 'subst -> 'context -> 'uri -> 'raw_thing -> - 'ugraph -> localization_tbl:'cichash -> ('refined_thing, - 'metasenv) test_result * 'ugraph) -> + 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) - list * 'metasenv * 'refined_thing * 'ugraph) + list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool val disambiguate_term : ?fresh_instances:bool -> dbd:HSql.dbd -> context:Cic.context -> - metasenv:Cic.metasenv -> ?goal:int -> + metasenv:Cic.metasenv -> + subst:Cic.substitution -> + ?goal:int -> ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) + Cic.substitution * Cic.term* CicUniv.universe_graph) list * (* disambiguated term *) bool @@ -985,6 +993,7 @@ sig CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) + Cic.substitution * Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) bool @@ -1028,8 +1037,8 @@ module Make (C: Callbacks) = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" - let disambiguate_thing ~dbd ~context ~metasenv - ~initial_ugraph ~hint + let disambiguate_thing ~dbd ~context ~metasenv ~subst + ~initial_ugraph:base_univ ~hint ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl @@ -1129,31 +1138,32 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" in let cic_thing = (fst hint) metasenv cic_thing in let foo () = - let k,ugraph1 = - refine_thing metasenv context uri cic_thing ugraph ~localization_tbl + let k = + refine_thing metasenv subst + context uri cic_thing ugraph ~localization_tbl in - let k, ugraph1 = (snd hint) k ugraph1 in - (k , ugraph1 ) + let k = (snd hint) k in + k in refine_profiler.HExtlib.profile foo () with - | Try_again msg -> Uncertain (None,msg), ugraph - | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph + | Try_again msg -> Uncertain (None,msg) + | Invalid_choice (loc,msg) -> Ko (loc,msg) in (* (4) build all possible interpretations *) let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in (* aux returns triples Ok/Uncertain/Ko *) (* rem_dom is the concatenation of all the remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ = + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); match todo_dom with | [] -> assert (lookup_in_todo_dom = None); (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ], [], [] - | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] - | Uncertain (loc,msg),new_univ -> - [],[aliases,diff,loc,msg,new_univ],[]) + | Ok (thing, metasenv,subst,new_univ) -> + [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] + | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] + | Uncertain (loc,msg) -> + [],[aliases,diff,loc,msg],[]) | Node (locs,item,inner_dom) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -1213,68 +1223,69 @@ in refine_profiler.HExtlib.profile foo () ok_l,uncertain_l,mark_not_significant error_l else outcome in - let rec filter univ = function + let rec filter = function | [] -> [],[],[] | codomain_item :: tl -> debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); let new_env = Environment.add item codomain_item aliases in let new_diff = (item,codomain_item)::diff in (match - test_env new_env (inner_dom@remaining_dom@rem_dom) univ + test_env new_env + (inner_dom@remaining_dom@rem_dom) base_univ with - | Ok (thing, metasenv),new_univ -> + | Ok (thing, metasenv,subst,new_univ) -> let res = (match inner_dom with | [] -> - [new_env,new_diff,metasenv,thing,new_univ], [], [] + [new_env,new_diff,metasenv,subst,thing,new_univ], + [], [] | _ -> aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) new_univ + (remaining_dom@rem_dom) ) in - res @@ filter univ tl - | Uncertain (loc,msg),new_univ -> + res @@ filter tl + | Uncertain (loc,msg) -> let res = (match inner_dom with - | [] -> [],[new_env,new_diff,loc,msg,new_univ],[] + | [] -> [],[new_env,new_diff,loc,msg],[] | _ -> aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) new_univ + (remaining_dom@rem_dom) ) in - res @@ filter univ tl - | Ko (loc,msg),_ -> + res @@ filter tl + | Ko (loc,msg) -> let res = [],[],[new_env,new_diff,loc,msg,true] in - res @@ filter univ tl) + res @@ filter tl) in let ok_l,uncertain_l,error_l = - classify_errors (filter base_univ choices) + classify_errors (filter choices) in let res_after_ok_l = List.fold_right - (fun (env,diff,_,_,univ) res -> - aux env diff None remaining_dom rem_dom univ @@ res + (fun (env,diff,_,_,_,_) res -> + aux env diff None remaining_dom rem_dom @@ res ) ok_l ([],[],error_l) in List.fold_right - (fun (env,diff,_,_,univ) res -> - aux env diff None remaining_dom rem_dom univ @@ res + (fun (env,diff,_,_) res -> + aux env diff None remaining_dom rem_dom @@ res ) uncertain_l res_after_ok_l in - let aux' aliases diff lookup_in_todo_dom todo_dom base_univ = + let aux' aliases diff lookup_in_todo_dom todo_dom = match test_env aliases todo_dom base_univ with - | Ok _,_ - | Uncertain _,_ -> - aux aliases diff lookup_in_todo_dom todo_dom [] base_univ - | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in - let base_univ = initial_ugraph in + | Ok _ + | 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 base_univ with + match aux' aliases [] None todo_dom with | [],uncertain,errors -> let errors = List.map - (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true) + (fun (env,diff,loc,msg) -> (env,diff,loc,msg,true) ) uncertain @ errors in let errors = @@ -1296,15 +1307,15 @@ in refine_profiler.HExtlib.profile foo () ) errors in raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,t,ugraph],_,_ -> + | [_,diff,metasenv,subst,t,ugraph],_,_ -> debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,t,ugraph], false + [diff,metasenv,subst,t,ugraph], false | l,_,_ -> debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map - (fun (env, _, _, _, _) -> + (fun (env, _, _, _, _, _) -> map_domain (fun locs domain_item -> let description = @@ -1318,7 +1329,8 @@ in refine_profiler.HExtlib.profile foo () C.interactive_interpretation_choice thing_txt thing_txt_prefix_len choices in - (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), + (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) + choosed), true in res @@ -1327,7 +1339,7 @@ in refine_profiler.HExtlib.profile foo () failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?goal + ~subst ?goal ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe (text,prefix_len,term) = @@ -1335,21 +1347,22 @@ in refine_profiler.HExtlib.profile foo () if fresh_instances then CicNotationUtil.freshen_term term else term in let hint = match goal with - | None -> (fun _ x -> x), fun k u -> k, u + | 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 - | Ok (t,m) -> fun ug -> + | Ok (t,m,s,ug) -> (match t with - | Cic.Cast(t,_) -> Ok (t,m), ug + | Cic.Cast(t,_) -> Ok (t,m,s,ug) | _ -> assert false) - | k -> fun ug -> k, ug + | k -> k in let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases + disambiguate_thing ~dbd ~context ~metasenv ~subst + ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) @@ -1365,10 +1378,10 @@ in refine_profiler.HExtlib.profile foo () in let hint = (fun _ x -> x), - fun k u -> k, u + fun k -> k in let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~dbd ~context:[] ~metasenv:[] + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[] ~aliases ~universe ~uri ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj ~initial_ugraph:CicUniv.empty_ugraph diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index c94273804..b21c2bbe0 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -48,10 +48,12 @@ type 'a disambiguator_input = string * int * 'a type domain = domain_tree list and domain_tree = Node of Stdpp.location list * DisambiguateTypes.domain_item * domain -type ('a,'m) test_result = - | Ok of 'a * 'm + +type ('term,'metasenv,'subst,'graph) test_result = + | Ok of 'term * 'metasenv * 'subst * 'graph | Ko of Stdpp.location option * string Lazy.t | Uncertain of Stdpp.location option * string Lazy.t + exception Try_again of string Lazy.t val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain @@ -61,11 +63,12 @@ sig val disambiguate_thing: dbd:HSql.dbd -> context:'context -> - metasenv:'metasenv -> + metasenv:'metasenv -> + subst:'subst -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv) test_result -> 'ugraph -> - ('refined_thing,'metasenv) test_result * 'ugraph) -> + (('refined_thing,'metasenv,'subst,'ugraph) test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> universe:DisambiguateTypes.codomain_item list DisambiguateTypes.Environment.t option -> @@ -76,40 +79,38 @@ sig env:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> uri:'uri -> - is_path:bool -> - 'ast_thing -> - localization_tbl:'cichash -> 'raw_thing) -> + is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) -> refine_thing:('metasenv -> + 'subst -> 'context -> 'uri -> 'raw_thing -> - 'ugraph -> localization_tbl:'cichash -> ('refined_thing, - 'metasenv) test_result * 'ugraph) -> + 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) - list * 'metasenv * 'refined_thing * 'ugraph) + list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool - (** @param fresh_instances when set to true fresh instances will be generated - * for each number _and_ symbol in the disambiguation domain. Instances of the - * input AST will be ignored. Defaults to false. *) val disambiguate_term : ?fresh_instances:bool -> dbd:HSql.dbd -> context:Cic.context -> - metasenv:Cic.metasenv -> ?goal:int -> + metasenv:Cic.metasenv -> + subst:Cic.substitution -> + ?goal:int -> ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) - Cic.term * + Cic.substitution * + Cic.term* CicUniv.universe_graph) list * (* disambiguated term *) - bool (* has interactive_interpretation_choice been invoked? *) + bool - (** @param fresh_instances as per disambiguate_term *) val disambiguate_obj : ?fresh_instances:bool -> dbd:HSql.dbd -> @@ -119,10 +120,10 @@ sig CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) + Cic.substitution * Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) - bool (* has interactive_interpretation_choice been invoked? *) - + bool end module Make (C : DisambiguateTypes.Callbacks) : Disambiguator diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 8983fdcb9..ad7f70ef1 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -46,18 +46,19 @@ let singleton msg = function HLog.debug debug; assert false (** @param term not meaningful when context is given *) -let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv term = +let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv +term = let lexicon_status = !lexicon_status_ref in - let (diff, metasenv, cic, _) = + let (diff, metasenv, subst, cic, _) = singleton "first" (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) ~aliases:lexicon_status.LexiconEngine.aliases ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~context ~metasenv (text,prefix_len,term)) + ~context ~metasenv ~subst:[] (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status_ref := lexicon_status; - metasenv,cic + metasenv,(*subst,*) cic ;; (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term @@ -68,12 +69,12 @@ let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv t let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = (fun context metasenv ugraph -> let lexicon_status = !lexicon_status_ref in - let (diff, metasenv, cic, ugraph) = + let (diff, metasenv, _, cic, ugraph) = singleton "second" (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~context ~metasenv ?goal + ~context ~metasenv ~subst:[] ?goal (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status_ref := lexicon_status; @@ -455,7 +456,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in - let (diff, metasenv, cic, _) = + let (diff, metasenv, _, cic, _) = singleton "third" (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) ~aliases:lexicon_status.LexiconEngine.aliases diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index 360d56f02..46b8397ba 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -200,19 +200,19 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) = in aux d in - (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices), + (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) -> [], a, b, c) choices), + (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), user_asked -let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?goal ?initial_ugraph +let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe term = assert (fresh_instances = None); let f = - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?goal ?initial_ugraph + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph in disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff term diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index 7861ca891..40ed34b5f 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -34,29 +34,29 @@ module Ast = CicNotationPt let debug_print _ = ();; -let refine_term metasenv context uri term ugraph ~localization_tbl = -(* if benchmark then incr actual_refinements; *) +let refine_term metasenv subst context uri term ugraph ~localization_tbl = assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); - try - let term', _, metasenv',ugraph1 = - NCicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in - (Disambiguate.Ok (term', metasenv')),ugraph1 - with - exn -> - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Disambiguate.Uncertain (loc,msg),ugraph - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Disambiguate.Ko (loc,msg),ugraph - | exn -> raise exn - in - process_exn None exn + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" + (NCicPp.ppterm ~metasenv ~subst ~context term))); + try + let localise t = + try NCic.NCicHash.find localization_tbl t + with Not_found -> assert false + in + let metasenv, subst, term, ty = + NCicRefine.typeof metasenv subst context term None ~localise + in + Disambiguate.Ok (term, metasenv, subst, ()) + with + | NCicRefine.Uncertain (loc, msg) -> + debug_print (lazy ("UNCERTAIN: [" ^ Lazy.force msg ^ "] " ^ + NCicPp.ppterm ~metasenv ~subst ~context term)) ; + Disambiguate.Uncertain (loc,msg,()) + | NCicRefine.RefineFailure (loc,msg) -> + debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" + (NCicPp.ppterm ~metasenv ~subst ~context term) (Lazy.force msg))); + Disambiguate.Ko (loc,msg,()) +;; let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -69,42 +69,43 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ? let find_in_context name context = let rec aux acc = function | [] -> raise Not_found - | Cic.Name hd :: tl when hd = name -> acc + | Cic.Name hd :: _ when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term + ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); + let rec aux ~localize loc context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in - if localize then Cic.CicHash.add localization_tbl res loc; + if localize then NCic.NCicHash.add localization_tbl res loc; res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () | CicNotationPt.Appl terms -> - Cic.Appl (List.map (aux ~localize loc context) terms) + NCic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option ~localize loc context (Some `Type) typ in let cic_name = CicNotationUtil.cic_name_of_name var in let cic_body = aux ~localize loc (cic_name :: context) body in (match binder_kind with - | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) + | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body) | `Pi - | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) + | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) | `Exists -> resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) + ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context None outtype in - let do_branch ((head, _, args), term) = + let do_branch ((_, _, args), term) = let rec do_branch' context = function | [] -> aux ~localize loc context term | (name, typ) :: tl -> @@ -112,10 +113,10 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with - | None -> Cic.Implicit (Some `Type) + | None -> NCic.Implicit (Some `Type) | Some typ -> aux ~localize loc context typ in - Cic.Lambda (cic_name, typ, cic_body) + NCic.Lambda (cic_name, typ, cic_body) in do_branch' context args in @@ -126,8 +127,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast match indty_ident with | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with - | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> + | NCic.MutInd (uri, tyno, _) -> (uri, tyno) + | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> @@ -140,9 +141,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")) in (match resolve env (Id (fst_constructor branches)) () with - | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> + | NCic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) - | Cic.Implicit _ -> + | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> @@ -158,7 +159,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ) branches else match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with - Cic.InductiveDefinition (il,_,leftsno,_) -> + NCic.InductiveDefinition (il,_,leftsno,_) -> let _,_,_,cl = try List.nth il indtype_no @@ -166,7 +167,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast in let rec count_prod t = match CicReduction.whd [] t with - Cic.Prod (_, _, t) -> 1 + (count_prod t) + NCic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let rec sort branches cl = @@ -238,22 +239,22 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast sort branches cl | _ -> assert false in - Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, + NCic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) | CicNotationPt.Cast (t1, t2) -> let cic_t1 = aux ~localize loc context t1 in let cic_t2 = aux ~localize loc context t2 in - Cic.Cast (cic_t1, cic_t2) + NCic.Cast (cic_t1, cic_t2) | CicNotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in let cic_typ = match typ with - | None -> Cic.Implicit (Some `Type) + | None -> NCic.Implicit (Some `Type) | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in - Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) + NCic.LetIn (cic_name, cic_def, cic_typ, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left @@ -264,8 +265,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast let cic_body = let unlocalized_body = aux ~localize:false loc context' body in match unlocalized_body with - Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n - | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> + NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n + | NCic.Appl (NCic.Rel n::l) when n <= List.length defs -> (try let l' = List.map @@ -315,29 +316,29 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast (HExtlib.map_option (add_binders `Pi) typ) in let name = match CicNotationUtil.cic_name_of_name name with - | Cic.Anonymous -> + | NCic.Anonymous -> CicNotationPt.fail loc "Recursive functions cannot be anonymous" - | Cic.Name name -> name + | NCic.Name name -> name in (name, decr_idx, cic_type, cic_body)) defs in let fix_or_cofix n = match kind with - `Inductive -> Cic.Fix (n,inductiveFuns) + `Inductive -> NCic.Fix (n,inductiveFuns) | `CoInductive -> let coinductiveFuns = List.map (fun (name, _, typ, body) -> name, typ, body) inductiveFuns in - Cic.CoFix (n,coinductiveFuns) + NCic.CoFix (n,coinductiveFuns) in let counter = ref ~-1 in - let build_term funs (var,_,ty,_) t = + let build_term _ (var,_,ty,_) t = incr counter; - Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) + NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t) in (match cic_body with `AvoidLetInNoAppl n -> @@ -345,7 +346,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast fix_or_cofix n' | `AvoidLetIn (n,l) -> let n' = List.length inductiveFuns - n in - Cic.Appl (fix_or_cofix n'::l) + NCic.Appl (fix_or_cofix n'::l) | `AddLetIn cic_body -> List.fold_right (build_term inductiveFuns) inductiveFuns cic_body) @@ -359,7 +360,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast let index = find_in_context name context in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here"; - Cic.Rel index + NCic.Rel index with Not_found -> let cic = if is_uri ast then (* we have the URI, build the term out of it *) @@ -383,23 +384,23 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast with Not_found -> raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst - | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) + | None -> List.map (fun uri -> uri, NCic.Implicit None) uris) in (try match cic with - | Cic.Const (uri, []) -> + | NCic.Const (uri, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in - Cic.Const (uri, mk_subst uris) - | Cic.Var (uri, []) -> + NCic.Const (uri, mk_subst uris) + | NCic.Var (uri, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in - Cic.Var (uri, mk_subst uris) - | Cic.MutInd (uri, i, []) -> + NCic.Var (uri, mk_subst uris) + | NCic.MutInd (uri, i, []) -> (try let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in - Cic.MutInd (uri, i, mk_subst uris) + NCic.MutInd (uri, i, mk_subst uris) with CicEnvironment.Object_not_found _ -> (* if we are here it is probably the case that during the @@ -408,12 +409,12 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast However, the inductive type is not yet in the environment *) (*here the explicit_named_substituion is assumed to be of length 0 *) - Cic.MutInd (uri,i,[])) - | Cic.MutConstruct (uri, i, j, []) -> + NCic.MutInd (uri,i,[])) + | NCic.MutConstruct (uri, i, j, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in - Cic.MutConstruct (uri, i, j, mk_subst uris) - | Cic.Meta _ | Cic.Implicit _ as t -> + NCic.MutConstruct (uri, i, j, mk_subst uris) + | NCic.Meta _ | NCic.Implicit _ as t -> (* debug_print (lazy (sprintf "Warning: %s must be instantiated with _[%s] but we do not enforce it" @@ -429,8 +430,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast with CicEnvironment.CircularDependency _ -> raise (Invalid_choice (None, lazy "Circular dependency in the environment")))) - | CicNotationPt.Implicit -> Cic.Implicit None - | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) + | CicNotationPt.Implicit -> NCic.Implicit None + | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () | CicNotationPt.Meta (index, subst) -> let cic_subst = @@ -440,16 +441,16 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | Some term -> Some (aux ~localize loc context term)) subst in - Cic.Meta (index, cic_subst) - | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop - | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set - | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) - | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) + NCic.Meta (index, cic_subst) + | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop + | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set + | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u) + | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function - | None -> Cic.Implicit annotation + | None -> NCic.Implicit annotation | Some term -> aux ~localize loc context term in aux ~localize:true HExtlib.dummy_floc context ast @@ -459,14 +460,14 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast = assert false (* - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in + let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast ~localization_tbl *) ;; let domain_of_term ~context = - let context = List.map (fun x -> Cic.Name (fst x)) context in + let context = List.map (fun x -> NCic.Name (fst x)) context in Disambiguate.domain_of_ast_term ~context ;; @@ -474,19 +475,20 @@ module Make (C : DisambiguateTypes.Callbacks) = struct module Disambiguator = Disambiguate.Make(C) let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - (text,prefix_len,term) = - let term = - if fresh_instances then CicNotationUtil.freshen_term term else term - in - let localization_tbl = Cic.CicHash.create 503 in - Disambiguator.disambiguate_thing + ?(initial_ugraph = ()) ~aliases ~universe + (text,prefix_len,term) + = + let term = + if fresh_instances then CicNotationUtil.freshen_term term else term + in + let localization_tbl = NCic.NCicHash.create 503 in + Disambiguator.disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases - ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl + ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term + ~domain_of_thing:domain_of_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~refine_thing:refine_term (text,prefix_len,term) + ~localization_tbl ;; end diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index 9b10e3448..5d845eb1f 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -11,8 +11,8 @@ (* $Id$ *) -exception RefineFailure of (Stdpp.location * string) Lazy.t;; -exception Uncertain of (Stdpp.location * string) Lazy.t;; +exception RefineFailure of Stdpp.location * (string Lazy.t);; +exception Uncertain of Stdpp.location * (string Lazy.t);; exception AssertFailure of string Lazy.t;; val typeof :