From a981dd18ae8ad9e9da79615fb80fe85dfe609f05 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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