]> matita.cs.unibo.it Git - helm.git/commitdiff
conversion half inplemented
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 13 Feb 2008 17:18:25 +0000 (17:18 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 13 Feb 2008 17:18:25 +0000 (17:18 +0000)
helm/software/components/ng_kernel/nCic.ml
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicTypeChecker.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/oCicTypeChecker.mli

index 961c84cfaa8394da488e73bfeb9ea0b72eac2514..639bab2b6ce5879fc856bb8a3f69ef078e07997b 100644 (file)
@@ -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 *)
 
index 9549f3c3cbcd92f260762b9e3aa5cf5ab8d0963a..37cebe647cc567bfc4437ba8ce9aff87e632423e 100644 (file)
@@ -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
 ;;
index ca943a828fd421a6cc630716cf9f786c41bb6555..30bde93171e9a6e999a4d6ce87edc8dec5e4e0f2 100644 (file)
@@ -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 _ -> ()
index c815358a5f3831e06fe5f5b3ef0a066c730dcf0a..b463452684f9f6a06de079a09a48a2dfd44b0d70 100644 (file)
@@ -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;;
index 86637b67a96c82425c825d5dc81e557b6ee8810e..bc58762a716d653b3d9b05917b35f5cd35375af3 100644 (file)
@@ -1 +1 @@
-val convert_obj: Cic.obj -> NCic.obj
+val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj
index 100e572af90db06f63e7b5892c08734b80f27156..2139654c7bd47280d155fa40c23cd2c2825898b1 100644 (file)
@@ -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
index 07ee59206468dc80775107a1bd91c5603d5764cb..165534310149d1627dfa997d682c357b730e566b 100644 (file)
@@ -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