From: Ferruccio Guidi Date: Tue, 12 Dec 2006 14:04:59 +0000 (+0000) Subject: we parametrized CicNotationPt.obj on 'term X-Git-Tag: make_still_working~6596 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git we parametrized CicNotationPt.obj on 'term --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 47bfe2748..6d70c22c9 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -79,6 +79,11 @@ let pp_attribute = | `Loc _ -> "@" | `ChildPos p -> sprintf "P(%s)" (pp_pos p) +let pp_capture_variable pp_term = + function + | term, None -> pp_term (* ~pp_parens:false *) term + | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")" + let rec pp_term ?(pp_parens = true) t = let t_pp = match t with @@ -94,7 +99,7 @@ let rec pp_term ?(pp_parens = true) t = (match typ with None -> "?" | Some typ -> pp_term typ) (pp_term ~pp_parens:true body) | Ast.Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var) (pp_term ~pp_parens:true body) | Ast.Case (term, indtype, typ, patterns) -> sprintf "match %s%s%s with %s" @@ -111,7 +116,7 @@ let rec pp_term ?(pp_parens = true) t = (pp_patterns patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) | Ast.LetIn (var, t1, t2) -> - sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1) + sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) | Ast.LetRec (kind, definitions, term) -> let rec get_guard i = function @@ -127,7 +132,7 @@ let rec pp_term ?(pp_parens = true) t = in sprintf "%s %s on %s: %s \\def %s" (pp_term ~pp_parens:false term) - (String.concat " " (List.map pp_capture_variable params)) + (String.concat " " (List.map (pp_capture_variable pp_term) params)) (pp_term ~pp_parens:false (get_guard i params)) (pp_term typ) (pp_term body) in @@ -183,17 +188,12 @@ and pp_pattern ((head, href, vars), term) = | [] -> head_pp | _ -> sprintf "(%s %s)" head_pp - (String.concat " " (List.map pp_capture_variable vars))) + (String.concat " " (List.map (pp_capture_variable pp_term) vars))) (pp_term term) and pp_patterns patterns = sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) -and pp_capture_variable = - function - | term, None -> pp_term ~pp_parens:false term - | term, Some typ -> "(" ^ pp_term ~pp_parens:false term ^ ": " ^ pp_term typ ^ ")" - and pp_box_spec (kind, spacing, indent) = let int_of_bool b = if b then 1 else 0 in let kind_string = @@ -257,9 +257,9 @@ let _pp_term = ref (pp_term ~pp_parens:false) let pp_term t = !_pp_term t let set_pp_term f = _pp_term := f -let pp_params = function +let pp_params pp_term = function | [] -> "" - | params -> " " ^ String.concat " " (List.map pp_capture_variable params) + | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) let pp_flavour = function | `Definition -> "definition" @@ -271,7 +271,7 @@ let pp_flavour = function | `Variant -> "variant" | `Axiom -> "axiom" -let pp_fields fields = +let pp_fields pp_term fields = (if fields <> [] then "\n" else "") ^ String.concat ";\n" (List.map @@ -281,7 +281,7 @@ let pp_fields fields = if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^ pp_term ty) fields) -let pp_obj = function +let pp_obj pp_term = function | Ast.Inductive (params, types) -> let pp_constructors constructors = String.concat "\n" @@ -297,7 +297,7 @@ let pp_obj = function | (name, inductive, typ, constructors) :: tl -> let fst_typ_pp = sprintf "%sinductive %s%s: %s \\def\n%s" - (if inductive then "" else "co") name (pp_params params) + (if inductive then "" else "co") name (pp_params pp_term params) (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) @@ -310,8 +310,8 @@ let pp_obj = function | None -> "" | Some body -> "\\def\n " ^ pp_term body) | Ast.Record (params,name,ty,fields) -> - "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ - " \\def {" ^ pp_fields fields ^ "\n}" + "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ + " \\def {" ^ pp_fields pp_term fields ^ "\n}" let rec pp_value = function | Env.TermValue t -> sprintf "$%s$" (pp_term t) diff --git a/helm/software/components/acic_content/cicNotationPp.mli b/helm/software/components/acic_content/cicNotationPp.mli index 2e60c7444..d883ddfc6 100644 --- a/helm/software/components/acic_content/cicNotationPp.mli +++ b/helm/software/components/acic_content/cicNotationPp.mli @@ -39,7 +39,7 @@ *) val pp_term: CicNotationPt.term -> string -val pp_obj: CicNotationPt.obj -> string +val pp_obj: ('term -> string) -> 'term CicNotationPt.obj -> string val pp_env: CicNotationEnv.t -> string val pp_value: CicNotationEnv.value -> string diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index f6652f63f..73eeb017d 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -59,9 +59,11 @@ type literal = type case_indtype = string * href option +type 'term capture_variable = 'term * 'term option + (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 1 +let magic = 2 type term = (* CIC AST *) @@ -69,13 +71,13 @@ type term = | AttributedTerm of term_attribute * term | Appl of term list - | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Binder of binder_kind * term capture_variable * term (* kind, name, body *) | Case of term * case_indtype option * term option * (case_pattern * term) list (* what to match, inductive type, out type, list *) | Cast of term * term - | LetIn of capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (capture_variable list * capture_variable * term * int) list * term + | LetIn of term capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term (* (params, name, body, decreasing arg) list, where *) | Ident of string * subst list option (* literal, substitutions. @@ -100,11 +102,10 @@ type term = | Variable of pattern_variable (* name, type. First component must be Ident or Variable (FreshVar _) *) -and capture_variable = term * term option and meta_subst = term option and subst = string * term -and case_pattern = string * href option * capture_variable list +and case_pattern = string * href option * term capture_variable list and box_kind = H | V | HV | HOV and box_spec = box_kind * bool * bool (* kind, spacing, indent *) @@ -163,10 +164,10 @@ type cic_appl_pattern = * true means inductive, false coinductive *) type 'term inductive_type = string * bool * 'term * (string * 'term) list -type obj = - | Inductive of capture_variable list * term inductive_type list +type 'term obj = + | Inductive of 'term capture_variable list * 'term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of Cic.object_flavour * string * term * term option + | Theorem of Cic.object_flavour * string * 'term * 'term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage @@ -174,7 +175,7 @@ type obj = * will be given in proof editing mode using the tactical language, * unless the flavour is an Axiom *) - | Record of capture_variable list * string * term * (string * term * bool * int) list + | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list (** left parameters, name, type, fields *) (** {2 Standard precedences} *) diff --git a/helm/software/components/acic_content/cicNotationUtil.mli b/helm/software/components/acic_content/cicNotationUtil.mli index 5d309d68f..2ead321f6 100644 --- a/helm/software/components/acic_content/cicNotationUtil.mli +++ b/helm/software/components/acic_content/cicNotationUtil.mli @@ -81,7 +81,7 @@ val name_of_cic_name: Cic.name -> CicNotationPt.term (** Symbol/Numbers instances *) val freshen_term: CicNotationPt.term -> CicNotationPt.term -val freshen_obj: CicNotationPt.obj -> CicNotationPt.obj +val freshen_obj: CicNotationPt.term CicNotationPt.obj -> CicNotationPt.term CicNotationPt.obj (** Notation id handling *) diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index dff9fcccd..0d89a167e 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -62,7 +62,7 @@ let out_preamble och (path, lines) = let out_command och cmd = let term_pp = NP.pp_term in let lazy_term_pp = NP.pp_term in - let obj_pp = NP.pp_obj in + let obj_pp = NP.pp_obj NP.pp_term in let s = GP.pp_statement ~term_pp ~lazy_term_pp ~obj_pp cmd in Printf.fprintf och "%s\n\n" s diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 9dc19c7c6..1d4a6a61e 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -838,7 +838,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj disambiguator_input -> + CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -1204,7 +1204,7 @@ in refine_profiler.HExtlib.profile foo () if fresh_instances then CicNotationUtil.freshen_obj obj else obj in disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri - ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj (text,prefix_len,obj) end diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index 021fe1c9d..123fcf969 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -73,7 +73,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj disambiguator_input -> + CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index 53182dc31..134a42c3c 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -56,7 +56,7 @@ val level2_ast_grammar: Grammar.g val term : CicNotationPt.term Grammar.Entry.e val let_defs : - (CicNotationPt.capture_variable list * CicNotationPt.capture_variable * CicNotationPt.term * int) list + (CicNotationPt.term CicNotationPt.capture_variable list * CicNotationPt.term CicNotationPt.capture_variable * CicNotationPt.term * int) list Grammar.Entry.e val protected_binder_vars : diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml index e09ca0b03..8306ea286 100644 --- a/helm/software/components/content_pres/content2Procedural.ml +++ b/helm/software/components/content_pres/content2Procedural.ml @@ -23,4 +23,40 @@ * http://cs.unibo.it/helm/. *) -let content2procedural ~ids_to_inner_sorts prefix annterm = [] +module H = HExtlib +module C = Content +module G = GrafiteAst + +(* grafite ast constructors *************************************************) + +let floc = H.dummy_floc + +let mk_note str = G.Comment (floc, G.Note (floc, str)) + +(* interface functions ******************************************************) + +let out_arg = function + | C.Aux _ -> "aux" + | C.Premise _ -> "premise" + | C.Lemma _ -> "lemma" + | C.Term _ -> "term" + | C.ArgProof _ -> "proof" + | C.ArgMethod _ -> "method" + +let out_args args = String.concat " " (List.map out_arg args) + +let out_name = function + | None -> "" + | Some str -> str + +let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = + if List.length params > 0 || xmenv <> None then assert false; + match obj with + | `Def (C.Const, t, `Proof { + C.proof_name = Some name; C.proof_context = []; + C.proof_apply_context = []; C.proof_conclude = { + C.conclude_conclusion = Some b + } + }) -> + [mk_note (Printf.sprintf "%s" name)] + | _ -> assert false diff --git a/helm/software/components/content_pres/content2Procedural.mli b/helm/software/components/content_pres/content2Procedural.mli index 14cf247dd..06123000e 100644 --- a/helm/software/components/content_pres/content2Procedural.mli +++ b/helm/software/components/content_pres/content2Procedural.mli @@ -27,6 +27,6 @@ val content2procedural: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> string -> Cic.annterm Content.cobj -> (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement list diff --git a/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml index 49936861f..7f272c679 100644 --- a/helm/software/components/content_pres/objPp.ml +++ b/helm/software/components/content_pres/objPp.ml @@ -33,7 +33,7 @@ let obj_to_string n style prefix obj = | GrafiteAst.Procedural -> let term_pp = CicNotationPp.pp_term in let lazy_term_pp = CicNotationPp.pp_term in - let obj_pp = CicNotationPp.pp_obj in + let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in let script = Content2Procedural.content2procedural ~ids_to_inner_sorts prefix cobj in - String.concat "" (List.map aux script) + "\n\n" ^ String.concat "" (List.map aux script) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index f78507042..7a2e2dda8 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -45,7 +45,7 @@ val disambiguate_command: LexiconEngine.status -> baseuri:string option -> Cic.metasenv -> - ((CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> + ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_macro: diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index a78ca8113..14802a629 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -35,7 +35,8 @@ type 'a localized_option = type ast_statement = (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement type statement = diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli index cb88940ff..6d941d5db 100644 --- a/helm/software/components/grafite_parser/grafiteParser.mli +++ b/helm/software/components/grafite_parser/grafiteParser.mli @@ -29,7 +29,8 @@ type 'a localized_option = type ast_statement = (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement type statement = diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 4272ccdc6..5a708cedd 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -285,7 +285,7 @@ let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () = in CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in - let obj_pp = CicNotationPp.pp_obj in + let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t in let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index f657ccbf1..02c7045ba 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -173,6 +173,7 @@ inline + procedural check hint set diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index b20aa2bd5..a03d1e7da 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -30,7 +30,7 @@ val eval_ast : GrafiteTypes.status -> string * int * ((CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement) -> ((GrafiteTypes.status * LexiconEngine.status) * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option @@ -54,7 +54,7 @@ val eval_from_stream : Ulexing.lexbuf -> (GrafiteTypes.status -> (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement -> unit) -> ((GrafiteTypes.status * LexiconEngine.status) * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 82a7ca32e..cb3b2d1c8 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -33,7 +33,7 @@ exception AttemptToInsertAnAlias let pp_ast_statement = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj + ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) (** {2 Initialization} *)