From 1dd6fc8c5d7bde039972a208c5eb03d3ea8303dd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 29 Apr 2007 15:41:14 +0000 Subject: [PATCH] GrafiteAstPp: \n's finally fixed acic_procedural: - elimination patterns are generated correctly - comments on elimination cases added --- components/acic_procedural/acic2Procedural.ml | 93 ++++++++++++------- .../acic_procedural/proceduralClassify.ml | 15 +-- .../acic_procedural/proceduralClassify.mli | 2 +- .../acic_procedural/proceduralConversion.ml | 8 +- .../acic_procedural/proceduralConversion.mli | 4 + components/acic_procedural/proceduralMode.ml | 2 +- components/acic_procedural/proceduralMode.mli | 3 +- components/acic_procedural/proceduralTypes.ml | 40 +++++--- components/grafite/grafiteAstPp.ml | 4 +- 9 files changed, 106 insertions(+), 65 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index c9423268c..ff8aaea88 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -50,7 +50,8 @@ type status = { max_depth: int option; depth: int; context: C.context; - intros: string list + intros: string list; + case: int list } (* helpers ******************************************************************) @@ -64,7 +65,7 @@ try let before2, after2 = HEL.split_nth n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" - + let string_of_head = function | C.ASort _ -> "sort" | C.AConst _ -> "const" @@ -90,6 +91,18 @@ let next st = {(clear st) with depth = succ st.depth} let add st entry intro = {st with context = entry :: st.context; intros = intro :: st.intros} +let push st = {st with case = 1 :: st.case} + +let inc st = + {st with case = match st.case with + | [] -> assert false + | hd :: tl -> succ hd :: tl + } + +let case st str = + let case = String.concat "." (List.rev_map string_of_int st.case) in + Printf.sprintf "case %s: %s" case str + let test_depth st = try let msg = Printf.sprintf "Depth %u: " st.depth in @@ -119,21 +132,7 @@ let is_fwd_rewrite_left hd tl = | C.ARel _ -> true | _ -> false else false -(* -let get_ind_name uri tno xcno = -try - let ts = match E.get_obj Un.empty_ugraph uri with - | C.InductiveDefinition (ts, _, _,_), _ -> ts - | _ -> assert false - in - let tname, cs = match List.nth ts tno with - | (name, _, _, cs) -> name, cs - in - match xcno with - | None -> tname - | Some cno -> fst (List.nth cs (pred cno)) -with Invalid_argument _ -> failwith "A2P.get_ind_name" -*) + let get_inner_types st v = try let id = Ut.id_of_annterm v in @@ -163,7 +162,17 @@ let get_entry st id = | _ :: tl -> aux tl in aux st.context - + +let get_ind_names uri tno = +try + let ts = match E.get_obj Un.empty_ugraph uri with + | C.InductiveDefinition (ts, _, _, _), _ -> ts + | _ -> assert false + in + match List.nth ts tno with + | (_, _, _, cs) -> List.map fst cs +with Invalid_argument _ -> failwith "A2P.get_ind_names" + (* proof construction *******************************************************) let unused_premise = "UNUSED" @@ -185,7 +194,7 @@ let convert st ?name v = match get_inner_types st v with | None -> [] | Some (sty, ety) -> - let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in + let e = Cn.hole "" in let csty, cety = cic sty, cic ety in if Ut.alpha_equivalence csty cety then [] else match name with @@ -278,39 +287,40 @@ 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 classes, rc = Cl.classify st.context ty in let goal_arity = match get_inner_types st what with | None -> 0 | Some (ity, _) -> snd (PEH.split_with_whd (st.context, cic ity)) in - let argsno = List.length classes in - let decurry = argsno - List.length tl in + let parsno, argsno = List.length classes, List.length tl in + let decurry = parsno - argsno in let diff = goal_arity - decurry in if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd))); let rec mk_synth a n = if n < 0 then a else mk_synth (I.S.add n a) (pred n) in let synth = mk_synth I.S.empty decurry in - let text = "" (* Printf.sprintf "%u %s" argsno (Cl.to_string h) *) in + let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in let script = List.rev (mk_arg st hd) @ convert st what in match rc with - | Some (i, j) -> + | Some (i, j, uri, tyno) -> 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 + let names = get_ind_names uri tyno in + let qs = proc_bkd_proofs (next st) synth names 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 predicate = List.nth tl (parsno - i) in + let e = Cn.mk_pattern 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 + let qs = proc_bkd_proofs (next st) synth [] classes tl in let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else @@ -331,15 +341,29 @@ and proc_proof st = function | 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 = +and proc_bkd_proofs st synth names classes ts = try + let get_note = + let names = ref (names, push st) in + fun f -> + match !names with + | [], st -> fun _ -> f st + | "" :: tl, st -> names := tl, st; fun _ -> f st + | hd :: tl, st -> + let note = case st hd in + names := tl, inc st; + fun b -> if b then T.Note note :: f st else f st + in 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 (proc_proof st v) else - Some [T.Apply (v, dtext ^ "dependent")] + if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else + Some (fun _ -> [T.Apply (v, dtext ^ "dependent")]) in - List.rev (T.list_map2_filter aux classes ts) + let ps = T.list_map2_filter aux classes ts in + let b = List.length ps > 1 in + List.rev_map (fun f -> f b) ps + with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) (* object costruction *******************************************************) @@ -353,7 +377,7 @@ let proc_obj st = function 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 ""] + T.Theorem (s, t, "") :: ast @ [T.Qed text] | _ -> failwith "not a theorem" @@ -367,7 +391,8 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = max_depth = depth; depth = 0; context = []; - intros = [] + intros = []; + case = [] } in HLog.debug "Procedural: level 2 transformation"; let steps = proc_obj st aobj in diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml index 4f9f99fce..755176e5c 100644 --- a/components/acic_procedural/proceduralClassify.ml +++ b/components/acic_procedural/proceduralClassify.ml @@ -23,6 +23,7 @@ * http://cs.unibo.it/helm/. *) +module UM = UriManager module C = Cic module D = Deannotate module I = CicInspect @@ -32,7 +33,7 @@ module H = ProceduralHelpers type dependence = I.S.t * bool -type conclusion = (int * int) option +type conclusion = (int * int * UM.uri * int) option (* debugging ****************************************************************) @@ -43,8 +44,8 @@ let string_of_entry (inverse, b) = let to_string (classes, rc) = let linearize = String.concat " " (List.map string_of_entry classes) in match rc with - | None -> linearize - | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j + | None -> linearize + | Some (i, j, _, _) -> Printf.sprintf "%s %u %u" linearize i j let out_table b = let map i (_, inverse) = @@ -67,11 +68,11 @@ let classify_conclusion vs = let inside i = i > 1 && i <= List.length vs in match vs with | v0 :: v1 :: _ -> - let hd0, argsno0 = get_argsno v0 in - let hd1, argsno1 = get_argsno v1 in + let hd0, a0 = get_argsno v0 in + let hd1, a1 = get_argsno v1 in begin match hd0, hd1 with - | C.Rel i, C.MutInd _ when inside i -> Some (i, argsno0) - | _ -> None + | C.Rel i, C.MutInd (u, n, _) when inside i -> Some (i, a0, u, n) + | _ -> None end | _ -> None diff --git a/components/acic_procedural/proceduralClassify.mli b/components/acic_procedural/proceduralClassify.mli index 9e478ca62..aea3c6e81 100644 --- a/components/acic_procedural/proceduralClassify.mli +++ b/components/acic_procedural/proceduralClassify.mli @@ -25,7 +25,7 @@ type dependence = CicInspect.S.t * bool -type conclusion = (int * int) option +type conclusion = (int * int * UriManager.uri * int) option val classify: Cic.context -> Cic.term -> dependence list * conclusion diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index 538981369..80aae9e7f 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -115,7 +115,7 @@ let generalize n = | C.AMutConstruct (id, _, _, _, _) | C.AMeta (id, _, _) -> meta id | C.ARel (id, _, m, _) -> - if m = succ (k - n) then hole id else meta id + if succ (k - n) <= m && m <= k then hole id else meta id | C.AAppl (id, ts) -> let ts = List.map (gen_term k) ts in if is_meta ts then meta id else C.AAppl (id, ts) @@ -139,6 +139,6 @@ let generalize n = in gen_term 0 -let mk_pattern rpsno predicate = - let body = generalize rpsno predicate in - clear_absts 0 rpsno body +let mk_pattern psno predicate = + let body = generalize psno predicate in + clear_absts 0 psno body diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli index 5cbb75da2..769cf3b9d 100644 --- a/components/acic_procedural/proceduralConversion.mli +++ b/components/acic_procedural/proceduralConversion.mli @@ -23,6 +23,10 @@ * http://cs.unibo.it/helm/. *) +val meta: Cic.id -> Cic.annterm + +val hole: Cic.id -> Cic.annterm + val lift: int -> int -> Cic.annterm -> Cic.annterm val mk_pattern: int -> Cic.annterm -> Cic.annterm diff --git a/components/acic_procedural/proceduralMode.ml b/components/acic_procedural/proceduralMode.ml index d2ddc6c98..e13846fc8 100644 --- a/components/acic_procedural/proceduralMode.ml +++ b/components/acic_procedural/proceduralMode.ml @@ -51,7 +51,7 @@ let bkd c t = let classes, rc = Cl.classify c t in let premises, _ = PEH.split_with_whd (c, t) in match rc with - | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true + | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true | _ -> let _, conclusion = List.hd premises in is_appl true conclusion diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli index b55188600..71356b6ff 100644 --- a/components/acic_procedural/proceduralMode.mli +++ b/components/acic_procedural/proceduralMode.mli @@ -22,7 +22,8 @@ * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) - +(* val is_eliminator: (Cic.context * Cic.term) list -> bool val bkd: Cic.context -> Cic.term -> bool +*) diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index ae153fe3d..a1d120f80 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -45,6 +45,10 @@ let list_map2_filter map l1 l2 = in filter [] (list_rev_map2 map l1 l2) +let list_init f i = + let rec aux a j = if j < 0 then a else aux (f j :: a) (pred j) in + aux [] i + (****************************************************************************) type name = string @@ -81,8 +85,14 @@ let floc = H.dummy_floc let mk_note str = G.Comment (floc, G.Note (floc, str)) -let mk_nlnote str a = - if str = "" then mk_note "" :: a else mk_note str :: mk_note "" :: a +let mk_tacnote str a = + if str = "" then mk_note "" :: a else mk_note "" :: mk_note str :: a + +let mk_notenote str a = + if str = "" then a else mk_note str :: a + +let mk_thnote str a = + if str = "" then a else mk_note "" :: mk_note str :: a let mk_theorem name t = let obj = N.Theorem (`Theorem, name, t, None) in @@ -158,22 +168,22 @@ let mk_vb = G.Shift floc (* rendering ****************************************************************) let rec render_step sep a = function - | Note s -> mk_note s :: a - | Theorem (n, t, s) -> mk_theorem n t :: mk_note s :: a - | Qed s -> mk_qed :: mk_nlnote s a - | Id s -> mk_id sep :: mk_nlnote s a - | Intros (c, ns, s) -> mk_intros c ns sep :: mk_nlnote s a - | Cut (n, t, s) -> mk_cut n t sep :: mk_nlnote s a - | LetIn (n, t, s) -> mk_letin n t sep :: mk_nlnote s a - | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_nlnote s a - | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_nlnote s a - | Apply (t, s) -> mk_apply t sep :: mk_nlnote s a - | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_nlnote s a - | ClearBody (n, s) -> mk_clearbody n sep :: mk_nlnote s a + | Note s -> mk_notenote s a + | Theorem (n, t, s) -> mk_theorem n t :: mk_thnote s a + | Qed s -> mk_qed :: mk_tacnote s a + | Id s -> mk_id sep :: mk_tacnote s a + | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a + | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a + | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a + | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a + | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a + | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a + | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a + | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a | Branch ([], s) -> a | Branch ([ps], s) -> render_steps sep a ps | Branch (ps :: pss, s) -> - let a = mk_ob :: mk_nlnote s a in + let a = mk_ob :: mk_tacnote s a in let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in mk_punctation sep :: render_steps mk_cb a ps diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 3602e9df5..67f771fbe 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -305,9 +305,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function | Note (_,"") -> Printf.sprintf "\n" - | Note (_,str) -> Printf.sprintf "(* %s *)\n" str + | Note (_,str) -> Printf.sprintf "\n(* %s *)" str | Code (_,code) -> - Printf.sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) + Printf.sprintf "\n(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function -- 2.39.2