From e869500069d11aadd7bbe8afddcdd9044d0b56a7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 8 Sep 2009 18:48:03 +0000 Subject: [PATCH] snapshot for CSC --- .../grafite_engine/grafiteEngine.ml | 16 ++- helm/software/components/ng_refiner/.depend | 20 ++-- helm/software/components/ng_refiner/Makefile | 2 +- .../components/ng_refiner/nCicCoercion.ml | 97 +++++++++++++++++-- .../components/ng_refiner/nCicCoercion.mli | 6 +- .../components/ng_refiner/nCicMetaSubst.ml | 23 ++--- .../components/ng_refiner/nCicRefiner.ml | 28 +++--- .../components/ng_refiner/nCicUnifHint.ml | 81 ++++++++++++---- .../components/ng_refiner/nCicUnifHint.mli | 5 + .../components/ng_refiner/nRstatus.ml | 5 +- .../components/ng_refiner/nRstatus.mli | 1 - .../components/ng_tactics/nCicElim.ml | 1 + 12 files changed, 204 insertions(+), 81 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c82fb457a..0904cf331 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -538,9 +538,18 @@ let term_at i t = let src_tgt_of_ty_cpos_arity ty cpos arity = let pis = count_prod ty in let tpos = pis - arity in - let rec aux i j = function + let rec pi_nth i j = function | NCic.Prod (_,s,_) when i = j -> s - | NCic.Prod (_,_,t) -> aux (i+1) j t + | NCic.Prod (_,_,t) -> pi_nth (i+1) j t + | t -> assert (i = j); t + in + let rec cleanup_prod = function + | NCic.Prod (_,_,t) -> NCic.Prod ("_",NCic.Implicit `Type, cleanup_prod t) + | _ -> NCic.Implicit `Type + in + let rec pi_tail i j = function + | NCic.Prod (_,_,_) as t when i = j -> cleanup_prod t + | NCic.Prod (_,_,t) -> pi_tail (i+1) j t | t -> assert (i = j); t in let mask t = @@ -552,7 +561,8 @@ let src_tgt_of_ty_cpos_arity ty cpos arity = in aux () t in - mask (aux 0 cpos ty), mask (aux 0 tpos ty) + mask (pi_nth 0 cpos ty), + mask (pi_tail 0 tpos ty) ;; let close_in_context t metasenv = diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 924b43fe8..35146bcc8 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,22 +1,26 @@ nDiscriminationTree.cmi: nCicMetaSubst.cmi: -nCicCoercion.cmi: nCicUnifHint.cmi: -nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi +nCicCoercion.cmi: nCicUnifHint.cmi +nRstatus.cmi: nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi nCicRefiner.cmi: nRstatus.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi -nCicCoercion.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicCoercion.cmi -nCicCoercion.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicCoercion.cmi nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi -nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi -nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi -nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi +nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi +nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmi +nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi +nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi +nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi nCicUnification.cmi +nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \ nCicRefiner.cmi nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \ diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 1fa79cd1c..9e0959c0d 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -4,8 +4,8 @@ PREDICATES = INTERFACE_FILES = \ nDiscriminationTree.mli \ nCicMetaSubst.mli \ - nCicCoercion.mli \ nCicUnifHint.mli \ + nCicCoercion.mli \ nRstatus.mli \ nCicUnification.mli \ nCicRefiner.mli diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index e48e77207..18540dcda 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -14,9 +14,10 @@ let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; -module COT : Set.OrderedType with type t = NCic.term * int * int = +module COT : Set.OrderedType with type t = NCic.term * int * int * NCic.term * +NCic.term = struct - type t = NCic.term * int * int + type t = NCic.term * int * int * NCic.term * NCic.term let compare = Pervasives.compare end @@ -31,18 +32,21 @@ let empty_db = DB.empty,DB.empty class status = object + inherit NCicUnifHint.status val db = empty_db method coerc_db = db method set_coerc_db v = {< db = v >} method set_coercion_status - : 'status. < coerc_db : db; .. > as 'status -> 'self - = fun o -> {< db = o#coerc_db >} + : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> + 'self + = fun o -> {< db = o#coerc_db >}#set_unifhint_status o end let index_coercion status c src tgt arity arg = let db_src,db_tgt = status#coerc_db in - let data = (c,arity,arg) in + let data = (c,arity,arg,src,tgt) in + let debug s = prerr_endline (Lazy.force s) in debug (lazy ("INDEX:" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^ @@ -103,17 +107,30 @@ let look_for_coercion status metasenv subst context infty expty = NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^ NCicPp.ppterm ~metasenv ~subst ~context expty)); - let set_src = DB.retrieve_unifiables db_src infty in - let set_tgt = DB.retrieve_unifiables db_tgt expty in + let src_class = infty :: NCicUnifHint.eq_class_of status infty in + let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in + + let set_src = + List.fold_left + (fun set infty -> + CoercionSet.union (DB.retrieve_unifiables db_src infty) set) + CoercionSet.empty src_class + in + let set_tgt = + List.fold_left + (fun set expty -> + CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set) + CoercionSet.empty tgt_class + in let candidates = CoercionSet.inter set_src set_tgt in debug (lazy ("CANDIDATES: " ^ - String.concat "," (List.map (fun (t,_,_) -> + String.concat "," (List.map (fun (t,_,_,_,_) -> NCicPp.ppterm ~metasenv ~subst ~context t) (CoercionSet.elements candidates)))); List.map - (fun (t,arity,arg) -> + (fun (t,arity,arg,_,_) -> let ty = try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t with NCicTypeChecker.TypeCheckerFailure s -> @@ -142,7 +159,7 @@ let match_coercion status ~metasenv ~subst ~context t = DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) [] in (HExtlib.list_findopt - (fun (p,arity,cpos) _ -> + (fun (p,arity,cpos,_,_) _ -> try let t = match p,t with @@ -165,3 +182,63 @@ let match_coercion status ~metasenv ~subst ~context t = Failure _ -> None (* raised by split_nth *) ) db) ;; + +let generate_dot_file status = + let module Pp = GraphvizPp.Dot in + let buf = Buffer.create 10240 in + let fmt = Format.formatter_of_buffer buf in + Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] + ~edge_attrs:["fontsize", "10"] fmt; + let src_db, _ = status#coerc_db in + let edges = ref [] in + DB.iter src_db (fun _ dataset -> + edges := !edges @ + List.map + (fun (t,a,g,sk,dk) -> + prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[] + ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk); + let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in + let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in + (t,a,g),eq_s,eq_t + ) + (CoercionSet.elements dataset); + ); + let nodes = + HExtlib.list_uniq + (List.sort compare + (List.flatten + (List.map + (fun (_,a,b) -> + [a;b] + ) + !edges))) + in + let names = ref [] in + let id = ref 0 in + let mangle l = + try List.assoc l !names + with Not_found -> + incr id; + names := (l,"node"^string_of_int!id) :: !names; + List.assoc l !names + in + List.iter + (fun cl -> + Pp.node (mangle cl) + ~attrs:["label",String.concat "\\n" + (List.map (fun t-> + NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:[] t ~margin:max_int + ) cl)] + fmt) + nodes; + List.iter + (fun ((t,a,b),src,tgt) -> + Pp.edge (mangle src) (mangle tgt) + ~attrs:["label", + NCicPp.ppterm ~metasenv:[] + ~subst:[] ~context:[] t] fmt) + !edges; + Pp.trailer fmt; + Buffer.contents buf +;; diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index ca65aa953..dc62cb86d 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -15,9 +15,11 @@ type db class status : object ('self) + inherit NCicUnifHint.status method coerc_db: db method set_coerc_db: db -> 'self - method set_coercion_status: -> 'self + method set_coercion_status: + -> 'self end val empty_db: db @@ -45,3 +47,5 @@ val look_for_coercion: val match_coercion: #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> context:NCic.context -> NCic.term -> (NCic.term * int * int) option + +val generate_dot_file: #status -> string diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 9cc6ac67c..927c288a0 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -254,7 +254,7 @@ let delift ~unify metasenv subst context n l t = in try aux () () t; false with Found -> true in - let unify_list ~alpha in_scope = + let unify_list in_scope = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> @@ -264,23 +264,16 @@ let delift ~unify metasenv subst context n l t = (fun (li,flexible) i -> if flexible || i < in_scope then None else let li = NCicSubstitution.lift (k+shift) li in - if alpha then - if NCicReduction.alpha_eq metasenv subst context li t then - Some ((metasenv,subst), NCic.Rel (i+1+k)) - else - None - else - match unify metasenv subst context li t with - | Some (metasenv,subst) -> - Some ((metasenv, subst), NCic.Rel (i+1+k)) - | None -> None) + match unify metasenv subst context li t with + | Some (metasenv,subst) -> + Some ((metasenv, subst), NCic.Rel (i+1+k)) + | None -> None) lb in let rec aux (context,k,in_scope) (metasenv, subst as ms) t = - match unify_list ~alpha:true in_scope metasenv subst context k t with + match unify_list in_scope metasenv subst context k t with | Some x -> x | None -> - try match t with | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> @@ -411,10 +404,6 @@ let delift ~unify metasenv subst context n l t = | t -> NCicUntrusted.map_term_fold_a (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t - with NotInTheList -> - match unify_list ~alpha:false in_scope metasenv subst context k t with - | Some x -> x - | None -> raise NotInTheList in try aux (context,0,0) (metasenv,subst) t with NotInTheList -> diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 26fc593b7..48d1eeb1c 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -378,7 +378,8 @@ and try_coercions rdb | NCicUnification.Uncertain _ as exc -> first exc tl in first exc - (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty) + (NCicCoercion.look_for_coercion + rdb metasenv subst context infty expty) and force_to_sort rdb metasenv subst context t orig_t localise ty = match NCicReduction.whd ~subst context ty with @@ -440,27 +441,26 @@ and guess_name subst ctx ty = and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args = (*D*)inside 'E'; try let rc = - let too_many_args = ref false in let rec aux metasenv subst args_so_far he ty_he = function | [] -> let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in - (match NCicReduction.whd ~subst context ty_he with - NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> - too_many_args := true; - | _ -> ()); force_ty true false metasenv subst context orig_t res ty_he expty | NCic.Implicit `Vector::tl -> + let has_some_more_pis x = + match NCicReduction.whd ~subst context x with + | NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false + | _ -> true + in (try - too_many_args := false; aux metasenv subst args_so_far he ty_he tl with - Uncertain _ - | RefineFailure _ as exc when !too_many_args <> true -> - try + | Uncertain _ + | RefineFailure _ as exc when has_some_more_pis ty_he -> + (try aux metasenv subst args_so_far he ty_he - (NCic.Implicit `Vector :: NCic.Implicit `Term :: tl) + (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl) with - Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)) + Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))) | arg::tl -> match NCicReduction.whd ~subst context ty_he with | C.Prod (_,s,t) -> @@ -490,7 +490,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); let metasenv, subst = - too_many_args := true; try NCicUnification.unify rdb metasenv subst context t flex_prod with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf ("The term %s has an inferred type %s, but is applied to the" ^^ @@ -506,14 +505,12 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he | C.Match (_,_,C.Meta _,_) | C.Match (_,_,C.Appl (C.Meta _ :: _),_) | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) -> - too_many_args := true; raise (Uncertain (lazy (localise orig_he, Printf.sprintf ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) (List.length args) (List.length args_so_far)))) | ty -> let metasenv, subst, newhead, newheadty = - too_many_args := true; try_coercions rdb ~localise metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) @@ -523,7 +520,6 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) (List.length args) (List.length args_so_far)))) in - too_many_args := false; aux metasenv subst [] newhead newheadty (arg :: tl) in (* We need to reverse the order of the new created metas since they diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index d166b1936..abca189d9 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -19,14 +19,21 @@ module COT : Set.OrderedType with type t = int * NCic.term = module HintSet = Set.Make(COT) -module DB = +module HDB = Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet) -type db = DB.t +module EQDB = + Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet) + +type db = + HDB.t * (* hint database: (dummy A B)[?] |-> \forall X.(summy a b)[X] *) + EQDB.t (* eqclass DB: A[?] |-> \forall X.B[X] and viceversa *) + +exception HintNotValid class status = object - val db = DB.empty + val db = HDB.empty, EQDB.empty method uhint_db = db method set_uhint_db v = {< db = v >} method set_unifhint_status @@ -45,29 +52,35 @@ let index_hint hdb context t1 t2 precedence = (match t2 with | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true) ); - let pair' = pair t1 t2 in - let data = + let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in + let t1_skeleton = + List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t1 context + in + let t2_skeleton = + List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t2 context + in + let src = pair t1_skeleton t2_skeleton in + let ctx2abstractions context t = List.fold_left (fun t (n,e) -> match e with | NCic.Decl ty -> NCic.Prod (n,ty,t) | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t)) - pair' context in - let src = - List.fold_left - (fun t (_,e) -> - match e with - | NCic.Decl _ -> - NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t - | NCic.Def _ -> - NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t) - pair' context in + t context + in + let data_hint = ctx2abstractions context (pair t1 t2) in + let data_t1 = t2_skeleton in + let data_t2 = t1_skeleton in (* prerr_endline ("INDEXING: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data); *) - hdb#set_uhint_db (DB.index hdb#uhint_db src (precedence, data)) + hdb#set_uhint_db ( + HDB.index (fst (hdb#uhint_db)) src (precedence, data_hint), + EQDB.index + (EQDB.index (snd (hdb#uhint_db)) t2_skeleton (precedence, data_t2)) + t1_skeleton (precedence, data_t1)) ;; let add_user_provided_hint db t precedence = @@ -75,7 +88,21 @@ let add_user_provided_hint db t precedence = let rec aux ctx = function | NCic.Appl l -> (match List.rev l with - | b::a::_ -> ctx, a, b + | b::a::_ -> + if + let ty_a = + NCicTypeChecker.typeof ~metasenv:[] ~subst:[] ctx a + in + let ty_b = + NCicTypeChecker.typeof ~metasenv:[] ~subst:[] ctx b + in + NCicReduction.are_convertible + ~metasenv:[] ~subst:[] ctx ty_a ty_b + && + NCicReduction.are_convertible + ~metasenv:[] ~subst:[] ctx a b + then ctx, a, b + else raise HintNotValid | _ -> 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 @@ -133,7 +160,7 @@ let db () = aux [] l r | _ -> [] in - let hints = + let _hints = List.fold_left (fun acc (_,_,l) -> acc @ @@ -173,19 +200,31 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = res, newmetasenv, arguments ;; +let eq_class_of hdb t1 = + if NDiscriminationTree.NCicIndexable.path_string_of t1 = + [Discrimination_tree.Variable] + then + [] (* if the trie is unable to handle the key, we skip the query since + it sould retulr the whole content of the trie *) + else + let candidates = EQDB.retrieve_unifiables (snd hdb#uhint_db) t1 in + let candidates = HintSet.elements candidates in + List.map snd (List.sort (fun (x,_) (y,_) -> compare x y) candidates) +;; + let look_for_hint hdb metasenv subst context t1 t2 = (* prerr_endline ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t1 t2)); prerr_endline ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t2 t1)); - DB.iter hdb + HDB.iter hdb (fun p ds -> prerr_endline ("ENTRY: " ^ NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^ String.concat "|" (List.map (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]) (HintSet.elements ds)))); *) - let candidates1 = DB.retrieve_unifiables hdb#uhint_db (pair t1 t2) in - let candidates2 = DB.retrieve_unifiables hdb#uhint_db (pair t2 t1) in + let candidates1 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t1 t2) in + let candidates2 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t2 t1) in let candidates1 = List.map (fun (prec,ty) -> prec,true,saturate ~delta:max_int metasenv subst context ty 0) diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 7b8536ba7..87519352c 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -13,6 +13,8 @@ type db +exception HintNotValid + class status : object ('self) method uhint_db: db @@ -32,3 +34,6 @@ val look_for_hint: NCic.term -> NCic.term -> (NCic.metasenv * (NCic.term * NCic.term) * (NCic.term * NCic.term) list) list + +val eq_class_of: + #status -> NCic.term -> NCic.term list diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index bb2d357d7..26482e61b 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -13,7 +13,6 @@ class status = object (self) - inherit NCicUnifHint.status inherit NCicCoercion.status inherit NCicLibrary.status method set_rstatus @@ -22,7 +21,7 @@ class status = uhint_db : NCicUnifHint.db; timestamp: NCicLibrary.timestamp; .. > as 'status -> 'self = fun o -> - ((self#set_unifhint_status o)#set_coercion_status o)#set_library_status o + (self#set_coercion_status o)#set_library_status o end type sstatus = status @@ -33,8 +32,8 @@ module Serializer = let require ~baseuri status = let rstatus = require ~baseuri (status : #status :> status) in - let status = status#set_uhint_db (rstatus#uhint_db) in let status = status#set_coerc_db (rstatus#coerc_db) in + let status = status#set_uhint_db (rstatus#uhint_db) in let status = status#set_timestamp (rstatus#timestamp) in status end diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 89f62ce1d..10a4a8a62 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -13,7 +13,6 @@ class status : object ('self) - inherit NCicUnifHint.status inherit NCicCoercion.status inherit NCicLibrary.status method set_rstatus: diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 9db98de49..d5cbca892 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -38,6 +38,7 @@ let mk_appl = function [] -> assert false | [x] -> x + | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2) | l -> CicNotationPt.Appl l ;; -- 2.39.2