Abst removed from the DTD.

Warning!!!! This breaks the most part of the code of HELM.

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index a556aadca6b184b213d0f2915bd2143964a10080..fd3e191a81a306461e8343bd764fb9639de81650 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -64,7 +64,6 @@ and term =
  | LetIn of name * term * term                      (* binder, term, target *)
  | Appl of term list                                (* arguments *)
  | Const of UriManager.uri * int                    (* uri, number of cookings*)
- | Abst of UriManager.uri                           (* uri *)
  | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)
@@ -116,7 +115,6 @@ and annterm =
  | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
  | AAppl of id * annterm list                       (* arguments *)
  | AConst of id * UriManager.uri * int              (* uri, number of cookings*)
- | AAbst of id * UriManager.uri                     (* uri *)
  | AMutInd of id * UriManager.uri * int * int       (* uri, cookingsno, typeno*)
  | AMutConstruct of id * UriManager.uri * int *     (* uri, cookingsno, *)
     int * int                                       (*  typeno, consno  *)

diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml
index 72882a186513e62dba5aa9f9dc263d7c9240cefa..8f87504acdc9239e5dd36d49947ad7738b3342a6 100644 (file)
--- a/helm/ocaml/cic/cicParser3.ml
+++ b/helm/ocaml/cic/cicParser3.ml
@@ -325,19 +325,6 @@ class eltype_sort =
   end
 ;;
 
-class eltype_abst =
-  object (self)
-
-    inherit cic_term
-
-    method to_cic_term =
-     let n = self#node in
-      let value = uri_of_xml_attr (n#attribute "uri")
-      and id = string_of_xml_attr (n#attribute "id") in
-       Cic.AAbst (id,value)
-  end
-;;
-
 class eltype_const =
   object (self)
 
@@ -495,7 +482,6 @@ let domspec =
       "LETIN",         (new D.element_impl (new eltype_letin)) ;
       "APPLY",         (new D.element_impl (new eltype_apply)) ;
       "CONST",         (new D.element_impl (new eltype_const)) ;
-      "ABST",          (new D.element_impl (new eltype_abst)) ;
       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;

diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml
index 27ea5b3b7335779eed38a17bb6dc8ee65d57c3e3..ec98b9774214bd6b684f42813711225812ad77ec 100644 (file)
--- a/helm/ocaml/cic/deannotate.ml
+++ b/helm/ocaml/cic/deannotate.ml
@@ -53,7 +53,6 @@ let rec deannotate_term =
       C.LetIn (name, deannotate_term so, deannotate_term ta)
    | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
    | C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno)
-   | C.AAbst (_,uri) -> C.Abst uri
    | C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
    | C.AMutConstruct (_,uri,cookingsno,i,j) ->
       C.MutConstruct (uri,cookingsno,i,j)

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 7ea0b7b6309937574d1cae19e93d9345928aed46..1961a2bc2c726ddd7c920729bd2998e6d7ea003d 100644 (file)
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -64,7 +64,6 @@ let print_term i2a =
            List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
         >]
      | C.AConst (id,_,_) -> print_ann i2a id
-     | C.AAbst (id,_) -> raise NotImplemented
      | C.AMutInd (id,_,_,_) -> print_ann i2a id
      | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
      | C.AMutCase (id,_,_,_,ty,te,patterns) ->

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index eef9880bcfb6eef4aa6acd674a5a3418735a3078..f2cb0ed409e4316155ab5036b0f868bbde9eea32 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -76,7 +76,6 @@ let get_ids_to_targets annobj =
          set_target id (C.Term t) ;
          List.iter add_target_term l
       | C.AConst (id,_,_)
-      | C.AAbst (id,_)
       | C.AMutInd (id,_,_,_)
       | C.AMutConstruct (id,_,_,_,_) ->
          set_target id (C.Term t)

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index c382bb361f7e554ad56b6ce243a11f27a365bb6e..2c5d0b439ffbaebea810e836fe772828d5c88dba 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -80,7 +80,6 @@ let cook curi cookingsno var is_letin =
           [C.Rel k])
        else
         C.Const (uri,UriManager.relative_depth curi uri cookingsno)
-    | C.Abst _ as t -> t
     | C.MutInd (uri,_,i) ->
        if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true

diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
index cb5875f73c3ef191f18eb5f654eaabebd066910d..bdc6e3a09d544b35167ef38631b94e61cb845e2d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
@@ -37,7 +37,6 @@ let rec letin_nf =
    | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
    | C.Appl l -> C.Appl (List.map letin_nf l)
    | C.Const _ as t -> t
-   | C.Abst _ as t -> t
    | C.MutInd _ as t -> t
    | C.MutConstruct _ as t -> t
    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 07e306b0be83e167708dd4a05266205e166bbeb1..d34bbb5df2f68a9c5f20c4f329bfe134960ded62 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -103,7 +103,6 @@ let rec pp t l =
         li ""
        ) ^ ")"
     | C.Const (uri,_) -> UriManager.name_of_uri uri
-    | C.Abst uri -> UriManager.name_of_uri uri
     | C.MutInd (uri,_,n) ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (dl,_,_) ->

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index d0e103521b88fedf16615c79c05cb2b79c8c858a..93335625a25c0951ef4ade711069f75ef3bc19fd 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -75,7 +75,6 @@ let unwind' m k e t =
     | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
     | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -172,7 +171,6 @@ let rec reduce : config -> Cic.term =
          | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | (k, e, (C.Abst _ as t), s) -> t (* s should be empty ????? *)
     | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in 
                                          if s = [] then t' else C.Appl (t'::s)
     | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) -> 
@@ -230,7 +228,7 @@ let rec reduce : config -> Cic.term =
                  eat_first (num_to_eat,tl)
               in
                reduce (k, e, (List.nth pl (j-1)),(ts@s)) 
-         | C.Abst _| C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ -> let t' = unwind k e t in
                 if s = [] then t' else C.Appl (t'::s)
@@ -294,7 +292,6 @@ let rec whd = let module C = Cic in
     | C.Appl [] -> raise (Impossible 1)
     | C.Appl (he::tl) -> reduce (0, [], he, tl)
     | C.Const _ as t -> reduce (0, [], t, [])
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase _ as t -> reduce (0, [], t, [])

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 86e58aa9faed497c82913b35d90f5f816292f8c5..f569e75cd451f196a83ef95e86db8a735e07e206 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -91,7 +91,6 @@ let whd context =
          | C.CurrentProof (_,_,body,_) -> whdaux l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,_,term,pl) as t->
@@ -146,7 +145,7 @@ let whd context =
                  eat_first (num_to_eat,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _| C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ -> if l = [] then t else C.Appl (t::l)
        )
@@ -276,7 +275,7 @@ let are_convertible =
               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
               fl1 fl2 true
-        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Cast _, _) | (_, C.Cast _)
         | (C.Implicit, _) | (_, C.Implicit) ->
            raise (Impossible 3) (* we don't trust our whd ;-) *)
         | (_,_) -> false

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index ae51f35803e20cfd6467b54983afbe6b0dd5747d..f312f556c9600fc3ea1179df2d1e54f72ee3867a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -53,7 +53,6 @@ let lift n =
     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
     | C.Appl l -> C.Appl (List.map (liftaux k) l)
     | C.Const _ as t -> t
-    | C.Abst _  as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -118,7 +117,6 @@ let subst arg =
         end
     | C.Appl _ -> assert false
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -208,7 +206,6 @@ let lift_meta l t =
     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2e8b5585f5190c6d2110ef8fab6a576b39f7b614..b539508a1212f10672a08f46691e486be41ba97e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -75,6 +75,7 @@ let rec cooked_type_of_constant uri cookingsno =
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()
          | C.CurrentProof (_,conjs,te,ty) ->
+             (*CSC: bisogna controllare anche il metasenv!!! *)
              let _ = type_of_aux' conjs [] ty in
               if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
               then
@@ -141,7 +142,6 @@ and does_not_occur context n nn te =
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ -> true
     | C.MutCase (_,_,_,out,te,pl) ->
@@ -444,8 +444,7 @@ and recursive_args context n nn te =
    | C.Lambda _
    | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
    | C.Appl _ -> []
-   | C.Const _
-   | C.Abst _ -> raise (Impossible 5)
+   | C.Const _ -> raise (Impossible 5)
    | C.MutInd _
    | C.MutConstruct _
    | C.MutCase _
@@ -537,7 +536,6 @@ and check_is_really_smaller_arg context n nn kl x safes te =
       check_is_really_smaller_arg context n nn kl x safes he
    | C.Appl [] -> raise (Impossible 11)
    | C.Const _
-   | C.Abst _
    | C.MutInd _ -> raise (Impossible 12)
    | C.MutConstruct _ -> false
    | C.MutCase (uri,_,i,outtype,term,pl) ->
@@ -697,7 +695,6 @@ and guarded_by_destructors context n nn kl x safes =
        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
        tl true
    | C.Const _
-   | C.Abst _
    | C.MutInd _
    | C.MutConstruct _ -> true
    | C.MutCase (uri,_,i,outtype,term,pl) ->
@@ -885,8 +882,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
             guarded_by_constructors context n nn true te tl coInductiveTypeURI
          | C.Appl _ ->
             does_not_occur context n nn te
-         | C.Const _
-         | C.Abst _ -> raise (Impossible 26)
+         | C.Const _ -> raise (Impossible 26)
          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
             guarded_by_constructors context n nn true te [] coInductiveTypeURI
          | C.MutInd _ ->
@@ -920,8 +916,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Appl _ -> 
             List.fold_left
              (fun i x -> i && does_not_occur context n nn x) true l
-         | C.Const _
-         | C.Abst _ -> raise (Impossible 31)
+         | C.Const _ -> raise (Impossible 31)
          | C.MutInd _ ->
             List.fold_left
              (fun i x -> i && does_not_occur context n nn x) true l
@@ -980,7 +975,6 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
    | C.Const _ -> true
-   | C.Abst _
    | C.MutInd _ -> assert false
    | C.MutConstruct _ -> true
    | C.MutCase (_,_,_,out,te,pl) ->
@@ -1110,10 +1104,14 @@ and type_of_branch context argsno need_dummy outtype term constype =
        else
         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
    | C.Prod (name,so,de) ->
-      C.Prod (C.Anonimous,so,type_of_branch
-       ((Some (name,(C.Decl so)))::context) argsno need_dummy
-       (CicSubstitution.lift 1 outtype)
-       (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
+      let term' =
+       match CicSubstitution.lift 1 term with
+          C.Appl l -> C.Appl (l@[C.Rel 1])
+        | t -> C.Appl [t ; C.Rel 1]
+      in
+       C.Prod (C.Anonimous,so,type_of_branch
+        ((Some (name,(C.Decl so)))::context) argsno need_dummy
+        (CicSubstitution.lift 1 outtype) term' de)
   | _ -> raise (Impossible 20)
 
 (* check_metasenv_consistency checks that the "canonical" context of a
@@ -1209,7 +1207,6 @@ and type_of_aux' metasenv context t =
       let cty = cooked_type_of_constant uri cookingsno in
        decr fdebug ;
        cty
-   | C.Abst _ -> raise (Impossible 22)
    | C.MutInd (uri,cookingsno,i) ->
       incr fdebug ;
       let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
@@ -1493,7 +1490,7 @@ let typecheck uri =
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
         | C.CurrentProof (_,conjs,te,ty) ->
-           (*CSC [] wrong *)
+            (*CSC: bisogna controllare anche il metasenv!!! *)
             let _ = type_of_aux' conjs [] ty in
              debug (type_of_aux' conjs [] te) [] ;
              if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 4a2cb243066b0a1b3efb0be2a7f88a54aaee65b4..cd1e7aa0c18709714f0e5295f0a2f84dfa57bc40 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -104,7 +104,6 @@ let delift context metasenv l t =
      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
      | C.Const _ as t -> t
-     | C.Abst _  as t -> t
      | C.MutInd _ as t -> t
      | C.MutConstruct _ as t -> t
      | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -229,8 +228,6 @@ prerr_endline "<DELIFT2" ; flush stderr ;
            fo_unif_l subst metasenv (lr1, lr2) 
        | (C.Const _, _) 
        | (_, C.Const _)
-       | (C.Abst _, _) 
-       | (_, C.Abst _) 
        | (C.MutInd  _, _) 
        | (_, C.MutInd _)
        | (C.MutConstruct _, _)
@@ -335,7 +332,6 @@ CSCSCS
        List.fold_left
          (function metasenv -> aux metasenv k) metasenv l
     | C.Const _
-    | C.Abst _
     | C.MutInd _ 
     | C.MutConstruct _ -> metasenv
     | C.MutCase (_,_,_,outty,t,pl) ->
@@ -447,7 +443,6 @@ prerr_endline "<DELIFT" ; flush stderr ;
         end
     | C.Appl _ -> assert false
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ as t -> t,metasenv
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
@@ -542,7 +537,6 @@ let apply_subst_reducing subst meta_to_reduce t =
          end
     | C.Appl _ -> assert false
     | C.Const _ as t -> t
-    | C.Abst _  as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->