Subst has been added to the kernel.

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e963ddce9b5062a941a45ff2b6e3cf44c89b8707..4b8099fed004c7e92ab152f190b5ca5599fde050 100644 (file)
--- 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