]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
Introduction of vectors of implicit (only for NG).
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index 29898eb13ace83196d7340d8f10ff653dc170cc6..1e759930ac4ef706175c85c181244657e3dd5558 100644 (file)
@@ -34,7 +34,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = true
+let debug_printing = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -117,14 +117,14 @@ let rec pp_term ?(pp_parens = true) t =
           (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
        let rec get_guard i = function
-          | []                   -> (*assert false*) Ast.Implicit
+          | []                   -> (*assert false*) Ast.Implicit `JustOne
           | [term, _] when i = 1 -> term
           | _ :: tl              -> get_guard (pred i) tl
        in
        let map (params, (id,typ), body, i) =
          let typ =
           match typ with
-             None -> Ast.Implicit
+             None -> Ast.Implicit `JustOne
            | Some typ -> typ
          in
           sprintf "%s %s on %s: %s \\def %s" 
@@ -138,21 +138,24 @@ let rec pp_term ?(pp_parens = true) t =
           (String.concat " and " (List.map map definitions))
           (pp_term term)
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
-    | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
-        name
+    | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+    | Ast.NRef nref -> NReference.string_of_reference nref
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
-    | Ast.Implicit -> "?"
+    | Ast.Implicit `Vector -> "?"
+    | Ast.Implicit `JustOne -> "..."
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
-            (List.map (function None -> "_" | Some t -> pp_term t) substs))
+            (List.map (function None -> "?" | Some t -> pp_term t) substs))
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
+    | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
+    | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""
@@ -164,7 +167,7 @@ let rec pp_term ?(pp_parens = true) t =
   in
   match pp_parens, t with
     | false, _ 
-    | true, Ast.Implicit
+    | true, Ast.Implicit _
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp
@@ -211,7 +214,10 @@ and pp_layout = function
   | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
   | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
   | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
-  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3)
+  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1)
+  (pp_term t2) (pp_term t3)
+  | Ast.Maction l -> sprintf "\\MACTION (%s)" 
+     (String.concat "," (List.map pp_term l))
   | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Ast.Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
@@ -226,6 +232,10 @@ and pp_layout = function
       sprintf "\\MSTYLE %s [%s]" 
         (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
         (String.concat " " (List.map pp_term terms))
+  | Ast.Mpadded (l,terms) -> 
+      sprintf "\\MSTYLE %s [%s]" 
+        (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
+        (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | Ast.List0 (t, sep_opt) ->
@@ -285,10 +295,12 @@ let pp_fields pp_term fields =
     (List.map 
       (fun (name,ty,coercion,arity) -> 
         " " ^ name ^ 
-        if coercion then (":" ^ 
-          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
-        pp_term ty) fields)
-        
+        (if coercion then 
+         (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") 
+       else ": ") ^
+      pp_term ty)
+    fields)
+
 let pp_obj pp_term = function
  | Ast.Inductive (params, types) ->
     let pp_constructors constructors =
@@ -348,8 +360,9 @@ let pp_env env =
 
 let rec pp_cic_appl_pattern = function
   | Ast.UriPattern uri -> UriManager.string_of_uri uri
+  | Ast.NRefPattern nref -> NReference.string_of_reference nref
   | Ast.VarPattern name -> name
-  | Ast.ImplicitPattern -> "_"
+  | Ast.ImplicitPattern -> "?"
   | Ast.ApplPattern aps ->
       sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))