From a484a2c1e0c022753aefae6a74fbce9fe4cf7983 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Aug 2012 15:44:16 +0000 Subject: [PATCH] Code extraction branched. --- matita/components/ng_kernel/.depend | 7 +++++++ matita/components/ng_kernel/.depend.opt | 7 +++++++ matita/components/ng_kernel/Makefile | 3 ++- .../components/ng_kernel/nCicEnvironment.mli | 4 ++++ .../components/ng_kernel/nCicExtraction.mli | 2 +- matita/components/ng_library/nCicLibrary.ml | 20 +++++++++++++------ matita/components/ng_library/nCicLibrary.mli | 3 ++- 7 files changed, 37 insertions(+), 9 deletions(-) diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend index 16f0d02cc..5273e5eb8 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -7,6 +7,7 @@ nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo nCicPp.cmi: nReference.cmi nCic.cmo +nCicExtraction.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -39,3 +40,9 @@ nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ nCicEnvironment.cmi nCic.cmo nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ nCicEnvironment.cmx nCic.cmx nCicPp.cmi +nCicExtraction.cmo: nUri.cmi nReference.cmi nCicUntrusted.cmi \ + nCicTypeChecker.cmi nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi \ + nCicEnvironment.cmi nCic.cmo nCicExtraction.cmi +nCicExtraction.cmx: nUri.cmx nReference.cmx nCicUntrusted.cmx \ + nCicTypeChecker.cmx nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx \ + nCicEnvironment.cmx nCic.cmx nCicExtraction.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index c57bf8efe..af21515ba 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -7,6 +7,7 @@ nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx nCicPp.cmi: nReference.cmi nCic.cmx +nCicExtraction.cmi: nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -39,3 +40,9 @@ nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ nCicEnvironment.cmi nCic.cmx nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ nCicEnvironment.cmx nCic.cmx nCicPp.cmi +nCicExtraction.cmo: nUri.cmi nReference.cmi nCicUntrusted.cmi \ + nCicTypeChecker.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \ + nCic.cmx nCicExtraction.cmi +nCicExtraction.cmx: nUri.cmx nReference.cmx nCicUntrusted.cmx \ + nCicTypeChecker.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ + nCic.cmx nCicExtraction.cmi diff --git a/matita/components/ng_kernel/Makefile b/matita/components/ng_kernel/Makefile index 35b89f3b1..6bca07465 100644 --- a/matita/components/ng_kernel/Makefile +++ b/matita/components/ng_kernel/Makefile @@ -10,7 +10,8 @@ INTERFACE_FILES = \ nCicReduction.mli \ nCicTypeChecker.mli \ nCicUntrusted.mli \ - nCicPp.mli + nCicPp.mli \ + nCicExtraction.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli index 80fcd2b68..a557ef563 100644 --- a/matita/components/ng_kernel/nCicEnvironment.mli +++ b/matita/components/ng_kernel/nCicEnvironment.mli @@ -24,6 +24,10 @@ val check_and_add_obj: #NCic.status -> NCic.obj -> unit val get_relevance: #NCic.status -> NReference.reference -> bool list +val get_checked_decl: + #NCic.status -> NReference.reference -> + NCic.relevance * string * NCic.term * NCic.c_attr * int + val get_checked_def: #NCic.status -> NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int diff --git a/matita/components/ng_kernel/nCicExtraction.mli b/matita/components/ng_kernel/nCicExtraction.mli index b11f38654..e1a068527 100644 --- a/matita/components/ng_kernel/nCicExtraction.mli +++ b/matita/components/ng_kernel/nCicExtraction.mli @@ -28,4 +28,4 @@ class virtual status : (* Haskell *) -val haskell_of_obj: (#status as 'status) -> NCic.obj -> 'status * string option +val haskell_of_obj: (#status as 'status) -> NCic.obj -> 'status * string diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index 729d62d0e..b509ce813 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -146,10 +146,11 @@ let init = load_db;; class virtual status = object - inherit NCic.status + inherit NCicExtraction.status val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} + (*CSC: bug here, we are not copying the NCicExtraction part of the status *) end let time_travel0 (sto,ali) = @@ -324,10 +325,10 @@ let aliases_of uri = if NUri.eq uri' uri then Some nref else None) !local_aliases ;; -let add_obj status ((u,_,_,_,_) as obj) = - NCicEnvironment.check_and_add_obj status obj; - storage := (`Obj (u,obj))::!storage; - let _,height,_,_,obj = obj in +let add_obj status ((u,_,_,_,_) as orig_obj) = + NCicEnvironment.check_and_add_obj status orig_obj; + storage := (`Obj (u,orig_obj))::!storage; + let _,height,_,_,obj = orig_obj in let references = match obj with NCic.Constant (_,name,None,_,_) -> @@ -356,7 +357,14 @@ let add_obj status ((u,_,_,_,_) as obj) = ) il) in local_aliases := references @ !local_aliases; - status#set_timestamp (!storage,!local_aliases) + let status = status#set_timestamp (!storage,!local_aliases) in + (* To test extraction *) + try + ignore (Helm_registry.get "extract_haskell"); + let status,msg = NCicExtraction.haskell_of_obj status orig_obj in + prerr_endline msg; status + with + Helm_registry.Key_not_found _ -> status ;; let add_constraint status u1 u2 = diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index 3d9ab02cb..3781a47e2 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -18,9 +18,10 @@ type timestamp class virtual status : object ('self) - inherit NCic.status + inherit NCicExtraction.status method timestamp: timestamp method set_timestamp: timestamp -> 'self + (*CSC: bug here, we are not copying the NCicExtraction part of the status *) end (* it also checks it and add it to the environment *) -- 2.39.2