X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=0d868c0027e1f0e7a53a8755086f213f5ba747ed;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=cdc0946e6f96bd2d992984bd1043ffc3a7aa9932;hpb=2647a6b8df8fd913b05e33ef8606197cae825281;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index cdc0946e6..0d868c002 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" @@ -54,12 +54,6 @@ let pp_literal = | `Keyword s | `Number s -> s) -let pp_assoc = - function - | Gramext.NonA -> "NonA" - | Gramext.LeftA -> "LeftA" - | Gramext.RightA -> "RightA" - let pp_pos = function (* `None -> "`None" *) @@ -74,11 +68,16 @@ let pp_attribute = sprintf "X(%s)" (String.concat ";" (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) - | `Level (prec, assoc) -> sprintf "L(%d%s)" prec (pp_assoc assoc) + | `Level (prec) -> sprintf "L(%d)" prec | `Raw _ -> "R" | `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 +93,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" @@ -110,34 +109,28 @@ let rec pp_term ?(pp_parens = true) t = (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term 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) - (pp_term ~pp_parens:true t2) + | Ast.LetIn ((var,t2), t1, t3) -> +(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) + sprintf "let %s \\def %s in %s" (pp_term var) +(* (pp_term ~pp_parens:true t2) *) + (pp_term ~pp_parens:true t1) + (pp_term ~pp_parens:true t3) | Ast.LetRec (kind, definitions, term) -> - let strip i t = - let rec aux i l = function - | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body - | body -> List.rev l, body - in - aux i [] t - in let rec get_guard i = function - | [] -> assert false + | [] -> (*assert false*) Ast.Implicit | [term, _] when i = 1 -> term | _ :: tl -> get_guard (pred i) tl in - let map (var, body, i) = - let id, vars, typ, body = match var with - | term, Some typ -> - let pvars, pbody = strip i typ in - let _, bbody = strip i body in - term, pvars, pbody, bbody - | _ -> assert false - in + let map (params, (id,typ), body, i) = + let typ = + match typ with + None -> Ast.Implicit + | Some typ -> typ + in sprintf "%s %s on %s: %s \\def %s" (pp_term ~pp_parens:false term) - (String.concat " " (List.map pp_capture_variable vars)) - (pp_term ~pp_parens:false (get_guard i vars)) + (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 sprintf "let %s %s in %s" @@ -145,8 +138,8 @@ 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) @@ -154,12 +147,14 @@ let rec pp_term ?(pp_parens = true) t = | 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 (`CProp _)-> "CProp" + | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" + | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" | Ast.Symbol (name, _) -> "'" ^ name | Ast.UserInput -> "" @@ -180,29 +175,28 @@ let rec pp_term ?(pp_parens = true) t = and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) -and pp_pattern ((head, href, vars), term) = - let head_pp = - head ^ - (match debug_printing, href with - | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) - | _ -> "") - in - sprintf "%s \\Rightarrow %s" - (match vars with - | [] -> head_pp - | _ -> - sprintf "(%s %s)" head_pp - (String.concat " " (List.map pp_capture_variable vars))) - (pp_term term) +and pp_pattern = + function + Ast.Pattern (head, href, vars), term -> + let head_pp = + head ^ + (match debug_printing, href with + | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "") + in + sprintf "%s \\Rightarrow %s" + (match vars with + | [] -> head_pp + | _ -> + sprintf "(%s %s)" head_pp + (String.concat " " (List.map (pp_capture_variable pp_term) vars))) + (pp_term term) + | Ast.Wildcard, term -> + sprintf "_ \\Rightarrow %s" (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 = @@ -219,6 +213,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.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) @@ -229,6 +227,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) -> @@ -258,7 +264,8 @@ and pp_sep_opt = function and pp_variable = function | Ast.NumVar s -> "number " ^ s | Ast.IdentVar s -> "ident " ^ s - | Ast.TermVar s -> "term " ^ s + | Ast.TermVar (s,Ast.Self _) -> s + | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l | Ast.Ascription (t, n) -> assert false | Ast.FreshVar n -> "fresh " ^ n @@ -266,17 +273,13 @@ 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 - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ)) - params) + | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) let pp_flavour = function | `Definition -> "definition" + | `MutualDefinition -> assert false | `Fact -> "fact" | `Goal -> "goal" | `Lemma -> "lemma" @@ -285,14 +288,17 @@ 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 - (fun (name,ty,coercion) -> - " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields) + (fun (name,ty,coercion,arity) -> + " " ^ name ^ + if coercion then (":" ^ + 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" @@ -308,10 +314,12 @@ 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)) + | Ast.Theorem (`MutualDefinition, name, typ, body) -> + sprintf "<>" | Ast.Theorem (flavour, name, typ, body) -> sprintf "%s %s:\n %s\n%s" (pp_flavour flavour) @@ -321,8 +329,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) @@ -334,7 +342,7 @@ let rec pp_value = function let rec pp_value_type = function - | Env.TermType -> "Term" + | Env.TermType l -> "Term "^string_of_int l | Env.StringType -> "String" | Env.NumType -> "Number" | Env.OptType t -> "Maybe " ^ pp_value_type t @@ -349,8 +357,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))