debian version 0.0.6-6

[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 4ef3ce9401fba300d6c1c366b663808682eec209..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 &&
@@ -802,10 +808,17 @@ let are_convertible =
                   | _,None  -> true
                   | Some t1',Some t2' -> aux test_equality_only context t1' t2'
               ) true l1 l2
-        | (C.Sort s1, C.Sort s2) when
-             s1 = s2 || (not test_equality_only) && s2 = C.Type
-           -> true
-        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+         (* TASSI: CONSTRAINTS *)
+       | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+           CicUniv.add_eq t2 t1
+         (* TASSI: CONSTRAINTS *)
+       | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+           CicUniv.add_ge t2 t1
+         (* TASSI: CONSTRAINTS *)
+       | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
+         (* TASSI: CONSTRAINTS *)
+        | (C.Sort s1, C.Sort s2) -> s1 = s2
+       | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
            aux true context s1 s2 &&
             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
@@ -893,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