From d17a38ddca548c784e9efa7c55e87c80203b024d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 May 2009 17:17:29 +0000 Subject: [PATCH] - cicInspect: relevant nodes count updated: letin nodes are not relevant - Procedural: reflexivity is now supported - grafiteAst: boolean flag for include to tag inclusion of a source file. This command is relevant for .ma generation only. [ the source file of a .mma is not included in the generated .ma ] - cicNotationLexer: unexpanded TeX macro symbols are now encoded with an extra space at the end. This is consistent with the concept of TeX sequence and fixes a bug in the renering of these symbols. The space is needed for reparsing! --- .../components/acic_procedural/procedural2.ml | 26 +++++++++- .../acic_procedural/proceduralClassify.ml | 10 ++-- .../acic_procedural/proceduralClassify.mli | 2 +- .../acic_procedural/proceduralTeX.ml | 2 + .../acic_procedural/proceduralTypes.ml | 52 +++++++++++++++---- .../acic_procedural/proceduralTypes.mli | 4 ++ .../components/binaries/transcript/engine.ml | 18 +++---- .../binaries/transcript/gallina8Parser.mly | 6 +-- .../components/binaries/transcript/grafite.ml | 14 ++--- .../components/binaries/transcript/types.ml | 2 +- helm/software/components/cic/cicInspect.ml | 2 +- .../content_pres/cicNotationLexer.ml | 4 +- .../software/components/grafite/grafiteAst.ml | 4 +- .../components/grafite/grafiteAstPp.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 2 +- .../grafite_parser/dependenciesParser.ml | 2 + .../grafite_parser/grafiteParser.ml | 12 +++-- .../components/tptp_grafite/tptp2grafite.ml | 2 +- helm/software/matita/matitacLib.ml | 1 + 19 files changed, 121 insertions(+), 47 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index e3a2d62e7..d91b00084 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -167,6 +167,25 @@ let get_sub_names head l = 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" @@ -235,6 +254,8 @@ let get_intro = function | 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 @@ -365,7 +386,10 @@ and proc_appl st what hd tl = 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 diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 53c363a42..a607bf60d 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -37,12 +37,14 @@ type conclusion = (int * int * UM.uri * int) option (* 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 diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli index d4662764e..fed7d9db7 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.mli +++ b/helm/software/components/acic_procedural/proceduralClassify.mli @@ -33,4 +33,4 @@ val classify: Cic.context -> Cic.term -> dependences * conclusion 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 diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml index 279ebecb9..402ef54fe 100644 --- a/helm/software/components/acic_procedural/proceduralTeX.ml +++ b/helm/software/components/acic_procedural/proceduralTeX.ml @@ -194,6 +194,8 @@ let rec xl frm = function | 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 -> diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index ed198d99b..55516bf34 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -86,6 +86,7 @@ type step = Note of note | Clear of hyp list * note | ClearBody of hyp * note | Branch of step list list * note + | Reflexivity of note (* annterm constructors *****************************************************) @@ -225,6 +226,10 @@ let mk_clearbody id punctation = 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 @@ -258,10 +263,11 @@ let rec render_step sep a = function | 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 @@ -281,16 +287,21 @@ let rec count_step a = function | 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 @@ -302,6 +313,7 @@ let rec count_node a = function | Inductive _ | Statement _ | Qed _ + | Reflexivity _ | Id _ | Intros _ | Clear _ @@ -317,3 +329,25 @@ let rec count_node a = function | 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 diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index 13161daad..34c7ba670 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -65,6 +65,7 @@ type step = Note of note | 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 -> @@ -76,3 +77,6 @@ val count_steps: val count_nodes: int -> step list -> int + +val note_of_step: + step -> note diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 3184aad36..6776bb1f3 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -179,8 +179,8 @@ let set_heading st name = 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 -> "" @@ -238,9 +238,9 @@ let produce st = 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) -> @@ -258,7 +258,7 @@ let produce st = | 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 = @@ -279,21 +279,21 @@ let produce st = 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 | _ -> diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly index 632bd7e1d..b51a3d76e 100644 --- a/helm/software/components/binaries/transcript/gallina8Parser.mly +++ b/helm/software/components/binaries/transcript/gallina8Parser.mly @@ -332,11 +332,11 @@ | 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 diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 8e98b3757..0037e6145 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -75,8 +75,8 @@ let command_of_obj obj = 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)) @@ -108,13 +108,13 @@ let check och src = 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 diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index 28641d3d3..1fa7971b7 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -43,7 +43,7 @@ type item = Heading of (string * int) | 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) diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml index 2016ed98c..7186fb1f1 100644 --- a/helm/software/components/cic/cicInspect.ml +++ b/helm/software/components/cic/cicInspect.ml @@ -134,7 +134,7 @@ let count_nodes ~meta n t = | 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) -> diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 71ea77731..17a5bd5bb 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -210,7 +210,9 @@ let expand_macro lexbuf = 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) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index c61319233..dcfaf6c05 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -171,7 +171,7 @@ type ('term,'lazy_term) macro = (** 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 *) @@ -184,7 +184,7 @@ type ('term,'obj) command = | 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 70acd56d8..b74677949 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -341,7 +341,8 @@ let pp_command ~term_pp ~obj_pp = function "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) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index a3748f3cd..a0fdb92d7 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -707,7 +707,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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, diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index c6b8adaf4..53fb7ab6d 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -56,6 +56,8 @@ let parse_dependencies lexbuf = 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) >] -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b8afc2b8d..d0a97072c 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -726,9 +726,11 @@ EXTEND 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: [ [ @@ -885,17 +887,17 @@ EXTEND 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) diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 6b98fe515..dc58c831c 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -370,7 +370,7 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam 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 diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 489e37c86..c96fdf82d 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -77,6 +77,7 @@ let dump f = (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 -- 2.39.2