X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=5c031f4733b6806f2da7c1b9ef683d8d589112ec;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=8828a417e5272c4cbb2731dcd3cde150e0342212;hpb=25f486e24d9d34e85476414771b4d01d2c468299;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8828a417e..5c031f473 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -287,7 +287,7 @@ and type_of_aux' metasenv context t ugraph =
 	       * Moreover the inferred type is closer to the expected one. 
                *)
 	      C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
-                subst',metasenv',ugraph2
+                subst'',metasenv'',ugraph2
 	| C.Appl (he::((_::_) as tl)) ->
 	    let he',hetype,subst',metasenv',ugraph1 = 
 	      type_of_aux subst metasenv context he ugraph 
@@ -434,7 +434,7 @@ and type_of_aux' metasenv context t ugraph =
              
            (match outtype with
            | C.Meta (n,l) ->
-               (let candidate,ugraph5,metasenv = 
+               (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
                       CicEnvironment.get_obj CicUniv.empty_ugraph uri 
@@ -503,39 +503,39 @@ and type_of_aux' metasenv context t ugraph =
                       add_lambdas (Cic.Meta (new_meta,irl))
                        arity_instantiated_with_left_args
                      in
-                     (Some candidate),ugraph4,metasenv
+                     (Some candidate),ugraph4,metasenv,subst
                  | (constructor_args_no,_,instance,_)::tl -> 
                      try
-                       let instance' = 
-                         CicSubstitution.delift constructor_args_no
-                           (CicMetaSubst.apply_subst subst instance)
+                       let instance',subst,metasenv = 
+                         CicMetaSubst.delift_rels subst metasenv
+                          constructor_args_no instance
                        in
-                       let candidate,ugraph,metasenv =
+                       let candidate,ugraph,metasenv,subst =
                          List.fold_left (
-                           fun (candidate_oty,ugraph,metasenv) 
+                           fun (candidate_oty,ugraph,metasenv,subst) 
                              (constructor_args_no,_,instance,_) ->
                                match candidate_oty with
-                               | None -> None,ugraph,metasenv
+                               | None -> None,ugraph,metasenv,subst
                                | Some ty ->
                                  try 
-                                   let instance' = 
-                                     CicSubstitution.delift
-                                      constructor_args_no
-                                       (CicMetaSubst.apply_subst subst instance)
+                                   let instance',subst,metasenv = 
+                                     CicMetaSubst.delift_rels subst metasenv
+                                      constructor_args_no instance
                                    in
-                                   let b,ugraph1 =
-                                      CicReduction.are_convertible context 
-                                        instance' ty ugraph
+                                   let subst,metasenv,ugraph =
+                                    fo_unif_subst subst context metasenv 
+                                      instance' ty ugraph
                                    in
-                                   if b then 
-                                     candidate_oty,ugraph1,metasenv 
-                                   else 
-                                     None,ugraph,metasenv
-                                 with Failure s -> None,ugraph,metasenv
-                         ) (Some instance',ugraph4,metasenv) tl
+                                    candidate_oty,ugraph,metasenv,subst
+                                 with
+                                    CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
+                                  | CicUnification.UnificationFailure _
+                                  | CicUnification.Uncertain _ ->
+                                     None,ugraph,metasenv,subst
+                         ) (Some instance',ugraph4,metasenv,subst) tl
                        in
                        match candidate with
-                       | None -> None, ugraph,metasenv
+                       | None -> None, ugraph,metasenv,subst
                        | Some t -> 
                           let rec add_lambdas n b =
                            function
@@ -547,19 +547,22 @@ and type_of_aux' metasenv context t ugraph =
                           in
                            Some
                             (add_lambdas 0 t arity_instantiated_with_left_args),
-                           ugraph,metasenv 
-                     with Failure s -> 
-                       None,ugraph4,metasenv
+                           ugraph,metasenv,subst
+                     with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+                       None,ugraph4,metasenv,subst
                in
                match candidate with
                | None -> raise (Uncertain "can't solve an higher order unification problem") 
                | Some candidate ->
-                   let s,m,u = 
+                   let subst,metasenv,ugraph = 
                      fo_unif_subst subst context metasenv 
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl (outtype::right_args@[term'])),s,m,u)
+                      CicReduction.head_beta_reduce
+                       (CicMetaSubst.apply_subst subst
+                        (Cic.Appl (outtype::right_args@[term']))),
+                     subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
@@ -583,8 +586,9 @@ and type_of_aux' metasenv context t ugraph =
                  (subst,metasenv,ugraph5) outtypeinstances 
              in
                C.MutCase (uri, i, outtype, term', pl'),
-                 CicReduction.whd ~subst	context 
-                   (C.Appl(outtype::right_args@[term])),
+                 CicReduction.head_beta_reduce
+                  (CicMetaSubst.apply_subst subst
+                   (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
 	| C.Fix (i,fl) ->
 	    let fl_ty',subst,metasenv,types,ugraph1 =
@@ -960,7 +964,99 @@ let type_of_aux' metasenv context term ugraph =
     type_of_aux' metasenv context term ugraph
   with 
     CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+
+(*CSC: this is a very very rough approximation; to be finished *)
+let are_all_occurrences_positive uri =
+ let rec aux =
+  (*CSC: here we should do a whd; but can we do that? *)
+  function
+     Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
+   | Cic.MutInd (uri',_,_) when uri = uri' -> ()
+   | Cic.Prod (_,_,t) -> aux t
+   | _ -> raise (RefineFailure "not well formed constructor type")
+ in
+  aux
     
+let typecheck metasenv uri obj =
+ let ugraph = CicUniv.empty_ugraph in
+ match obj with
+    Cic.Constant (name,Some bo,ty,args,attrs) ->
+     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+     let bo' = CicMetaSubst.apply_subst subst bo' in
+     let ty' = CicMetaSubst.apply_subst subst ty' in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+      Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
+  | Cic.Constant (name,None,ty,args,attrs) ->
+     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+      Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+  | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
+     assert (metasenv' = metasenv);
+     (* Here we do not check the metasenv for correctness *)
+     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+     let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     begin
+      match sort with
+         Cic.Sort _
+       (* instead of raising Uncertain, let's hope that the meta will become
+          a sort *)
+       | Cic.Meta _ -> ()
+       | _ -> raise (RefineFailure "The term provided is not a type")
+     end;
+     let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+     let bo' = CicMetaSubst.apply_subst subst bo' in
+     let ty' = CicMetaSubst.apply_subst subst ty' in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+      Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
+  | Cic.Variable _ -> assert false (* not implemented *)
+  | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
+     (*CSC: this code is greately simplified and many many checks are missing *)
+     (*CSC: e.g. the constructors are not required to build their own types,  *)
+     (*CSC: the arities are not required to have as type a sort, etc.         *)
+     let uri = match uri with Some uri -> uri | None -> assert false in
+     let typesno = List.length tys in
+     (* first phase: we fix only the types *)
+     let metasenv,ugraph,tys =
+      List.fold_right
+       (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+         let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+          metasenv,ugraph,(name,b,ty',cl)::res
+       ) tys (metasenv,ugraph,[]) in
+     let con_context =
+      List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
+     (* second phase: we fix only the constructors *)
+     let metasenv,ugraph,tys =
+      List.fold_right
+       (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+         let metasenv,ugraph,cl' =
+          List.fold_right
+           (fun (name,ty) (metasenv,ugraph,res) ->
+             let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+             let ty',_,metasenv,ugraph =
+              type_of_aux' metasenv con_context ty ugraph in
+             let undebrujin t =
+              snd
+               (List.fold_right
+                 (fun (name,_,_,_) (i,t) ->
+                   (* here the explicit_named_substituion is assumed to be *)
+                   (* of length 0 *)
+                   let t' = Cic.MutInd (uri,i,[])  in
+                   let t = CicSubstitution.subst t' t in
+                    i - 1,t
+                 ) tys (typesno - 1,t)) in
+             let ty' = undebrujin ty' in
+              metasenv,ugraph,(name,ty')::res
+           ) cl (metasenv,ugraph,[])
+         in
+          metasenv,ugraph,(name,b,ty,cl')::res
+       ) tys (metasenv,ugraph,[]) in
+     (* third phase: we check the positivity condition *)
+     List.iter
+      (fun (_,_,_,cl) ->
+        List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
+      ) tys ;
+     Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
 
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =