From: Ferruccio Guidi Date: Wed, 7 Mar 2007 11:11:22 +0000 (+0000) Subject: Procedural : cic object preprocessor added X-Git-Tag: make_still_working~6436 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da240cc33abae83ca35782dee48b1a9a3a87ff76;p=helm.git Procedural : cic object preprocessor added depend[.opt]: some fixes --- diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 1b2fc5ff0..8cb9645ae 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,14 +1,20 @@ +proceduralPreprocess.cmo: proceduralPreprocess.cmi +proceduralPreprocess.cmx: proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -proceduralClassify.cmo: proceduralClassify.cmi -proceduralClassify.cmx: proceduralClassify.cmi -proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi -proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \ - proceduralConversion.cmi -proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \ - proceduralConversion.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ - proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ - proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi +proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi +proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi +proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \ + proceduralMode.cmi +proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \ + proceduralMode.cmi +proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ + proceduralMode.cmi proceduralConversion.cmi +proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ + proceduralMode.cmx proceduralConversion.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ + proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \ + acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ + proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \ + acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 1b2fc5ff0..8cb9645ae 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,14 +1,20 @@ +proceduralPreprocess.cmo: proceduralPreprocess.cmi +proceduralPreprocess.cmx: proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -proceduralClassify.cmo: proceduralClassify.cmi -proceduralClassify.cmx: proceduralClassify.cmi -proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi -proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi -proceduralConversion.cmo: proceduralTypes.cmi proceduralClassify.cmi \ - proceduralConversion.cmi -proceduralConversion.cmx: proceduralTypes.cmx proceduralClassify.cmx \ - proceduralConversion.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ - proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ - proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi +proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi +proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi +proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \ + proceduralMode.cmi +proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \ + proceduralMode.cmi +proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ + proceduralMode.cmi proceduralConversion.cmi +proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ + proceduralMode.cmx proceduralConversion.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ + proceduralMode.cmi proceduralConversion.cmi proceduralClassify.cmi \ + acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ + proceduralMode.cmx proceduralConversion.cmx proceduralClassify.cmx \ + acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index 8b3ea3695..379f5518b 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/components/acic_procedural/Makefile @@ -2,6 +2,7 @@ PACKAGE = acic_procedural PREDICATES = INTERFACE_FILES = \ + proceduralPreprocess.mli \ proceduralTypes.mli \ proceduralClassify.mli \ proceduralMode.mli \ diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index bbc358f71..28fa98947 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -37,6 +37,7 @@ module Ut = CicUtil module E = CicEnvironment module PER = ProofEngineReduction +module P = ProceduralPreprocess module Cl = ProceduralClassify module M = ProceduralMode module T = ProceduralTypes @@ -292,7 +293,7 @@ and mk_proof st = function let script = if proceed then let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in let (classes, rc) as h = Cl.classify st.context ty in - let premises, _ = Cl.split st.context ty in + let premises, _ = P.split st.context ty in let decurry = List.length classes - List.length tl in if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 6fd8a5e60..2fd2d979d 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -24,10 +24,11 @@ *) module C = Cic -module R = CicReduction module D = Deannotate module I = CicInspect +module P = ProceduralPreprocess + type conclusion = (int * int) option (* debugging ****************************************************************) @@ -55,15 +56,6 @@ let out_table b = let id x = x -let split c t = - let add s v c = Some (s, C.Decl v) :: c in - let rec aux whd a n c = function - | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t - | v when whd -> v :: a, n - | v -> aux true a n c (R.whd ~delta:true c v) - in - aux false [] 0 c t - let classify_conclusion = function | C.Rel i -> Some (i, 0) | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) @@ -71,7 +63,7 @@ let classify_conclusion = function let classify c t = try - let vs, h = split c t in + let vs, h = P.split c t in let rc = classify_conclusion (List.hd vs) in let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in let l, h = List.fold_left map ([], 0) vs in diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli index 35c07ab47..90c2c7852 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.mli +++ b/helm/software/components/acic_procedural/proceduralClassify.mli @@ -28,5 +28,3 @@ type conclusion = (int * int) option val classify: Cic.context -> Cic.term -> CicInspect.S.t list * conclusion val to_string: CicInspect.S.t list * conclusion -> string - -val split: Cic.context -> Cic.term -> Cic.term list * int diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 3bee4dd57..3df6802ff 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -30,8 +30,8 @@ module TC = CicTypeChecker module D = Deannotate module UM = UriManager +module P = ProceduralPreprocess module T = ProceduralTypes -module Cl = ProceduralClassify module M = ProceduralMode (* helpers ******************************************************************) @@ -174,7 +174,7 @@ try if is_recursive premise then 0, lift (succ k) 1 case, succ k else 0, case, succ k in - let premises, _ = Cl.split context cty in + let premises, _ = P.split context cty in let _, lifted_case, _ = List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises)) in diff --git a/helm/software/components/acic_procedural/proceduralMode.ml b/helm/software/components/acic_procedural/proceduralMode.ml index 433966d1b..2b233a4bf 100644 --- a/helm/software/components/acic_procedural/proceduralMode.ml +++ b/helm/software/components/acic_procedural/proceduralMode.ml @@ -24,6 +24,8 @@ *) module C = Cic + +module P = ProceduralPreprocess module Cl = ProceduralClassify let is_eliminator = function @@ -47,9 +49,9 @@ let rec is_appl b = function let bkd c t = let classes, rc = Cl.classify c t in - let premises, _ = Cl.split c t in + let premises, _ = P.split c t in match rc with | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true | _ -> - let ts, _ = Cl.split c t in + let ts, _ = P.split c t in is_appl true (List.hd ts) diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index 0d1e0cafc..a1a32d457 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -5,6 +5,7 @@ cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo discrimination_tree.cmi: cic.cmo path_indexing.cmi: cic.cmo +cicInspect.cmi: cic.cmo cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx unshare.cmo: cic.cmo unshare.cmi diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 94eaa78b8..21644fbe7 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -5,6 +5,7 @@ cicUtil.cmi: cic.cmx helmLibraryObjects.cmi: cic.cmx discrimination_tree.cmi: cic.cmx path_indexing.cmi: cic.cmx +cicInspect.cmi: cic.cmx cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx unshare.cmo: cic.cmx unshare.cmi diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index 8b943bb3d..add1a46c3 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -17,9 +17,9 @@ matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi matitaWiki.cmo gragrep.cmi + matitacLib.cmi matitaWiki.cmo matitaInit.cmi matitaEngine.cmi gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx matitaWiki.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt index b0119369b..fd3810b97 100644 --- a/helm/software/matita/.depend.opt +++ b/helm/software/matita/.depend.opt @@ -17,9 +17,9 @@ matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi matitaWiki.cmx gragrep.cmi + matitacLib.cmi matitaWiki.cmx matitaInit.cmi matitaEngine.cmi gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx matitaWiki.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx matitaInit.cmx matitaEngine.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index f1c1f496d..cff93ace3 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -35,6 +35,8 @@ (* $Id$ *) +module G = GrafiteAst + let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) @@ -156,27 +158,34 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = remove_closed_substs s let txt_of_cic_object ?map_unicode_to_tex n style prefix obj = - let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = - try Cic2acic.acic_object_of_cic_object obj + let get_aobj obj = + try + let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = + Cic2acic.acic_object_of_cic_object obj + in + aobj, ids_to_inner_sorts, ids_to_inner_types with e -> let msg = "txt_of_cic_object: " ^ Printexc.to_string e in failwith msg in match style with - | GrafiteAst.Declarative -> - let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in + | G.Declarative -> + let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in + let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in remove_closed_substs ("\n\n" ^ BoxPp.render_to_string ?map_unicode_to_tex (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) ) - | GrafiteAst.Procedural depth -> + | G.Procedural depth -> + let obj = ProceduralPreprocess.pp_obj obj in + let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in let term_pp = term2pres (n - 8) ids_to_inner_sorts in let lazy_term_pp = term_pp in let obj_pp = CicNotationPp.pp_obj term_pp in let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in - let script = Acic2Procedural.acic2procedural + let script = Acic2Procedural.acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in "\n" ^ String.concat "" (List.map aux script)