X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=f5684a9510196194727e7a9e48bc9aaf2954146d;hb=b6658a4a5c874be0223f44c7c1b99900185cbc60;hp=e963ddce9b5062a941a45ff2b6e3cf44c89b8707;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e963ddce9..f5684a951 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -498,7 +498,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
    unwind' 0 
   ;;
   
-  let reduce context : config -> Cic.term = 
+  let reduce ?(subst = []) context : config -> Cic.term = 
    let module C = Cic in
    let module S = CicSubstitution in 
    let rec reduce =
@@ -542,9 +542,13 @@ if List.mem uri params then prerr_endline "---- OK2" ;
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
-     | (k, e, ens, (C.Meta _ as t), s) ->
-        let t' = unwind k e ens t in
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (k, e, ens, (C.Meta (n,l) as t), s) ->
+        (try 
+	   let (_, term,_) = CicUtil.lookup_subst n subst in
+           reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
+	 with  CicUtil.Subst_not_found _ ->
+           let t' = unwind k e ens t in
+           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
@@ -722,10 +726,10 @@ if List.mem uri params then prerr_endline "---- OK2" ;
      | (uri,t)::tl ->
          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
    in
-    reduce
+    reduce 
   ;;
   
-  let rec whd context t = reduce context (0, [], [], t, []);;
+  let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);;
   
 (* DEBUGGING ONLY
 let whd context t =
@@ -769,7 +773,7 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 let whd = R.whd;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible =
+let are_convertible ?(subst=[]) ?(metasenv=[]) =
  let module U = UriManager in
  let rec aux test_equality_only context t1 t2 =
   let aux2 test_equality_only t1 t2 =
@@ -792,8 +796,10 @@ let are_convertible =
               with
                Invalid_argument _ -> false
              )
-        | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
+        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
             n1 = n2 &&
+             let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+             let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
              List.fold_left2
               (fun b t1 t2 ->
                 b &&
@@ -900,10 +906,18 @@ let are_convertible =
   in
    if aux2 test_equality_only t1 t2 then true
    else
-    begin
+     begin
      debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 in
-     let t2' = whd context t2 in
+     (* 
+     (match t1 with 
+	 Cic.Meta _ -> 
+	   prerr_endline (CicPp.ppterm t1);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
+	   prerr_endline (CicPp.ppterm t2);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
+       | _ -> ()); *)
+     let t1' = whd ~subst context t1 in
+     let t2' = whd ~subst context t2 in
       debug t1' [t2'] "POSTWHD";
       aux2 test_equality_only t1' t2'
     end