we parametrized CicNotationPt.obj on 'term

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 47bfe2748693c07975996bd6f7662fb91ddc44d4..6d70c22c98ef09e80f5bb52e685fea06f4eef762 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/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/components/acic_content/cicNotationPp.mli b/components/acic_content/cicNotationPp.mli
index 2e60c74446cc207ed269304801686652906983bb..d883ddfc624e34a6702dbdf90c3cc392937d365d 100644 (file)
--- a/components/acic_content/cicNotationPp.mli
+++ b/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/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml
index f6652f63fd592f5d6393e4a4293bf762a807eed8..73eeb017dad00d781bbb61f9242b2eeb8f631186 100644 (file)
--- a/components/acic_content/cicNotationPt.ml
+++ b/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, <pattern,action> 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/components/acic_content/cicNotationUtil.mli b/components/acic_content/cicNotationUtil.mli
index 5d309d68fdf959bfa1efad2ee7abc2815eeaa5cf..2ead321f69f52badc233f21753c8e62bb15e668c 100644 (file)
--- a/components/acic_content/cicNotationUtil.mli
+++ b/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/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml
index dff9fcccde610ac830b8ff2e9b9b4e21537520bb..0d89a167e6c8293a9e279bf1e94f193c1c24b4f9 100644 (file)
--- a/components/binaries/transcript/grafite.ml
+++ b/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/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 9dc19c7c6a3b281056d4c0c9c640b41d58217a43..1d4a6a61ef9ecd8a1cbf8613035014c768fc568c 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/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/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 021fe1c9d676bb59a9a7cfcd6fbc93bcbaa0e35a..123fcf96928f82fd10f0f43cb3d26b3b30648450 100644 (file)
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/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/components/content_pres/cicNotationParser.mli b/components/content_pres/cicNotationParser.mli
index 53182dc3167d6d8ae8e119b444561d7137a0547a..134a42c3caf3236c20778c6ba62d64f79580610b 100644 (file)
--- a/components/content_pres/cicNotationParser.mli
+++ b/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/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index e09ca0b03a3ce124d467061d2db83b4fabd6f19d..8306ea286ed59d8442885814f924dd2a8cdc99b2 100644 (file)
--- a/components/content_pres/content2Procedural.ml
+++ b/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/components/content_pres/content2Procedural.mli b/components/content_pres/content2Procedural.mli
index 14cf247dd21710ebb89227b063506a6f461f23a4..06123000e21755132aaf2849a1213ee478496e60 100644 (file)
--- a/components/content_pres/content2Procedural.mli
+++ b/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/components/content_pres/objPp.ml b/components/content_pres/objPp.ml
index 49936861f2b2f8bbd12c0ea19ac1b9cab068e630..7f272c679aee07418216e1cc4a34d98cc122a37d 100644 (file)
--- a/components/content_pres/objPp.ml
+++ b/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/components/grafite_parser/grafiteDisambiguate.mli b/components/grafite_parser/grafiteDisambiguate.mli
index f78507042e18d174c6a66f357d018cd99a2fe2f0..7a2e2dda877280596bbefae2bd39cbaa673eda98 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.mli
+++ b/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/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index a78ca811332486a2fced5260c7651f6aee9ae116..14802a629e8cd32360a33c33d1550f506fc50b84 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/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/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli
index cb88940ffde19daea908157bc497b83acc0c4a3b..6d941d5db4286fce0156b700927592bdcfaf58a7 100644 (file)
--- a/components/grafite_parser/grafiteParser.mli
+++ b/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/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml
index 4272ccdc6002b4548be90ae81adbc0b67490d983..5a708ceddb8deb46c9a91602c6652d95a814c8e3 100644 (file)
--- a/components/tptp_grafite/tptp2grafite.ml
+++ b/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/matita/matita.lang b/matita/matita.lang
index f657ccbf166969fcc5e8816100574709e17fd0a6..02c7045ba0eac86922e58324157e6f0e96c0b510 100644 (file)
--- a/matita/matita.lang
+++ b/matita/matita.lang
@@ -173,6 +173,7 @@
 
   <keyword-list _name = "Matita Macro" style = "Others 3" case-sensitive="TRUE">
     <keyword>inline</keyword>
+    <keyword>procedural</keyword>
     <keyword>check</keyword>
     <keyword>hint</keyword>
     <keyword>set</keyword>

diff --git a/matita/matitaEngine.mli b/matita/matitaEngine.mli
index b20aa2bd503ddb0835d2880a6c9e8c9c5b5df363..a03d1e7dad2416f799ebc2f8fffee8fb949e57fd 100644 (file)
--- a/matita/matitaEngine.mli
+++ b/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/matita/matitacLib.ml b/matita/matitacLib.ml
index 82a7ca32ef1189ada1ff5cfb2e65629cecdf6b1b..cb3b2d1c8bf8184d71c80ae3c27e6ebd185dce20 100644 (file)
--- a/matita/matitacLib.ml
+++ b/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} *)