From: Andrea Asperti Date: Fri, 29 Oct 2010 11:27:11 +0000 (+0000) Subject: - grammar of // changed to move the justification inside; X-Git-Tag: make_still_working~2757 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ce27112fe93ced5f67cc6af8fc63037eba3f322;p=helm.git - grammar of // changed to move the justification inside; reason: that brain damaged piece of software that is CAMLP5 does a lookahead and then it forgets to rollback the token (why??? is it a bug). As a consequence matita used to work (since it parses a statement at a time), but not matitac (since the lookahead destroyed the next command) - core_notation.moo: \frac used to be at level 90, but this is incorrect during parsing and incompatible with the new syntax; \frac is now used only in output - minor dead code removal here and there --- diff --git a/matita/components/content_pres/cicNotationLexer.ml b/matita/components/content_pres/cicNotationLexer.ml index 21031d002..e0225d72e 100644 --- a/matita/components/content_pres/cicNotationLexer.ml +++ b/matita/components/content_pres/cicNotationLexer.ml @@ -52,8 +52,6 @@ let regexp we_proved = "we" utf8_blank+ "proved" let regexp we_have = "we" utf8_blank+ "have" let regexp let_rec = "let" utf8_blank+ "rec" let regexp let_corec = "let" utf8_blank+ "corec" -let regexp nlet_rec = "nlet" utf8_blank+ "rec" -let regexp nlet_corec = "nlet" utf8_blank+ "corec" let regexp ident_decoration = '\'' | '?' | '`' let regexp ident_cont = ident_letter | xml_digit | '_' let regexp ident_start = ident_letter @@ -307,8 +305,6 @@ and level2_ast_token = lexer | let_rec -> return lexbuf ("LETREC","") | let_corec -> return lexbuf ("LETCOREC","") - | nlet_rec -> return lexbuf ("NLETREC","") - | nlet_corec -> return lexbuf ("NLETCOREC","") | we_proved -> return lexbuf ("WEPROVED","") | we_have -> return lexbuf ("WEHAVE","") | utf8_blank+ -> ligatures_token level2_ast_token lexbuf diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 43d03b9af..d38344824 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -63,22 +63,23 @@ let rec pp_ntactic ~map_unicode_to_tex = (String.concat "," (List.map NotationPp.pp_term l)) ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term what ^ - assert false ^ " " ^ assert false + "...to be implemented..." ^ " " ^ "...to be implemented..." | NConstructor (_,None,l) -> "@ " ^ String.concat " " (List.map NotationPp.pp_term l) | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ String.concat " " (List.map NotationPp.pp_term l) | NCase1 (_,n) -> "*" ^ n ^ ":" - | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ + | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^ " with " ^ NotationPp.pp_term wwhat | NCut (_,t) -> "ncut " ^ NotationPp.pp_term t (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *) | NDestruct (_,dom,skip) -> "ndestruct ..." | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^ - assert false ^ " " ^ assert false + "...to be implemented..." ^ " " ^ "...to be implemented..." | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n + | NIntros (_,l) -> "#" ^ String.concat " " l | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^ assert false ^ " " ^ assert false | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t @@ -86,19 +87,19 @@ let rec pp_ntactic ~map_unicode_to_tex = (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^ " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED" - | NDot _ -> "##." - | NSemicolon _ -> "##;" - | NBranch _ -> "##[" - | NShift _ -> "##|" - | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":" - | NPosbyname (_, s) -> "##" ^ s ^ ":" - | NWildcard _ -> "##*:" - | NMerge _ -> "##]" + | NDot _ -> "." + | NSemicolon _ -> ";" + | NBranch _ -> "[" + | NShift _ -> "|" + | NPos (_, l) -> String.concat "," (List.map string_of_int l)^ ":" + | NPosbyname (_, s) -> s ^ ":" + | NWildcard _ -> "*:" + | NMerge _ -> "]" | NFocus (_,l) -> - Printf.sprintf "##focus %s" + Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int l)) - | NUnfocus _ -> "##unfocus" - | NSkip _ -> "##skip" + | NUnfocus _ -> "unfocus" + | NSkip _ -> "skip" | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac | NAssumption _ -> "nassumption" | NBlock (_,l) -> diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 22a8dd224..3a9e87eea 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -340,7 +340,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = | _ -> obj_kind in let obj = uri,height,[],[],obj_kind in - prerr_endline ("pp new obj \n"^NCicPp.ppobj obj); let old_status = status in let status = NCicLibrary.add_obj status obj in let index_obj = @@ -390,6 +389,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = if nstatus#ng_mode <> `CommandMode then begin (*HLog.warn "error in generating projection/eliminator";*) + assert(status#ng_mode = `CommandMode); status, uris end else diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index f0da64a51..0679c8895 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -218,28 +218,25 @@ EXTEND SYMBOL <:unicode>; concl = tactic_term -> (List.rev hyps,concl) ] -> G.NTactic(loc,[G.NAssert (loc, seqs)]) - | IDENT "auto"; params = auto_params -> - G.NTactic(loc,[G.NAuto (loc, params)]) + (*| IDENT "auto"; params = auto_params -> + G.NTactic(loc,[G.NAuto (loc, params)])*) | SYMBOL "/"; num = OPT NUMBER ; - params = nauto_params; SYMBOL "/" ; - just = OPT [ IDENT "by"; by = - [ univ = tactic_term_list1 -> `Univ univ - | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv - | SYMBOL "_" -> `Trace ] -> by ] -> + just_and_params = auto_params; SYMBOL "/" -> + let just,params = just_and_params in let depth = match num with Some n -> n | None -> "1" in (match just with | None -> - G.NTactic(loc, - [G.NAuto(loc,(None,["slir","";"depth",depth]@params))]) + G.NTactic(loc, + [G.NAuto(loc,(None,["depth",depth]@params))]) | Some (`Univ univ) -> - G.NTactic(loc, - [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))]) + G.NTactic(loc, + [G.NAuto(loc,(Some univ,["depth",depth]@params))]) | Some `EmptyUniv -> - G.NTactic(loc, - [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))]) + G.NTactic(loc, + [G.NAuto(loc,(Some [],["depth",depth]@params))]) | Some `Trace -> - G.NMacro(loc, - G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params)))) + G.NMacro(loc, + G.NAutoInteractive (loc, (None,["depth",depth]@params)))) | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc) | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t)) | IDENT "screenshot"; fname = QSTRING -> @@ -310,18 +307,10 @@ EXTEND i = auto_fixed_param -> i,"" | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ]; - tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl, - (* (match tl with Some l -> l | None -> []), *) - params - ] -]; - nauto_params: [ - [ params = - LIST0 [ - i = auto_fixed_param -> i,"" - | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> - string_of_int v | v = IDENT -> v ] -> i,v ] -> - params + just = OPT [ IDENT "by"; by = + [ univ = tactic_term_list1 -> `Univ univ + | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv + | SYMBOL "_" -> `Trace ] -> by ] -> just,params ] ]; diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 5080e34bf..95a9e713d 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -1740,7 +1740,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = oldstatus#set_status s in let s = up_to depth depth in - print (print_stat statistics); + debug_print (print_stat statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy diff --git a/matita/matita/core_notation.moo b/matita/matita/core_notation.moo index 6f5d78d03..8ba56a73d 100644 --- a/matita/matita/core_notation.moo +++ b/matita/matita/core_notation.moo @@ -163,7 +163,7 @@ notation "hvbox(a break \mod b)" left associative with precedence 55 for @{ 'module $a $b }. -notation "a \frac b" +notation < "a \frac b" non associative with precedence 90 for @{ 'divide $a $b }.