1) Implemented inference of the outtype for empty inductive types

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

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