New handling of substitution:

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e8ea0769de76416d369ba4d5f5b9ff63ee0ed945..c1b70df8d4e6ece7d71de3b8950914efb6d3c5f4 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -132,11 +132,12 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | _ -> raise (AssertFailure "Prod or MutInd expected")
 
 and type_of_aux' metasenv context t =
- let rec type_of_aux subst metasenv context =
+ let rec type_of_aux subst metasenv context t =
   let module C = Cic in
   let module S = CicSubstitution in
   let module U = UriManager in
-   function
+  match t with
+(*    function *)
       C.Rel n ->
        (try
          match List.nth context (n - 1) with
@@ -156,11 +157,20 @@ and type_of_aux' metasenv context t =
       in
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
-        let subst',metasenv' =
-         check_metasenv_consistency n subst metasenv context canonical_context l
-        in
-        CicSubstitution.lift_meta l ty, subst', metasenv'
+        (try
+          let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in
+          let subst,metasenv =
+            check_metasenv_consistency n subst metasenv context
+              canonical_context l
+          in
+          type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
+        with CicMetaSubst.SubstNotFound _ ->
+          let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+          let subst,metasenv =
+            check_metasenv_consistency n subst metasenv context
+              canonical_context l
+          in
+          CicSubstitution.lift_meta l ty, subst, metasenv)
      (* TASSI: CONSTRAINT *)
     | C.Sort (C.Type t) -> 
         let t' = CicUniv.fresh() in 
@@ -214,7 +224,7 @@ and type_of_aux' metasenv context t =
        (* One-step LetIn reduction. Even faster than the previous solution.
           Moreover the inferred type is closer to the expected one. *)
        CicSubstitution.subst s inferredty,subst',metasenv'
-   | C.Appl (he::tl) when List.length tl > 0 ->
+   | C.Appl (he::((_::_) as tl)) ->
       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
       let tlbody_and_type,subst'',metasenv'' =
        List.fold_right
@@ -267,13 +277,13 @@ and type_of_aux' metasenv context t =
        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
+         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 context no_right_params in
+         else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
        let metasenv,exp_named_subst = 
-         CicMkImplicit.fresh_subst metasenv context expl_params in
+         CicMkImplicit.fresh_subst metasenv subst context expl_params in
        let expected_type = 
          if no_args = 0 then 
            C.MutInd (uri,i,exp_named_subst)
@@ -452,6 +462,7 @@ and type_of_aux' metasenv context t =
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: why was this code here? it is wrong
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
@@ -463,16 +474,19 @@ and type_of_aux' metasenv context t =
             (RefineFailure
              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
        ) ;
+*)
        let typeoft,metasubst',metasenv' =
         type_of_aux metasubst metasenv context t
        in
-        try
-         let metasubst'',metasenv'' =
+        let metasubst'',metasenv'' =
+         try
           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
-         in
-          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
-        with _ ->
-         raise (RefineFailure "Wrong Explicit Named Substitution")
+         with _ ->
+          raise (RefineFailure
+           ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
+            " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
+        in
+         check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
   in
    check_exp_named_subst_aux metasubst metasenv []
 
@@ -502,7 +516,7 @@ and type_of_aux' metasenv context t =
           * 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_sort metasenv in
+          CicMkImplicit.mk_implicit_sort metasenv subst in
          let (subst, metasenv) =
            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
          in
@@ -517,13 +531,13 @@ and type_of_aux' metasenv context t =
  let rec mk_prod metasenv context =
   function
      [] ->
-       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
        let irl =
         CicMkImplicit.identity_relocation_list_for_metavariable context
        in
         metasenv,Cic.Meta (idx, irl)
    | (_,argty)::tl ->
-      let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+      let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
       let irl =
        CicMkImplicit.identity_relocation_list_for_metavariable context
       in
@@ -535,8 +549,8 @@ and type_of_aux' metasenv context t =
         (* then I generate a name --- using the hint name_hint *)
         (* --- that is fresh in (context'@context).            *)
         let name_hint =
-         FreshNamesGenerator.mk_fresh_name
-          (CicMetaSubst.apply_subst_metasenv subst metasenv)
+         FreshNamesGenerator.mk_fresh_name metasenv
+(*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
           (CicMetaSubst.apply_subst_context subst context)
           Cic.Anonymous
           (CicMetaSubst.apply_subst subst argty)
@@ -626,8 +640,8 @@ and type_of_aux' metasenv context t =
   in
    let substituted_t = CicMetaSubst.apply_subst subst' t in
    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
-   let substituted_metasenv =
-    CicMetaSubst.apply_subst_metasenv subst' metasenv'
+   let substituted_metasenv = metasenv'
+(*     CicMetaSubst.apply_subst_metasenv subst' metasenv' *)
    in
     let cleaned_t =
      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in