]> matita.cs.unibo.it Git - helm.git/commitdiff
procedural: bug fixes
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 26 Apr 2007 19:06:42 +0000 (19:06 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 26 Apr 2007 19:06:42 +0000 (19:06 +0000)
matita: some \n rearranged
GrafiteAstPp: some \n rearranged
GrafiteParser: added callback

helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralOptimizer.ml
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/grafite_parser/grafiteParser.mli
helm/software/matita/applyTransformation.ml
helm/software/matita/matitac.ml

index bff721a3e7b5a247e9bca1e0f442b9202ee31a53..c9423268ccb9d144cb1c536ee5cd258307d780b4 100644 (file)
@@ -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 *******************************************************)
 
index 67b3af94091650d924b0269fe2af8d1f04c077c7..9d95d100ba83c375d1ba9f35d17d8ca73268b90c 100644 (file)
@@ -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
index 8dac90f26bde2c20a7d9e0a5ebee5adcc986960e..c30251f4838b20c1409e2df321255ee4e3842bbe 100644 (file)
@@ -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 *****************************************************************)
 
index 97ca7fdbb98bd21518673169db3d2d97fcd4f2f0..9659a94ecca3ab9ae514d50244bfdf3708cdd495 100644 (file)
 
 (* 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
index 710761ed9a44537881a73c825f2618eb59ee7900..3602e9df526ad60c25e27500baca1ba1bb9c6cab 100644 (file)
@@ -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
index 7b515472d2ef386385855a7d78abbf6543513618..63df8ab7f37d1b6a208e89bd16b599ec67da2512 100644 (file)
@@ -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
index 6d941d5db4286fce0156b700927592bdcfaf58a7..f8754df0c4715f14c098e9072310e7d53be25a86 100644 (file)
@@ -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 
index b5aa06f9d1d87ffd0e74b3a5023884af3be90b1c..4883deaf8665ba06816412cc121d04e5fdd7b323 100644 (file)
@@ -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   
index 34e0639e3aa62ebfd422fb7a02c7a5ac7e5d1d6b..fc1a95e1606aba56cb321cc95a6b6d3289a63cb1 100644 (file)
@@ -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