From c7a74f0ef29118fc97c1a6283f4249a0ed4b0ba1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Jun 2009 23:00:56 +0000 Subject: [PATCH] 1) unification hint now takes NG terms (as it should have been from the very beginning) 2) refresh_uris_in_term is now passed to the constructor of the existential/universal data type in NCicLibrary 3) URIs are now refreshed in unification hint data --- helm/software/components/grafite/grafiteAst.ml | 2 +- helm/software/components/grafite/grafiteAstPp.ml | 2 +- .../components/grafite_engine/grafiteEngine.ml | 14 +++++++++++--- .../grafite_parser/grafiteDisambiguate.ml | 8 +------- helm/software/components/ng_kernel/nCicLibrary.ml | 10 ++++++++-- helm/software/components/ng_kernel/nCicLibrary.mli | 5 ++++- .../software/components/ng_refiner/nCicUnifHint.ml | 9 +++------ .../components/ng_refiner/nCicUnifHint.mli | 2 +- 8 files changed, 30 insertions(+), 22 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 27afd3904..fe060d415 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -196,7 +196,7 @@ type ('term,'obj) command = int (* arity *) * int (* saturations *) | PreferCoercion of loc * 'term | Inverter of loc * string * 'term * bool list - | UnificationHint of loc * 'term * int (* term, precedence *) + | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | Default of loc * string * UriManager.uri list | Drop of loc | Include of loc * bool (* normal? *) * string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 98d33464b..c1c83ee09 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -360,7 +360,7 @@ let pp_command ~term_pp ~obj_pp = function | Inverter (_,n,ty,params) -> "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params | UnificationHint (_,t, n) -> - "unification hint " ^ string_of_int n ^ " " ^ term_pp t + "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,true,path) -> "include \"" ^ path ^ "\"" diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 98bfef9d6..6e6a5bc73 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -478,10 +478,19 @@ let basic_eval_unification_hint (t,n) status = ;; let inject_unification_hint = - NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint + let basic_eval_unification_hint (t,n) ~refresh_uri_in_term = + let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) + in + NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint ;; let eval_unification_hint status t n = + let estatus = GrafiteTypes.get_estatus status in + let metasenv,subst,estatus,t = + GrafiteDisambiguate.disambiguate_nterm None estatus [] [] [] ("",0,t) in + assert (metasenv=[]); + let t = NCicUntrusted.apply_subst subst [] t in + let status = GrafiteTypes.set_estatus estatus status in let rstatus = basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in let status = GrafiteTypes.set_rstatus rstatus status in @@ -721,8 +730,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status Inversion_principle.build_inverter ~add_obj status uri indty_uri params in res,`Old uris - | GrafiteAst.UnificationHint (loc, t, n) -> - eval_unification_hint status t n + | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,`Old [] diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 64c4c8ebe..0dfab7a37 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -834,13 +834,7 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= let metasenv,indty = disambiguate_term metasenv indty in { estatus with NEstatus.lstatus = !lexicon_status_ref }, metasenv, GrafiteAst.Inverter (loc,n,indty,params) - | GrafiteAst.UnificationHint (loc, t, n) -> - let lexicon_status_ref = ref estatus.NEstatus.lstatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let metasenv,t = disambiguate_term metasenv t in - { estatus with NEstatus.lstatus = !lexicon_status_ref }, - metasenv, GrafiteAst.UnificationHint (loc,t,n) + | GrafiteAst.UnificationHint _ | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 80b0911b2..cc13dde6e 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -79,7 +79,10 @@ module type Serializer = sig type status type obj - val register: string -> ('a -> status -> status) -> ('a -> obj) + val register: + string -> + ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) val serialize: baseuri:NUri.uri -> obj list -> unit val require: baseuri:NUri.uri -> status -> status end @@ -97,7 +100,10 @@ module Serializer(S: sig type status end) = already_registered := tag :: !already_registered; require1 := (fun (tag',data) as x -> - if tag=tag' then require (Obj.magic data) else !require1 x); + if tag=tag' then + require (Obj.magic data) ~refresh_uri_in_term + else + !require1 x); (fun x -> tag,Obj.repr x) let serialize = serialize diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 2d04b7d11..526632565 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -31,7 +31,10 @@ module type Serializer = sig type status type obj - val register: string -> ('a -> status -> status) -> ('a -> obj) + val register: + string -> + ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) val serialize: baseuri:NUri.uri -> obj list -> unit val require: baseuri:NUri.uri -> status -> status end diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 9532ba985..c09e08d3c 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -63,20 +63,17 @@ let index_hint hdb context t1 t2 precedence = let empty_db = DB.empty ;; let add_user_provided_hint db t precedence = - let u = UriManager.uri_of_string "cic:/foo/bar.con" in let c, a, b = let rec aux ctx = function | NCic.Appl l -> (match List.rev l with | b::a::_ -> ctx, a, b | _ -> assert false) - | NCic.Prod (n,s,t) -> - aux ((n, NCic.Decl s) :: ctx) t - | NCic.LetIn (n,ty,t,b) -> - aux ((n, NCic.Def (t,ty)) :: ctx) b + | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t + | NCic.LetIn (n,ty,t,b) -> aux ((n, NCic.Def (t,ty)) :: ctx) b | _ -> assert false in - aux [] (fst (OCic2NCic.convert_term u t)) + aux [] t in index_hint db c a b precedence ;; diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index bb8bc6af1..21820ace4 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -16,7 +16,7 @@ type db val index_hint: db -> NCic.context -> NCic.term -> NCic.term -> int -> db -val add_user_provided_hint : db -> Cic.term -> int -> db +val add_user_provided_hint : db -> NCic.term -> int -> db val empty_db : db -- 2.39.2