X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=c82919f4d693640891588165a30ee9e1662c1ad7;hb=38ec119c163b0e6f97a9800933d5b71c065332e8;hp=cfd8c8a308956cdef0466d57f5adc231c85e36ab;hpb=d063ddede0424eb1f47a4c9769eaefbb16d90700;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index cfd8c8a30..c82919f4d 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -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) @@ -222,6 +228,14 @@ and pp_layout = function (String.concat " " (List.map pp_term terms)) | Ast.Group terms -> sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) + | Ast.Mstyle (l,terms) -> + 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) -> @@ -281,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 = @@ -344,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))