let set_convert_term f = convert_term := f;;
module COT : Set.OrderedType
-with type t = string * NCic.term * int * int * NCic.term *
-NCic.term =
+with type t = string * NCic.term * int * int * NCic.term * NCic.term =
struct
type t = string * NCic.term * int * int * NCic.term * NCic.term
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module CoercionSet = Set.Make(COT)
method coerc_db: db
end
-class status =
+class virtual 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. #g_status as 'status -> 'self
+ : 'status. (#g_status as 'status) -> 'self
= fun o -> {< db = o#coerc_db >}#set_unifhint_status o
end
-let index_coercion status name c src tgt arity arg =
+let index_coercion (status:#status) name c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
let data = (name,c,arity,arg,src,tgt) in
debug (lazy ("INDEX:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
string_of_int arg ^ " " ^ string_of_int arity));
let db_src = DB.index db_src src data in
let db_tgt = DB.index db_tgt tgt data in
let look_for_coercion status metasenv subst context infty expty =
let db_src,db_tgt = status#coerc_db in
match
- NCicUntrusted.apply_subst subst context infty,
- NCicUntrusted.apply_subst subst context expty
+ NCicUntrusted.apply_subst status subst context infty,
+ NCicUntrusted.apply_subst status subst context expty
with
| (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
(NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
| infty, expty ->
debug (lazy ("LOOK FOR COERCIONS: " ^
- NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
- NCicPp.ppterm ~metasenv ~subst ~context expty));
+ status#ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
+ status#ppterm ~metasenv ~subst ~context expty));
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
+ DB.Collector.union (DB.retrieve_unifiables_sorted db_src infty) set)
+ DB.Collector.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
+ DB.Collector.union (DB.retrieve_unifiables_sorted db_tgt expty) set)
+ DB.Collector.empty tgt_class
in
debug (lazy ("CANDIDATES SRC: " ^
String.concat "," (List.map (fun (name,t,_,_,_,_) ->
- name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
- (CoercionSet.elements set_src))));
+ name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t)
+ (DB.Collector.to_list set_src))));
debug (lazy ("CANDIDATES TGT: " ^
String.concat "," (List.map (fun (name,t,_,_,_,_) ->
- name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
- (CoercionSet.elements set_tgt))));
+ name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t)
+ (DB.Collector.to_list set_tgt))));
- let candidates = CoercionSet.inter set_src set_tgt in
+ let candidates = DB.Collector.inter set_src set_tgt in
debug (lazy ("CANDIDATES: " ^
String.concat "," (List.map (fun (name,t,_,_,_,_) ->
- name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
- (CoercionSet.elements candidates))));
+ name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t)
+ candidates)));
List.map
(fun (name,t,arity,arg,_,_) ->
let ty =
- try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
+ try NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] t
with NCicTypeChecker.TypeCheckerFailure s ->
prerr_endline ("illtyped coercion: "^Lazy.force s);
- prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ prerr_endline (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
assert false
in
let ty, metasenv, args =
- NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
+ NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty arity
in
debug (lazy (
- NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
- NCicPp.ppterm ~metasenv ~subst ~context
+ status#ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
+ status#ppterm ~metasenv ~subst ~context
(NCicUntrusted.mk_appl t args) ^ " --- " ^
string_of_int (List.length args) ^ " == " ^ string_of_int arg));
name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
- (CoercionSet.elements candidates)
+ candidates
;;
(* CSC: very inefficient implementation!
| _,NCic.Appl (he::_) -> he
| _,_ -> t
in
- let b = NCicReduction.alpha_eq metasenv subst context p t in
+ let b = NCicReduction.alpha_eq status metasenv subst context p t in
if not b then None else
- let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+ let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] p in
let pis =
let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
aux ty
) db)
;;
-let generate_dot_file status fmt =
+let generate_dot_file (status:#status) fmt =
let module Pp = GraphvizPp.Dot in
let src_db, _ = status#coerc_db in
let edges = ref [] in
edges := !edges @
List.map
(fun (name,t,a,g,sk,dk) ->
- debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+ debug(lazy (let p = status#ppterm ~metasenv:[] ~context:[]
~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
let eq_s= sk::NCicUnifHint.eq_class_of status sk in
let eq_t= dk::NCicUnifHint.eq_class_of status dk in
Pp.node (mangle cl)
~attrs:["label",String.concat "\\n"
(List.map (fun t->
- NCicPp.ppterm ~metasenv:[] ~subst:[]
+ status#ppterm ~metasenv:[] ~subst:[]
~context:[] t ~margin:max_int
) cl)]
fmt)