]> matita.cs.unibo.it Git - helm.git/commitdiff
Coercions rework:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:24:13 +0000 (13:24 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:24:13 +0000 (13:24 +0000)
- new functions:
  - coerce_to_sort
  - coerce_to_something
  - coerce_atom_to_something
- added call in Cast
- coerce_to_something goes under lambdas in both
  variant and contravarian positions, to if there are
  c1: B -> B1 and c2:A1 -> C coercions, you can cast a function
  f: A -> B to A1 -> B1.

helm/software/components/cic_unification/cicRefine.ml

index 856c9a58622480d6f938cbeb0e8a25c1ce913473..ad5ae94dcb350c5772939dc5681343a8be8e6542 100644 (file)
@@ -326,6 +326,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
+(*
     let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
      let subst,metasenv,ugraph =
       fo_unif_subst subst context metasenv last t ugraph
@@ -339,6 +340,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       with 
       | RefineFailure _ | Uncertain _ -> None
     in
+*)
      let (t',_,_,_,_) as res =
       match t with
           (*    function *)
@@ -420,76 +422,26 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    inferredty ty' ugraph2
                in
                 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
-              with
-               exn ->
-                enrich localization_tbl te'
-                 ~f:(fun _ ->
-                   lazy ("(3)The term " ^
-                    CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
-                     context ^ " has type " ^
-                    CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
-                     context ^ " but is here used with type " ^
-                    CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn
-             )
-        | C.Prod (name,s,t) ->
-            let carr t subst context = CicMetaSubst.apply_subst subst t in
-            let coerce_to_sort in_source tgt_sort t type_to_coerce
-                 subst context metasenv uragph 
-            =
-              if not !insert_coercions then
-                t,type_to_coerce,subst,metasenv,ugraph
-              else
-                let coercion_src = carr type_to_coerce subst context in
-                match coercion_src with
-                | Cic.Sort _ -> 
-                    t,type_to_coerce,subst,metasenv,ugraph
-                | Cic.Meta _ as meta -> 
-                    t, meta, subst, metasenv, ugraph
-                | Cic.Cast _ as cast -> 
-                    t, cast, subst, metasenv, ugraph
-                | term -> 
-                    let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
-                    let boh =
-                     CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
+              with 
+              | Uncertain _ | RefineFailure _ ->
+                  let exn = 
+                    RefineFailure (lazy ("(3)The term " ^
+                      CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
+                       context ^ " has type " ^
+                      CicMetaSubst.ppterm_in_context metasenv'' 
+                        subst'' inferredty context ^ 
+                      " but is here used with type " ^
+                      CicMetaSubst.ppterm_in_context 
+                        metasenv'' subst'' ty' context))
+                  in
+                  try 
+                    let (te, ty), subst, metasenv, ugraph =
+                      coerce_to_something te' inferredty ty'
+                        subst'' metasenv'' context exn ugraph2
                     in
-                    (match boh with
-                    | CoercGraph.NoCoercion
-                    | CoercGraph.SomeCoercionToTgt _
-                    | CoercGraph.NotHandled _ ->
-                       enrich localization_tbl t
-                        (RefineFailure 
-                          (lazy ("(4)The term " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
-                          " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv
-                           subst coercion_src context ^ " that is not a sort")))
-                    | CoercGraph.NotMetaClosed -> 
-                       enrich localization_tbl t
-                        (Uncertain 
-                          (lazy ("(5)The term " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
-                          " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv
-                           subst coercion_src context ^ " that is not a sort")))
-                    | CoercGraph.SomeCoercion candidates -> 
-                        let selected = 
-                          HExtlib.list_findopt
-                            (try_coercion t subst context ugraph coercion_tgt)
-                            candidates
-                        in
-                        match selected with
-                        | Some x -> x
-                        | None -> 
-                            enrich localization_tbl t
-                              (RefineFailure 
-                                (lazy ("(6)The term " ^ 
-                                CicMetaSubst.ppterm_in_context ~metasenv
-                                  subst t context ^ 
-                                  " is not a type since it has type " ^ 
-                                  CicMetaSubst.ppterm_in_context ~metasenv
-                                  subst coercion_src context ^ 
-                                  " that is not a sort")))) 
-            in
+                    C.Cast (te, ty'), ty', subst, metasenv, ugraph
+                  with exn -> enrich localization_tbl te' exn)
+        | C.Prod (name,s,t) ->
             let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph 
             in
@@ -513,54 +465,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
         | C.Lambda (n,s,t) ->
             let s',sort1,subst',metasenv',ugraph1 = 
-              type_of_aux subst metasenv context s ugraph in
+              type_of_aux subst metasenv context s ugraph 
+            in
             let s',sort1,subst',metasenv',ugraph1 =
-              if not !insert_coercions then
-                s',sort1, subst', metasenv', ugraph1
-              else
-                match CicReduction.whd ~subst:subst' context sort1 with
-                  | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
-                  | coercion_src ->
-                     let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
-                     let boh =
-                      CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
-                     in
-                      match boh with
-                      | CoercGraph.NoCoercion
-                      | CoercGraph.SomeCoercionToTgt _
-                      |  CoercGraph.NotHandled _ ->
-                        enrich localization_tbl s'
-                         (RefineFailure 
-                          (lazy ("(7)The term " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
-                          " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv
-                           subst coercion_src context ^ " that is not a sort")))
-                      | CoercGraph.NotMetaClosed -> 
-                        enrich localization_tbl s'
-                         (Uncertain 
-                          (lazy ("(8)The term " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
-                          " is not a type since it has type " ^ 
-                          CicMetaSubst.ppterm_in_context ~metasenv 
-                           subst coercion_src context ^ " that is not a sort")))
-                      | CoercGraph.SomeCoercion candidates -> 
-                        let selected = 
-                          HExtlib.list_findopt
-                           (try_coercion s' subst' context ugraph1 coercion_tgt)
-                           candidates
-                        in
-                        match selected with
-                        | Some x -> x
-                        | None -> 
-                           enrich localization_tbl s'
-                            (RefineFailure 
-                             (lazy ("(9)The term " ^ 
-                              CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
-                              " is not a type since it has type " ^ 
-                              CicMetaSubst.ppterm_in_context ~metasenv
-                              subst coercion_src context ^ 
-                              " that is not a sort")))
+              coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+              s' sort1 subst' context metasenv' ugraph1
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let t',type2,subst'',metasenv'',ugraph2 =
@@ -685,8 +594,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                expected_type' actual_type ugraph2
             with
              exn ->
-               prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
-               prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
               enrich localization_tbl term' exn
                ~f:(function _ ->
                  lazy ("(10)The term " ^
@@ -852,8 +759,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                                     candidate_oty,ugraph,metasenv,subst
                                  with
                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
-                                  | CicUnification.UnificationFailure _
-                                  | CicUnification.Uncertain _ ->
+                                  | RefineFailure _ | Uncertain _ ->
                                      None,ugraph,metasenv,subst
                          ) (Some instance',ugraph4,metasenv,subst) tl
                        in
@@ -1393,9 +1299,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     debug_print (lazy " success!");
                     Some (subst,metasenv,ugraph,tty,t,remainder) 
                   with 
-                  | Uncertain _ | RefineFailure _
-                  | CicUnification.UnificationFailure _ 
-                  | CicUnification.Uncertain _ -> 
+                  | Uncertain _ | RefineFailure _ ->
                       try 
                         let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
                           fix_arity
@@ -1430,84 +1334,18 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
             match (CicReduction.whd ~subst context hetype) with 
             | Cic.Prod (n,s,t) ->
                 let arg,subst,metasenv,ugraph1 =
-                  try
+                 try
+                  (try
                     let subst,metasenv,ugraph1 = 
                       fo_unif_subst_eat_prods2 
                         subst context metasenv hety s ugraph
                     in
                       (hete,hety),subst,metasenv,ugraph1
-                  (* {{{ we search a coercion from hety to s if fails *)
                   with RefineFailure _ | Uncertain _ as exn 
                   when allow_coercions && !insert_coercions ->
-                    let coer, tgt_carr = 
-                      let carr t subst context = 
-                        CicReduction.whd ~delta:false 
-                          context (CicMetaSubst.apply_subst subst t )
-                      in
-                      let c_hety = carr hety subst context in
-                      let c_s = carr s subst context in 
-                      CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
-                    in
-                    (match coer with
-                    | CoercGraph.NoCoercion 
-                    | CoercGraph.SomeCoercionToTgt _
-                    | CoercGraph.NotHandled _ ->
-                        enrich localization_tbl hete exn
-                         ~f:(fun _ ->
-                           (lazy ("(15)The term " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst hete
-                              context ^ " has type " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst hety
-                              context ^ " but is here used with type " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst s context
-                              (* "\nReason: " ^ Lazy.force e*))))
-                    | CoercGraph.NotMetaClosed -> 
-                        enrich localization_tbl hete exn
-                         ~f:(fun _ ->
-                           (lazy ("(16)The term " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst hete
-                              context ^ " has type " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst hety
-                              context ^ " but is here used with type " ^
-                             CicMetaSubst.ppterm_in_context ~metasenv subst s context
-                              (* "\nReason: " ^ Lazy.force e*))))
-                    | CoercGraph.SomeCoercion candidates -> 
-                        let selected = 
-                          HExtlib.list_findopt
-                            (fun (metasenv,last,c) -> 
-                             try
-                              let subst,metasenv,ugraph =
-                               fo_unif_subst subst context metasenv last hete
-                                ugraph in
-                              let newt,newhety,subst,metasenv,ugraph = 
-                               type_of_aux subst metasenv context
-                                c ugraph 
-                              in
-                              let newt, newty, subst, metasenv, ugraph = 
-                               avoid_double_coercion context subst metasenv
-                                ugraph newt tgt_carr 
-                              in
-                              let subst,metasenv,ugraph1 = 
-                                fo_unif_subst subst context metasenv 
-                                   newhety s ugraph
-                              in
-                               Some ((newt,newty), subst, metasenv, ugraph)
-                             with Uncertain _ | RefineFailure _ -> None)
-                            candidates
-                        in
-                        (match selected with
-                        | Some x -> x
-                        | None ->  
-                           enrich localization_tbl hete
-                            ~f:(fun _ ->
-                             (lazy ("(1)The term " ^
-                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
-                               context ^ " has type " ^
-                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
-                               context ^ " but is here used with type " ^
-                              CicMetaSubst.ppterm_in_context ~metasenv subst s context
-                               (* "\nReason: " ^ Lazy.force e*)))) exn))
-                  | exn ->
+                     coerce_to_something 
+                       hete hety s subst metasenv context exn ugraph) 
+                 with exn ->
                      enrich localization_tbl hete
                       ~f:(fun _ ->
                         (lazy ("(2)The term " ^
@@ -1515,9 +1353,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                            context ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst hety
                            context ^ " but is here used with type " ^
-                          CicMetaSubst.ppterm_in_context ~metasenv subst s context
+                          CicMetaSubst.ppterm_in_context 
+                            ~metasenv subst s context
                            (* "\nReason: " ^ Printexc.to_string exn*)))) exn
-                  (* }}} end coercion stuff *)
                 in
                   eat_prods_and_args pristinemenv metasenv subst context pristinehe he
                     (CicSubstitution.subst (fst arg) t) 
@@ -1556,6 +1394,107 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
     in
     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
+
+  and coerce_to_something t infty expty subst metasenv context exn ugraph =
+    if not !insert_coercions then
+      raise exn
+    else
+    let clean t subst context = 
+      CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
+    in
+    let infty = clean infty subst context in
+    let expty = clean expty subst context in
+    match infty, expty with
+    | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> 
+        (* covariant part *)
+        let name_con = Cic.Name "name_con" in
+        let name_t, ty_s_bo, bo = 
+          match t with
+          | Cic.Lambda (name, src, bo) -> name, src, bo
+          | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
+        in
+        let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
+        let (bo, _), subst, metasenv, ugraph = 
+          coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
+        in
+        (* contravariant part *)
+        let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
+        let (rel1, _), subst, metasenv, ugraph = 
+          coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
+            (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn 
+            ugraph 
+        in
+        let coerced = 
+          Cic.Lambda (name_t,src2,
+            CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
+        in
+          (coerced, expty), subst, metasenv, ugraph
+    | _ -> 
+       coerce_atom_to_something t infty expty subst metasenv context exn ugraph
+
+  and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
+    let coer = 
+      CoercGraph.look_for_coercion metasenv subst context infty expty
+    in
+      match coer with
+      | CoercGraph.NotMetaClosed -> 
+          (match exn with
+          | RefineFailure s -> raise (Uncertain s)
+          | HExtlib.Localized _ -> assert false
+          | _ -> raise exn)
+      | CoercGraph.NoCoercion 
+      | CoercGraph.SomeCoercionToTgt _
+      | CoercGraph.NotHandled _ -> 
+                      raise exn
+      | CoercGraph.SomeCoercion candidates -> 
+          let selected = 
+            HExtlib.list_findopt
+              (fun (metasenv,last,c) -> 
+               try
+                let subst,metasenv,ugraph =
+                 fo_unif_subst subst context metasenv last t
+                  ugraph in
+                let newt,newhety,subst,metasenv,ugraph = 
+                 type_of_aux subst metasenv context
+                  c ugraph 
+                in
+                let newt, newty, subst, metasenv, ugraph = 
+                 avoid_double_coercion context subst metasenv
+                  ugraph newt expty 
+                in
+                let subst,metasenv,ugraph1 = 
+                  fo_unif_subst subst context metasenv 
+                     newhety expty ugraph
+                in
+                 Some ((newt,newty), subst, metasenv, ugraph)
+               with Uncertain _ | RefineFailure _ -> None)
+              candidates
+          in
+          match selected with
+          | Some x -> x
+          | None -> raise exn
+
+  and coerce_to_sort 
+        in_source tgt_sort t type_to_coerce subst context metasenv uragph =
+      match CicReduction.whd ~subst:subst context type_to_coerce with
+      | Cic.Meta _ | Cic.Sort _ -> 
+          t,type_to_coerce, subst, metasenv, ugraph
+      | src ->
+         let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+         let exn = 
+           RefineFailure (lazy ("(7)The term " ^ 
+            CicMetaSubst.ppterm_in_context ~metasenv subst t context 
+            ^ " is not a type since it has type " ^ 
+            CicMetaSubst.ppterm_in_context ~metasenv subst src context
+            ^ " that is not a sort"))
+         in
+         try
+           let (t, ty_t), subst, metasenv, ugraph =
+             coerce_to_something t src tgt
+               subst metasenv context exn ugraph
+           in
+           t, ty_t, subst, metasenv, ugraph
+         with exn -> enrich localization_tbl t exn
   in
   
   (* eat prods ends here! *)
@@ -1792,7 +1731,6 @@ let pack_coercion metasenv ctx t =
       let l = List.map (merge_coercions ctx) l in
       let t = C.Appl l in
        let b,_,_,_,_ = is_a_double_coercion t in
-       (* prerr_endline "CANDIDATO!!!!"; *)
        if b then
          let ugraph = CicUniv.oblivion_ugraph in
          let old_insert_coercions = !insert_coercions in