let get_type msg st t = H.get_type msg st.context (H.cic t)
+let get_uri_of_head = function
+ | C.AConst (_, u, _)
+ | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
+ | C.AMutInd (_, u, i, _)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
+ | C.AMutConstruct (_, u, i, j, _)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
+ | _ -> None
+
+let get_uri_of_apply = function
+ | T.Exact (t, _)
+ | T.Apply (t, _) -> get_uri_of_head t
+ | _ -> None
+
+let is_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "UNNAMED"
| C.Name s -> Some s
let mk_preamble st what script = match script with
+ | step :: script when is_reflexivity st step ->
+ convert st what @ T.Reflexivity (T.note_of_step step) :: script
| T.Exact _ :: _ -> script
| _ -> convert st what @ script
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" parsno (Cl.to_string h) *) in
+ let text = if !debug
+ then Printf.sprintf "%u %s" parsno (Cl.to_string synth (classes, rc))
+ else ""
+ in
let script = List.rev (mk_arg st hd) in
let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in
match rc with
(* debugging ****************************************************************)
-let string_of_entry (inverse, b) =
- if I.S.mem 0 inverse then begin if b then "CF" else "C" end else
+let string_of_entry synth (inverse, b) =
+ if I.overlaps synth inverse then begin if b then "CF" else "C" end else
if I.S.is_empty inverse then "I" else "P"
-let to_string (classes, rc) =
- let linearize = String.concat " " (List.map string_of_entry classes) in
+let to_string synth (classes, rc) =
+ let linearize =
+ String.concat " " (List.map (string_of_entry synth) classes)
+ in
match rc with
| None -> linearize
| Some (i, j, _, _) -> Printf.sprintf "%s %u %u" linearize i j
val adjust: Cic.context -> Cic.annterm list -> ?goal:Cic.term -> dependences -> dependences
-val to_string: dependences * conclusion -> string
+val to_string: CicInspect.S.t -> dependences * conclusion -> string
| T.Statement _ :: l
| T.Qed _ :: l ->
xl frm l
+ | T.Reflexivity _ :: l ->
+ F.fprintf frm "\\Reflexivity"; xl frm l
| T.Exact (t, _) :: l ->
F.fprintf frm "\\Exact{%a}" xat t; xl frm l
| T.Intros (_, [r], _) :: l ->
| Clear of hyp list * note
| ClearBody of hyp * note
| Branch of step list list * note
+ | Reflexivity of note
(* annterm constructors *****************************************************)
let tactic = G.ClearBody (floc, id) in
mk_tactic tactic punctation
+let mk_reflexivity punctation =
+ let tactic = G.Reflexivity floc in
+ mk_tactic tactic punctation
+
let mk_ob =
let punctation = G.Branch floc in
mk_punctation punctation
| 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) ->
+ | Branch (ps :: pss, s) ->
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
+ | Reflexivity s -> mk_reflexivity sep :: mk_tacnote s a
and render_steps sep a = function
| [] -> a
| Note _
| Statement _
| Inductive _
- | Qed _
-(* level 0 *)
- | Intros (Some 0, [], _)
+ | Qed _ -> a
+(* level A0 *)
+ | Branch (pps, _) -> List.fold_left count_steps a pps
+ | Clear _
+ | ClearBody _
| Id _
+ | Intros (Some 0, [], _)
+(* leval A1 *)
| Exact _
- | Change _
- | Clear _
- | ClearBody _ -> a
- | Branch (pps, _) -> List.fold_left count_steps a pps
-(* level 1 *)
+(* level B1 *)
+ | Cut _
+ | LetIn _
+(* level B2 *)
+ | Change _ -> a
+(* level C *)
| _ -> succ a
and count_steps a = List.fold_left count_step a
| Inductive _
| Statement _
| Qed _
+ | Reflexivity _
| Id _
| Intros _
| Clear _
| Branch (ss, _) -> List.fold_left count_nodes a ss
and count_nodes a = List.fold_left count_node a
+
+(* helpers ******************************************************************)
+
+let rec note_of_step = function
+ | Note s
+ | Statement (_, _, _, _, s)
+ | Inductive (_, _, s)
+ | Qed s
+ | Exact (_, s)
+ | Id s
+ | Intros (_, _, s)
+ | Cut (_, _, s)
+ | LetIn (_, _, s)
+ | Rewrite (_, _, _, _, s)
+ | Elim (_, _, _, s)
+ | Cases (_, _, s)
+ | Apply (_, s)
+ | Change (_, _, _, _, s)
+ | Clear (_, s)
+ | ClearBody (_, s)
+ | Reflexivity s
+ | Branch (_, s) -> s
| Clear of hyp list * note
| ClearBody of hyp * note
| Branch of step list list * note
+ | Reflexivity of note
val render_steps:
(what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, hyp) GrafiteAst.statement list ->
val count_nodes:
int -> step list -> int
+
+val note_of_step:
+ step -> note
let heading = st.heading_path, st.heading_lines in
set_items st name [T.Heading heading]
-let require st name inc =
- set_items st name [T.Include inc]
+let require st name src inc =
+ set_items st name [T.Include (src, inc)]
let get_coercion st str =
try List.assoc str st.coercions with Not_found -> ""
let full_s = Filename.concat in_base_uri s in
let params = params @ get_iparams st (Filename.concat name obj) in
path, Some (T.Inline (b, k, full_s, p, f, params))
- | T.Include s ->
+ | T.Include (src, s) ->
begin
- try path, Some (T.Include (List.assoc s st.requires))
+ try path, Some (T.Include (src, List.assoc s st.requires))
with Not_found -> path, None
end
| T.Coercion (b, obj) ->
| item -> path, Some item
in
let set_includes st name =
- try require st name (List.assoc name st.includes)
+ try require st name false (List.assoc name st.includes)
with Not_found -> ()
in
let rec remove_lines ich n =
set_items st st.input_package (comment :: global_items);
init name;
begin match st.input_type with
- | T.Grafite "" -> require st name file
- | _ -> require st name st.input_package
+ | T.Grafite "" -> require st name true file
+ | _ -> require st name true st.input_package
end;
set_includes st name; set_items st name local_items; commit st name
with e ->
prerr_endline (Printexc.to_string e); close_in ich
in
is_ma st st.input_package;
- init st.input_package; require st st.input_package "preamble";
+ init st.input_package; require st st.input_package false "preamble";
match st.input_type with
| T.Grafite "" ->
List.iter (produce st) st.files
| T.Grafite s ->
let theory = Filename.concat st.input_path s in
- require st st.input_package theory;
+ require st st.input_package true theory;
List.iter (produce st) st.files;
commit st st.input_package
| _ ->
| unx xskips FS
{ out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
| req xp ident FS
- { out "REQ" $3; [T.Include (trim $3)] }
+ { out "REQ" $3; [T.Include (false, trim $3)] }
| req ident FS
- { out "REQ" $2; [T.Include (trim $2)] }
+ { out "REQ" $2; [T.Include (false, trim $2)] }
| load str FS
- { out "REQ" $2; [T.Include (strip2 (trim $2))] }
+ { out "REQ" $2; [T.Include (false, strip2 (trim $2))] }
| coerc qid spcs skips FS
{ out "COERCE" (hd $2); coercion (hd $2) }
| id coerc qid spcs skips FS
let command_of_macro macro =
G.Executable (floc, G.Macro (floc, macro))
-let require value =
- command_of_obj (G.Include (floc, value ^ ".ma"))
+let require src value =
+ command_of_obj (G.Include (floc, src, value ^ ".ma"))
let coercion value =
command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
let commit kind och items =
let trd (_, _, x) = x in
let commit = function
- | T.Heading heading -> out_preamble och heading
- | T.Line line ->
+ | T.Heading heading -> out_preamble och heading
+ | T.Line line ->
if !O.comments then out_line_comment och line
- | T.Include script -> out_command och (require script)
- | T.Coercion specs ->
+ | T.Include (src, script) -> out_command och (require src script)
+ | T.Coercion specs ->
if !O.comments then out_unexported och "COERCION" (snd specs)
- | T.Notation specs ->
+ | T.Notation specs ->
if !O.comments then out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _, _, _) ->
if !O.comments then out_unexported och "UNEXPORTED" src
| Line of string
| Comment of string
| Unexport of string
- | Include of string
+ | Include of (bool * string)
| Coercion of (local * string)
| Notation of (local * string)
| Section of (local * string * string)
| C.Cast (t1, t2) -> aux (aux (offset + n) t2) t1
| C.Lambda (_, t1, t2)
| C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
- | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + 1 + n) t2) ty) t1
+ | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + n) t2) ty) t1
| C.MutCase (_, _, t1, t2, ss) ->
aux (aux (List.fold_left aux (offset + 1 + n) ss) t2) t1
| C.Fix (_, ss) ->
in
try
("SYMBOL", Utf8Macro.expand macro)
- with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf
+ with Utf8Macro.Macro_not_found _ ->
+(* FG: unexpanded TeX macros are terminated by a space for rendering *)
+ "SYMBOL", (Ulexing.utf8_lexeme lexbuf ^ " ")
let remove_quotes s = String.sub s 1 (String.length s - 2)
let remove_left_quote s = String.sub s 1 (String.length s - 1)
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 20
+let magic = 21
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
| UnificationHint of loc * 'term * int (* term, precedence *)
| Default of loc * string * UriManager.uri list
| Drop of loc
- | Include of loc * string
+ | Include of loc * bool (* source? *) * string
| Obj of loc * 'obj
| Relation of
loc * string * 'term * 'term * 'term option * 'term option * 'term option
"unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,path) -> "include \"" ^ path ^ "\""
+ | Include (_,true,path) -> "include source \"" ^ path ^ "\""
| Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
| Relation (_,id,a,aeq,refl,sym,trans) ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,`Old []
| GrafiteAst.Drop loc -> raise Drop
- | GrafiteAst.Include (loc, baseuri) ->
+ | GrafiteAst.Include (loc, _, baseuri) ->
let moopath_rw, moopath_r =
LibraryMisc.obj_file_of_baseuri
~must_exist:false ~baseuri ~writable:true,
true, (UriDep (UriManager.uri_of_string u) :: acc)
| [< '("IDENT", "include"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
+ | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] ->
+ true, (IncludeDep fname :: acc)
| [< '("IDENT", "include'"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
| [< '("IDENT", "inline"); '("QSTRING", fname) >] ->
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,L.WithPreferences
+ loc,path,false,L.WithPreferences
+ | IDENT "include" ; IDENT "source" ; path = QSTRING ->
+ loc,path,true,L.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,L.WithoutPreferences
+ loc,path,false,L.WithoutPreferences
]];
grafite_command: [ [
let stm = G.Comment (loc, com) in
!grafite_callback status stm;
status, LSome stm
- | (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ | (iloc,fname,source,mode) = include_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, source, fname)))
in
!grafite_callback status stm;
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
in
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, source, buri)))
in
let status =
if never_include then raise (NoInclusionPerformed fullpath)
match raw_preamble with
| None ->
pp (GA.Executable(floc,
- GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
+ GA.Command(floc,GA.Include(floc,false,"logic/equality.ma"))))
| Some s -> s buri
in
let extra_statements_end = [] in
(Helm_registry.get_bool "matita.paste_unicode_as_tex")
in
output_string och str
+ | G.Executable (loc, G.Command (_, G.Include (_, true, _))) -> ()
| stm ->
output_string och (pp_statement stm); nl (); nl ()
in
projects / helm.git / commitdiff