X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=bb6430873c0af142fea6f17b5634487bd3fa7d49;hb=HEAD;hp=04fddee83fdee339546a4bf42484bdf3e23d8f73;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_refiner/nCicCoercion.ml b/matita/components/ng_refiner/nCicCoercion.ml index 04fddee83..bb6430873 100644 --- a/matita/components/ng_refiner/nCicCoercion.ml +++ b/matita/components/ng_refiner/nCicCoercion.ml @@ -18,11 +18,10 @@ let convert_term = ref (fun _ _ -> assert false);; 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) @@ -40,81 +39,43 @@ class type g_status = 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 status#set_coerc_db (db_src, db_tgt) ;; -let index_old_db odb (status : #status) = - List.fold_left - (fun status (_,tgt,clist) -> - List.fold_left - (fun status (uri,_,arg) -> - try - let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in - let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in - let src, tgt = - let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in - let scty, metasenv,_ = - NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) - in - match scty with - | NCic.Prod (_, src, tgt) -> - let tgt = - NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt - in -(* - debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1) - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src) - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt)); -*) - src, tgt - | t -> - debug (lazy ( - NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t)); - assert false - in - index_coercion status "foo" c src tgt arity arg - with - | NCicEnvironment.BadDependency _ - | NCicTypeChecker.TypeCheckerFailure _ -> status) - status clist) - status (CoercDb.to_list odb) -;; - 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 @@ -122,53 +83,53 @@ let look_for_coercion status metasenv subst context infty expty = 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! @@ -189,9 +150,9 @@ let match_coercion status ~metasenv ~subst ~context t = | _,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 @@ -202,7 +163,7 @@ let match_coercion status ~metasenv ~subst ~context t = ) 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 @@ -210,7 +171,7 @@ let generate_dot_file status fmt = 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 @@ -242,7 +203,7 @@ let generate_dot_file status fmt = 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)