X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=4a6e6cadf798ef6fd16c154da24d513a4520a968;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=24171327c80adce776de9ada770c26ffd62e43fc;hpb=b26c4349ed1401d2ac9904deb47efbd4c454d98e;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 24171327c..4a6e6cadf 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,12 +47,14 @@ let rec split l n =
 ;;
 
 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
     prerr_endline "TROVATA coercion";
-    Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con")
+    Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
     end
   else 
     begin
@@ -60,6 +62,7 @@ let look_for_coercion src tgt =
       (CicPp.ppterm tgt));
     None
     end
+  *)
 ;;
 
 
@@ -76,8 +79,8 @@ let rec type_of_constant uri ugraph =
     *)
   let obj,u= CicEnvironment.get_obj ugraph uri in
     match obj with
-	C.Constant (_,_,ty,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_) -> ty,u
+	C.Constant (_,_,ty,_,_) -> ty,u
+      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
       | _ ->
 	  raise
 	    (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
@@ -95,7 +98,7 @@ and type_of_variable uri ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-	C.Variable (_,_,ty,_) -> ty,u
+	C.Variable (_,_,ty,_,_) -> ty,u
       |  _ ->
 	   raise
 	    (RefineFailure
@@ -114,7 +117,7 @@ and type_of_mutual_inductive_defs uri i ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-	C.InductiveDefinition (dl,_,_) ->
+	C.InductiveDefinition (dl,_,_,_) ->
 	  let (_,_,arity,_) = List.nth dl i in
 	    arity,u
       | _ ->
@@ -135,7 +138,7 @@ and type_of_mutual_inductive_constr uri i j ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-	C.InductiveDefinition (dl,_,_) ->
+	C.InductiveDefinition (dl,_,_,_) ->
 	  let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,u
@@ -178,7 +181,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")
 
@@ -222,17 +227,17 @@ and type_of_aux' metasenv context t ugraph =
 		   canonical_context l ugraph 
                in
 		 (* trust or check ??? *)
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv', ugraph1
 		   (* type_of_aux subst metasenv 
-		      context (CicSubstitution.lift_meta l term) *)
+		      context (CicSubstitution.subst_meta l term) *)
              with CicUtil.Subst_not_found _ ->
                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
                let l',subst',metasenv', ugraph1 =
 		 check_metasenv_consistency n subst metasenv context
 		   canonical_context l ugraph
                in
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv',ugraph1)
 	| C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
@@ -357,131 +362,155 @@ 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) -> 
+		  C.InductiveDefinition (l,expl_params,parsno,_) -> 
 		    List.nth l i , expl_params, parsno, u
 		| _ ->
 		    raise
 		      (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 ->
+                   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
@@ -579,14 +608,14 @@ and type_of_aux' metasenv context t ugraph =
 	function
             [] -> []
 	  | (Some (n,C.Decl t))::tl ->
-              (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+              (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,None)))::tl ->
-              (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+              (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 	  | None::tl -> None::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,Some ty)))::tl ->
               (Some (n,
-		     C.Def ((S.lift_meta l (S.lift i t)),
-			    Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+		     C.Def ((S.subst_meta l (S.lift i t)),
+			    Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
       in
 	aux 1 canonical_context 
     in
@@ -851,6 +880,13 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
+let type_of_aux' metasenv context term ugraph =
+  try 
+    type_of_aux' metasenv context term ugraph
+  with 
+    CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+    
+
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try