From: Enrico Tassi Date: Tue, 17 May 2005 15:24:11 +0000 (+0000) Subject: fixed Whelp stuff X-Git-Tag: single_binding~48 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git fixed Whelp stuff --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 9b0617bc8..5e70ff571 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -485,9 +485,15 @@ EXTEND TacticAst.Check (loc, t) | [ IDENT "hint" ] -> TacticAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> - TacticAst.Match (loc,t) + TacticAst.WMatch (loc,t) | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> - TacticAst.Instance (loc,t) + TacticAst.WInstance (loc,t) + | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> + TacticAst.WLocate (loc,id) + | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> + TacticAst.WElim (loc, t) + | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> + TacticAst.WHint (loc,t) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) ]]; diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index ef79ab4ad..fdffe8276 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -261,7 +261,7 @@ and proof2pres term2pres p = [B.H([Some "helm", "xref", "ce_"^hd_xref], [ce2pres hd]); continuation']) - + and ce2pres = let module Con = Content in function @@ -304,8 +304,10 @@ and proof2pres term2pres p = term]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> - B.Text ([],"jointdef") + | `Joint ho -> assert false (* + B.H ([], + (B.Text ([],"JOINT ") + :: List.map ce2pres ho.Content.joint_defs)) *) and acontext2pres ac continuation indent = let module Con = Content in @@ -380,7 +382,11 @@ and proof2pres term2pres p = let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t - | _ -> assert false) in + | [Con.Premise p] -> + (match p.Con.premise_binder with + | None -> assert false; (* unnamed hypothesis ??? *) + | Some s -> B.Text([],s)) + | err -> assert false) in (match conclude.Con.conclude_conclusion with None -> B.b_h [] [B.b_kw "Consider"; B.b_space; arg] diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 692d4679e..ae9143dab 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -92,12 +92,17 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] type 'term macro = + (* Whelp's stuff *) + | WHint of loc * 'term + | WMatch of loc * 'term + | WInstance of loc * 'term + | WLocate of loc * string + | WElim of loc * 'term + (* real macros *) | Abort of loc | Print of loc * string | Check of loc * 'term | Hint of loc - | Match of loc * 'term - | Instance of loc * 'term | Quit of loc | Redo of loc * int option | Undo of loc * int option diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 9fb8455f9..f10443c2d 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -112,6 +112,13 @@ let pp_search_kind = function | `Elim -> "elim" let pp_macro pp_term = function + (* Whelp *) + | WInstance (_, term) -> "whelp instance " ^ pp_term term + | WHint (_, t) -> "whelp hint " ^ pp_term t + | WLocate (_, s) -> "whelp locate " ^ s + | WElim (_, t) -> "whelp elim " ^ pp_term t + | WMatch (_, term) -> "whelp match " ^ pp_term term + (* real macros *) | Abort _ -> "Abort" | Check (_, term) -> sprintf "Check %s" (pp_term term) | Hint _ -> "hint" @@ -125,8 +132,6 @@ let pp_macro pp_term = function | Undo (_, Some n) -> sprintf "Undo %d" n | Print (_, name) -> sprintf "Print \"%s\"" name | Quit _ -> "Quit" - | Instance _ - | Match _ -> assert false let pp_macro_ast = pp_macro pp_term_ast let pp_macro_cic = pp_macro pp_term_cic