From 5abe94a6813fc8fc810df6a35bdb32eaac179536 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 26 Apr 2007 19:06:42 +0000 Subject: [PATCH] procedural: bug fixes matita: some \n rearranged GrafiteAstPp: some \n rearranged GrafiteParser: added callback --- components/acic_procedural/acic2Procedural.ml | 40 +++--- .../acic_procedural/proceduralOptimizer.ml | 2 +- components/acic_procedural/proceduralTypes.ml | 134 ++++++++---------- .../acic_procedural/proceduralTypes.mli | 6 +- components/grafite/grafiteAstPp.ml | 78 +++++----- components/grafite_parser/grafiteParser.ml | 14 +- components/grafite_parser/grafiteParser.mli | 2 + matita/applyTransformation.ml | 2 +- matita/matitac.ml | 16 ++- 9 files changed, 145 insertions(+), 149 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index bff721a3e..c9423268c 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -35,8 +35,9 @@ module HObj = HelmLibraryObjects module A = Cic2acic module Ut = CicUtil module E = CicEnvironment -module PEH = ProofEngineHelpers module Pp = CicPp +module PEH = ProofEngineHelpers +module HEL = HExtlib module Cl = ProceduralClassify module T = ProceduralTypes @@ -59,8 +60,8 @@ let cic = D.deannotate_term let split2_last l1 l2 = try let n = pred (List.length l1) in - let before1, after1 = T.list_split n l1 in - let before2, after2 = T.list_split n l2 in + let before1, after1 = HEL.split_nth n l1 in + let before2, after2 = HEL.split_nth n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" @@ -167,16 +168,16 @@ let get_entry st id = let unused_premise = "UNUSED" -let mk_exp_args hd tl classes = +let mk_exp_args hd tl classes synth = let meta id = C.AImplicit (id, None) in let map v (cl, b) = - if I.S.mem 0 cl && b then v else meta "" + if I.overlaps synth cl && b then v else meta "" in let rec aux = function | [] -> [] | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl) in - let args = List.rev_map2 map tl classes in + let args = T.list_rev_map2 map tl classes in let args = aux args in if args = [] then hd else C.AAppl ("", hd :: args) @@ -247,7 +248,7 @@ and proc_letin st what name v t = | 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 + let qs = [proc_proof (next st) v; [T.Id ""]] in [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in C.Decl (cic ity), rqv @@ -278,11 +279,19 @@ and proc_appl st what hd tl = 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 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 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 decurry = argsno - List.length tl 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 script = List.rev (mk_arg st hd) @ convert st what in match rc with | Some (i, j) -> @@ -302,7 +311,7 @@ and proc_appl st what hd tl = [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth classes tl in - let hd = mk_exp_args hd tl classes in + let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else [T.Apply (what, dtext)] @@ -314,7 +323,6 @@ and proc_other st what = 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 @@ -330,9 +338,9 @@ try 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")] - in - T.list_map2_filter aux classes ts -with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs" + in + List.rev (T.list_map2_filter aux classes ts) +with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) (* object costruction *******************************************************) diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml index 67b3af940..9d95d100b 100644 --- a/components/acic_procedural/proceduralOptimizer.ml +++ b/components/acic_procedural/proceduralOptimizer.ml @@ -269,6 +269,6 @@ let optimize_obj = function C.Constant (name, Some bo, ty, pars, attrs) in Printf.eprintf "BEGIN: %s\n" name; - begin try opt1_term (opt2_term g []) true [] bo + begin try opt1_term g (* (opt2_term g []) *) true [] bo with e -> failwith ("PPP: " ^ Printexc.to_string e) end | obj -> obj diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index 8dac90f26..c30251f48 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -30,41 +30,20 @@ module N = CicNotationPt (* functions to be moved ****************************************************) +let list_rev_map2 map l1 l2 = + let rec aux res = function + | hd1 :: tl1, hd2 :: tl2 -> aux (map hd1 hd2 :: res) (tl1, tl2) + | _ -> res + in + aux [] (l1, l2) + let list_map2_filter map l1 l2 = let rec filter l = function | [] -> l | None :: tl -> filter l tl | Some a :: tl -> filter (a :: l) tl in - filter [] (List.rev_map2 map l1 l2) - -let rec list_split n l = - if n = 0 then [], l else - let l1, l2 = list_split (pred n) (List.tl l) in - List.hd l :: l1, l2 - -let cont sep a = match sep with - | None -> a - | Some sep -> sep :: a - -let list_rev_map_concat map sep a l = - let rec aux a = function - | [] -> a - | [x] -> map a x - | x :: y :: l -> aux (sep :: map a x) (y :: l) - in - aux a l - -let is_atomic = function - | C.ASort _ - | C.AConst _ - | C.AMutInd _ - | C.AMutConstruct _ - | C.AVar _ - | C.ARel _ - | C.AMeta _ - | C.AImplicit _ -> true - | _ -> false + filter [] (list_rev_map2 map l1 l2) (****************************************************************************) @@ -98,11 +77,13 @@ let mk_arel i b = Cic.ARel ("", "", i, b) (* grafite ast constructors *************************************************) -(* 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_theorem name t = let obj = N.Theorem (`Theorem, name, t, None) in G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) @@ -110,86 +91,91 @@ let mk_theorem name t = let mk_qed = G.Executable (floc, G.Command (floc, G.Qed floc)) -let mk_tactic tactic = - G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None)) +let mk_tactic tactic punctation = + G.Executable (floc, G.Tactic (floc, Some tactic, punctation)) + +let mk_punctation punctation = + G.Executable (floc, G.Tactic (floc, None, punctation)) -let mk_id = +let mk_id punctation = let tactic = G.IdTac floc in - mk_tactic tactic + mk_tactic tactic punctation -let mk_intros xi ids = +let mk_intros xi ids punctation = let tactic = G.Intros (floc, xi, ids) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_cut name what = +let mk_cut name what punctation = let tactic = G.Cut (floc, Some name, what) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_letin name what = +let mk_letin name what punctation = let tactic = G.LetIn (floc, what, name) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_rewrite direction what where pattern = +let mk_rewrite direction what where pattern punctation = let direction = if direction then `RightToLeft else `LeftToRight in let pattern, rename = match where with | None -> (None, [], Some pattern), [] | Some (premise, name) -> (None, [premise, pattern], None), [name] in let tactic = G.Rewrite (floc, direction, what, pattern, rename) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_elim what using pattern = +let mk_elim what using pattern punctation = let pattern = None, [], Some pattern in let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_apply t = +let mk_apply t punctation = let tactic = G.Apply (floc, t) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_change t where pattern = +let mk_change t where pattern punctation = let pattern = match where with | None -> None, [], Some pattern | Some (premise, _) -> None, [premise, pattern], None in let tactic = G.Change (floc, pattern, t) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_clearbody id = +let mk_clearbody id punctation = let tactic = G.ClearBody (floc, id) in - mk_tactic tactic + mk_tactic tactic punctation -let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None)) +let mk_ob = + let punctation = G.Branch floc in + mk_punctation punctation -let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None)) +let mk_dot = G.Dot floc -let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None)) +let mk_sc = G.Semicolon floc -let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None)) +let mk_cb = G.Merge floc -let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None)) +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_note s :: mk_theorem n t :: a - | Qed s -> (* mk_note s :: *) mk_qed :: a - | Id s -> mk_note s :: cont sep (mk_id :: a) - | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) - | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) - | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) - | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a) - | Elim (t, xu, e, s) -> mk_note s :: cont sep (mk_elim t xu e :: a) - | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a) - | Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a) - | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: 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 | Branch ([], s) -> a | Branch ([ps], s) -> render_steps sep a ps - | Branch (pss, s) -> - let a = mk_ob :: a in - let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in - mk_note s :: cont sep body + | Branch (ps :: pss, s) -> + let a = mk_ob :: mk_nlnote s a in + let a = List.fold_left (render_steps mk_vb) a pss in + mk_punctation sep :: render_steps mk_cb a ps and render_steps sep a = function | [] -> a @@ -197,13 +183,11 @@ and render_steps sep a = function | p :: Branch ([], _) :: ps -> render_steps sep a (p :: ps) | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) -> - render_steps sep (render_step (Some mk_sc) a p) ps + render_steps sep (render_step mk_sc a p) ps | p :: ps -> - render_steps sep (render_step (Some mk_dot) a p) ps + render_steps sep (render_step mk_dot a p) ps -let render_steps a = render_steps None a -*) -let render_steps sep a = assert false +let render_steps a = render_steps mk_dot a (* counting *****************************************************************) diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index 97ca7fdbb..9659a94ec 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -25,14 +25,12 @@ (* functions to be moved ****************************************************) -val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list +val list_rev_map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list -val list_split: int -> 'a list -> 'a list * 'a list +val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list val mk_arel: int -> string -> Cic.annterm -val is_atomic:Cic.annterm -> bool - (****************************************************************************) type name = string diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 710761ed9..3602e9df5 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - open GrafiteAst let tactical_terminator = "" @@ -48,15 +46,15 @@ let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = let what_text = match what with | None -> "" - | Some t -> sprintf "in match (%s) " (lazy_term_pp t) in + | Some t -> Printf.sprintf "in match (%s) " (lazy_term_pp t) in let hyp_text = String.concat " " - (List.map (fun (name, p) -> sprintf "%s:(%s)" name (term_pp p)) hyp) in + (List.map (fun (name, p) -> Printf.sprintf "%s:(%s)" name (term_pp p)) hyp) in let goal_text = match goal with | None -> "" - | Some t -> sprintf "\\vdash (%s)" (term_pp t) in - sprintf "%sin %s%s" what_text hyp_text goal_text + | Some t -> Printf.sprintf "\\vdash (%s)" (term_pp t) in + Printf.sprintf "%sin %s%s" what_text hyp_text goal_text let pp_intros_specs = function | None, [] -> "" @@ -76,17 +74,17 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = function (* Higher order tactics *) | Do (_, count, tac) -> - sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac) + Printf.sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac) | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs | Then (_, tac, tacs) -> - sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac) + Printf.sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac) (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) | First (_, tacs) -> - sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) + Printf.sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac | Solve (_, tac) -> - sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac) + Printf.sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac) | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac (* First order tactics *) | Absurd (_, term) -> "absurd" ^ term_pp term @@ -99,41 +97,41 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Assumption _ -> "assumption" - | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^ + | Cases (_, term, idents) -> Printf.sprintf "cases " ^ term_pp term ^ pp_intros_specs (None, idents) | Change (_, where, with_what) -> - sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) - | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids) - | ClearBody (_,id) -> sprintf "clearbody %s" id + Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) + | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_idents ids) + | ClearBody (_,id) -> Printf.sprintf "clearbody %s" id | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> "cut " ^ term_pp term ^ (match ident with None -> "" | Some id -> " as " ^ id) | Decompose (_, names) -> - sprintf "decompose%s" (pp_intros_specs (None, names)) + Printf.sprintf "decompose%s" (pp_intros_specs (None, names)) | Demodulate _ -> "demodulate" | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, what, using, pattern, num, idents) -> - sprintf "elim %s%s %s%s" + Printf.sprintf "elim %s%s %s%s" (term_pp what) (match using with None -> "" | Some term -> " using " ^ term_pp term) (pp_tactic_pattern pattern) (pp_intros_specs (num, idents)) | ElimType (_, term, using, num, idents) -> - sprintf "elim type " ^ term_pp term ^ + Printf.sprintf "elim type " ^ term_pp term ^ (match using with None -> "" | Some term -> " using " ^ term_pp term) ^ pp_intros_specs (num, idents) | Exact (_, term) -> "exact " ^ term_pp term | Exists _ -> "exists" | Fold (_, kind, term, pattern) -> - sprintf "fold %s %s %s" (pp_reduction_kind kind) + Printf.sprintf "fold %s %s %s" (pp_reduction_kind kind) (lazy_term_pp term) (pp_tactic_pattern pattern) | FwdSimpl (_, hyp, idents) -> - sprintf "fwd %s%s" hyp + Printf.sprintf "fwd %s%s" hyp (match idents with [] -> "" | idents -> " as " ^ pp_idents idents) | Generalize (_, pattern, ident) -> - sprintf "generalize %s%s" (pp_tactic_pattern pattern) + Printf.sprintf "generalize %s%s" (pp_tactic_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) | Fail _ -> "fail" | Fourier _ -> "fourier" @@ -141,11 +139,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Intros (_, None, []) -> "intros" | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> - sprintf "intros%s%s" + Printf.sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | LApply (_, linear, level_opt, terms, term, ident_opt) -> - sprintf "lapply %s%s%s%s%s" + Printf.sprintf "lapply %s%s%s%s%s" (if linear then " linear " else "") (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") (term_pp term) @@ -153,14 +151,14 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (match ident_opt with None -> "" | Some ident -> " as " ^ ident) | Left _ -> "left" | LetIn (_, term, ident) -> - sprintf "letin %s \\def %s" ident (term_pp term) + Printf.sprintf "letin %s \\def %s" ident (term_pp term) | Reduce (_, kind, pat) -> - sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) + Printf.sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" | Replace (_, pattern, t) -> - sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) + Printf.sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) | Rewrite (_, pos, t, pattern, names) -> - sprintf "rewrite %s %s %s%s" + Printf.sprintf "rewrite %s %s %s%s" (if pos = `LeftToRight then ">" else "<") (term_pp t) (pp_tactic_pattern pattern) @@ -214,10 +212,10 @@ let pp_macro ~term_pp = let style_pp = function | Declarative -> "" | Procedural None -> "procedural " - | Procedural (Some i) -> sprintf "procedural %u " i + | Procedural (Some i) -> Printf.sprintf "procedural %u " i in let prefix_pp prefix = - if prefix = "" then "" else sprintf " \"%s\"" prefix + if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix in function (* Whelp *) @@ -227,17 +225,17 @@ let pp_macro ~term_pp = | WElim (_, t) -> "whelp elim " ^ term_pp t | WMatch (_, term) -> "whelp match " ^ term_pp term (* real macros *) - | Check (_, term) -> sprintf "check %s" (term_pp term) + | Check (_, term) -> Printf.sprintf "check %s" (term_pp term) | Hint _ -> "hint" | Inline (_, style, suri, prefix) -> - sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) + Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" | Gramext.NonA -> "non associative" -let pp_precedence i = sprintf "with precedence %d" i +let pp_precedence i = Printf.sprintf "with precedence %d" i let pp_dir_opt = function | None -> "" @@ -245,11 +243,11 @@ let pp_dir_opt = function | Some `RightToLeft -> "< " let pp_default what uris = - sprintf "default \"%s\" %s" what + Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) let pp_coercion uri do_composites arity = - sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity + Printf.sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity (if do_composites then "compounds" else "no compounds") let pp_command ~term_pp ~obj_pp = function @@ -272,7 +270,7 @@ let pp_command ~term_pp ~obj_pp = function Some r -> " transitivity proved by " ^ term_pp r | None -> "") | Print (_,s) -> "print " ^ s - | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value + | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value let pp_punctuation_tactical ~term_pp ~lazy_term_pp = function @@ -280,14 +278,14 @@ let pp_punctuation_tactical ~term_pp ~lazy_term_pp = | Semicolon _ -> ";" | Branch _ -> "[" | Shift _ -> "|" - | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i)) + | Pos (_, i) -> Printf.sprintf "%s:" (String.concat "," (List.map string_of_int i)) | Wildcard _ -> "*:" | Merge _ -> "]" let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = function | Focus (_, goals) -> - sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) + Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) | Unfocus _ -> "unfocus" | Skip _ -> "skip" @@ -302,14 +300,14 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = | NonPunctuationTactical (_, tac, punct) -> pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct - | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n" + | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function - | Note (_,"") -> sprintf "\n" - | Note (_,str) -> sprintf "(* %s *)\n" str + | Note (_,"") -> Printf.sprintf "\n" + | Note (_,str) -> Printf.sprintf "(* %s *)\n" str | Code (_,code) -> - sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) + Printf.sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 7b515472d..63df8ab7f 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -25,7 +25,8 @@ (* $Id$ *) -open Printf +let out = ref ignore +let set_callback f = out := f module Ast = CicNotationPt @@ -460,10 +461,10 @@ EXTEND LexiconAst.Ident_alias (id, uri) else raise - (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) + (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( - sprintf "Not a valid identifier: %s" id))) + Printf.sprintf "Not a valid identifier: %s" id))) | IDENT "symbol"; symbol = QSTRING; instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; SYMBOL "="; dsc = QSTRING -> @@ -501,11 +502,11 @@ EXTEND IDENT "for"; p2 = [ blob = UNPARSED_AST -> - add_raw_attribute ~text:(sprintf "@{%s}" blob) + add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob) (CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string blob)) | blob = UNPARSED_META -> - add_raw_attribute ~text:(sprintf "${%s}" blob) + add_raw_attribute ~text:(Printf.sprintf "${%s}" blob) (CicNotationParser.parse_level2_meta (Ulexing.from_utf8_string blob)) ] -> @@ -661,13 +662,14 @@ EXTEND fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let buri, fullpath = + let buri, fullpath = DependenciesParser.baseuri_of_script ~include_paths fname in let status = LexiconEngine.eval_command status (LexiconAst.Include (iloc,buri,mode,fullpath)) in + !out fname; status, LSome (GrafiteAst.Executable diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli index 6d941d5db..f8754df0c 100644 --- a/components/grafite_parser/grafiteParser.mli +++ b/components/grafite_parser/grafiteParser.mli @@ -42,3 +42,5 @@ val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) val statement: statement Grammar.Entry.e +(* this callback is called on every include command *) +val set_callback: (string -> unit) -> unit diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml index b5aa06f9d..4883deaf8 100644 --- a/matita/applyTransformation.ml +++ b/matita/applyTransformation.ml @@ -188,7 +188,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj = let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in let script = Acic2Procedural.acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in - "\n" ^ String.concat "" (List.map aux script) + String.concat "" (List.map aux script) ^ "\n\n" let txt_of_inline_macro style suri prefix = let dbd = LibraryDb.instance () in diff --git a/matita/matitac.ml b/matita/matitac.ml index 34e0639e3..fc1a95e16 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -27,6 +27,7 @@ module G = GrafiteAst module L = LexiconAst +module H = HExtlib (* from transcript *) @@ -58,24 +59,27 @@ let pp_ast_statement = (**) let dump f = + let floc = H.dummy_floc in + let nl_ast = G.Comment (floc, G.Note (floc, "")) in let och = open_out f in let atexit () = close_out och in + let nl () = output_string och (pp_ast_statement nl_ast) in let rt_base_dir = Filename.dirname Sys.argv.(0) in let path = Filename.concat rt_base_dir "matita.ma.templ" in let lines = 14 in out_preamble och (path, lines); - let lexicon_engine_cb = function - | L.Include _ as ast -> output_string och (LexiconAstPp.pp_command ast) - | _ -> () + let grafite_parser_cb fname = + let ast = G.Executable (floc, G.Command (floc, G.Include (floc, fname))) in + output_string och (pp_ast_statement ast); nl (); nl () in let matita_engine_cb = function | G.Executable (_, G.Macro (_, G.Inline _)) | G.Executable (_, G.Command (_, G.Include _)) -> () - | ast -> - output_string och (pp_ast_statement ast) + | ast -> + output_string och (pp_ast_statement ast); nl (); nl () in let matitac_lib_cb = output_string och in - LexiconEngine.set_callback lexicon_engine_cb; + GrafiteParser.set_callback grafite_parser_cb; MatitaEngine.set_callback matita_engine_cb; MatitacLib.set_callback matitac_lib_cb; at_exit atexit -- 2.39.2