X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=e48e772079b86ef6d0d0eb8fafc9fca6706b3852;hb=67d5f78ad9593d51846bd6a69fca27e9a4ef0e6d;hp=a4b10296f2f5f960d7074285abebcc34bccb3cbd;hpb=84e770b58ae08a345087de816aba29bc2fc727ba;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index a4b10296f..e48e77207 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -11,6 +11,9 @@ (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) +let debug s = prerr_endline (Lazy.force s);; +let debug _ = ();; + module COT : Set.OrderedType with type t = NCic.term * int * int = struct type t = NCic.term * int * int @@ -24,24 +27,39 @@ module DB = type db = DB.t * DB.t -let index_coercion (db_src,db_tgt) c src tgt arity arg = +let empty_db = DB.empty,DB.empty + +class status = + object + 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 >} + 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 -(* - prerr_endline ("INDEX:" ^ + + debug (lazy ("INDEX:" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c); -*) + NCicPp.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 - db_src, db_tgt + status#set_coerc_db (db_src, db_tgt) ;; -let db () = +let index_old_db odb (status : #status) = List.fold_left - (fun db (_,tgt,clist) -> + (fun status (_,tgt,clist) -> List.fold_left - (fun db (uri,_,arg) -> + (fun status (uri,_,arg) -> + try let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in let src, tgt = @@ -55,55 +73,95 @@ let db () = NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt in (* - prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" + 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 -> - prerr_endline ( - NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); + debug (lazy ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t)); assert false in - index_coercion db c src tgt arity arg) - db clist) - (DB.empty,DB.empty) (CoercDb.to_list ()) + index_coercion status c src tgt arity arg + with + | NCicEnvironment.BadDependency _ + | NCicTypeChecker.TypeCheckerFailure _ -> status) + status clist) + status (CoercDb.to_list odb) ;; -let empty_db = (DB.empty,DB.empty) ;; - - -let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty = +let look_for_coercion status metasenv subst context infty expty = + let db_src,db_tgt = status#coerc_db in match infty, expty with | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] | _ -> -(* - prerr_endline ("LOOK FOR COERCIONS: " ^ + + debug (lazy ("LOOK FOR COERCIONS: " ^ NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^ - NCicPp.ppterm ~metasenv ~subst ~context expty); -*) + 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 candidates = CoercionSet.inter set_src set_tgt in -(* - prerr_endline ("CANDIDATES: " ^ + + debug (lazy ("CANDIDATES: " ^ String.concat "," (List.map (fun (t,_,_) -> NCicPp.ppterm ~metasenv ~subst ~context t) - (CoercionSet.elements candidates))); -*) + (CoercionSet.elements candidates)))); + List.map (fun (t,arity,arg) -> - let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in + let ty = + try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t + with NCicTypeChecker.TypeCheckerFailure s -> + prerr_endline ("illtyped coercion: "^Lazy.force s); + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + assert false + in let ty, metasenv, args = NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity in - (* prerr_endline ( + + debug (lazy ( NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicUntrusted.mk_appl t args) ^ " --- " ^ - string_of_int (List.length args) ^ " == " ^ string_of_int arg); *) + string_of_int (List.length args) ^ " == " ^ string_of_int arg)); + metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) (CoercionSet.elements candidates) ;; + +(* CSC: very inefficient implementation! + Enrico, can we use a discrimination tree here? *) +let match_coercion status ~metasenv ~subst ~context t = + let db = + DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) [] + in + (HExtlib.list_findopt + (fun (p,arity,cpos) _ -> + try + let t = + match p,t with + NCic.Appl lp, NCic.Appl lt -> + (match fst (HExtlib.split_nth (List.length lp) lt) with + [t] -> t + | l -> NCic.Appl l) + | _,NCic.Appl (he::_) -> he + | _,_ -> t + in + let b = NCicReduction.alpha_eq metasenv subst context p t in + if not b then None else + let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in + let pis = + let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in + aux ty + in + Some (p,pis - arity - cpos - 1,cpos) + with + Failure _ -> None (* raised by split_nth *) + ) db) +;;