X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=3fc0dcf5a4003585b10f17e19240fc0932c04994;hb=2f4e2076f4b53f0c3e277bff67268cb80bfae967;hp=881c72bfd516852218105dc56ce71653219ce4d8;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 881c72bfd..3fc0dcf5a 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -23,16 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open Printf
+
 exception Impossible of int;;
 exception NotRefinable of string;;
 exception Uncertain of string;;
 exception WrongUriToConstant of string;;
 exception WrongUriToVariable of string;;
+exception ListTooShort;;
 exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
+exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
 let debug t context =
@@ -46,6 +48,15 @@ let debug t context =
    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
 ;;
 
+let debug_print = prerr_endline
+
+let rec split l n =
+ match (l,n) with
+    (l,0) -> ([], l)
+  | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
+  | (_,_) -> raise ListTooShort
+;;
+
 let rec type_of_constant uri =
  let module C = Cic in
  let module R = CicReduction in
@@ -85,6 +96,42 @@ and type_of_mutual_inductive_constr uri i j =
    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+
+(* the check_branch function checks if a branch of a case is refinable. 
+   It returns a pair (outype_instance,args), a subst and a metasenv.
+   outype_instance is the expected result of applying the case outtype 
+   to args. 
+   The problem is that outype is in general unknown, and we should
+   try to synthesize it from the above information, that is in general
+   a second order unification problem. *)
+ 
+and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
+  let module C = Cic in
+  let module R = CicMetaSubst in
+  let module Un = CicUnification in 
+  match R.whd subst context expectedtype with
+     C.MutInd (_,_,_) ->
+       (n,context,actualtype, [term]), subst, metasenv
+   | C.Appl (C.MutInd (_,_,_)::tl) ->
+       let (_,arguments) = split tl left_args_no in
+       (n,context,actualtype, arguments@[term]), subst, metasenv
+   | C.Prod (name,so,de) ->
+      (* we expect that the actual type of the branch has the due 
+         number of Prod *)
+      (match R.whd subst context actualtype with
+           C.Prod (name',so',de') ->
+             let subst, metasenv = 
+                Un.fo_unif_subst subst context metasenv so so' in
+             let term' =
+               (match CicSubstitution.lift 1 term with
+                   C.Appl l -> C.Appl (l@[C.Rel 1])
+                 | 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 
+	 | _ -> raise WrongArgumentNumber)
+  | _ -> raise (NotRefinable "Prod or MutInd expected")
+
 and type_of_aux' metasenv context t =
  let rec type_of_aux subst metasenv context =
   let module C = Cic in
@@ -98,7 +145,6 @@ and type_of_aux' metasenv context t =
             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
           | Some (_,C.Def (bo,None)) ->
-             prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
              type_of_aux subst metasenv context (S.lift n bo)
 	  | None -> raise RelToHiddenHypothesis
         with
@@ -114,16 +160,11 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        try
-         List.find (function (m,_,_) -> n = m) metasenv
-        with
-         Not_found -> raise (FreeMetaFound n)
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
          check_metasenv_consistency subst metasenv context canonical_context l
         in
-         CicSubstitution.lift_meta l ty, subst', metasenv'
+        CicSubstitution.lift_meta l ty, subst', metasenv'
     | C.Sort s ->
        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
         subst,metasenv
@@ -132,7 +173,7 @@ and type_of_aux' metasenv context t =
        let _,subst',metasenv' =
         type_of_aux subst metasenv context ty in
        let inferredty,subst'',metasenv'' =
-        type_of_aux subst' metasenv' context ty
+        type_of_aux subst' metasenv' context te
        in
         (try
           let subst''',metasenv''' =
@@ -209,9 +250,140 @@ and type_of_aux' metasenv context t =
         (type_of_mutual_inductive_constr uri i j)
       in
        cty,subst',metasenv'
-   | C.MutCase _
-   | C.Fix _
-   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+   | C.MutCase (uri, i, outtype, term, pl) ->
+       (* first, get the inductive type (and noparams) in the environment  *)
+       let (_,b,arity,constructors), expl_params, no_left_params =
+         match CicEnvironment.get_cooked_obj ~trust:true uri with
+            C.InductiveDefinition (l,expl_params,parsno) -> 
+              List.nth l i , expl_params, parsno
+          | _ ->
+            raise
+             (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+       let rec count_prod t =
+         match CicMetaSubst.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 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 context no_right_params in
+       let metasenv,exp_named_subst = 
+         CicMkImplicit.fresh_subst metasenv 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 actual_type,subst,metasenv = 
+         type_of_aux subst metasenv context term in
+       let _, subst, metasenv =
+         type_of_aux subst metasenv context expected_type
+       in
+       let actual_type = CicMetaSubst.whd subst context actual_type in
+       let subst,metasenv =
+         Un.fo_unif_subst subst context metasenv expected_type actual_type
+       in
+       (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+       let (_,outtypeinstances,subst,metasenv) =
+          List.fold_left
+           (fun (j,outtypeinstances,subst,metasenv) 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 actual_type,subst,metasenv = 
+               type_of_aux subst metasenv context p in
+             let expected_type, subst, metasenv = 
+               type_of_aux subst metasenv context constructor in
+             let outtypeinstance,subst,metasenv =
+               check_branch 
+                0 context metasenv subst 
+                no_left_params actual_type constructor expected_type in
+             (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
+            (1,[],subst,metasenv) 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 =
+          type_of_aux subst metasenv context
+            (C.Appl ((outtype :: right_args) @ [term]))
+        in
+        let (subst,metasenv) = 
+          List.fold_left
+            (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+              let instance' = 
+                let appl =
+                  let outtype' =
+                    CicSubstitution.lift constructor_args_no outtype
+                  in
+                  C.Appl (outtype'::args)
+                in
+(*
+                (* if appl is not well typed then the type_of below solves the
+                 * problem *)
+                let (_, subst, metasenv) =
+                  type_of_aux subst metasenv context appl
+                in
+*)
+                CicMetaSubst.whd subst context appl
+              in
+               Un.fo_unif_subst subst context metasenv instance instance')
+             (subst,metasenv) outtypeinstances in
+        CicMetaSubst.whd subst
+          context (C.Appl(outtype::right_args@[term])),subst,metasenv
+   | C.Fix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,_,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,x,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift subst len ty)
+         ) (subst,metasenv) fl in
+        let (_,_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
+   | C.CoFix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            Un.fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
 
  (* check_metasenv_consistency checks that the "canonical" context of a
  metavariable is consitent - up to relocation via the relocation list l -
@@ -229,14 +401,18 @@ and type_of_aux' metasenv context t =
        | (Some (n,C.Def (t,None)))::tl ->
           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
-       | (Some (_,C.Def (_,Some _)))::_ -> assert false
+       | (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)
      in
       aux 1 canonical_context
     in
      List.fold_left2 
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
-           _,None -> subst,metasenv
+           _,None ->
+             subst,metasenv
          | Some t,Some (_,C.Def (ct,_)) ->
             (try
               CicUnification.fo_unif_subst subst context metasenv t ct
@@ -246,9 +422,11 @@ and type_of_aux' metasenv context t =
              type_of_aux subst metasenv context t
             in
              (try
-               CicUnification.fo_unif_subst subst context metasenv inferredty ct
+               CicUnification.fo_unif_subst
+                subst' context metasenv' inferredty ct
              with _ -> raise MetasenvInconsistency)
-         | _, _  -> raise MetasenvInconsistency
+         | _, _  ->
+             raise MetasenvInconsistency
       ) (subst,metasenv) l lifted_canonical_context 
 
  and check_exp_named_subst metasubst metasenv context =
@@ -283,86 +461,93 @@ and type_of_aux' metasenv context t =
  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
   let module C = Cic in
    (* ti could be a metavariable in the domain of the substitution *)
-   let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
-   let t1' = CicUnification.apply_subst subst' t1 in
-   let t2' = CicUnification.apply_subst subst' t2 in
-    let t1'' = CicReduction.whd context t1' in
-    let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
+   let t1' = CicMetaSubst.apply_subst subst t1 in
+   let t2' = CicMetaSubst.apply_subst subst t2 in
+    let t1'' = CicMetaSubst.whd subst context t1' in
+    let t2'' =
+      CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2'
+    in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
-         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
-          C.Sort s2,subst',metasenv'
+         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
+          C.Sort s2,subst,metasenv
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst',metasenv'
-     | (C.Meta _,_)
-     | (_,C.Meta _) ->
-       raise
-        (Uncertain
-          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
-           CicPp.ppterm t2''))
+         C.Sort C.Type,subst,metasenv
+     | (C.Meta _,_) | (_,C.Meta _) ->
+         (* TODO how can we force the meta to become a sort? If we don't we
+          * brake the invariant that refine produce only well typed terms *)
+         (* TODO if we check the non meta term and if it is a sort then we are
+          * likely to know the exact value of the result e.g. if the rhs is a
+          * Sort (Prop | Set | CProp) then the result is the rhs *)
+         let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in
+         let irl =
+           CicMkImplicit.identity_relocation_list_for_metavariable context
+         in
+         C.Meta (idx, irl), subst, metasenv
      | (_,_) ->
-       raise
-        (NotRefinable
-         ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
+         raise (NotRefinable (sprintf
+          "Two types were expected, found %s of type %s and %s of type %s"
+          (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
+          (CicPp.ppterm t2'')))
+
+ and eat_prods subst metasenv context hetype tlbody_and_type =
+   (* TODO to be reviewed *)
+  List.fold_left
+    (fun (resty, subst, metasenv) (arg, argty) ->
+      let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in
+      let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in
+      let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context'
+      in
+      let newmeta = Cic.Meta (idx, irl) in
+      let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
+      let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
+      let (subst, metasenv) =
+        CicUnification.fo_unif_subst subst context metasenv resty prod
+      in
+      (CicMetaSubst.subst subst arg newmeta, subst, metasenv))
+    (hetype, subst, metasenv) tlbody_and_type
 
- and eat_prods subst metasenv context hetype =
-  function
-     [] -> hetype,subst,metasenv
-   | (hete, hety)::tl ->
-    (match (CicReduction.whd context hetype) with
-        Cic.Prod (n,s,t) ->
-         let subst',metasenv' =
-          try
-           CicUnification.fo_unif_subst subst context metasenv s hety
-          with _ ->
-           raise (NotRefinable "Appl: wrong parameter-type")
-         in
-          CicReduction.fdebug := -1 ;
-          eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
-      | Cic.Meta _ as t ->
-         raise
-          (Uncertain
-            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
-      | _ -> raise (NotRefinable "Appl: wrong Prod-type")
-    )
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
    (* we get rid of the metavariables that have been instantiated *)
-   let metasenv''' =
+   let metasenv'' =
     List.filter
-     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
-     metasenv''
+     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'))
+     metasenv'
    in
-    CicUnification.apply_subst subst'' t,
-     CicUnification.apply_subst subst'' ty,
-     subst'', metasenv'''
+    CicMetaSubst.apply_subst subst' t,
+     CicMetaSubst.apply_subst subst' ty,
+      subst', metasenv''
 ;;
 
 (* DEBUGGING ONLY *)
 let type_of_aux' metasenv context term =
  try
-  let (t,ty,s,m) =
-   type_of_aux' metasenv context term
-  in
-   List.iter
-    (function (i,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
-   List.iter
-    (function (i,_,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
-   prerr_endline
-    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
+  let (t,ty,s,m) = type_of_aux' metasenv context term in
+   debug_print
+    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
+(*
+   debug_print
+    ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s);
+   debug_print
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
+*)
    (t,ty,s,m)
  with
-  e ->
-   List.iter
-    (function (i,_,t) ->
-      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
-    metasenv ;
-   prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
+ | CicUnification.AssertFailure msg as e ->
+     debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
+     debug_print msg;
+     raise e
+ | CicUnification.UnificationFailure msg as e ->
+     debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
+     debug_print msg;
+     raise e
+ | e ->
+   debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
    raise e
 ;;
+