From 1859726f40a0a14c2e1b4f1b44041ce1e552f729 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 20 Feb 2008 16:53:59 +0000 Subject: [PATCH] added small test, fixed some bugs --- helm/software/components/ng_kernel/Makefile | 17 ++++- .../components/ng_kernel/nCic2OCic.ml | 30 ++++++--- .../components/ng_kernel/nCic2OCic.mli | 2 +- .../components/ng_kernel/nCicEnvironment.ml | 3 +- .../components/ng_kernel/nReference.ml | 10 ++- .../components/ng_kernel/oCic2NCic.ml | 63 ++++++++++--------- .../components/ng_kernel/oCic2NCic.mli | 2 +- .../components/ng_kernel/oCicTypeChecker.ml | 3 +- helm/software/components/ng_kernel/rt.ml | 17 +++++ helm/software/components/ng_kernel/test.ma | 23 +++++++ 10 files changed, 123 insertions(+), 47 deletions(-) create mode 100644 helm/software/components/ng_kernel/rt.ml create mode 100644 helm/software/components/ng_kernel/test.ma diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index cda5a9950..29e1fbe06 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -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 diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index e6a15d315..70d174e60 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -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 ;; diff --git a/helm/software/components/ng_kernel/nCic2OCic.mli b/helm/software/components/ng_kernel/nCic2OCic.mli index ab08d1bd9..edaaa3803 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.mli +++ b/helm/software/components/ng_kernel/nCic2OCic.mli @@ -1 +1 @@ -val convert_nobj: NCic.obj -> Cic.obj +val convert_nobj: NCic.obj -> (UriManager.uri * Cic.obj) list diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 8d0ae1a4f..02b3baab6 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -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 ;; diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 9d9ed88a6..d83fee65a 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -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 -> diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b81635581..dd91bbc32 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -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] ;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index 3930caea2..05e13643c 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -1 +1 @@ -val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj * NCic.obj list +val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml index 878706b9e..396144a5d 100644 --- a/helm/software/components/ng_kernel/oCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/oCicTypeChecker.ml @@ -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 index 000000000..74ed2eed9 --- /dev/null +++ b/helm/software/components/ng_kernel/rt.ml @@ -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 index 000000000..e1c496ca3 --- /dev/null +++ b/helm/software/components/ng_kernel/test.ma @@ -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 -- 2.39.2