From 5d492df3e2715395a554f64dc3f040e13f892974 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jul 2009 16:11:36 +0000 Subject: [PATCH] initial implementation of coercion composition --- .../grafite_engine/grafiteEngine.ml | 220 +++++++++++++++--- .../components/ng_refiner/nCicCoercion.ml | 8 +- 2 files changed, 199 insertions(+), 29 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 49bd25638..1fd62d2b1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -495,8 +495,159 @@ let eval_unification_hint status t n = status,`New [] ;; +let product f l1 l2 = + List.fold_left + (fun acc x -> + List.fold_left + (fun acc y -> + f x y :: acc) + acc l2) + [] l1 +;; + +let pos_in_list x l = + match + HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l + with + | Some i -> i + | None _ -> assert false +;; + +let pos_of x t = + match t with + | NCic.Appl l -> pos_in_list x l + | _ -> assert false +;; + +let rec count_prod = function + | NCic.Prod (_,_,x) -> 1 + count_prod x + | _ -> 0 +;; + +let term_at i t = + match t with + | NCic.Appl l -> + (match + HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l + with + | Some i -> i + | None _ -> assert false) + | _ -> assert false +;; + +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 + | NCic.Prod (_,s,_) when i = j -> s + | NCic.Prod (_,_,t) -> aux (i+1) j t + | t -> assert (i = j); t + in + let mask t = + let rec aux () = function + | NCic.Meta _ + | NCic.Implicit _ as x -> x + | NCic.Rel _ -> NCic.Implicit `Type + | t -> NCicUtils.map (fun _ () -> ()) () aux t + in + aux () t + in + mask (aux 0 cpos ty), mask (aux 0 tpos ty) +;; + +let close_in_context t metasenv = + let rec aux m_subst subst ctx = function + | (i,(tag,[],ty)) :: tl -> + let name = "x" ^ string_of_int (List.length ctx) in + let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in + let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in + let m_subst m = + (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m) + in + NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl) + | [] -> NCicUntrusted.apply_subst subst ctx + (NCicSubstitution.lift (List.length ctx) t) + | _ -> assert false + in + aux (fun _ -> []) [] [] metasenv +;; + +let toposort metasenv = + let module T = HTopoSort.Make( + struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end) + in + let deps (_,(_,_,t)) = + List.filter (fun (j,_) -> + List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv + in + T.topological_sort metasenv deps +;; + let basic_eval_ncoercion (name,t,s,d,p,a) status = - NCicCoercion.index_coercion status t s d a p + let to_s = + NCicCoercion.look_for_coercion status [] [] [] (NCic.Implicit `Type) s + in + let from_d = + NCicCoercion.look_for_coercion status [] [] [] d (NCic.Implicit `Type) + in + let status = NCicCoercion.index_coercion status t s d a p in + let c = + List.find + (function (_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) + (NCicCoercion.look_for_coercion status [] [] [] s d) + in + let composites = + let to_s_o_c = + product (fun (m1,t1,_,j) (mc,c,_,i) -> m1@mc,c,[i,t1],j,a) + to_s [c] + in + let c_o_from_d = + product (fun (mc,c,_,j) (m1,t1,ty,i) -> m1@mc,t1,[i,c],j,count_prod ty) + [c] from_d + in + let to_s_o_c_o_from_d = + product (fun (m1,t1,_,j) (m,t,upl,i,a)-> + m@m1,t,(i,t1)::upl,j,a) + to_s c_o_from_d + in + to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d + in + let composites = + HExtlib.filter_map + (fun (metasenv, bo, upl, p, arity) -> + try + let metasenv, subst = + List.fold_left + (fun (metasenv,subst) (a,b) -> + NCicUnification.unify status metasenv subst [] a b) + (metasenv,[]) upl + in + let bo = NCicUntrusted.apply_subst subst [] bo in + let metasenv = toposort metasenv in + let bo = close_in_context bo metasenv in + let pos = + match p with + | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) + | _ -> assert false + in + let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in + let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in + prerr_endline ( + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ + " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity); + Some (bo,src,tgt,arity,pos) + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ -> None + ) composites + in + List.fold_left + (fun st (t,s,d,a,p) -> NCicCoercion.index_coercion st t s d a p) + status composites ;; let inject_ncoercion = @@ -506,6 +657,44 @@ let inject_ncoercion = NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion ;; +let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = + let status, src, cpos = + let rec aux cpos ctx = function + | NCic.Prod (name,ty,bo) -> + if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo + else + (try + let metasenv,subst,status,src = + GrafiteDisambiguate.disambiguate_nterm + None status ctx [] [] ("",0,src) in + let src = NCicUntrusted.apply_subst subst [] src in + (* CHECK that the declared pattern matches the abstraction *) + let _ = NCicUnification.unify status metasenv subst ctx ty src in + status, src, cpos + with + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ + | MultiPassDisambiguator.DisambiguationError _ -> + raise (GrafiteTypes.Command_error "bad source pattern")) + | _ -> assert false + in + aux 0 [] ty + in + let status, tgt, arity = + let metasenv,subst,status,tgt = + GrafiteDisambiguate.disambiguate_nterm + None status [] [] [] ("",0,tgt) in + let tgt = NCicUntrusted.apply_subst subst [] tgt in + (* CHECK che sia unificabile mancante *) + let rec count_prod = function + | NCic.Prod (_,_,x) -> 1 + count_prod x + | _ -> 0 + in + status, tgt, count_prod tgt + in + status, src, tgt, cpos, arity +;; + let eval_ncoercion status name t ty (id,src) tgt = let metasenv,subst,status,ty = @@ -517,33 +706,8 @@ let eval_ncoercion status name t ty (id,src) tgt = assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in - let src, cpos = - let rec aux cpos ctx = function - | NCic.Prod (name,ty,bo) -> - if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo - else - let metasenv,subst,status,src = - GrafiteDisambiguate.disambiguate_nterm - None status ctx [] [] ("",0,src) in - let src = NCicUntrusted.apply_subst subst [] src in - (* HMM: ma tanto se ignori l'informazione, a che serve?? *) - let _ = NCicUnification.unify status metasenv subst ctx ty src in - src, cpos - | _ -> assert false - in - aux 0 [] ty - in - let tgt, arity = - let metasenv,subst,status,tgt = - GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,tgt) in - let tgt = NCicUntrusted.apply_subst subst [] tgt in - (* CHECK *) - let rec count_prod = function - | NCic.Prod (_,_,x) -> 1 + count_prod x - | _ -> 0 - in - tgt, count_prod tgt + let status, src, tgt, cpos, arity = + src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 31768a62d..8a6e8a1c8 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -114,7 +114,13 @@ let look_for_coercion status metasenv subst context infty expty = 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 -- 2.39.2