type_of_aux' exported.

[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 285e660a8fce5dcdc26ab14c8bdc587b525f4ecf..ac1b50d31afd8340b82c188b64ad54a8ce62fecd 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
@@ -86,14 +74,14 @@ let whd =
          | he::tl -> whdaux tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
+    | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,cookingsno) as t ->
        (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
        )
@@ -214,7 +202,6 @@ let are_convertible t1 t2 =
      let t1' = whd t1 
      and t2' = whd t2 in
      debug t1' [t2'] "POSTWHD";
-     (*if !fdebug = 0 then ignore(Unix.system "read" );*)
       match (t1',t2') with
          (C.Rel n1, C.Rel n2) -> n1 = n2
        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2