From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 10 Jul 2009 16:11:36 +0000 (+0000)
Subject: initial implementation of coercion composition
X-Git-Tag: make_still_working~3699
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5d492df3e2715395a554f64dc3f040e13f892974

initial implementation of coercion composition
---

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