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 =
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 =
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 \
INTERFACE_FILES = \
nDiscriminationTree.mli \
nCicMetaSubst.mli \
- nCicCoercion.mli \
nCicUnifHint.mli \
+ nCicCoercion.mli \
nRstatus.mli \
nCicUnification.mli \
nCicRefiner.mli
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
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 ^ " := " ^
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 ->
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
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
+;;
class status :
object ('self)
+ inherit NCicUnifHint.status
method coerc_db: db
method set_coerc_db: db -> 'self
- method set_coercion_status: <coerc_db: db; ..> -> 'self
+ method set_coercion_status: <coerc_db: db; uhint_db: NCicUnifHint.db; ..>
+ -> 'self
end
val empty_db: db
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
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 ->
(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 ->
| 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 ->
| 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
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) ->
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" ^^
| 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))
"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
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
(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 =
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
aux [] l r
| _ -> []
in
- let hints =
+ let _hints =
List.fold_left
(fun acc (_,_,l) ->
acc @
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)
type db
+exception HintNotValid
+
class status :
object ('self)
method uhint_db: db
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
class status =
object (self)
- inherit NCicUnifHint.status
inherit NCicCoercion.status
inherit NCicLibrary.status
method set_rstatus
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
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
class status :
object ('self)
- inherit NCicUnifHint.status
inherit NCicCoercion.status
inherit NCicLibrary.status
method set_rstatus:
function
[] -> assert false
| [x] -> x
+ | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2)
| l -> CicNotationPt.Appl l
;;
projects / helm.git / commitdiff