New experimental commit: metavariables representation is changed again,

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 1ab5e92bc49a64fe89a4829326658b7cdcab98e5..089906b6d6628472b05c5342b31795a631e0b35b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -46,6 +46,7 @@ exception ReferenceToAxiom;;
 exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
 
 (* takes a well-typed term *)
 let whd context =
@@ -55,8 +56,9 @@ let whd context =
    function
       C.Rel n as t ->
        (match List.nth context (n-1) with
-           C.Decl _ -> if l = [] then t else C.Appl (t::l)
-         | C.Def bo -> whdaux l (S.lift n bo)
+           Some (C.Decl _) -> if l = [] then t else C.Appl (t::l)
+         | Some (C.Def bo) -> whdaux l (S.lift n bo)
+        | None -> raise RelToHiddenHypothesis
        )
     | C.Var uri as t ->
        (match CicEnvironment.get_cooked_obj uri 0 with
@@ -204,14 +206,15 @@ let are_convertible =
        match (t1,t2) with
           (C.Rel n1, C.Rel n2) -> n1 = n2
         | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
-        | (C.Meta n1, C.Meta n2) -> n1 = n2
+        | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
+           if n1 = n2 then (assert (l1=l2);true) else false
         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
         | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
+           aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2
         | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
+           aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2
         | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) ->
-           aux context s1 s2 && aux ((C.Def s1)::context) t1 t2
+           aux context s1 s2 && aux ((Some (C.Def s1))::context) t1 t2
         | (C.Appl l1, C.Appl l2) ->
            (try
              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
@@ -247,8 +250,7 @@ let are_convertible =
              aux context term1 term2 &&
              List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-(*CSC: C.Decl e' giusto? *)
-           let tys = List.map (function (_,_,ty,_) -> C.Decl ty) fl1 in
+           let tys = List.map (function (_,_,ty,_) -> Some (C.Decl ty)) fl1 in
             i1 = i2 &&
              List.fold_right2
               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
@@ -256,8 +258,7 @@ let are_convertible =
                  aux (tys@context) bo1 bo2)
               fl1 fl2 true
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-(*CSC: C.Decl e' giusto? *)
-           let tys = List.map (function (_,ty,_) -> C.Decl ty) fl1 in
+           let tys = List.map (function (_,ty,_) -> Some (C.Decl ty)) fl1 in
             i1 = i2 &&
              List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) b ->