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
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"
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)
| 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
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) ->
[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)]
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
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 *******************************************************)
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
(* 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)
(****************************************************************************)
(* 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)))
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
| 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 *****************************************************************)
(* 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
(* $Id$ *)
-open Printf
-
open GrafiteAst
let tactical_terminator = ""
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, [] -> ""
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
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"
| 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)
(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)
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 *)
| 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 -> ""
| 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
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
| 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"
| 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
(* $Id$ *)
-open Printf
+let out = ref ignore
+let set_callback f = out := f
module Ast = CicNotationPt
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 ->
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))
] ->
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
val statement: statement Grammar.Entry.e
+(* this callback is called on every include command *)
+val set_callback: (string -> unit) -> unit
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
module G = GrafiteAst
module L = LexiconAst
+module H = HExtlib
(* from transcript *)
(**)
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
projects / helm.git / commitdiff