- pretty printer made robust in face of list_nth

- bugfixed in generation of aliases in nCicLibrary:
  contructor index are 1-based
- refinement of indtypes fixed:
  - missing undebujinate added
  - index for current indty was in the wrong order
- apply_subst moved to nCicUntrusted
- new iterator for obj_kind

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 97af8a06f7e0ab0d54b8652e11231fc259d0689d..4ab7412d832c60f4e0c0c0aab339e5ef9f2a652e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -758,7 +758,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
              else
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-               uri,height,[],[],NTacStatus.apply_subst_obj subst obj
+               uri,height,[],[],
+                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj
               in
                NCicLibrary.add_obj uri obj;
                {status with 
@@ -784,7 +785,8 @@ prerr_endline "CSC: here we should fix the height!!!";
           (* CSC: cut&paste code from NQed *)
           let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
+           uri,height,[],[],
+            NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst nsubst) nobj
           in
            NCicLibrary.add_obj uri obj;
            {status with 

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 86822aa74b28f56878e4fdeffd4cb6e563178654..e2d800157dd4d57c4f44852dd6735b6dfc6ebd0e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -56,7 +56,7 @@ let add_obj u obj =
            HExtlib.list_mapi
             (fun (_,cname,_) j->
               u,cname,
-               NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+               NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
             ) cl @
            [u,iname,
              NReference.reference_of_spec u

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 6a38873fc360d9b238f3ff13bbed0174fc521bd7..47cdfa3ca8ff5bb29a6438ef9f8a7ce4ddf7147e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -43,7 +43,11 @@ let r2s pp_fix_name r =
             else 
               NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
         | _ -> assert false)
-  with NCicLibrary.ObjectNotFound _ -> R.string_of_reference r
+  with 
+  | NCicLibrary.ObjectNotFound _ 
+  | Failure "nth" 
+  | Invalid_argument "List.nth" -> R.string_of_reference r
+
 ;;
 
 let string_of_implicit_annotation = function

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f459c602432ae5888539bca809925da3ae49f775..65f17ee38ef4c356e4e5a5d1f6c3a3d16d36778c 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -350,7 +350,9 @@ let type_of_branch ~subst context leftno outty cons tycons =
         | t -> C.Appl [t ; C.Rel 1]
        in
         C.Prod (name,so, aux (liftno+1) ((name,(C.Decl so))::context) cons de)
-   | _ -> raise (AssertFailure (lazy "type_of_branch"))
+   | t -> raise (AssertFailure 
+      (lazy ("type_of_branch, the contructor has type: " ^ NCicPp.ppterm
+       ~metasenv:[] ~context:[] ~subst:[] t)))
  in
   aux 0 context cons tycons
 ;;

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 4dcf01c53b1a43f2793cf29ca374e456cbdba62c..95f40da5368ff06fe99991f33dc372c3d67f6d57 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -95,3 +95,52 @@ let mk_appl he args =
   | NCic.Appl l -> NCic.Appl (l@args)
   | _ -> NCic.Appl (he::args)
 ;;
+
+let map_obj_kind f =
+ function
+    NCic.Constant (relev,name,bo,ty,attrs) ->
+     NCic.Constant (relev,name,HExtlib.map_option f bo, f ty,attrs)
+  | NCic.Fixpoint (ind,fl,attrs) ->
+     let fl =
+      List.map
+       (function (relevance,name,recno,ty,bo) -> relevance,name,recno,f ty,f bo)
+       fl
+     in
+      NCic.Fixpoint (ind,fl,attrs)
+  | NCic.Inductive (is_ind,lno,itl,attrs) ->
+      let itl = 
+        List.map
+         (fun (relevance,name,ty,cl) ->
+           let cl = 
+             List.map (fun (relevance, name, ty) ->
+                relevance, name, f ty)
+             cl
+           in
+           relevance, name, f ty, cl)
+         itl
+      in
+      NCic.Inductive (is_ind,lno,itl,attrs)
+;;
+
+let apply_subst subst t = 
+ let rec apply_subst subst () =
+ function
+    NCic.Meta (i,lc) ->
+     (try
+       let _,_,t,_ = NCicUtils.lookup_subst i subst in
+       let t = NCicSubstitution.subst_meta lc t in
+        apply_subst subst () t
+      with
+       Not_found ->
+        match lc with
+           _,NCic.Irl _ -> NCic.Meta (i,lc)
+         | n,NCic.Ctx l ->
+            NCic.Meta
+             (i,(0,NCic.Ctx
+                 (List.map (fun t ->
+                   apply_subst subst () (NCicSubstitution.lift n t)) l))))
+  | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
+ in
+  apply_subst subst () t
+;;
+

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index 79ac48c3874fe3433d13863298205730d0618f84..31be9c0d2dbdefe81e9e361de8c42c4ce78d1a3f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -15,8 +15,12 @@ val map_term_fold_a:
  (NCic.hypothesis -> 'k -> 'k) -> 'k ->
  ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term
 
+val map_obj_kind: (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind
+
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
 
 module NCicHash : Hashtbl.S with type key = NCic.term
 
 val mk_appl : NCic.term -> NCic.term list -> NCic.term 
+
+val apply_subst : NCic.substitution -> NCic.term -> NCic.term

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 4807e5271938291a8e63e3b921ea7f220029caef..e38842ac82c57c6c454582438a5726f6f89ba86a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -538,19 +538,19 @@ let typeof_obj hdb
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   ~look_for_coercion (uri,height,metasenv,subst,obj)
 = 
-  let check_type metasenv subst (ty as orig_ty) =  (* XXX fattorizza *)
+  let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
     let metasenv, subst, ty, sort = 
-      typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None
+      typeof hdb ~localise ~look_for_coercion metasenv subst context ty None
     in
     let metasenv, subst, ty, sort = 
       force_to_sort hdb ~look_for_coercion 
-        metasenv subst [] ty orig_ty localise sort
+        metasenv subst context ty orig_ty localise sort
     in
       metasenv, subst, ty, sort
   in
   match obj with 
   | C.Constant (relevance, name, bo, ty , attr) ->
-       let metasenv, subst, ty, _ = check_type metasenv subst ty in
+       let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
        let metasenv, subst, bo, ty, height = 
          match bo with
          | Some bo ->
@@ -569,7 +569,7 @@ let typeof_obj hdb
       let types, metasenv, subst, rev_fl =
         List.fold_left
          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
-           let metasenv, subst, ty, _ = check_type metasenv subst ty in
+           let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
            let dbo = NCicTypeChecker.debruijn uri len [] bo in
            let localise = relocalise localise dbo bo in
             (name,C.Decl ty)::types,
@@ -606,7 +606,7 @@ let typeof_obj hdb
      let metasenv,subst,rev_itl,tys =
       List.fold_left
        (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
-         let metasenv, subst, ty, _ = check_type metasenv subst ty in
+          let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
           metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
        ) (metasenv,subst,[],[]) itl in
      let metasenv,subst,itl,_ =
@@ -666,7 +666,9 @@ let typeof_obj hdb
                 ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false
              in
-             let metasenv, subst, te, con_sort = check_type metasenv subst te in
+             let metasenv, subst, te, con_sort = 
+               check_type metasenv subst context te 
+             in
               (match
                 NCicReduction.whd ~subst context con_sort,
                 NCicReduction.whd ~subst [] ty_sort
@@ -698,11 +700,18 @@ let typeof_obj hdb
                     (lazy (localise te,
                       "Non positive occurence in " ^ NUri.string_of_uri uri)))
               else
+               let te = 
+                 NCicSubstitution.psubst 
+                  (fun i -> NCic.Const (NReference.reference_of_spec uri
+                     (NReference.Ind (ind,i,leftno))))
+                  (List.rev (HExtlib.list_seq 0 (List.length itl)))
+                   te 
+               in      
                metasenv,subst,(k_relev,n,te)::res
               ) cl (metasenv,subst,[])
          in
-          metasenv,subst,(it_relev,n,ty,cl)::res,i-1
-       ) (metasenv,subst,[],List.length rev_itl) rev_itl
+          metasenv,subst,(it_relev,n,ty,cl)::res,i+1
+       ) (metasenv,subst,[],1) rev_itl
      in
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index eeca351c228f01462ce591e70569109d7c2642c4..323b1e6fc0ee1b744f77c1405c73a26d5d7430bc 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -326,45 +326,8 @@ let analyse_indty status ty =
 
 let mk_cic_term c t = None,c,t ;;
 
-(* CSC: next two functions to be moved elsewhere *)
-let rec apply_subst subst ctx =
- function
-    NCic.Meta (i,lc) ->
-     (try
-       let _,_,t,_ = NCicUtils.lookup_subst i subst in
-       let t = NCicSubstitution.subst_meta lc t in
-        apply_subst subst ctx t
-      with
-       Not_found ->
-        match lc with
-           _,NCic.Irl _ -> NCic.Meta (i,lc)
-         | n,NCic.Ctx l ->
-            NCic.Meta
-             (i,(0,NCic.Ctx
-                 (List.map (fun t ->
-                   apply_subst subst ctx (NCicSubstitution.lift n t)) l))))
-  | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx (apply_subst subst) t
-;;
-
-let apply_subst_obj subst =
- function
-    NCic.Constant (relev,name,bo,ty,attrs) ->
-     NCic.Constant
-      (relev,name,HExtlib.map_option (apply_subst subst []) bo,
-        apply_subst subst [] ty,attrs)
-  | NCic.Fixpoint (ind,fl,attrs) ->
-     let fl =
-      List.map
-       (function (relevance,name,recno,ty,bo) ->
-         relevance,name,recno,apply_subst subst [] ty,apply_subst subst [] bo
-       ) fl
-     in
-      NCic.Fixpoint (ind,fl,attrs)
-  | _ -> assert false (* not implemented yet *)
-;;
-
 let apply_subst status ctx t =
  let status, (name,_,t) = relocate status ctx t in
  let _,_,_,subst,_ = status.pstatus in
-  status, (name, ctx, apply_subst subst ctx t)
+  status, (name, ctx, NCicUntrusted.apply_subst subst t)
 ;;

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 59ef3559264563ae6c2e2393e687eeb949df0af7..0653223af39fcae890932ec36878835485a572c2 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -60,9 +60,6 @@ val refine:
 val apply_subst:
   lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 
-(* CSC: this function must be moved elsewhere *)
-val apply_subst_obj: NCic.substitution -> NCic.obj_kind -> NCic.obj_kind
-
 val get_goalty: lowtac_status -> int -> cic_term
 val mk_meta: 
    lowtac_status -> ?name:string -> NCic.context ->