]> matita.cs.unibo.it Git - helm.git/commitdiff
coercions under Fix and Case. Code refactoring needed
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 6 Sep 2007 13:11:17 +0000 (13:11 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 6 Sep 2007 13:11:17 +0000 (13:11 +0000)
helm/software/components/cic_unification/cicRefine.ml

index 4c825c8a7313ac8385d85d8610520a0a1e84ba6a..7f378ed4b9919fb8b7003ddce9b756143f712e03 100644 (file)
@@ -1360,6 +1360,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
   =
     let module CS = CicSubstitution in
+    let module CR = CicReduction in
     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
       let coer = 
         CoercGraph.look_for_coercion metasenv subst context infty expty
@@ -1384,7 +1385,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                 let newt, newty, subst, metasenv, ugraph = 
                  avoid_double_coercion context subst metasenv ugraph newt expty 
                 in
-                let subst,metasenv,ugraph1 = 
+                let subst,metasenv,ugraph = 
                   fo_unif_subst subst context metasenv newhety expty ugraph in
                  Some ((newt,newty), subst, metasenv, ugraph)
                with 
@@ -1420,18 +1421,160 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                    let context_bo =
                     Some (Cic.Name name,Cic.Decl expty)::context in
                    let (rel1, _), subst, metasenv, ugraph =
-                    coerce_to_something_aux (Cic.Rel 1) expty infty subst
+                    coerce_to_something_aux (Cic.Rel 1) 
+                      (CS.lift 1 expty) (CS.lift 1 infty) subst
                      metasenv context_bo ugraph in
                    let bo =
                     CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
                    in
                    let (bo,_), subst, metasenv, ugraph =
-                    coerce_to_something_aux bo infty expty subst
+                    coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
+                    expty) subst
                      metasenv context_bo ugraph
                    in
                     (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
-               | _ -> assert false (* not implemented yet *)
-             )
+               | _ -> assert false (* not implemented yet *))
+          | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
+              (* move this stuff away *)
+              let get_cl_and_left_p uri tyno outty ugraph =
+                match CicEnvironment.get_obj ugraph uri with
+                | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
+                    let count_pis t =
+                      let rec aux ctx t = 
+                        match CicReduction.whd ~delta:false ctx t with
+                        | Cic.Prod (name,src,tgt) ->
+                            let ctx = Some (name, Cic.Decl src) :: ctx in
+                            1 + aux ctx tgt
+                        | _ -> 0
+                      in
+                        aux [] t
+                    in
+                    let rec skip_lambda_delifting t n =
+                      match t,n with
+                      | _,0 -> t
+                      | Cic.Lambda (_,_,t),n -> 
+                          skip_lambda_delifting
+                            (CS.subst (Cic.Implicit None) t) (n - 1)
+                      | _ -> assert false
+                    in
+                    let get_l_r_p n = function
+                            | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+                      | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
+                          HExtlib.split_nth n args
+                      | _ -> assert false
+                    in
+                    let _, _, ty, cl = List.nth tl tyno in
+                    let pis = count_pis ty in
+                    let rno = pis - leftno in
+                    let t = skip_lambda_delifting outty rno in
+                    let left_p, _ = get_l_r_p leftno t in
+                    let instantiale_with_left cl =
+                      List.map 
+                        (fun ty -> 
+                          List.fold_left 
+                            (fun t p -> CS.subst ~avoid_beta_redexes:true p t)
+                            ty left_p) 
+                        cl 
+                    in
+                    let cl = instantiale_with_left (List.map snd cl) in
+                    cl, left_p, leftno, rno, ugraph
+                | _ -> raise exn
+              in
+              let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+                match t,n with
+                | _,0 ->
+                  let rec mkr n = function 
+                    | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
+                  in
+                  let bo =
+                  CicReplace.replace_lifting
+                    ~equality:(fun _ -> CicUtil.alpha_equivalence)
+                    ~context:ctx
+                    ~what:(matched::right_p)
+                    ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
+                    ~where:bo
+                  in
+                  bo
+                | Cic.Lambda (name, src, tgt),_ ->
+                    Cic.Lambda (name, src,
+                      keep_lambdas_and_put_expty 
+                       (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
+                       (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
+                | _ -> assert false
+              in
+              let add_params uri tyno cty outty leftno i =
+                let mytl = function [] -> [] | _::tl -> tl in
+                let rec aux outty par k = function
+                  | Cic.Prod (name, src, tgt) ->
+                      Cic.Prod (name, src, 
+                        aux (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+                  | 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.Appl (Cic.MutInd _::pl) ->
+                      let par = mytl par in
+                      let left_p,right_p = HExtlib.split_nth leftno pl in
+                      let k = 
+                        let k = Cic.MutConstruct (uri,tyno,i,[]) in
+                        Cic.Appl (k::left_p@par)
+                      in
+                      CR.head_beta_reduce ~delta:false 
+                        (Cic.Appl (outty ::right_p @ [k]))
+                  | _ -> assert false
+                in
+                  aux outty [] 1 cty
+              in
+              let rec add_params2 expty = function
+                | Cic.Prod (name, src, tgt) ->
+                    Cic.Prod (name, src, add_params2 (CS.lift 1 expty) tgt)
+                | Cic.MutInd _ | Cic.Appl (Cic.MutInd _::_) -> expty
+                | _ -> assert false
+              in
+              (* 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 = 
+                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)
+                  | _ -> assert false
+                with CicTypeChecker.TypeCheckerFailure _ ->
+                  let rec foo = 
+                    function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
+                  in 
+                   foo rno
+              in
+              let new_outty =
+                keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+              in
+              let _,pl,subst,metasenv,ugraph = 
+                List.fold_right2
+                  (fun cty pbo (i, acc, subst, metasenv, ugraph) -> 
+                     (* Pi k_par, outty right_par (K_i left_par k_par)*)
+                     let infty_pbo = add_params uri tyno cty outty leftno i in
+                     (* Pi k_par, expty *)
+                     let expty_pbo = add_params2 expty cty in
+                     let (pbo, _), subst, metasenv, ugraph =
+                       coerce_to_something_aux pbo infty_pbo expty_pbo 
+                         subst metasenv context ugraph
+                     in
+                     (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
+              (t, expty), subst, metasenv, ugraph
           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
               let name_con = Cic.Name "name_con" in
               let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
@@ -1444,11 +1587,11 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               (* covariant part: the result of f(c x); x:src2; (c x):src *)
               let name_t, bo = 
                 match t with
-                | Cic.Lambda (n,_,bo) -> n, CS.subst rel1 (CS.lift_from 2 1 bo)
+                | Cic.Lambda (n,_,bo) -> n, CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
                 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
               in
               (* we fix the possible dependency problem in the source ty *)
-              let ty = CS.subst rel1 (CS.lift_from 2 1 ty) in
+              let ty = CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 ty) in
               let (bo, _), subst, metasenv, ugraph = 
                 coerce_to_something_aux
                   bo ty ty2 subst metasenv context_src2 ugraph