From db10f4aee3571b87d24c3f52a61721311c384dd2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 2 Apr 2007 12:09:35 +0000 Subject: [PATCH] Cic2acic : added some debugging information Procedural: some refactoring and improvements --- components/acic_procedural/.depend | 20 +- components/acic_procedural/.depend.opt | 20 +- components/acic_procedural/Makefile | 1 + components/acic_procedural/acic2Procedural.ml | 222 +++++++++--------- .../acic_procedural/proceduralClassify.ml | 13 +- .../acic_procedural/proceduralHelpers.ml | 151 ++++++++++++ .../acic_procedural/proceduralHelpers.mli | 51 ++++ .../acic_procedural/proceduralPreprocess.ml | 178 ++++---------- components/cic_acic/cic2acic.ml | 12 +- components/cic_acic/cic2acic.mli | 2 +- 10 files changed, 395 insertions(+), 275 deletions(-) create mode 100644 components/acic_procedural/proceduralHelpers.ml create mode 100644 components/acic_procedural/proceduralHelpers.mli diff --git a/components/acic_procedural/.depend b/components/acic_procedural/.depend index c1c6561c2..02ce90009 100644 --- a/components/acic_procedural/.depend +++ b/components/acic_procedural/.depend @@ -1,7 +1,11 @@ -proceduralClassify.cmo: proceduralClassify.cmi -proceduralClassify.cmx: proceduralClassify.cmi -proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi -proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi +proceduralHelpers.cmo: proceduralHelpers.cmi +proceduralHelpers.cmx: proceduralHelpers.cmi +proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi +proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi +proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ + proceduralPreprocess.cmi +proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ + proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi @@ -10,7 +14,7 @@ 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 \ - proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ - proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + proceduralClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + proceduralClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/.depend.opt b/components/acic_procedural/.depend.opt index c1c6561c2..02ce90009 100644 --- a/components/acic_procedural/.depend.opt +++ b/components/acic_procedural/.depend.opt @@ -1,7 +1,11 @@ -proceduralClassify.cmo: proceduralClassify.cmi -proceduralClassify.cmx: proceduralClassify.cmi -proceduralPreprocess.cmo: proceduralClassify.cmi proceduralPreprocess.cmi -proceduralPreprocess.cmx: proceduralClassify.cmx proceduralPreprocess.cmi +proceduralHelpers.cmo: proceduralHelpers.cmi +proceduralHelpers.cmx: proceduralHelpers.cmi +proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi +proceduralClassify.cmx: proceduralHelpers.cmx proceduralClassify.cmi +proceduralPreprocess.cmo: proceduralHelpers.cmi proceduralClassify.cmi \ + proceduralPreprocess.cmi +proceduralPreprocess.cmx: proceduralHelpers.cmx proceduralClassify.cmx \ + proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi @@ -10,7 +14,7 @@ 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 \ - proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ - proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + proceduralClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + proceduralClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/Makefile b/components/acic_procedural/Makefile index 780462786..78d3e3b09 100644 --- a/components/acic_procedural/Makefile +++ b/components/acic_procedural/Makefile @@ -2,6 +2,7 @@ PACKAGE = acic_procedural PREDICATES = INTERFACE_FILES = \ + proceduralHelpers.mli \ proceduralClassify.mli \ proceduralPreprocess.mli \ proceduralTypes.mli \ diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 3cf4bb596..7fd8290ba 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -26,7 +26,6 @@ module C = Cic module I = CicInspect module D = Deannotate -module DTI = DoubleTypeInference module TC = CicTypeChecker module Un = CicUniv module UM = UriManager @@ -39,7 +38,6 @@ module PEH = ProofEngineHelpers module PER = ProofEngineReduction module Pp = CicPp -module P = ProceduralPreprocess module Cl = ProceduralClassify module T = ProceduralTypes module Cn = ProceduralConversion @@ -143,14 +141,14 @@ try | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st) with Not_found -> None with Invalid_argument _ -> failwith "A2P.get_inner_types" - +(* let get_inner_sort st v = try let id = Ut.id_of_annterm v in try Hashtbl.find st.sorts id with Not_found -> `Type (CicUniv.fresh()) with Invalid_argument _ -> failwith "A2P.get_sort" - +*) let get_type msg st bo = try let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in @@ -177,139 +175,133 @@ let get_intro = function | C.Name s -> s let mk_intros st script = -try if st.intros = [] then script else let count = List.length st.intros in T.Intros (Some count, List.rev st.intros, "") :: script -with Invalid_argument _ -> failwith "A2P.mk_intros" -let rec mk_arg st = function - | C.ARel (_, _, _, name) as what -> convert st ~name what, what - | what -> [], what +let mk_arg st = function + | C.ARel (_, _, _, name) as what -> convert st ~name what + | _ -> [] -and mk_fwd_rewrite st dtext name tl direction = +let mk_fwd_rewrite st dtext name tl direction = assert (List.length tl = 6); let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in match where with | C.ARel (_, _, _, premise) -> - let script, what = mk_arg st what in - T.Rewrite (direction, what, Some (premise, name), e, dtext) :: script + let script = mk_arg st what in + let where = Some (premise, name) in + T.Rewrite (direction, what, where, e, dtext) :: script | _ -> assert false -and mk_rewrite st dtext script t what qs tl direction = +let mk_rewrite st dtext what qs tl direction = assert (List.length tl = 5); let predicate = List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in - List.rev script @ convert st t @ [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")] -and mk_fwd_proof st dtext name = function - | C.AAppl (_, hd :: tl) as v -> - if is_fwd_rewrite_right hd tl then mk_fwd_rewrite st dtext name tl true else - if is_fwd_rewrite_left hd tl then mk_fwd_rewrite st dtext name tl false else - let ty = get_type "TC1" st hd in - begin match get_inner_types st v with - | Some (ity, _) -> - let qs = [[T.Id ""]; mk_proof (next st) v] in - [T.Branch (qs, ""); T.Cut (name, ity, dtext)] - | _ -> - let (classes, rc) as h = Cl.classify st.context ty in - let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in - [T.LetIn (name, v, dtext ^ text)] - end - | C.AMutCase _ -> assert false - | C.ACast _ -> assert false - | v -> - match get_inner_types st v with +let rec proc_lambda st name v t = + let entry = Some (name, C.Decl (cic v)) in + let intro = get_intro name in + proc_proof (add st entry intro) t + +and proc_letin st what name v t = + let intro = get_intro name in + let proceed, dtext = test_depth st in + let script = if proceed then + let hyp, rqv = match get_inner_types st v with | Some (ity, _) -> - let qs = [[T.Id ""]; mk_proof (next st) v] in - [T.Branch (qs, ""); T.Cut (name, ity, dtext)] - | _ -> - [T.LetIn (name, v, dtext)] - -and mk_proof st = function - | C.ALambda (_, name, v, t) -> - let entry = Some (name, C.Decl (cic v)) in - let intro = get_intro name in - mk_proof (add st entry intro) t - | C.ALetIn (_, name, v, t) as what -> - let proceed, dtext = test_depth st in - let script = if proceed then - let entry = Some (name, C.Def (cic v, None)) in - let intro = get_intro name in - let q = mk_proof (next (add st entry intro)) t in - List.rev_append (mk_fwd_proof st dtext intro v) q - else - [T.Apply (what, dtext)] - in - mk_intros st script - | C.ARel _ as what -> - let _, dtext = test_depth st in - let text = "assumption" in - let script = [T.Apply (what, dtext ^ text)] in - mk_intros st script - | C.AMutConstruct _ as what -> - let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in - mk_intros st script - | C.AAppl (_, hd :: tl) as t -> - let proceed, dtext = test_depth st in - let script = if proceed then - let ty = get_type "TC2" st hd in - let (classes, rc) as h = Cl.classify st.context ty in - let decurry = List.length classes - List.length tl in - if decurry <> 0 then begin - let msg = Printf.sprintf "Decurry: %i\nTerm: %s\nContext: %s" - decurry (Pp.ppterm (cic t)) (Pp.ppcontext st.context) + let rqv = match v with + | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl -> + mk_fwd_rewrite st dtext intro tl true + | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl -> + mk_fwd_rewrite st dtext intro tl false + | v -> + let qs = [[T.Id ""]; proc_proof (next st) v] in + [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in - HLog.warn msg; assert false - end; - let synth = I.S.singleton 0 in - let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in - match rc with - | Some (i, j) -> - let classes, tl, _, what = split2_last classes tl in - let script, what = mk_arg st what in - let synth = I.S.add 1 synth in - let qs = mk_bkd_proofs (next st) synth classes tl in - if is_rewrite_right hd then - mk_rewrite st dtext script t what qs tl false - else if is_rewrite_left hd then - mk_rewrite st dtext script t what qs tl true - else - let l = succ (List.length tl) in - let predicate = List.nth tl (l - i) in - let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in - let using = Some hd in - List.rev script @ convert st t @ - [T.Elim (what, using, e, dtext ^ text); T.Branch (qs, "")] - | None -> - let qs = mk_bkd_proofs (next st) synth classes tl in - let script, hd = mk_arg st hd in - List.rev script @ convert st t @ - [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] - else - [T.Apply (t, dtext)] + C.Decl (get_type "TC1" st v), rqv + | None -> + C.Def (cic v, None), [T.LetIn (intro, v, dtext)] in - mk_intros st script - | C.AMutCase _ -> assert false - | C.ACast _ -> assert false - | t -> - let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in - let script = [T.Note text] in - mk_intros st script - -and mk_bkd_proofs st synth classes ts = + let entry = Some (name, hyp) in + let qt = proc_proof (next (add st entry intro)) t in + List.rev_append rqv qt + else + [T.Apply (what, dtext)] + in + mk_intros st script + +and proc_rel st what = + let _, dtext = test_depth st in + let text = "assumption" in + let script = [T.Apply (what, dtext ^ text)] in + mk_intros st script + +and proc_mutconstruct st what = + let _, dtext = test_depth st in + let script = [T.Apply (what, dtext)] in + mk_intros st script + +and proc_appl st what hd tl = + let proceed, dtext = test_depth st in + let script = if proceed then + let ty = get_type "TC2" st hd in + let (classes, rc) as h = Cl.classify st.context ty in + let argsno = List.length classes in + let diff = argsno - List.length tl in + if diff <> 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd))); + let synth = I.S.singleton 0 in + let text = Printf.sprintf "%u %s" argsno (Cl.to_string h) in + let script = List.rev (mk_arg st hd) @ convert st what in + match rc with + | Some (i, j) -> + let classes, tl, _, where = split2_last classes tl in + let script = List.rev (mk_arg st where) @ script in + let synth = I.S.add 1 synth in + let qs = proc_bkd_proofs (next st) synth classes tl in + if is_rewrite_right hd then + script @ mk_rewrite st dtext where qs tl false + else if is_rewrite_left hd then + script @ mk_rewrite st dtext where qs tl true + else + let predicate = List.nth tl (argsno - i) in + let e = Cn.mk_pattern 0 (T.mk_arel 1 "") (* j predicate *) in + let using = Some hd in + script @ + [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] + | None -> + let qs = proc_bkd_proofs (next st) synth classes tl in + script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + else + [T.Apply (what, dtext)] + in + mk_intros st script + +and proc_other st what = + let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in + let script = [T.Note text] in + mk_intros st script + + +and proc_proof st = function + | C.ALambda (_, name, w, t) -> proc_lambda st name w t + | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t + | C.ARel _ as what -> proc_rel st what + | C.AMutConstruct _ as what -> proc_mutconstruct st what + | C.AAppl (_, hd :: tl) as what -> proc_appl st what hd tl + | what -> proc_other st what + +and proc_bkd_proofs st synth classes ts = try let _, dtext = test_depth st in let aux (inv, _) v = if I.overlaps synth inv then None else - if I.S.is_empty inv then Some (mk_proof st v) else + if I.S.is_empty inv then Some (proc_proof st v) else Some [T.Apply (v, dtext ^ "dependent")] in T.list_map2_filter aux classes ts -with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs" +with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs" (* object costruction *******************************************************) @@ -317,9 +309,9 @@ let is_theorem pars = List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars -let mk_obj st = function +let proc_obj st = function | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars -> - let ast = mk_proof st v in + let ast = proc_proof st v in let count = T.count_steps 0 ast in let text = Printf.sprintf "tactics: %u" count in T.Theorem (s, t, text) :: ast @ [T.Qed ""] @@ -338,7 +330,7 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = context = []; intros = [] } in - HLog.debug "Level 2 transformation"; - let steps = mk_obj st aobj in - HLog.debug "grafite rendering"; + HLog.debug "Procedural: level 2 transformation"; + let steps = proc_obj st aobj in + HLog.debug "Procedural: grafite rendering"; List.rev (T.render_steps [] steps) diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml index 6c1e482c2..4f9f99fce 100644 --- a/components/acic_procedural/proceduralClassify.ml +++ b/components/acic_procedural/proceduralClassify.ml @@ -28,6 +28,8 @@ module D = Deannotate module I = CicInspect module PEH = ProofEngineHelpers +module H = ProceduralHelpers + type dependence = I.S.t * bool type conclusion = (int * int) option @@ -52,12 +54,8 @@ let out_table b = in Array.iteri map b; prerr_newline () - -(****************************************************************************) - -let identity x = x -let fst3 (x, _, _) = x +(* classification ***********************************************************) let classify_conclusion vs = let rec get_argsno = function @@ -83,12 +81,13 @@ try let rc = classify_conclusion vs in let map (b, h) (c, v) = let _, argsno = PEH.split_with_whd (c, v) in - (I.get_rels_from_premise h v, I.S.empty, argsno > 0) :: b, succ h + let iu = H.is_unsafe h (List.hd vs) in + (I.get_rels_from_premise h v, I.S.empty, argsno > 0 && iu) :: b, succ h in let l, h = List.fold_left map ([], 0) vs in let b = Array.of_list (List.rev l) in let mk_closure b h = - let map j = if j < h then I.S.union (fst3 b.(j)) else identity in + let map j = if j < h then I.S.union (H.fst3 b.(j)) else H.identity in for i = pred h downto 0 do let direct, unused, fa = b.(i) in b.(i) <- I.S.fold map direct direct, unused, fa diff --git a/components/acic_procedural/proceduralHelpers.ml b/components/acic_procedural/proceduralHelpers.ml new file mode 100644 index 000000000..39607fefd --- /dev/null +++ b/components/acic_procedural/proceduralHelpers.ml @@ -0,0 +1,151 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module Rf = CicRefine +module Un = CicUniv +module Pp = CicPp +module TC = CicTypeChecker +module PEH = ProofEngineHelpers +module E = CicEnvironment +module UM = UriManager + +(* fresh name generator *****************************************************) + +let split name = + let rec aux i = + if i <= 0 then assert false else + let c = name.[pred i] in + if c >= '0' && c <= '9' then aux (pred i) + else Str.string_before name i, Str.string_after name i + in + let before, after = aux (String.length name) in + let i = if after = "" then -1 else int_of_string after in + before, i + +let join (s, i) = + C.Name (if i < 0 then s else s ^ string_of_int i) + +let mk_fresh_name context name = + let rec aux i = function + | [] -> name, i + | Some (C.Name s, _) :: entries -> + let m, j = split s in + if m = name && j >= i then aux (succ j) entries else aux i entries + | _ :: entries -> aux i entries + in + join (aux (-1) context) + +let mk_fresh_name context = function + | C.Anonymous -> C.Anonymous + | C.Name s -> mk_fresh_name context s + +(* helper functions *********************************************************) + +let rec list_map_cps g map = function + | [] -> g [] + | hd :: tl -> + let h hd = + let g tl = g (hd :: tl) in + list_map_cps g map tl + in + map h hd + +let identity x = x + +let compose f g x = f (g x) + +let fst3 (x, _, _) = x + +let refine c t = + try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t + with e -> + Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e); + Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c); + Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t); + raise e + +let get_type c t = + try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty + with e -> + Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c); + Printf.eprintf "TC: term : %s\n" (Pp.ppterm t); + raise e + +let get_tail c t = + match PEH.split_with_whd (c, t) with + | (_, hd) :: _, _ -> hd + | _ -> assert false + +let is_proof c t = + match get_tail c (get_type c (get_type c t)) with + | C.Sort C.Prop -> true + | C.Sort _ -> false + | _ -> assert false + +let is_unsafe h (c, t) = true + +let is_not_atomic = function + | C.Sort _ + | C.Rel _ + | C.Const _ + | C.Var _ + | C.MutInd _ + | C.MutConstruct _ -> false + | _ -> true + +let get_ind_type uri tyno = + match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno + | _ -> assert false + +let get_default_eliminator context uri tyno ty = + let _, (name, _, _, _) = get_ind_type uri tyno in + let ext = match get_tail context (get_type context ty) with + | C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.CProp -> "_rec" + | C.Sort (C.Type _) -> "_rect" + | t -> + Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t); + assert false + in + let buri = UM.buri_of_uri uri in + let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in + C.Const (uri, []) + +let get_ind_parameters c t = + let ty = get_type c t in + let ps = match get_tail c ty with + | C.MutInd _ -> [] + | C.Appl (C.MutInd _ :: args) -> args + | _ -> assert false + in + let disp = match get_tail c (get_type c ty) with + | C.Sort C.Prop -> 0 + | C.Sort _ -> 1 + | _ -> assert false + in + ps, disp diff --git a/components/acic_procedural/proceduralHelpers.mli b/components/acic_procedural/proceduralHelpers.mli new file mode 100644 index 000000000..84844942a --- /dev/null +++ b/components/acic_procedural/proceduralHelpers.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val mk_fresh_name: + Cic.context -> Cic.name -> Cic.name +val list_map_cps: + ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b +val identity: + 'a -> 'a +val compose: + ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val fst3: + 'a * 'b * 'c -> 'a +val refine: + Cic.context -> Cic.term -> Cic.term +val get_type: + Cic.context -> Cic.term -> Cic.term +val is_proof: + Cic.context -> Cic.term -> bool +val is_unsafe: + int -> Cic.context * Cic.term -> bool +val is_not_atomic: + Cic.term -> bool +val get_ind_type: + UriManager.uri -> int -> int * Cic.inductiveType +val get_default_eliminator: + Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term +val get_ind_parameters: + Cic.context -> Cic.term -> Cic.term list * int diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml index 6b84dd9b9..2b8e1ea3d 100644 --- a/components/acic_procedural/proceduralPreprocess.ml +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -23,120 +23,32 @@ * http://cs.unibo.it/helm/. *) -module UM = UriManager module C = Cic module Pp = CicPp -module Un = CicUniv module I = CicInspect -module E = CicEnvironment module S = CicSubstitution -module TC = CicTypeChecker -module Rf = CicRefine module DTI = DoubleTypeInference module HEL = HExtlib module PEH = ProofEngineHelpers +module H = ProceduralHelpers module Cl = ProceduralClassify -(* helper functions *********************************************************) - -let rec list_map_cps g map = function - | [] -> g [] - | hd :: tl -> - let h hd = - let g tl = g (hd :: tl) in - list_map_cps g map tl - in - map h hd - -let identity x = x - -let comp f g x = f (g x) - -let refine c t = - try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t - with e -> - Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e); - Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c); - Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t); - raise e - -let get_type c t = - try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty - with e -> - Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c); - Printf.eprintf "TC: term : %s\n" (Pp.ppterm t); - raise e - -let get_tail c t = - match PEH.split_with_whd (c, t) with - | (_, hd) :: _, _ -> hd - | _ -> assert false - -let is_proof c t = - match get_tail c (get_type c (get_type c t)) with - | C.Sort C.Prop -> true - | C.Sort _ -> false - | _ -> assert false - -let is_not_atomic = function - | C.Sort _ - | C.Rel _ - | C.Const _ - | C.Var _ - | C.MutInd _ - | C.MutConstruct _ -> false - | _ -> true - -let get_ind_type uri tyno = - match E.get_obj Un.empty_ugraph uri with - | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno - | _ -> assert false - -let get_default_eliminator context uri tyno ty = - let _, (name, _, _, _) = get_ind_type uri tyno in - let ext = match get_tail context (get_type context ty) with - | C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" - | C.Sort (C.Type _) -> "_rect" - | t -> - Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t); - assert false - in - let buri = UM.buri_of_uri uri in - let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in - C.Const (uri, []) - -let get_ind_parameters c t = - let ty = get_type c t in - let ps = match get_tail c ty with - | C.MutInd _ -> [] - | C.Appl (C.MutInd _ :: args) -> args - | _ -> assert false - in - let disp = match get_tail c (get_type c ty) with - | C.Sort C.Prop -> 0 - | C.Sort _ -> 1 - | _ -> assert false - in - ps, disp - (* term preprocessing: optomization 1 ***************************************) let defined_premise = "DEFINED" -let define c v = +let define v = let name = C.Name defined_premise in C.LetIn (name, v, C.Rel 1) let clear_absts m = let rec aux k n = function - | C.Lambda (s, v, t) when k > 0 -> + | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, aux (pred k) n t) - | C.Lambda (_, _, t) when n > 0 -> + | C.Lambda (_, _, t) when n > 0 -> aux 0 (pred n) (S.lift (-1) t) - | t when n > 0 -> + | t when n > 0 -> Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t); assert false | t -> t @@ -149,15 +61,17 @@ let rec add_abst k = function | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t) let rec opt1_letin g es c name v t = + let name = H.mk_fresh_name c name in let entry = Some (name, C.Def (v, None)) in let g t = if DTI.does_not_occur 1 t then begin - HLog.warn "Optimizer: remove 1"; g (S.lift (-1) t) + let x = S.lift (-1) t in + HLog.warn "Optimizer: remove 1"; opt1_proof g true c x end else let g = function - | C.LetIn (nname, vv, tt) when is_proof c v -> - let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in - HLog.warn "Optimizer: swap 1"; opt1_proof g false c x + | C.LetIn (nname, vv, tt) when H.is_proof c v -> + let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in + HLog.warn "Optimizer: swap 1"; opt1_proof g true c x | v -> g (C.LetIn (name, v, t)) in @@ -166,6 +80,7 @@ let rec opt1_letin g es c name v t = if es then opt1_proof g es (entry :: c) t else g t and opt1_lambda g es c name w t = + let name = H.mk_fresh_name c name in let entry = Some (name, C.Decl w) in let g t = let name = if DTI.does_not_occur 1 t then C.Anonymous else name in @@ -179,43 +94,42 @@ and opt1_appl g es c t vs = | C.LetIn (mame, vv, tt) -> let vs = List.map (S.lift 1) vs in let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in - HLog.warn "Optimizer: swap 2"; opt1_proof g false c x + HLog.warn "Optimizer: swap 2"; opt1_proof g true c x | C.Lambda (name, ww, tt) -> let v, vs = List.hd vs, List.tl vs in let x = C.Appl (C.LetIn (name, v, tt) :: vs) in - HLog.warn "Optimizer: remove 2"; opt1_proof g false c x + HLog.warn "Optimizer: remove 2"; opt1_proof g true c x | C.Appl vvs -> let x = C.Appl (vvs @ vs) in - HLog.warn "Optimizer: nested application"; opt1_proof g false c x + HLog.warn "Optimizer: nested application"; opt1_proof g true c x | t -> let rec aux d rvs = function - | [], _ -> + | [], _ -> let x = C.Appl (t :: List.rev rvs) in - if d then opt1_proof g false c x else g x - | v :: vs, (c, b) :: cs -> - if is_not_atomic v && I.S.mem 0 c && b then begin + if d then opt1_proof g true c x else g x + | v :: vs, (cc, bb) :: cs -> + if H.is_not_atomic v && I.S.mem 0 cc && bb then begin HLog.warn "Optimizer: anticipate 1"; - aux true (define c v :: rvs) (vs, cs) + aux true (define v :: rvs) (vs, cs) end else aux d (v :: rvs) (vs, cs) - | _, [] -> assert false + | _, [] -> assert false in let h () = - let classes, conclusion = Cl.classify c (get_type c t) in + let classes, conclusion = Cl.classify c (H.get_type c t) in let csno, vsno = List.length classes, List.length vs in - if csno < vsno && csno > 0 then + if csno < vsno then let vvs, vs = HEL.split_nth csno vs in - let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in - HLog.warn "Optimizer: anticipate 2"; opt1_proof g false c x + let x = C.Appl (define (C.Appl (t :: vvs)) :: vs) in + HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x else match conclusion, List.rev vs with - | Some _, rv :: rvs when csno = vsno && is_not_atomic rv -> - let x = C.Appl (t :: List.rev rvs @ [define c rv]) in - HLog.warn "Optimizer: anticipate 3"; opt1_proof g false c x + | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv -> + let x = C.Appl (t :: List.rev rvs @ [define rv]) in + HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x | Some _, _ -> g (C.Appl (t :: vs)) | None, _ -> - if csno > 0 then aux false [] (vs, classes) - else g (C.Appl (t :: vs)) + aux false [] (vs, classes) in let rec aux h prev = function | C.LetIn (name, vv, tt) :: vs -> @@ -224,7 +138,7 @@ and opt1_appl g es c t vs = let vs = List.map (S.lift 1) vs in let y = C.Appl (t :: List.rev prev @ tt :: vs) in let x = C.LetIn (name, vv, y) in - HLog.warn "Optimizer: swap 3"; opt1_proof g false c x + HLog.warn "Optimizer: swap 3"; opt1_proof g true c x | v :: vs -> aux h (v :: prev) vs | [] -> h () in @@ -232,12 +146,12 @@ and opt1_appl g es c t vs = in if es then opt1_proof g es c t else g t in - if es then list_map_cps g (fun h -> opt1_term h es c) vs else g vs + if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs and opt1_mutcase g es c uri tyno outty arg cases = - let eliminator = get_default_eliminator c uri tyno outty in - let lpsno, (_, _, _, constructors) = get_ind_type uri tyno in - let ps, sort_disp = get_ind_parameters c arg in + let eliminator = H.get_default_eliminator c uri tyno outty in + let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in + let ps, sort_disp = H.get_ind_parameters c arg in let lps, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in let predicate = clear_absts rpsno (1 - sort_disp) outty in @@ -260,7 +174,7 @@ and opt1_mutcase g es c uri tyno outty arg cases = in let lifted_cases = List.map2 map2 cases constructors in let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in - let x = refine c (C.Appl args) in + let x = H.refine c (C.Appl args) in HLog.warn "Optimizer: remove 3"; opt1_proof g es c x and opt1_cast g es c t w = @@ -279,7 +193,7 @@ and opt1_proof g es c = function | t -> opt1_other g es c t and opt1_term g es c t = - if is_proof c t then opt1_proof g es c t else g t + if H.is_proof c t then opt1_proof g es c t else g t (* term preprocessing: optomization 2 ***************************************) @@ -292,10 +206,10 @@ let eta_expand g tys t = let arg i = C.Rel (succ i) in let rec aux i f a = function | [] -> f, a - | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl + | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl in let n = List.length tys in - let absts, args = aux 0 identity [] tys in + let absts, args = aux 0 H.identity [] tys in let t = match S.lift n t with | C.Appl ts -> C.Appl (ts @ args) | t -> C.Appl (t :: args) @@ -319,18 +233,18 @@ and opt2_appl g c t vs = let g vs = let x = C.Appl (t :: vs) in let vsno = List.length vs in - let _, csno = PEH.split_with_whd (c, get_type c t) in + let _, csno = PEH.split_with_whd (c, H.get_type c t) in if vsno < csno then - let tys, _ = PEH.split_with_whd (c, get_type c x) in + let tys, _ = PEH.split_with_whd (c, H.get_type c x) in let tys = List.rev (List.tl tys) in let tys, _ = HEL.split_nth (csno - vsno) tys in HLog.warn "Optimizer: eta 1"; eta_expand g tys x else g x in - list_map_cps g (fun h -> opt2_term h c) vs + H.list_map_cps g (fun h -> opt2_term h c) vs and opt2_other g c t = - let tys, csno = PEH.split_with_whd (c, get_type c t) in + let tys, csno = PEH.split_with_whd (c, H.get_type c t) in if csno > 0 then begin let tys = List.rev (List.tl tys) in HLog.warn "Optimizer: eta 2"; eta_expand g tys t @@ -343,13 +257,17 @@ and opt2_proof g c = function | t -> opt2_other g c t and opt2_term g c t = - if is_proof c t then opt2_proof g c t else g t + if H.is_proof c t then opt2_proof g c t else g t (* object preprocessing *****************************************************) let pp_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> - let g bo = C.Constant (name, Some bo, ty, pars, attrs) in + let g bo = + Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo); + let _ = H.get_type [] (C.Cast (bo, ty)) in + C.Constant (name, Some bo, ty, pars, attrs) + in Printf.eprintf "BEGIN: %s\n" name; begin try opt1_term (opt2_term g []) true [] bo with e -> failwith ("PPP: " ^ Printexc.to_string e) end diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml index 98b142982..89d3d00b4 100644 --- a/components/cic_acic/cic2acic.ml +++ b/components/cic_acic/cic2acic.ml @@ -82,16 +82,16 @@ let fresh_id seed ids_to_terms ids_to_father_ids = let source_id_of_id id = "#source#" ^ id;; -exception NotEnoughElements;; +exception NotEnoughElements of string;; (*CSC: cut&paste da cicPp.ml *) (* get_nth l n returns the nth element of the list l if it exists or *) (* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = +let rec get_nth msg l n = match (n,l) with (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements + | (n, he::tail) when n > 1 -> get_nth msg tail (n-1) + | (_,_) -> raise (NotEnoughElements msg) ;; @@ -224,7 +224,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes match tt with C.Rel n -> let id = - match get_nth context n with + match get_nth "1" context n with (Some (C.Name s,_)) -> s | _ -> "__" ^ string_of_int n in @@ -643,7 +643,7 @@ let plain_acic_term_of_cic_term = match t with C.Rel n -> let idref,id = - match get_nth context n with + match get_nth "2" context n with idref,(Some (C.Name s,_)) -> idref,s | idref,_ -> idref,"__" ^ string_of_int n in diff --git a/components/cic_acic/cic2acic.mli b/components/cic_acic/cic2acic.mli index e6379283d..b63a585e6 100644 --- a/components/cic_acic/cic2acic.mli +++ b/components/cic_acic/cic2acic.mli @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception NotEnoughElements +exception NotEnoughElements of string val source_id_of_id : string -> string -- 2.39.2