]> matita.cs.unibo.it Git - helm.git/commitdiff
added small test, fixed some bugs
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 20 Feb 2008 16:53:59 +0000 (16:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 20 Feb 2008 16:53:59 +0000 (16:53 +0000)
helm/software/components/ng_kernel/Makefile
helm/software/components/ng_kernel/nCic2OCic.ml
helm/software/components/ng_kernel/nCic2OCic.mli
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nReference.ml
helm/software/components/ng_kernel/oCic2NCic.ml
helm/software/components/ng_kernel/oCic2NCic.mli
helm/software/components/ng_kernel/oCicTypeChecker.ml
helm/software/components/ng_kernel/rt.ml [new file with mode: 0644]
helm/software/components/ng_kernel/test.ma [new file with mode: 0644]

index cda5a99504e3afc3d7f3ead1e76bd7ac8e0d4ad8..29e1fbe06890d1907b17d42eb68cd863d89c998f 100644 (file)
@@ -2,12 +2,27 @@ PACKAGE = ng_kernel
 PREDICATES =
 
 INTERFACE_FILES = \
-       nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli nCicSubstitution.mli nCicUtils.mli nCicReduction.mli nCic2OCic.mli
+       nUri.mli \
+       nReference.mli \
+       oCic2NCic.mli  \
+       nCicEnvironment.mli \
+       nCicTypeChecker.mli \
+       oCicTypeChecker.mli \
+       nCicUtils.mli \
+       nCicSubstitution.mli \
+       nCicReduction.mli \
+       nCic2OCic.mli
+
 IMPLEMENTATION_FILES = \
   nCic.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 OCAMLOPTIONS += -w Ae
 
+all: rt
+rt: rt.ml $(PACKAGE).cma
+       $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $<
+       
+
 include ../../Makefile.defs
 include ../Makefile.common
index e6a15d3158902099616a4fd0a47ec33e7dacef97..70d174e60c84ce3ba4b274b39f679b91cea1fb68 100644 (file)
@@ -1,14 +1,19 @@
+let nn_2_on = function
+  | "_" -> Cic.Anonymous
+  | s -> Cic.Name s
+;;
+
 let convert_term uri n_fl t =
  let rec convert_term k = function (* pass k along *)
  | NCic.Rel i -> Cic.Rel i
  | NCic.Meta _ -> assert false
  | NCic.Appl l -> Cic.Appl (List.map (convert_term k) l)
  | NCic.Prod (n,s,t) -> 
-     Cic.Prod (Cic.Name n,convert_term k s, convert_term (k+1) t)
+     Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t)
  | NCic.Lambda  (n,s,t) -> 
-     Cic.Lambda(Cic.Name n,convert_term k s, convert_term (k+1) t)
+     Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t)
  | NCic.LetIn (n,_,s,t) -> 
-     Cic.LetIn (Cic.Name n,convert_term k s, convert_term (k+1) t)
+     Cic.LetIn (nn_2_on n,convert_term k s, convert_term (k+1) t)
  | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop 
  | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp 
  | NCic.Sort NCic.Set -> Cic.Sort Cic.Set 
@@ -57,12 +62,21 @@ let convert_fix is_fix uri k fl =
 
 let convert_nobj = function 
  | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) ->
-     Cic.Constant (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])
+     [NUri.ouri_of_nuri u,Cic.Constant 
+        (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])]
  | u,_,_,_,NCic.Constant (_, name,  None, ty, _) ->
-     Cic.Constant (name, None, convert_term u 0 ty, [],[])
+     [NUri.ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])]
  | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) ->
-     Cic.Constant (UriManager.name_of_uri (NUri.ouri_of_nuri u), 
-       Some (convert_fix is_fix u 0 fl), 
-       convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], [])
+     List.map 
+      (fun nth ->
+        let name = UriManager.name_of_uri (NUri.ouri_of_nuri u) in
+        let buri = UriManager.buri_of_uri (NUri.ouri_of_nuri u) in
+        let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in
+        uri,
+        Cic.Constant (name, 
+         Some (convert_fix is_fix u nth fl), 
+          convert_term u 0 (let _,_,_,ty,_ = List.hd fl in ty), [], []))
+     (let rec seq = function 0 -> [0]|n -> n::seq (n-1) in 
+      seq (List.length fl-1))
  | _,_,_,_,NCic.Inductive _ -> assert false
 ;;
index ab08d1bd975526d34ae3b58c6982def5bad4643d..edaaa3803fe6248f4812eedc4299bb780918fb43 100644 (file)
@@ -1 +1 @@
-val convert_nobj: NCic.obj -> Cic.obj
+val convert_nobj: NCic.obj -> (UriManager.uri * Cic.obj) list
index 8d0ae1a4f9e7e1a86225a23f2e5866fee1b8e3c0..02b3baab68e414f102277ea362d68df17323e4db 100644 (file)
@@ -7,7 +7,8 @@ let get_checked_obj u =
     let o,_ = 
       CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
         ouri in
-    let no,_ = OCic2NCic.convert_obj ouri o in
+    (* FIX: add all objects to the environment and give back the last one *)
+    let no = HExtlib.list_last (OCic2NCic.convert_obj ouri o) in
     NUri.UriHash.add cache u no;
     no
 ;;
index 9d9ed88a6a4098b18c446d530bade36934e8171f..d83fee65ab20ca6d67acefe078c0cfa295293a9e 100644 (file)
@@ -59,11 +59,9 @@ let set_of_reference = ref MapStringsToReference.empty;;
  *)
 
 let uri_suffix_of_ref_suffix = function
-    | "dec" 
-    | "def" -> "con"
-    | "ind" 
-    | "con" -> "ind"
-    | _ -> assert false
+    | "dec" | "fix" | "cfx" | "def" -> "con"
+    | "ind" | "con" -> "ind"
+    | x -> prerr_endline (x ^ " not a valid suffix"); assert false
 ;;
 
 let reference_of_string =
@@ -76,7 +74,7 @@ let reference_of_string =
     i,j
   in
   let get1 s dot =
-    let i = int_of_string (String.sub s (dot+5) (String.length s-1)) in
+    let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
     i
   in
 fun s ->
index b81635581b924c18e1c74378cb1247493d32cee7..dd91bbc320ce9206b8e884289c0231eed6fe0493 100644 (file)
@@ -38,7 +38,7 @@ let splat_args ctx t =
       | 0 -> []
       | n -> 
          (match List.nth ctx (n+bound) with
-         | Fix (refe, _, _) when n < primo_ce_dopo_fix -> (NCic.Const refe)
+         | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> (NCic.Const refe)
          | Fix _ | Ce _ -> NCic.Rel (n+bound)) :: aux (n-1)
     in
     NCic.Appl (t:: aux free)
@@ -50,18 +50,20 @@ let splat_args ctx t =
 let convert_term uri t = 
   let rec aux octx (ctx : ctx list) n_fix uri = function
     | Cic.CoFix (k, fl) ->
+        let buri = 
+          UriManager.uri_of_string 
+           (UriManager.buri_of_uri uri^"/"^
+            UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con")
+        in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
             (fun (name,ty,_) (ctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
-              let r = NReference.reference_of_ouri uri(NReference.CoFix idx) in
+              let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in
               ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1)
-            fl (ctx, [], [], 0)
-        in
-        let buri = 
-          UriManager.uri_of_string 
-           (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con")
+            fl ([], [], [], 0)
         in
+        let bctx = bctx @ ctx in
         let n_fl = List.length fl in
         let boctx,_ =
          List.fold_left
@@ -72,19 +74,24 @@ let convert_term uri t =
         let fl, fixpoints =
           List.fold_right2 
             (fun (name,_,bo) ty  (l,fixpoints) -> 
-               let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in
+               let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in
                (([],name,~-1,splat true ctx ty, splat false ctx bo)::l),
                fixpoints_bo @ fixpoints)
             fl tys ([],fixpoints_tys)
         in
         let obj = 
-          NUri.nuri_of_ouri uri,0,[],[],
+          NUri.nuri_of_ouri buri,0,[],[],
             NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
         in
-        splat_args ctx 
-         (NCic.Const (NReference.reference_of_ouri uri (NReference.CoFix k))),
-        obj::fixpoints
+        splat_args bctx 
+         (NCic.Const (NReference.reference_of_ouri buri (NReference.CoFix k))),
+        fixpoints @ [obj]
     | Cic.Fix (k, fl) ->
+        let buri = 
+          UriManager.uri_of_string 
+           (UriManager.buri_of_uri uri^"/"^
+            UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con")
+        in
         let rno = ref 0 in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
@@ -92,15 +99,12 @@ let convert_term uri t =
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
               if idx = k then rno := recno;
               let r = 
-                NReference.reference_of_ouri uri (NReference.Fix (idx,recno)) 
+                NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) 
               in
               ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1)
-            fl (ctx, [], [], 0)
-        in
-        let buri = 
-          UriManager.uri_of_string 
-           (UriManager.string_of_uri uri^string_of_int (List.length ctx)^".con")
+            fl ([], [], [], 0)
         in
+        let bctx = bctx @ ctx in
         let n_fl = List.length fl in
         let boctx,_ =
          List.fold_left
@@ -111,26 +115,29 @@ let convert_term uri t =
         let fl, fixpoints =
           List.fold_right2 
             (fun (name,rno,_,bo) ty (l,fixpoints) -> 
-               let bo, fixpoints_bo = aux boctx bctx (n_fix + n_fl) buri bo in
-               let rno = rno + List.length ctx - n_fix in
+               let bo, fixpoints_bo = aux boctx bctx n_fl buri bo in
+               let _, free, _ = context_tassonomy bctx in
+               let rno = rno + free in
                (([],name,rno,splat true ctx ty, splat false ctx bo)::l),
                fixpoints_bo @ fixpoints)
             fl tys ([],fixpoints_tys)
         in
         let obj = 
-          NUri.nuri_of_ouri uri,0,[],[],
+          NUri.nuri_of_ouri buri,0,[],[],
             NCic.Fixpoint (true, fl, (`Generated, `Definition)) 
         in
-        splat_args ctx
+        splat_args bctx
           (NCic.Const 
-            (NReference.reference_of_ouri uri (NReference.Fix (k,!rno)))),
-        obj::fixpoints
+            (NReference.reference_of_ouri buri (NReference.Fix (k,!rno)))),
+        fixpoints @ [obj]
     | Cic.Rel n ->
-        let _, _, primo_ce_dopo_fix = context_tassonomy ctx in
-        (match List.nth ctx n with
+        let bound, _, primo_ce_dopo_fix = context_tassonomy ctx in
+        (match List.nth ctx (n-1) with
         | Fix (r,_,_) when n < primo_ce_dopo_fix -> 
             splat_args ctx (NCic.Const r), []
-        | Fix (_,_,_) | Ce _ -> NCic.Rel (n-n_fix), [])
+        | Ce _ when n <= bound -> NCic.Rel n, []
+        | Fix _ (* BUG 3 fix nested *) 
+        | Ce _ -> NCic.Rel (n-n_fix), [])
     | Cic.Lambda (name, (s as old_s), t) ->
         let s, fixpoints_s = aux octx ctx n_fix uri s in
         let ctx = Ce (cn_to_s name, NCic.Decl s) :: ctx in
@@ -227,5 +234,5 @@ let convert_obj_aux uri = function
 let convert_obj uri obj = 
   let o, fixpoints = convert_obj_aux uri obj in
   let obj = NUri.nuri_of_ouri uri,0, [], [], o in
-  obj, fixpoints
+  fixpoints @ [obj]
 ;;
index 3930caea2c2982f094832b8f434798b5c98846ad..05e13643c3d007b36b30844c2f86afd2b815145f 100644 (file)
@@ -1 +1 @@
-val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj * NCic.obj list
+val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list
index 878706b9effb106430a71000f1995c5d4a68d384..396144a5d3c9b499dd7fb6829e282292e5a0a16b 100644 (file)
@@ -1,7 +1,8 @@
 
 let typecheck_obj uri obj =
   try 
-    NCicTypeChecker.typecheck_obj (fst (OCic2NCic.convert_obj uri obj)); true
+    NCicTypeChecker.typecheck_obj (HExtlib.list_last (OCic2NCic.convert_obj uri
+    obj)); true
   with 
     | NCicTypeChecker.TypeCheckerFailure _
     | NCicTypeChecker.AssertFailure _ -> false
diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_kernel/rt.ml
new file mode 100644 (file)
index 0000000..74ed2ee
--- /dev/null
@@ -0,0 +1,17 @@
+let _ =
+  Helm_registry.load_from "conf.xml";
+  let u = UriManager.uri_of_string "cic:/matita/tests/f.con" in
+  let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
+  let l = OCic2NCic.convert_obj u o in
+  let objs = 
+    List.flatten 
+    (List.map NCic2OCic.convert_nobj l) in
+  List.iter 
+   (fun (u,o) -> 
+     prerr_endline ("------- " ^ UriManager.string_of_uri u);
+     prerr_endline (CicPp.ppobj o);
+     try CicTypeChecker.typecheck_obj u o
+     with CicTypeChecker.TypeCheckerFailure s ->
+       prerr_endline (Lazy.force s)) 
+   objs;
+;;
diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma
new file mode 100644 (file)
index 0000000..e1c496c
--- /dev/null
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/nat.ma".
+
+let rec f n := 
+  match n with
+  [ O => O
+  | S m => let rec g x := 
+             match x with
+             [ O => f m
+             | S q => g q] in g m].
\ No newline at end of file