1) Implemented inference of the outtype for empty inductive types

2) The inferred outtype (of non empty ind types) used to omit the lambda abstraction (worked using an amazing feature ot the type checker meant for backward compatibility with Coq 7... ask Claudio).

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index fbde6a82093c17f316e14cbc6cd32da06d7219c0..eda04d36e33dcd68e54c5eefffee5e8b0ce2f355 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -46,26 +46,6 @@ let rec split l n =
   | (_,_) -> raise (AssertFailure "split: list too short")
 ;;
 
-let look_for_coercion src tgt =
-  None
-  (*
-  if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
-     (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con")) 
-  then
-    begin
-    debug_print "TROVATA coercion";
-    Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
-    end
-  else 
-    begin
-    debug_print (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src) 
-      (CicPp.ppterm tgt));
-    None
-    end
-  *)
-;;
-
-
 let rec type_of_constant uri ugraph =
   let module C = Cic in
   let module R = CicReduction in
@@ -256,7 +236,7 @@ and type_of_aux' metasenv context t ugraph =
               (try
                 let subst''',metasenv''',ugraph3 =
                   fo_unif_subst subst'' context metasenv'' 
-                     inferredty ty' ugraph2
+                     inferredty ty ugraph2
                 in
                   C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
                with
@@ -443,20 +423,57 @@ and type_of_aux' metasenv context t ugraph =
              
            (match outtype with
            | C.Meta (n,l) ->
-               (let candidate,ugraph5 = 
+               (let candidate,ugraph5,metasenv = 
+                 let exp_name_subst, metasenv = 
+                    let o,_ = 
+                      CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                    in
+                    let uris = CicUtil.params_of_obj o in
+                    List.fold_right (
+                      fun uri (acc,metasenv) -> 
+                        let metasenv',new_meta = 
+                           CicMkImplicit.mk_implicit metasenv subst context
+                        in
+                        let irl =
+                          CicMkImplicit.identity_relocation_list_for_metavariable 
+                            context
+                        in
+                        (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
+                    ) uris ([],metasenv)
+                 in
+                 let ty = Cic.MutInd(uri, i, exp_name_subst) in
+                 let fresh_name = 
+                   FreshNamesGenerator.mk_fresh_name ~subst metasenv 
+                     context Cic.Anonymous ~typ:ty
+                 in
                  match outtypeinstances with
-                 | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
+                 | [] -> 
+                     let extended_context = 
+                       Some (fresh_name,Cic.Decl ty)::context 
+                     in
+                     let metasenv,new_meta = 
+                       CicMkImplicit.mk_implicit metasenv subst extended_context
+                     in
+                    let irl =
+                       CicMkImplicit.identity_relocation_list_for_metavariable 
+                         extended_context
+                     in
+                     let candidate = 
+                       Cic.Lambda(fresh_name, ty, Cic.Meta (new_meta,irl))
+                     in
+                     (Some candidate),ugraph4,metasenv
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
                        let instance' = 
                          CicSubstitution.delift constructor_args_no
                            (CicMetaSubst.apply_subst subst instance)
                        in
+                       let candidate,ugraph,metasenv =
                          List.fold_left (
-                           fun (candidate_oty,ugraph) 
+                           fun (candidate_oty,ugraph,metasenv) 
                              (constructor_args_no,_,instance,_) ->
                                match candidate_oty with
-                               | None -> None,ugraph 
+                               | None -> None,ugraph,metasenv
                                | Some ty ->
                                  try 
                                    let instance' = 
@@ -468,14 +485,20 @@ and type_of_aux' metasenv context t ugraph =
                                       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
+                                   if b then 
+                                     candidate_oty,ugraph1,metasenv 
+                                   else 
+                                     None,ugraph,metasenv
+                                 with Failure s -> None,ugraph,metasenv
+                         ) (Some instance',ugraph4,metasenv) tl
+                       in
+                       match candidate with
+                       | None -> None, ugraph,metasenv
+                       | Some t -> 
+                           Some (Cic.Lambda (fresh_name, ty, 
+                             CicSubstitution.lift 1 t)),ugraph,metasenv 
                      with Failure s -> 
-                       None,ugraph4
+                       None,ugraph4,metasenv
                in
                match candidate with
                | None -> raise (Uncertain "can't solve an higher order unification problem") 
@@ -484,7 +507,8 @@ and type_of_aux' metasenv context t ugraph =
                      fo_unif_subst subst context metasenv 
                        candidate outtype ugraph5
                    in
-                     C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
+                     C.MutCase (uri, i, outtype, term', pl'),
+                       (Cic.Appl [outtype; term']),s,m,u)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
@@ -809,9 +833,9 @@ and type_of_aux' metasenv context t ugraph =
                          hete,subst,metasenv,ugraph1
                     with exn ->
                        (* we search a coercion from hety to s *)
-                       let coer = look_for_coercion 
+                       let coer = None (* CoercGraph.look_for_coercion  
                          (CicMetaSubst.apply_subst subst hety) 
-                         (CicMetaSubst.apply_subst subst s) 
+                         (CicMetaSubst.apply_subst subst s) *)
                        in
                        match coer with
                        | None -> raise exn