* Major code cleanup.

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

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index a6f6ee23b8e638452caf4a681ca1c6bf96585e96..e0ad91f59b2414c3c855fb07287edc0f0e341c88 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -31,27 +31,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None,
-    C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
-     C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
-      C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
-       C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
-        C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
-         C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
-          C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
-           C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
-            C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
-             t
-            )
-           )
-          )
-         )
-        )
-       )
-      )
-     )
-    )
-    )) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    begin
@@ -74,7 +54,15 @@ let whd =
   let module S = CicSubstitution in
    function
       C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
-    | C.Var _ as t -> if l = [] then t else C.Appl (t::l)
+    | C.Var uri as t ->
+       (match CicEnvironment.get_cooked_obj uri 0 with
+           C.Definition _ -> raise ReferenceToDefinition
+         | C.Axiom _ -> raise ReferenceToAxiom
+         | C.CurrentProof _ -> raise ReferenceToCurrentProof
+         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+         | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
+         | C.Variable (_,Some body,_) -> whdaux l body
+       )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
     | C.Implicit as t -> t
@@ -93,8 +81,7 @@ let whd =
        (match CicEnvironment.get_cooked_obj uri cookingsno with
            C.Definition (_,body,_,_) -> whdaux l body
          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
-         (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *)
-         | C.Variable _ -> if l = [] then t else C.Appl (t::l)
+         | C.Variable _ -> raise ReferenceToVariable
          | C.CurrentProof (_,_,body,_) -> whdaux l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
@@ -272,7 +259,9 @@ let are_convertible t1 t2 =
        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
        | (C.Implicit, _) | (_, C.Implicit) ->
           raise (Impossible 3) (* we don't trust our whd ;-) *)
-       | (_,_) -> false
+       | (_,_) ->
+          debug t1' [t2'] "NOT-CONVERTIBLE" ;
+          false
    end
  in
   aux t1 t2