From a981dd18ae8ad9e9da79615fb80fe85dfe609f05 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2008 17:18:25 +0000 Subject: [PATCH] conversion half inplemented --- helm/software/components/ng_kernel/nCic.ml | 5 +- .../components/ng_kernel/nCicEnvironment.ml | 2 +- .../components/ng_kernel/nCicTypeChecker.ml | 2 +- .../components/ng_kernel/oCic2NCic.ml | 53 ++++++++++++++++++- .../components/ng_kernel/oCic2NCic.mli | 2 +- .../components/ng_kernel/oCicTypeChecker.ml | 4 +- .../components/ng_kernel/oCicTypeChecker.mli | 2 +- 7 files changed, 61 insertions(+), 9 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 961c84cfa..639bab2b6 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -88,10 +88,11 @@ type def_pragma = (* pragmatic of the object *) | `Projection (* record projection *) | `InversionPrinciple (* inversion principle *) | `Variant - | `Local ] (* Local = hidden technicality *) + | `Local + | `Regular ] (* Local = hidden technicality *) type ind_pragma = (* pragmatic of the object *) - [ `Record of (string * bool * int) list ] + [ `Record of (string * bool * int) list | `Regular ] (* inductive type that encodes a record; the arguments are the record * fields names and if they are coercions and then the coercion arity *) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 9549f3c3c..37cebe647 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -7,7 +7,7 @@ let get_checked_obj u = let o,_ = CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri in - let no = OCic2NCic.convert_obj o in + let no = OCic2NCic.convert_obj ouri o in NUri.UriHash.add cache u no; no ;; diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index ca943a828..30bde9317 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -3,4 +3,4 @@ exception TypeCheckerFailure of string Lazy.t exception AssertFailure of string Lazy.t (* typechecks the object, raising an exception if illtyped *) -let typecheck_obj obj = () +let typecheck_obj obj = match obj with _ -> () diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index c815358a5..b46345268 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -1,2 +1,53 @@ +let convert_term = Obj.magic;; -let convert_obj obj = Obj.magic obj +let cn_to_s = function + | Cic.Anonymous -> "_" + | Cic.Name s -> s +;; + +let rec convert_fix_definition acc = function + | Cic.Lambda (n,s,t) -> + convert_fix_definition ((n,s)::acc) t + | Cic.Fix (_, [name,rno,ty,bo]) -> + let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in + let ty = convert_term ty in + let bo = convert_term bo in + Some (true,[[],name,rno, + List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty, + List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo]) + | Cic.CoFix (_, [name,ty,bo]) -> + let acc = List.map (fun (n,s) -> cn_to_s n, convert_term s) acc in + let ty = convert_term ty in + let bo = convert_term bo in + Some (false,[[],name,0, + List.fold_right (fun (n,s) acc -> NCic.Prod(n,s,acc)) acc ty, + List.fold_right (fun (n,s) acc -> NCic.Lambda(n,s,acc)) acc bo]) + | _ -> None +;; + +let convert_obj_aux = function + | Cic.Constant (name, None, ty, _, _) -> + NCic.Constant ([], name, None, convert_term ty, + (`Provided,`Theorem,`Regular)) + | Cic.Constant (name, Some bo, ty, _, _) -> + (match convert_fix_definition [] bo with + | None -> + NCic.Constant ([], name, Some (convert_term bo), convert_term ty, + (`Provided,`Theorem,`Regular)) + | Some (recursive, ifl) -> + NCic.Fixpoint (recursive, ifl, (`Provided, `Definition))) + | Cic.InductiveDefinition (itl,_,leftno,_) -> + let ind = let _,x,_,_ = List.hd itl in x in + let itl = + List.map + (fun name, _, ty, cl -> + [], name, convert_term ty, + List.map (fun name, ty -> [], name, convert_term ty) cl) + itl + in + NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false +;; + +let convert_obj uri obj = NUri.nuri_of_ouri uri,0, [], [], convert_obj_aux obj;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index 86637b67a..bc58762a7 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -1 +1 @@ -val convert_obj: Cic.obj -> NCic.obj +val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml index 100e572af..2139654c7 100644 --- a/helm/software/components/ng_kernel/oCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/oCicTypeChecker.ml @@ -1,7 +1,7 @@ -let typecheck_obj obj = +let typecheck_obj uri obj = try - NCicTypeChecker.typecheck_obj (OCic2NCic.convert_obj obj); true + NCicTypeChecker.typecheck_obj (OCic2NCic.convert_obj uri obj); true with | NCicTypeChecker.TypeCheckerFailure _ | NCicTypeChecker.AssertFailure _ -> false diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.mli b/helm/software/components/ng_kernel/oCicTypeChecker.mli index 07ee59206..165534310 100644 --- a/helm/software/components/ng_kernel/oCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/oCicTypeChecker.mli @@ -26,5 +26,5 @@ (* typechecks the OLD object using the NEW type checker, * if illtyped returns false (no exceptions raised) *) -val typecheck_obj : Cic.obj -> bool +val typecheck_obj : UriManager.uri -> Cic.obj -> bool -- 2.39.2