]> matita.cs.unibo.it Git - helm.git/commitdiff
when a coercion is passed through a case on right-params-free term m,
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 15:46:51 +0000 (15:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 15:46:51 +0000 (15:46 +0000)
branches and outtype are adjusted to receive an extra argument (refl m)
to have extra assumptions on it substituded. see tests/coercions_russell.ma

helm/software/components/cic_unification/cicRefine.ml

index 026fc9cb1b3a72432043e279af82d7747b77645c..e3e92d098f0f4ed34935543f7a666ec5bb246475 100644 (file)
@@ -34,8 +34,10 @@ exception AssertFailure of string Lazy.t;;
 let insert_coercions = ref true
 let pack_coercions = ref true
 
-let debug_print = fun _ -> ();;
-(*let debug_print x = prerr_endline (Lazy.force x);;*)
+let debug = false;;
+
+let debug_print = 
+  if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
 
 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
 
@@ -1425,8 +1427,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
           let infty = clean infty subst context in
           let expty = clean expty subst context in
+          let t = clean t subst context in
           match infty, expty, t with
           | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
+              debug_print (lazy "FIX");
              (match fl with
                  [name,i,_(* infty *),bo] ->
                    let context_bo =
@@ -1444,7 +1448,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
                | _ -> assert false (* not implemented yet *))
           | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
-              (* move this stuff away *)
+              debug_print (lazy "CASE");
+              (* {{{ helper functions *)
               let get_cl_and_left_p uri tyno outty ugraph =
                 match CicEnvironment.get_obj ugraph uri with
                 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
@@ -1514,26 +1519,36 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
                 | _ -> assert false
               in
+              let eq_uri, eq, eq_refl = 
+                match LibraryObjects.eq_URI () with 
+                | None -> HLog.warn "no default equality"; raise exn
+                | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
+              in
               let add_params 
-                metasenv subst context uri tyno cty outty leftno i 
+                metasenv subst context uri tyno cty outty mty m leftno i 
               =
-                let mytl = function [] -> [] | _::tl -> tl in
-                let rec aux context outty par k = function
+                let rec aux context outty par k mty m = function
                   | Cic.Prod (name, src, tgt) ->
-                      Cic.Prod (name, src, 
+                      let t,k = 
                         aux 
                           (Some (name, Cic.Decl src) :: context)
-                        (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+                          (CS.lift 1 outty) (Cic.Rel k::par) (k+1) 
+                          (CS.lift 1 mty) (CS.lift 1 m) tgt
+                      in
+                      Cic.Prod (name, src, t), k
                   | Cic.MutInd _ ->
-                      let par = mytl par in
                       let k = 
                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
                         if par <> [] then Cic.Appl (k::par) else k
                       in
-                      CR.head_beta_reduce ~delta:false 
-                        (Cic.Appl [outty;k])
+                      Cic.Prod (Cic.Name "p", 
+                       Cic.Appl [eq; mty; m; k],
+                       (CS.lift 1
+                        (CR.head_beta_reduce ~delta:false 
+                         (Cic.Appl [outty;k])))),k
                   | Cic.Appl (Cic.MutInd _::pl) ->
-                      let left_p,_ = HExtlib.split_nth leftno pl in
+                      let left_p,right_p = HExtlib.split_nth leftno pl in
+                      let has_rights = right_p <> [] in
                       let k = 
                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
                         Cic.Appl (k::left_p@par)
@@ -1548,57 +1563,116 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                         | _ -> assert false
                         with CicTypeChecker.TypeCheckerFailure _ -> assert false
                       in
-                      CR.head_beta_reduce ~delta:false 
-                        (Cic.Appl (outty ::right_p @ [k]))
+                      if has_rights then
+                        CR.head_beta_reduce ~delta:false 
+                          (Cic.Appl (outty ::right_p @ [k])),k
+                      else
+                        Cic.Prod (Cic.Name "p", 
+                         Cic.Appl [eq; mty; m; k],
+                         (CS.lift 1
+                          (CR.head_beta_reduce ~delta:false 
+                           (Cic.Appl (outty ::right_p @ [k]))))),k
                   | _ -> assert false
                 in
-                  aux context outty [] 1 cty
+                  aux context outty [] 1 mty m cty
+              in
+              let add_lambda_for_refl_m pbo rno mty m k cty =
+                (* k lives in the right context *)
+                if rno <> 0 then pbo else
+                let rec aux mty m = function 
+                  | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
+                     Cic.Lambda (name,src,
+                      (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
+                  | t,_ -> 
+                      Cic.Lambda (Cic.Name "p",
+                        Cic.Appl [eq; mty; m; k],CS.lift 1 t)
+                in
+                aux mty m (pbo,cty)
               in
+              let add_pi_for_refl_m new_outty mty m rno =
+                if rno <> 0 then new_outty else
+                  let rec aux m mty = function
+                    | Cic.Lambda (name, src, tgt) ->
+                        Cic.Lambda (name, src, 
+                          aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
+                    | t ->
+                        Cic.Prod 
+                          (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
+                          CS.lift 1 t)
+                  in
+                    aux m mty new_outty
+              in (* }}} end helper functions *)
               (* constructors types with left params already instantiated *)
               let outty = CicMetaSubst.apply_subst subst outty in
               let cl, left_p, leftno,rno,ugraph = 
                 get_cl_and_left_p uri tyno outty ugraph 
               in
-              let right_p = 
+              let right_p, mty = 
                 try
                   match 
                     CicTypeChecker.type_of_aux' ~subst metasenv context m
                       CicUniv.oblivion_ugraph 
                   with
-                  | Cic.MutInd _,_ -> []
-                  | Cic.Appl (Cic.MutInd _::args),_ ->
-                      snd (HExtlib.split_nth leftno args)
+                  | Cic.MutInd _ as mty,_ -> [], mty
+                  | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+                      snd (HExtlib.split_nth leftno args), mty
                   | _ -> assert false
-                with CicTypeChecker.TypeCheckerFailure _ ->
-                  let rec foo = 
-                    function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
-                  in 
-                   foo rno
+                with CicTypeChecker.TypeCheckerFailure _ -> assert false
               in
               let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
               in
+              debug_print 
+                (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
+                 ~metasenv subst new_outty context));
               let _,pl,subst,metasenv,ugraph = 
                 List.fold_right2
-                  (fun cty pbo (i, acc, s, m, ugraph) -> 
-                     (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
-                     let infty_pbo = 
-                       add_params m s context uri tyno cty outty leftno i in
-                     let expty_pbo = 
-                       add_params m s context uri tyno cty new_outty leftno i in
+                  (fun cty pbo (i, acc, s, menv, ugraph) -> 
+                    (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
+                     *   (new_)outty right_par (K_i left_par k_par) *)
+                     let infty_pbo, _ = 
+                       add_params menv s context uri tyno 
+                         cty outty mty m leftno i in
+                     debug_print 
+                       (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
+                       ~metasenv subst infty_pbo context));
+                     let expty_pbo, k = (* k is (K_i left_par k_par) *)
+                       add_params menv s context uri tyno 
+                         cty new_outty mty m leftno i in
+                     debug_print 
+                       (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
+                       ~metasenv subst expty_pbo context));
+                     let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
+                     debug_print 
+                       (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
+                       ~metasenv subst pbo context));
                      let (pbo, _), subst, metasenv, ugraph =
                        coerce_to_something_aux pbo infty_pbo expty_pbo 
-                         s m context ugraph
+                         s menv context ugraph
                      in
+                     debug_print 
+                       (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
+                       ~metasenv subst pbo context));
                      (i-1, pbo::acc, subst, metasenv, ugraph))
                   cl pl (List.length pl, [], subst, metasenv, ugraph)
               in
-              let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
+              let new_outty = add_pi_for_refl_m new_outty mty m rno in
+              debug_print 
+                (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
+                 ~metasenv subst new_outty context));
+              let t = 
+                if rno = 0 then
+                  let refl_m=Cic.Appl[eq_refl;mty;m]in
+                  Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] 
+                else 
+                  Cic.MutCase(uri,tyno,new_outty,m,pl)
+              in
               (t, expty), subst, metasenv, ugraph
           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
+              debug_print (lazy "LAM");
               let name_con = 
                 FreshNamesGenerator.mk_fresh_name 
-                  ~subst metasenv context Cic.Anonymous ~typ:src2
+                  ~subst metasenv context ~typ:src2 Cic.Anonymous
               in
               let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
               (* contravariant part: the argument of f:src->ty *)
@@ -1624,6 +1698,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                 ~metasenv subst coerced context));
               (coerced, expty), subst, metasenv, ugraph
           | _ -> 
+              debug_print (lazy "ATOM");
             coerce_atom_to_something t infty expty subst metasenv context ugraph
     in
     try