X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d822ec34112215e198d8f9c239dac2caa0a30c79;hb=044618edc33fa1cf00ec345e84c2a62939746751;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..d822ec341 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -28,11 +28,13 @@ 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,13 @@ let debug t context =
    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
 ;;
 
+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 +94,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 context metasenv subst left_args_no actualtype term expectedtype =
+  let module C = Cic in
+  let module R = CicReduction in
+  let module Un = CicUnification in 
+  match R.whd context expectedtype with
+     C.MutInd (_,_,_) ->
+       (actualtype, [term]), subst, metasenv
+   | C.Appl (C.MutInd (_,_,_)::tl) ->
+       let (_,arguments) = split tl left_args_no in
+       (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 context actualtype with
+           C.Prod (name',so',de') ->
+             let subst,metsaenv = 
+                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 ((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
@@ -209,7 +254,78 @@ and type_of_aux' metasenv context t =
         (type_of_mutual_inductive_constr uri i j)
       in
        cty,subst',metasenv'
-   | C.MutCase _
+   | 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 CicReduction.whd 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 =
+         Un.fo_unif_subst 
+           subst 
+           context 
+           metasenv expected_type (CicReduction.whd context 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 
+                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) = 
+          List.fold_left
+            (fun (subst,metasenv) (instance,args) ->
+               let instance' = 
+                 CicReduction.whd context (C.Appl(outtype::args)) in
+               Un.fo_unif_subst subst context metasenv instance instance')
+             (subst,metasenv) outtypeinstances in
+        CicReduction.whd 
+          context (C.Appl(outtype::right_args@[term])),subst,metasenv
    | C.Fix _
    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
 
@@ -290,7 +406,7 @@ and type_of_aux' metasenv context t =
     let t2'' = CicReduction.whd ((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!!! *)
+         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
           C.Sort s2,subst',metasenv'
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
@@ -366,3 +482,13 @@ let type_of_aux' metasenv context term =
    prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
    raise e
 ;;
+
+
+
+
+
+
+
+
+
+