]> matita.cs.unibo.it Git - helm.git/commitdiff
refactoring of all coercions code and add a check to not perform a coercion check...
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 16:25:17 +0000 (16:25 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 16:25:17 +0000 (16:25 +0000)
helm/software/components/cic_unification/cicRefine.ml

index ad5ae94dcb350c5772939dc5681343a8be8e6542..a73313ebae5f6047de9f40d464493a39336b18fc 100644 (file)
@@ -416,37 +416,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
-             (try
-               let subst''',metasenv''',ugraph3 =
-                 fo_unif_subst subst'' context metasenv'' 
-                   inferredty ty' ugraph2
-               in
-                C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
-              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
-                    C.Cast (te, ty'), ty', subst, metasenv, ugraph
-                  with exn -> enrich localization_tbl te' exn)
+            let (te', ty'), subst''',metasenv''',ugraph3 =
+              coerce_to_something true localization_tbl te' inferredty ty'
+                subst'' metasenv'' context ugraph2
+            in
+             C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
         | C.Prod (name,s,t) ->
             let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph 
             in
             let s',sort1,subst', metasenv',ugraph1 = 
-              coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+              coerce_to_sort localization_tbl 
               s' sort1 subst' context metasenv' ugraph1
             in
             let context_for_t = ((Some (name,(C.Decl s')))::context) in
@@ -455,7 +435,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 context_for_t t ugraph1
             in
             let t',sort2,subst'',metasenv'',ugraph2 = 
-              coerce_to_sort false (Cic.Type(CicUniv.fresh()))
+              coerce_to_sort localization_tbl 
               t' sort2 subst'' context_for_t metasenv'' ugraph2
             in
               let sop,subst''',metasenv''',ugraph3 =
@@ -468,7 +448,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               type_of_aux subst metasenv context s ugraph 
             in
             let s',sort1,subst',metasenv',ugraph1 =
-              coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+              coerce_to_sort localization_tbl 
               s' sort1 subst' context metasenv' ugraph1
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
@@ -1333,33 +1313,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         | (hete, hety)::tl ->
             match (CicReduction.whd ~subst context hetype) with 
             | Cic.Prod (n,s,t) ->
-                let arg,subst,metasenv,ugraph1 =
-                 try
-                  (try
-                    let subst,metasenv,ugraph1 = 
-                      fo_unif_subst_eat_prods2 
-                        subst context metasenv hety s ugraph
-                    in
-                      (hete,hety),subst,metasenv,ugraph1
-                  with RefineFailure _ | Uncertain _ as exn 
-                  when allow_coercions && !insert_coercions ->
-                     coerce_to_something 
-                       hete hety s subst metasenv context exn ugraph) 
-                 with exn ->
-                     enrich localization_tbl hete
-                      ~f:(fun _ ->
-                        (lazy ("(2)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: " ^ Printexc.to_string exn*)))) exn
-                in
-                  eat_prods_and_args pristinemenv metasenv subst context pristinehe he
-                    (CicSubstitution.subst (fst arg) t) 
-                    ugraph1 (newargs@[arg]) tl
+                let arg,subst,metasenv,ugraph =
+                  coerce_to_something allow_coercions localization_tbl 
+                    hete hety s subst metasenv context ugraph in
+                eat_prods_and_args 
+                  pristinemenv metasenv subst context pristinehe he
+                  (CicSubstitution.subst (fst arg) t) 
+                  ugraph (newargs@[arg]) tl
             | _ -> 
                 try
                   let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
@@ -1368,7 +1328,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                        (newargs@[hete,hety]@tl) ugraph
                   in
                   eat_prods_and_args metasenv
-                    metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+                    metasenv subst context pristinehe he hetype' 
+                    ugraph [] args_bo_and_ty
                 with RefineFailure _ | Uncertain _ as exn ->
                   (* unable to fix arity *)
                    more_args_than_expected localization_tbl metasenv
@@ -1395,106 +1356,126 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     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
+  and coerce_to_something 
+    allow_coercions localization_tbl t infty expty subst metasenv context ugraph
+  =
+    let coerce_atom_to_something t infty expty subst metasenv context 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.NotMetaClosed -> raise (Uncertain (lazy
+          "coerce_atom_to_something fails since not meta closed"))
       | CoercGraph.NoCoercion 
       | CoercGraph.SomeCoercionToTgt _
-      | CoercGraph.NotHandled _ -> 
-                      raise exn
+      | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+          "coerce_atom_to_something fails since no coercions found"))
       | CoercGraph.SomeCoercion candidates -> 
+          let uncertain = ref false in
           let selected = 
             HExtlib.list_findopt
               (fun (metasenv,last,c) -> 
                try
                 let subst,metasenv,ugraph =
-                 fo_unif_subst subst context metasenv last t
-                  ugraph in
+                 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
+                 type_of_aux subst metasenv context c ugraph in
                 let newt, newty, subst, metasenv, ugraph = 
-                 avoid_double_coercion context subst metasenv
-                  ugraph newt expty 
+                 avoid_double_coercion context subst metasenv ugraph newt expty 
                 in
                 let subst,metasenv,ugraph1 = 
-                  fo_unif_subst subst context metasenv 
-                     newhety expty ugraph
-                in
+                  fo_unif_subst subst context metasenv newhety expty ugraph in
                  Some ((newt,newty), subst, metasenv, ugraph)
-               with Uncertain _ | RefineFailure _ -> None)
+               with 
+               | Uncertain _ -> uncertain := true; None
+               | RefineFailure _ -> None)
               candidates
           in
           match selected with
           | Some x -> x
-          | None -> raise exn
+          | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
+          | None -> raise (RefineFailure (lazy "coerce_atom fails"))
+    in
+    let rec coerce_to_something_aux 
+      t infty expty subst metasenv context ugraph 
+    =
+      try            
+        let subst, metasenv, ugraph =
+          fo_unif_subst subst context metasenv infty expty ugraph
+        in
+        (t, expty), subst, metasenv, ugraph
+      with Uncertain _ | RefineFailure _ as exn ->
+        if not allow_coercions || not !insert_coercions then
+          enrich localization_tbl t 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_aux
+                  bo ty ty2 subst metasenv context_bo ugraph
+              in
+              (* contravariant part *)
+              let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
+              let (rel1, _), subst, metasenv, ugraph = 
+                coerce_to_something_aux
+                 (Cic.Rel 1) (CicSubstitution.lift 1 src2) 
+                 (CicSubstitution.lift 1 src) subst metasenv context_rel1 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 ugraph
+    in
+    try
+      coerce_to_something_aux t infty expty subst metasenv context ugraph
+    with Uncertain _ | RefineFailure _ ->
+      let exn = 
+        RefineFailure (lazy ("The term " ^
+          CicMetaSubst.ppterm_in_context metasenv subst t context ^ 
+          " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
+          infty context ^ " but is here used with type " ^ 
+          CicMetaSubst.ppterm_in_context metasenv subst expty context))
+      in
+        enrich localization_tbl t 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 " ^ 
+  and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
+    match CicReduction.whd ~subst:subst context infty with
+    | Cic.Meta _ | Cic.Sort _ -> 
+        t,infty, subst, metasenv, ugraph
+    | src ->
+       let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+       try
+         let (t, ty_t), subst, metasenv, ugraph =
+           coerce_to_something true
+             localization_tbl t src tgt subst metasenv context ugraph
+         in
+         t, ty_t, subst, metasenv, ugraph
+       with HExtlib.Localized (_, exn) -> 
+         let f _ = 
+           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"))
+            ^ " 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
+           enrich localization_tbl ~f t exn
   in
   
   (* eat prods ends here! *)