added a pretty printing of the new object and use argv[1] as uri

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 7b98a59be775fe79e02ec35f3e7e497c694554b0..dd25edac4fd0531e665ebfd26e444082cf4f1e0b 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te =
          Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
-    | C.Meta (_,l) ->
+    | C.Meta (mno,l) ->
        List.fold_right
         (fun x i ->
           match x with
              None -> i
            | Some x -> i && does_not_occur ~subst context n nn x) l true &&
        (try
-         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+         let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in
           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
         with
          CicUtil.Subst_not_found _ -> true)
@@ -934,10 +934,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
   function
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
-      (match List.nth context (n-1) with
+      (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
+           guarded_by_destructors ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -1374,11 +1374,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   let arity1 = CicReduction.whd ~subst context arity1 in
   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
    match arity1, CicReduction.whd ~subst context arity2 with
-     (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
+     (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
        if b then
-        check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+        check_allowed_sort_elimination ~subst ~metasenv ~logger 
+           ((Some (name,C.Decl so1))::context) uri i
           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
           ugraph1
        else
@@ -2202,6 +2203,9 @@ let typecheck_obj0 ~logger uri ugraph =
       let _,ugraph = type_of ~logger ty ugraph in
        ugraph
    | C.CurrentProof (_,conjs,te,ty,_,_) ->
+      (* this block is broken since the metasenv should 
+       * be topologically sorted before typing metas *)
+      ignore(assert false);
       let _,ugraph =
        List.fold_left
         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->