bumped changelog line to match upload date

[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..f53471414b660a53e7e4c04310c1c0b0383ef54d 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 =
@@ -765,17 +769,21 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
 
 let whd = R.whd;;
 
+  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+    * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
 (* t1, t2 must be well-typed *)
-let are_convertible =
- let module U = UriManager in
+let are_convertible ?(subst=[]) ?(metasenv=[]) =
  let rec aux test_equality_only context t1 t2 =
   let aux2 test_equality_only t1 t2 =
    (* this trivial euristic cuts down the total time of about five times ;-) *)
    (* this because most of the time t1 and t2 are "sintactically" the same   *)
-   if t1 = t2 then
+   if t1 === t2 then
     true
    else
     begin
@@ -792,8 +800,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 &&
@@ -898,12 +908,22 @@ let are_convertible =
         | (_,_) -> false
     end
   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