- removed metasenv argument from kernel proxies invocations

- lift_meta over defs with an explicit type implemented
- reimplemented eat_prods (open bug: when an application has more than
  one argument and its type is a meta then the outtype is a Meta whose
  context is not general enough. To be implemented)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 979c9637ede5591125cf64dfa4786d08299a2648..3fc0dcf5a4003585b10f17e19240fc0932c04994 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -109,7 +109,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
   let module C = Cic in
   let module R = CicMetaSubst in
   let module Un = CicUnification in 
-  match R.whd metasenv subst context expectedtype with
+  match R.whd subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -118,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd metasenv subst context actualtype with
+      (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
@@ -164,7 +164,7 @@ and type_of_aux' metasenv context t =
         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
@@ -260,7 +260,7 @@ and type_of_aux' metasenv context t =
             raise
              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd metasenv subst context t with
+         match CicMetaSubst.whd subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -285,7 +285,7 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd metasenv subst context actual_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
@@ -335,11 +335,11 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd metasenv subst context appl
+                CicMetaSubst.whd subst context appl
               in
                Un.fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd metasenv subst
+        CicMetaSubst.whd subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
    | C.Fix (i,fl) ->
       let subst,metasenv,types =
@@ -358,9 +358,8 @@ and type_of_aux' metasenv context t =
             type_of_aux subst metasenv context' bo
            in
             Un.fo_unif_subst subst context' metasenv
-              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+              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) ->
@@ -380,7 +379,7 @@ and type_of_aux' metasenv context t =
             type_of_aux subst metasenv context' bo
            in
             Un.fo_unif_subst subst context' metasenv
-              ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+              ty_of_bo (CicMetaSubst.lift subst len ty)
          ) (subst,metasenv) fl in
       
         let (_,ty,_) = List.nth fl i in
@@ -402,7 +401,10 @@ 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
@@ -459,79 +461,81 @@ 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' = CicMetaSubst.unwind_subst metasenv subst in
-   let t1' = CicMetaSubst.apply_subst subst' t1 in
-   let t2' = CicMetaSubst.apply_subst subst' t2 in
-    let t1'' = CicMetaSubst.whd metasenv subst' context t1' 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 metasenv subst' ((Some (name,C.Decl s))::context) 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 or s2 = C.CProp) -> (* 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.Sort C.Type,subst,metasenv
      | (C.Meta _,_) | (_,C.Meta _) ->
-         let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
+         (* 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'
+         C.Meta (idx, irl), subst, metasenv
      | (_,_) ->
          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 =
-  function
-     [] -> hetype,subst,metasenv
-   | (hete, hety)::tl ->
-    (match (CicMetaSubst.whd metasenv subst context hetype) with
-        Cic.Prod (n,s,t) ->
-         let subst',metasenv' =
-           CicUnification.fo_unif_subst subst context metasenv s hety
-         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")
-    )
+ 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
+
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   let subst'',metasenv'' = CicMetaSubst.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
-    CicMetaSubst.apply_subst subst'' t,
-     CicMetaSubst.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
+   debug_print
+    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 (*
-   List.iter
-    (function (i,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
-   List.iter
-    (function (i,_,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
-*)
    debug_print
-    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
+    ("@@@ REFINE SUCCESSFUL (subst):\n" ^ CicMetaSubst.ppsubst s);
+   debug_print
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
+*)
    (t,ty,s,m)
  with
  | CicUnification.AssertFailure msg as e ->
@@ -543,12 +547,6 @@ let type_of_aux' metasenv context term =
      debug_print msg;
      raise e
  | e ->
-(*
-   List.iter
-    (function (i,_,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
-    metasenv ;
-*)
    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
    raise e
 ;;