]> matita.cs.unibo.it Git - helm.git/commitdiff
Added outtype inference to MutCase
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)
helm/ocaml/cic_unification/cicRefine.ml

index d8b822d82cf6f6b39287025869e22bef114a7482..38e822c33cd468f5169fad859ea7b43caeed29aa 100644 (file)
@@ -178,7 +178,9 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
                       | t -> C.Appl [t ; C.Rel 1]) in
                   (* we should also check that the name variable is anonymous in
                      the actual type de' ?? *)
-                  check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1
+                  check_branch (n+1) 
+                     ((Some (name,(C.Decl so)))::context) 
+                       metasenv subst left_args_no de' term' de ugraph1
              | _ -> raise (AssertFailure "Wrong number of arguments"))
       | _ -> raise (AssertFailure "Prod or MutInd expected")
 
@@ -357,13 +359,6 @@ and type_of_aux' metasenv context t ugraph =
            (* first, get the inductive type (and noparams) 
              * in the environment  *)
            let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
-             (*
-               let obj =
-               try
-               CicEnvironment.get_cooked_obj ~trust:true uri
-               with Not_found -> assert false
-               in
-             *)
              let obj,u = CicEnvironment.get_obj ugraph uri in
               match obj with
                  C.InductiveDefinition (l,expl_params,parsno,_) -> 
@@ -373,115 +368,147 @@ and type_of_aux' metasenv context t ugraph =
                      (RefineFailure
                         ("Unkown mutual inductive definition " ^ 
                          U.string_of_uri uri)) 
-            in
-           let rec count_prod t =
-              match CicReduction.whd ~subst context t with
-                 C.Prod (_, _, t) -> 1 + (count_prod t)
-               | _ -> 0 
-            in 
-           let no_args = count_prod arity in
-             (* now, create a "generic" MutInd *)
-           let metasenv,left_args = 
-              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
-            in
-           let metasenv,right_args = 
-              let no_right_params = no_args - no_left_params in
-               if no_right_params < 0 then assert false
-               else CicMkImplicit.n_fresh_metas 
-                       metasenv subst context no_right_params 
-            in
-           let metasenv,exp_named_subst = 
-              CicMkImplicit.fresh_subst metasenv subst context expl_params in
-           let expected_type = 
-              if no_args = 0 then 
-               C.MutInd (uri,i,exp_named_subst)
-              else
-               C.Appl 
-                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
-           in
-             (* check consistency with the actual type of term *)
-           let term',actual_type,subst,metasenv,ugraph1 = 
-              type_of_aux subst metasenv context term ugraph in
-           let expected_type',_, subst, metasenv,ugraph2 =
-              type_of_aux subst metasenv context expected_type ugraph1
-           in
-           let actual_type = CicReduction.whd ~subst context actual_type in
-           let subst,metasenv,ugraph3 =
-              fo_unif_subst subst context metasenv 
-                expected_type' actual_type ugraph2
-           in
-             (* TODO: check if the sort elimination 
-               * is allowed: [(I q1 ... qr)|B] *)
-           let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
-              List.fold_left
-               (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
-                  let constructor =
-                    if left_args = [] then
-                      (C.MutConstruct (uri,i,j,exp_named_subst))
-                    else
-                      (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
-                  in
-                  let p',actual_type,subst,metasenv,ugraph1 = 
-                    type_of_aux subst metasenv context p ugraph 
-                   in
-                  let constructor',expected_type, subst, metasenv,ugraph2 = 
-                    type_of_aux subst metasenv context constructor ugraph1 
-                   in
-                  let outtypeinstance,subst,metasenv,ugraph3 =
-                    check_branch 0 context metasenv subst no_left_params 
-                       actual_type constructor expected_type ugraph2 
-                   in
-                    (pl @ [p'],j+1,
-                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
-               ([],1,[],subst,metasenv,ugraph3) pl 
-            in
-              (* we are left to check that the outype matches his instances.
-                The easy case is when the outype is specified, that amount
-                to a trivial check. Otherwise, we should guess a type from
-                its instances *)
-
-            (* easy case *)
-            let _,_, subst, metasenv,ugraph5 =
-              type_of_aux subst metasenv context
-               (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
-            in
-            let (subst,metasenv,ugraph6) = 
-              List.fold_left
-               (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) ->
-                  let instance' = 
-                     let appl =
-                       let outtype' =
-                        CicSubstitution.lift constructor_args_no outtype
+           in
+          let rec count_prod t =
+             match CicReduction.whd ~subst context t with
+                C.Prod (_, _, t) -> 1 + (count_prod t)
+              | _ -> 0 
+           in 
+          let no_args = count_prod arity in
+            (* now, create a "generic" MutInd *)
+          let metasenv,left_args = 
+             CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
+           in
+          let metasenv,right_args = 
+             let no_right_params = no_args - no_left_params in
+              if no_right_params < 0 then assert false
+              else CicMkImplicit.n_fresh_metas 
+                      metasenv subst context no_right_params 
+           in
+          let metasenv,exp_named_subst = 
+             CicMkImplicit.fresh_subst metasenv subst context expl_params in
+          let expected_type = 
+             if no_args = 0 then 
+              C.MutInd (uri,i,exp_named_subst)
+             else
+              C.Appl 
+                 (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
+          in
+            (* check consistency with the actual type of term *)
+          let term',actual_type,subst,metasenv,ugraph1 = 
+             type_of_aux subst metasenv context term ugraph in
+          let expected_type',_, subst, metasenv,ugraph2 =
+             type_of_aux subst metasenv context expected_type ugraph1
+          in
+          let actual_type = CicReduction.whd ~subst context actual_type in
+          let subst,metasenv,ugraph3 =
+             fo_unif_subst subst context metasenv 
+               expected_type' actual_type ugraph2
+          in
+            (* TODO: check if the sort elimination 
+              * is allowed: [(I q1 ... qr)|B] *)
+          let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
+             List.fold_left
+              (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+                 let constructor =
+                   if left_args = [] then
+                     (C.MutConstruct (uri,i,j,exp_named_subst))
+                   else
+                     (C.Appl 
+                        (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
+                 in
+                 let p',actual_type,subst,metasenv,ugraph1 = 
+                   type_of_aux subst metasenv context p ugraph 
+                  in
+                 let constructor',expected_type, subst, metasenv,ugraph2 = 
+                   type_of_aux subst metasenv context constructor ugraph1 
+                  in
+                 let outtypeinstance,subst,metasenv,ugraph3 =
+                   check_branch 0 context metasenv subst no_left_params 
+                      actual_type constructor' expected_type ugraph2 
+                  in
+                   (pl @ [p'],j+1,
+                     outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
+              ([],1,[],subst,metasenv,ugraph3) pl 
+           in
+           
+             (* we are left to check that the outype matches his instances.
+               The easy case is when the outype is specified, that amount
+               to a trivial check. Otherwise, we should guess a type from
+               its instances 
+             *)
+             
+           (match outtype with
+           | C.Meta (n,l) ->
+               (let candidate,ugraph5 = 
+                 match outtypeinstances with
+                 | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
+                 | (constructor_args_no,_,instance,_)::tl -> 
+                     try
+                       let instance' = 
+                         CicSubstitution.delift constructor_args_no
+                           (CicMetaSubst.apply_subst subst instance)
                        in
-                        C.Appl (outtype'::args)
-                     in
-                      (*
-                       (* if appl is not well typed then the type_of below solves the
-                        * problem *)
-                        let (_, subst, metasenv,ugraph1) =
-                        type_of_aux subst metasenv context appl ugraph
-                        in
-                      *)
-                       (* DEBUG 
-                         let prova1 = CicMetaSubst.whd subst context appl in
-                         let prova2 = CicReduction.whd ~subst context appl in
-                         if not (prova1 = prova2) then
-                         begin 
-                         prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
-                         prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
-                         end;
-                       *)
-                       (* CicMetaSubst.whd subst context appl *)
-                       CicReduction.whd ~subst context appl
-                  in
-                    fo_unif_subst subst context metasenv 
-                       instance instance' ugraph)
-               (subst,metasenv,ugraph5) outtypeinstances 
-            in
-              C.MutCase (uri, i, outtype, term', pl'),
-                CicReduction.whd ~subst        context 
-                  (C.Appl(outtype::right_args@[term])),
-                subst,metasenv,ugraph6
+                         List.fold_left (
+                           fun (candidate_oty,ugraph) 
+                             (constructor_args_no,_,instance,_) ->
+                               match candidate_oty with
+                               | None -> None,ugraph 
+                               | Some ty ->
+                                 try 
+                                   let instance' = 
+                                     CicSubstitution.delift
+                                      constructor_args_no
+                                       (CicMetaSubst.apply_subst subst instance)
+                                   in
+                                   let b,ugraph1 =
+                                      CicReduction.are_convertible context 
+                                        instance' ty ugraph
+                                   in
+                                     if b then 
+                                       candidate_oty,ugraph1 
+                                     else 
+                                       None,ugraph
+                                 with Failure s -> None,ugraph 
+                         ) (Some instance',ugraph4) tl
+                     with Failure s -> 
+                       None,ugraph4
+               in
+               match candidate with
+               | None -> raise (Uncertain "can't solve an higher order unification problem") 
+               | Some candidate ->
+                   prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
+                   let s,m,u = 
+                     fo_unif_subst subst context metasenv 
+                       candidate outtype ugraph5
+                   in
+                     C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
+           | _ ->    (* easy case *)
+             let _,_, subst, metasenv,ugraph5 =
+               type_of_aux subst metasenv context
+                 (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
+             in
+             let (subst,metasenv,ugraph6) = 
+               List.fold_left
+                 (fun (subst,metasenv,ugraph) 
+                        (constructor_args_no,context,instance,args) ->
+                    let instance' = 
+                      let appl =
+                        let outtype' =
+                          CicSubstitution.lift constructor_args_no outtype
+                        in
+                          C.Appl (outtype'::args)
+                      in
+                        CicReduction.whd ~subst context appl
+                    in
+                    fo_unif_subst subst context metasenv 
+                        instance instance' ugraph)
+                 (subst,metasenv,ugraph5) outtypeinstances 
+             in
+               C.MutCase (uri, i, outtype, term', pl'),
+                 CicReduction.whd ~subst       context 
+                   (C.Appl(outtype::right_args@[term])),
+                 subst,metasenv,ugraph6)
        | C.Fix (i,fl) ->
            let fl_ty',subst,metasenv,types,ugraph1 =
              List.fold_left