module O = Options
module UM = UriManager
-module NP = CicNotationPp
+module NP = NotationPp
module GP = GrafiteAstPp
module G = GrafiteAst
module H = HExtlib
content.cmi:
-cicNotationUtil.cmi: cicNotationPt.cmo
-cicNotationEnv.cmi: cicNotationPt.cmo
-cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
-interpretations.cmi: cicNotationPt.cmo
-cicNotationPt.cmo:
-cicNotationPt.cmx:
+notationUtil.cmi:
+notationEnv.cmi:
+notationPp.cmi:
+interpretations.cmi: notationPt.cmo
+notationPt.cmo:
+notationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
-cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi
-cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi
-cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi
-cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi
-cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi
-cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi
-interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmo \
- interpretations.cmi
-interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
- interpretations.cmi
+notationUtil.cmo: notationPt.cmo notationUtil.cmi
+notationUtil.cmx: notationPt.cmx notationUtil.cmi
+notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi
+notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
+notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi
+notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+interpretations.cmo: notationUtil.cmi notationPt.cmo interpretations.cmi
+interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi
content.cmi:
-cicNotationUtil.cmi: cicNotationPt.cmx
-cicNotationEnv.cmi: cicNotationPt.cmx
-cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
-interpretations.cmi: cicNotationPt.cmx
-cicNotationPt.cmo:
-cicNotationPt.cmx:
+notationUtil.cmi:
+notationEnv.cmi:
+notationPp.cmi:
+interpretations.cmi: notationPt.cmx
+notationPt.cmo:
+notationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
-cicNotationUtil.cmo: cicNotationPt.cmx cicNotationUtil.cmi
-cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi
-cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationEnv.cmi
-cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi
-cicNotationPp.cmo: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmi
-cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi
-interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmx \
- interpretations.cmi
-interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
- interpretations.cmi
+notationUtil.cmo: notationPt.cmx notationUtil.cmi
+notationUtil.cmx: notationPt.cmx notationUtil.cmi
+notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi
+notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
+notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi
+notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+interpretations.cmo: notationUtil.cmi notationPt.cmx interpretations.cmi
+interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi
INTERFACE_FILES = \
content.mli \
- cicNotationUtil.mli \
- cicNotationEnv.mli \
- cicNotationPp.mli \
+ notationUtil.mli \
+ notationEnv.mli \
+ notationPp.mli \
interpretations.mli \
$(NULL)
IMPLEMENTATION_FILES = \
- cicNotationPt.ml \
+ notationPt.ml \
$(INTERFACE_FILES:%.mli=%.ml)
include ../../Makefile.defs
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-module Ast = CicNotationPt
-
-type value =
- | TermValue of Ast.term
- | StringValue of string
- | NumValue of string
- | OptValue of value option
- | ListValue of value list
-
-type value_type =
- | TermType of int
- | StringType
- | NumType
- | OptType of value_type
- | ListType of value_type
-
-exception Value_not_found of string
-exception Type_mismatch of string * value_type
-
-type declaration = string * value_type
-type binding = string * (value_type * value)
-type t = binding list
-
-let lookup env name =
- try
- List.assoc name env
- with Not_found -> raise (Value_not_found name)
-
-let lookup_value env name =
- try
- snd (List.assoc name env)
- with Not_found -> raise (Value_not_found name)
-
-let remove_name env name = List.remove_assoc name env
-
-let remove_names env names =
- List.filter (fun name, _ -> not (List.mem name names)) env
-
-let lookup_term env name =
- match lookup env name with
- | _, TermValue x -> x
- | ty, _ -> raise (Type_mismatch (name, ty))
-
-let lookup_num env name =
- match lookup env name with
- | _, NumValue x -> x
- | ty, _ -> raise (Type_mismatch (name, ty))
-
-let lookup_string env name =
- match lookup env name with
- | _, StringValue x -> x
- | ty, _ -> raise (Type_mismatch (name, ty))
-
-let lookup_opt env name =
- match lookup env name with
- | _, OptValue x -> x
- | ty, _ -> raise (Type_mismatch (name, ty))
-
-let lookup_list env name =
- match lookup env name with
- | _, ListValue x -> x
- | ty, _ -> raise (Type_mismatch (name, ty))
-
-let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
-let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
-let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
-let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
-let opt_declaration (n, ty) = (n, OptType ty)
-let list_declaration (n, ty) = (n, ListType ty)
-
-let declaration_of_var = function
- | Ast.NumVar s -> s, NumType
- | Ast.IdentVar s -> s, StringType
- | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l
- | _ -> assert false
-
-let value_of_term = function
- | Ast.Num (s, _) -> NumValue s
- | Ast.Ident (s, None) -> StringValue s
- | t -> TermValue t
-
-let term_of_value = function
- | NumValue s -> Ast.Num (s, 0)
- | StringValue s -> Ast.Ident (s, None)
- | TermValue t -> t
- | _ -> assert false (* TO BE UNDERSTOOD *)
-
-let rec well_typed ty value =
- match ty, value with
- | TermType _, TermValue _
- | StringType, StringValue _
- | OptType _, OptValue None
- | NumType, NumValue _ -> true
- | OptType ty', OptValue (Some value') -> well_typed ty' value'
- | ListType ty', ListValue vl ->
- List.for_all (fun value' -> well_typed ty' value') vl
- | _ -> false
-
-let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
-let declarations_of_term p =
- List.map declaration_of_var (CicNotationUtil.variables_of_term p)
-
-let rec combine decls values =
- match decls, values with
- | [], [] -> []
- | (name, ty) :: decls, v :: values ->
- (name, (ty, v)) :: (combine decls values)
- | _ -> assert false
-
-let coalesce_env declarations env_list =
- let env0 = List.map list_binding_of_name declarations in
- let grow_env_entry env n v =
- List.map
- (function
- | (n', (ty, ListValue vl)) as entry ->
- if n' = n then n', (ty, ListValue (v :: vl)) else entry
- | _ -> assert false)
- env
- in
- let grow_env env_i env =
- List.fold_left
- (fun env (n, (_, v)) -> grow_env_entry env n v)
- env env_i
- in
- List.fold_right grow_env env_list env0
-
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(** {2 Types} *)
-
-type value =
- | TermValue of CicNotationPt.term
- | StringValue of string
- | NumValue of string
- | OptValue of value option
- | ListValue of value list
-
-type value_type =
- | TermType of int (* the level of the expected term *)
- | StringType
- | NumType
- | OptType of value_type
- | ListType of value_type
-
- (** looked up value not found in environment *)
-exception Value_not_found of string
-
- (** looked up value has the wrong type
- * parameters are value name and value type in environment *)
-exception Type_mismatch of string * value_type
-
-type declaration = string * value_type
-type binding = string * (value_type * value)
-type t = binding list
-
-val declaration_of_var: CicNotationPt.pattern_variable -> declaration
-val value_of_term: CicNotationPt.term -> value
-val term_of_value: value -> CicNotationPt.term
-val well_typed: value_type -> value -> bool
-
-val declarations_of_env: t -> declaration list
-val declarations_of_term: CicNotationPt.term -> declaration list
-val combine: declaration list -> value list -> t (** @raise Invalid_argument *)
-
-(** {2 Environment lookup} *)
-
-val lookup_value: t -> string -> value (** @raise Value_not_found *)
-
-(** lookup_* functions below may raise Value_not_found and Type_mismatch *)
-
-val lookup_term: t -> string -> CicNotationPt.term
-val lookup_string: t -> string -> string
-val lookup_num: t -> string -> string
-val lookup_opt: t -> string -> value option
-val lookup_list: t -> string -> value list
-
-val remove_name: t -> string -> t
-val remove_names: t -> string list -> t
-
-(** {2 Bindings mangling} *)
-
-val opt_binding_some: binding -> binding (* v -> Some v *)
-val opt_binding_none: binding -> binding (* v -> None *)
-
-val opt_binding_of_name: declaration -> binding (* None binding *)
-val list_binding_of_name: declaration -> binding (* [] binding *)
-
-val opt_declaration: declaration -> declaration (* t -> OptType t *)
-val list_declaration: declaration -> declaration (* t -> ListType t *)
-
-(** given a list of environments bindings a set of names n_1, ..., n_k, returns
- * a single environment where n_i is bound to the list of values bound in the
- * starting environments *)
-val coalesce_env: declaration list -> t list -> t
-
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-module Ast = CicNotationPt
-module Env = CicNotationEnv
-
- (* when set to true debugging information, not in sync with input syntax, will
- * 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 = false
-
-let pp_binder = function
- | `Lambda -> "lambda"
- | `Pi -> "Pi"
- | `Exists -> "exists"
- | `Forall -> "forall"
-
-let pp_literal =
- if debug_printing then
- (function (* debugging version *)
- | `Symbol s -> sprintf "symbol(%s)" s
- | `Keyword s -> sprintf "keyword(%s)" s
- | `Number s -> sprintf "number(%s)" s)
- else
- (function
- | `Symbol s
- | `Keyword s
- | `Number s -> s)
-
-let pp_pos =
- function
-(* `None -> "`None" *)
- | `Left -> "`Left"
- | `Right -> "`Right"
- | `Inner -> "`Inner"
-
-let pp_attribute =
- function
- | `IdRef id -> sprintf "x(%s)" id
- | `XmlAttrs attrs ->
- sprintf "X(%s)"
- (String.concat ";"
- (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
- | `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
- | Ast.AttributedTerm (attr, term) when debug_printing ->
- sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term)
- | Ast.AttributedTerm (`Raw text, _) -> text
- | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
- | Ast.Appl terms ->
- sprintf "%s" (String.concat " " (List.map pp_term terms))
- | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
- | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
- sprintf "%s \\to %s"
- (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 pp_term var)
- (pp_term ~pp_parens:true body)
- | Ast.Case (term, indtype, typ, patterns) ->
- sprintf "match %s%s%s with %s"
- (pp_term term)
- (match indtype with
- | None -> ""
- | Some (ty, href_opt) ->
- sprintf " in %s%s" ty
- (match debug_printing, href_opt with
- | true, Some uri ->
- sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
- | _ -> ""))
- (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,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 rec get_guard i = function
- | [] -> (*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 `JustOne
- | 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 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"
- (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
- (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.NRef nref -> NReference.string_of_reference nref
- | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
- | Ast.Ident (name, Some substs)
- | Ast.Uri (name, Some substs) ->
- sprintf "%s \\subst [%s]" name (pp_substs substs)
- | Ast.Implicit `Vector -> "…"
- | Ast.Implicit `JustOne -> "?"
- | Ast.Implicit (`Tagged name) -> "?"^name
- | Ast.Meta (index, substs) ->
- sprintf "%d[%s]" index
- (String.concat "; "
- (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 -> "%"
-
- | Ast.Literal l -> pp_literal l
- | Ast.Layout l -> pp_layout l
- | Ast.Magic m -> pp_magic m
- | Ast.Variable v -> pp_variable v
- in
- match pp_parens, t with
- | false, _
- | true, Ast.Implicit _
- | true, Ast.UserInput
- | true, Ast.Sort _
- | true, Ast.Ident (_, Some [])
- | true, Ast.Ident (_, None) -> t_pp
- | _ -> sprintf "(%s)" t_pp
-
-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 =
- 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_box_spec (kind, spacing, indent) =
- let int_of_bool b = if b then 1 else 0 in
- let kind_string =
- match kind with
- Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV"
- in
- sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
-
-and pp_layout = function
- | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
- | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
- | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
- | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2)
- | 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)
- | Ast.Break -> "\\BREAK"
-(* | Space -> "\\SPACE" *)
- | Ast.Box (box_spec, terms) ->
- sprintf "\\%s [%s]" (pp_box_spec box_spec)
- (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) ->
- sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | Ast.List1 (t, sep_opt) ->
- sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | Ast.Opt t -> sprintf "opt %s" (pp_term t)
- | Ast.Fold (kind, p_base, names, p_rec) ->
- let acc = match names with acc :: _ -> acc | _ -> assert false in
- sprintf "fold %s %s rec %s %s"
- (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec)
- | Ast.Default (p_some, p_none) ->
- sprintf "default %s %s" (pp_term p_some) (pp_term p_none)
- | Ast.If (p_test, p_true, p_false) ->
- sprintf "if %s then %s else %s"
- (pp_term p_test) (pp_term p_true) (pp_term p_false)
- | Ast.Fail -> "fail"
-
-and pp_fold_kind = function
- | `Left -> "left"
- | `Right -> "right"
-
-and pp_sep_opt = function
- | None -> ""
- | Some sep -> sprintf " sep %s" (pp_literal sep)
-
-and pp_variable = function
- | Ast.NumVar s -> "number " ^ s
- | Ast.IdentVar s -> "ident " ^ 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
-
-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 pp_term = function
- | [] -> ""
- | 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"
- | `Remark -> "remark"
- | `Theorem -> "theorem"
- | `Variant -> "variant"
- | `Axiom -> "axiom"
-
-let pp_fields pp_term fields =
- (if fields <> [] then "\n" else "") ^
- String.concat ";\n"
- (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)
-
-let pp_obj pp_term = function
- | Ast.Inductive (params, types) ->
- let pp_constructors constructors =
- String.concat "\n"
- (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
- constructors)
- in
- let pp_type (name, _, typ, constructors) =
- sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
- (pp_constructors constructors)
- in
- (match types with
- | [] -> assert false
- | (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 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 "<<pretty printing of mutual definitions not implemented yet>>"
- | Ast.Theorem (flavour, name, typ, body,_) ->
- sprintf "%s %s:\n %s\n%s"
- (pp_flavour flavour)
- name
- (pp_term typ)
- (match body with
- | None -> ""
- | Some body -> "\\def\n " ^ pp_term body)
- | Ast.Record (params,name,ty,fields) ->
- "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)
- | Env.StringValue s -> sprintf "\"%s\"" s
- | Env.NumValue n -> n
- | Env.OptValue (Some v) -> "Some " ^ pp_value v
- | Env.OptValue None -> "None"
- | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
-
-let rec pp_value_type =
- function
- | Env.TermType l -> "Term "^string_of_int l
- | Env.StringType -> "String"
- | Env.NumType -> "Number"
- | Env.OptType t -> "Maybe " ^ pp_value_type t
- | Env.ListType l -> "List " ^ pp_value_type l
-
-let pp_env env =
- String.concat "; "
- (List.map
- (fun (name, (ty, value)) ->
- sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
- 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.ApplPattern aps ->
- sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))
-
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(** ZACK
- * This module does not print terms and object properly, it has been created
- * mainly for debugging reason. There is no guarantee that printed strings are
- * re-parsable. Moreover, actually there is no way at all to proper print
- * objects in a way that is re-parsable.
- *
- * TODO the proper implementation of a pp_obj function like the one below should
- * be as follows. Change its type to
- * pp_obj: CicNotationPt.obj -> CicNotationPres.markup
- * and parametrize it over a function with the following type
- * pp_term: CicNotationPt.term -> CicNotationPres.markup
- * The obtained markup can then be printed using CicNotationPres.print_xml or
- * BoxPp.render_to_string(s)
- *)
-
-val pp_term: CicNotationPt.term -> string
-val pp_obj: ('term -> string) -> 'term CicNotationPt.obj -> string
-
-val pp_env: CicNotationEnv.t -> string
-val pp_value: CicNotationEnv.value -> string
-val pp_value_type: CicNotationEnv.value_type -> string
-
-val pp_pos: CicNotationPt.child_pos -> string
-val pp_attribute: CicNotationPt.term_attribute -> string
-
-val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string
-
- (** non re-entrant change of pp_term function above *)
-val set_pp_term: (CicNotationPt.term -> string) -> unit
-
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-(** CIC Notation Parse Tree *)
-
-type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
-type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
-CicUniv.universe | `NType of string |`NCProp of string]
-type fold_kind = [ `Left | `Right ]
-
-type location = Stdpp.location
-let fail floc msg =
- let (x, y) = HExtlib.loc_of_floc floc in
- failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
-
-type href = UriManager.uri
-
-type child_pos = [ `Left | `Right | `Inner ]
-
-type term_attribute =
- [ `Loc of location (* source file location *)
- | `IdRef of string (* ACic pointer *)
- | `Level of int
- | `XmlAttrs of (string option * string * string) list
- (* list of XML attributes: namespace, name, value *)
- | `Raw of string (* unparsed version *)
- ]
-
-type literal =
- [ `Symbol of string
- | `Keyword of string
- | `Number of string
- ]
-
-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 = 6
-
-type term =
- (* CIC AST *)
-
- | AttributedTerm of term_attribute * term
-
- | Appl of term list
- | 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 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.
- * Some [] -> user has given an empty explicit substitution list
- * None -> user has given no explicit substitution list *)
- | Implicit of [`Vector | `JustOne | `Tagged of string]
- | Meta of int * meta_subst list
- | Num of string * int (* literal, instance *)
- | Sort of sort_kind
- | Symbol of string * int (* canonical name, instance *)
-
- | UserInput (* place holder for user input, used by MatitaConsole, not to be
- used elsewhere *)
- | Uri of string * subst list option (* as Ident, for long names *)
- | NRef of NReference.reference
-
- | NCic of NCic.term
-
- (* Syntax pattern extensions *)
-
- | Literal of literal
- | Layout of layout_pattern
-
- | Magic of magic_term
- | Variable of pattern_variable
-
- (* name, type. First component must be Ident or Variable (FreshVar _) *)
-
-and meta_subst = term option
-and subst = string * term
-and case_pattern =
- Pattern of string * href option * term capture_variable list
- | Wildcard
-
-and box_kind = H | V | HV | HOV
-and box_spec = box_kind * bool * bool (* kind, spacing, indent *)
-
-and layout_pattern =
- | Sub of term * term
- | Sup of term * term
- | Below of term * term
- | Above of term * term
- | Frac of term * term
- | Over of term * term
- | Atop of term * term
- | InfRule of term * term * term
-(* | array of term * literal option * literal option
- |+ column separator, row separator +| *)
- | Maction of term list
- | Sqrt of term
- | Root of term * term (* argument, index *)
- | Break
- | Box of box_spec * term list
- | Group of term list
- | Mstyle of (string * string) list * term list
- | Mpadded of (string * string) list * term list
-
-and magic_term =
- (* level 1 magics *)
- | List0 of term * literal option (* pattern, separator *)
- | List1 of term * literal option (* pattern, separator *)
- | Opt of term
-
- (* level 2 magics *)
- | Fold of fold_kind * term * string list * term
- (* base case pattern, recursive case bound names, recursive case pattern *)
- | Default of term * term (* "some" case pattern, "none" case pattern *)
- | Fail
- | If of term * term * term (* test, pattern if true, pattern if false *)
-
-and term_level = Self of int | Level of int
-
-and pattern_variable =
- (* level 1 and 2 variables *)
- | NumVar of string
- | IdentVar of string
- | TermVar of string * term_level
-
- (* level 1 variables *)
- | Ascription of term * string
-
- (* level 2 variables *)
- | FreshVar of string
-
-type argument_pattern =
- | IdentArg of int * string (* eta-depth, name *)
-
-type cic_appl_pattern =
- | UriPattern of UriManager.uri
- | NRefPattern of NReference.reference
- | VarPattern of string
- | ImplicitPattern
- | ApplPattern of cic_appl_pattern list
-
- (** <name, inductive/coinductive, type, constructor list>
- * true means inductive, false coinductive *)
-type 'term inductive_type = string * bool * 'term * (string * 'term) 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 * NCic.def_pragma
- (** flavour, name, type, body
- * - name is absent when an unnamed theorem is being proved, tipically in
- * interactive usage
- * - body is present when its given along with the command, otherwise it
- * will be given in proof editing mode using the tactical language,
- * unless the flavour is an Axiom
- *)
- | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
- (** left parameters, name, type, fields *)
-
-(** {2 Standard precedences} *)
-
-let let_in_prec = 10
-let binder_prec = 20
-let apply_prec = 70
-let simple_prec = 90
-
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-module Ast = CicNotationPt
-
-let visit_ast ?(special_k = fun _ -> assert false)
- ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x)
- ?(map_case_outtype=
- fun k x -> match x with None -> None | Some x -> Some (k x))
- k
-=
- let rec aux = function
- | Ast.Appl terms -> Ast.Appl (List.map k terms)
- | Ast.Binder (kind, var, body) ->
- Ast.Binder (kind, aux_capture_variable var, k body)
- | Ast.Case (term, indtype, typ, patterns) ->
- Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ,
- aux_patterns map_xref_option patterns)
- | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
- | Ast.LetIn (var, t1, t3) ->
- Ast.LetIn (aux_capture_variable var, k t1, k t3)
- | Ast.LetRec (kind, definitions, term) ->
- let definitions =
- List.map
- (fun (params, var, ty, decrno) ->
- List.map aux_capture_variable params, aux_capture_variable var,
- k ty, decrno)
- definitions
- in
- Ast.LetRec (kind, definitions, k term)
- | Ast.Ident (name, Some substs) ->
- Ast.Ident (name, Some (aux_substs substs))
- | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
- | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
- | (Ast.AttributedTerm _
- | Ast.Layout _
- | Ast.Literal _
- | Ast.Magic _
- | Ast.Variable _) as t -> special_k t
- | (Ast.Ident _
- | Ast.NRef _
- | Ast.NCic _
- | Ast.Implicit _
- | Ast.Num _
- | Ast.Sort _
- | Ast.Symbol _
- | Ast.Uri _
- | Ast.UserInput) as t -> t
- and aux_opt = function
- | None -> None
- | Some term -> Some (k term)
- and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
- and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns
- and aux_pattern k_xref =
- function
- Ast.Pattern (head, hrefs, vars), term ->
- Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
- | Ast.Wildcard, term -> Ast.Wildcard, k term
- and aux_subst (name, term) = (name, k term)
- and aux_substs substs = List.map aux_subst substs
- in
- aux
-
-let visit_layout k = function
- | Ast.Sub (t1, t2) -> Ast.Sub (k t1, k t2)
- | Ast.Sup (t1, t2) -> Ast.Sup (k t1, k t2)
- | Ast.Below (t1, t2) -> Ast.Below (k t1, k t2)
- | Ast.Above (t1, t2) -> Ast.Above (k t1, k t2)
- | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
- | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
- | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
- | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
- | Ast.Sqrt t -> Ast.Sqrt (k t)
- | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
- | Ast.Break -> Ast.Break
- | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
- | Ast.Group terms -> Ast.Group (List.map k terms)
- | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
- | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
- | Ast.Maction terms -> Ast.Maction (List.map k terms)
-
-let visit_magic k = function
- | Ast.List0 (t, l) -> Ast.List0 (k t, l)
- | Ast.List1 (t, l) -> Ast.List1 (k t, l)
- | Ast.Opt t -> Ast.Opt (k t)
- | Ast.Fold (kind, t1, names, t2) -> Ast.Fold (kind, k t1, names, k t2)
- | Ast.Default (t1, t2) -> Ast.Default (k t1, k t2)
- | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3)
- | Ast.Fail -> Ast.Fail
-
-let visit_variable k = function
- | Ast.NumVar _
- | Ast.IdentVar _
- | Ast.TermVar _
- | Ast.FreshVar _ as t -> t
- | Ast.Ascription (t, s) -> Ast.Ascription (k t, s)
-
-let variables_of_term t =
- let rec vars = ref [] in
- let add_variable v =
- if List.mem v !vars then ()
- else vars := v :: !vars
- in
- let rec aux = function
- | Ast.Magic m -> Ast.Magic (visit_magic aux m)
- | Ast.Layout l -> Ast.Layout (visit_layout aux l)
- | Ast.Variable v -> Ast.Variable (aux_variable v)
- | Ast.Literal _ as t -> t
- | Ast.AttributedTerm (_, t) -> aux t
- | t -> visit_ast aux t
- and aux_variable = function
- | (Ast.NumVar _
- | Ast.IdentVar _
- | Ast.TermVar _) as t ->
- add_variable t ;
- t
- | Ast.FreshVar _ as t -> t
- | Ast.Ascription _ -> assert false
- in
- ignore (aux t) ;
- !vars
-
-let names_of_term t =
- let aux = function
- | Ast.NumVar s
- | Ast.IdentVar s
- | Ast.TermVar (s,_) -> s
- | _ -> assert false
- in
- List.map aux (variables_of_term t)
-
-let keywords_of_term t =
- let rec keywords = ref [] in
- let add_keyword k = keywords := k :: !keywords in
- let rec aux = function
- | Ast.AttributedTerm (_, t) -> aux t
- | Ast.Layout l -> Ast.Layout (visit_layout aux l)
- | Ast.Literal (`Keyword k) as t ->
- add_keyword k;
- t
- | Ast.Literal _ as t -> t
- | Ast.Magic m -> Ast.Magic (visit_magic aux m)
- | Ast.Variable _ as v -> v
- | t -> visit_ast aux t
- in
- ignore (aux t) ;
- !keywords
-
-let rec strip_attributes t =
- let special_k = function
- | Ast.AttributedTerm (_, term) -> strip_attributes term
- | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m)
- | Ast.Variable _ as t -> t
- | t -> assert false
- in
- visit_ast ~special_k strip_attributes t
-
-let rec get_idrefs =
- function
- | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
- | Ast.AttributedTerm (_, t) -> get_idrefs t
- | _ -> []
-
-let meta_names_of_term term =
- let rec names = ref [] in
- let add_name n =
- if List.mem n !names then ()
- else names := n :: !names
- in
- let rec aux = function
- | Ast.AttributedTerm (_, term) -> aux term
- | Ast.Appl terms -> List.iter aux terms
- | Ast.Binder (_, _, body) -> aux body
- | Ast.Case (term, indty, outty_opt, patterns) ->
- aux term ;
- aux_opt outty_opt ;
- List.iter aux_branch patterns
- | Ast.LetIn (_, t1, t3) ->
- aux t1 ;
- aux t3
- | Ast.LetRec (_, definitions, body) ->
- List.iter aux_definition definitions ;
- aux body
- | Ast.Uri (_, Some substs) -> aux_substs substs
- | Ast.Ident (_, Some substs) -> aux_substs substs
- | Ast.Meta (_, substs) -> aux_meta_substs substs
-
- | Ast.Implicit _
- | Ast.Ident _
- | Ast.Num _
- | Ast.Sort _
- | Ast.Symbol _
- | Ast.Uri _
- | Ast.UserInput -> ()
-
- | Ast.Magic magic -> aux_magic magic
- | Ast.Variable var -> aux_variable var
-
- | _ -> assert false
- and aux_opt = function
- | Some term -> aux term
- | None -> ()
- and aux_capture_var (_, ty_opt) = aux_opt ty_opt
- and aux_branch (pattern, term) =
- aux_pattern pattern ;
- aux term
- and aux_pattern =
- function
- Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
- | Ast.Wildcard -> ()
- and aux_definition (params, var, term, decrno) =
- List.iter aux_capture_var params ;
- aux_capture_var var ;
- aux term
- and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
- and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
- and aux_variable = function
- | Ast.NumVar name -> add_name name
- | Ast.IdentVar name -> add_name name
- | Ast.TermVar (name,_) -> add_name name
- | Ast.FreshVar _ -> ()
- | Ast.Ascription _ -> assert false
- and aux_magic = function
- | Ast.Default (t1, t2)
- | Ast.Fold (_, t1, _, t2) ->
- aux t1 ;
- aux t2
- | Ast.If (t1, t2, t3) ->
- aux t1 ;
- aux t2 ;
- aux t3
- | Ast.Fail -> ()
- | _ -> assert false
- in
- aux term ;
- !names
-
-let rectangular matrix =
- let columns = Array.length matrix.(0) in
- try
- Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix;
- true
- with Exit -> false
-
-let ncombine ll =
- let matrix = Array.of_list (List.map Array.of_list ll) in
- assert (rectangular matrix);
- let rows = Array.length matrix in
- let columns = Array.length matrix.(0) in
- let lists = ref [] in
- for j = 0 to columns - 1 do
- let l = ref [] in
- for i = 0 to rows - 1 do
- l := matrix.(i).(j) :: !l
- done;
- lists := List.rev !l :: !lists
- done;
- List.rev !lists
-
-let string_of_literal = function
- | `Symbol s
- | `Keyword s
- | `Number s -> s
-
-let boxify = function
- | [ a ] -> a
- | l -> Ast.Layout (Ast.Box ((Ast.H, false, false), l))
-
-let unboxify = function
- | Ast.Layout (Ast.Box ((Ast.H, false, false), [ a ])) -> a
- | l -> l
-
-let group = function
- | [ a ] -> a
- | l -> Ast.Layout (Ast.Group l)
-
-let ungroup =
- let rec aux acc =
- function
- [] -> List.rev acc
- | Ast.Layout (Ast.Group terms) :: terms' -> aux acc (terms @ terms')
- | term :: terms -> aux (term :: acc) terms
- in
- aux []
-
-let dress ~sep:sauce =
- let rec aux =
- function
- | [] -> []
- | [hd] -> [hd]
- | hd :: tl -> hd :: sauce :: aux tl
- in
- aux
-
-let dressn ~sep:sauces =
- let rec aux =
- function
- | [] -> []
- | [hd] -> [hd]
- | hd :: tl -> hd :: sauces @ aux tl
- in
- aux
-
-let find_appl_pattern_uris ap =
- let rec aux acc =
- function
- | Ast.UriPattern uri -> `Uri uri :: acc
- | Ast.NRefPattern nref -> `NRef nref :: acc
- | Ast.ImplicitPattern
- | Ast.VarPattern _ -> acc
- | Ast.ApplPattern apl -> List.fold_left aux acc apl
- in
- let uris = aux [] ap in
- let cmp u1 u2 =
- match u1,u2 with
- `Uri u1, `Uri u2 -> UriManager.compare u1 u2
- | `NRef r1, `NRef r2 -> NReference.compare r1 r2
- | `Uri _,`NRef _ -> -1
- | `NRef _, `Uri _ -> 1
- in
- HExtlib.list_uniq (List.fast_sort cmp uris)
-
-let rec find_branch =
- function
- Ast.Magic (Ast.If (_, Ast.Magic Ast.Fail, t)) -> find_branch t
- | Ast.Magic (Ast.If (_, t, _)) -> find_branch t
- | t -> t
-
-let cic_name_of_name = function
- | Ast.Ident ("_", None) -> Cic.Anonymous
- | Ast.Ident (name, None) -> Cic.Name name
- | _ -> assert false
-
-let name_of_cic_name =
-(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *)
- (* ZACK why we used to generate dummy xrefs? *)
- let add_dummy_xref t = t in
- function
- | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None))
- | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None))
-
-let fresh_index = ref ~-1
-
-type notation_id = int
-
-let fresh_id () =
- incr fresh_index;
- !fresh_index
-
- (* TODO ensure that names generated by fresh_var do not clash with user's *)
- (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
-let fresh_name () = "eta" ^ string_of_int (fresh_id ())
-
-let rec freshen_term ?(index = ref 0) term =
- let freshen_term = freshen_term ~index in
- let fresh_instance () = incr index; !index in
- let special_k = function
- | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, freshen_term t)
- | Ast.Layout l -> Ast.Layout (visit_layout freshen_term l)
- | Ast.Magic m -> Ast.Magic (visit_magic freshen_term m)
- | Ast.Variable v -> Ast.Variable (visit_variable freshen_term v)
- | Ast.Literal _ as t -> t
- | _ -> assert false
- in
- match term with
- | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
- | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
- | t -> visit_ast ~special_k freshen_term t
-
-let freshen_obj obj =
- let index = ref 0 in
- let freshen_term = freshen_term ~index in
- let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
- let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
- let freshen_capture_variables =
- List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
- in
- match obj with
- | CicNotationPt.Inductive (params, indtypes) ->
- let indtypes =
- List.map
- (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
- indtypes
- in
- CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
- | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
- let ty_opt =
- match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
- in
- CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
- | CicNotationPt.Record (params, n, ty, fields) ->
- CicNotationPt.Record (freshen_capture_variables params, n,
- freshen_term ty, freshen_name_ty_b fields)
-
-let freshen_term = freshen_term ?index:None
-
+++ /dev/null
-(* Copyright (C) 2004-2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val fresh_name: unit -> string
-
-val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list
-val names_of_term: CicNotationPt.term -> string list
-
- (** extract all keywords (i.e. string literals) from a level 1 pattern *)
-val keywords_of_term: CicNotationPt.term -> string list
-
-val visit_ast:
- ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
- ?map_xref_option:(CicNotationPt.href option -> CicNotationPt.href option) ->
- ?map_case_indty:(CicNotationPt.case_indtype option ->
- CicNotationPt.case_indtype option) ->
- ?map_case_outtype:((CicNotationPt.term -> CicNotationPt.term) ->
- CicNotationPt.term option -> CicNotationPt.term
- option) ->
- (CicNotationPt.term -> CicNotationPt.term) ->
- CicNotationPt.term ->
- CicNotationPt.term
-
-val visit_layout:
- (CicNotationPt.term -> CicNotationPt.term) ->
- CicNotationPt.layout_pattern ->
- CicNotationPt.layout_pattern
-
-val visit_magic:
- (CicNotationPt.term -> CicNotationPt.term) ->
- CicNotationPt.magic_term ->
- CicNotationPt.magic_term
-
-val visit_variable:
- (CicNotationPt.term -> CicNotationPt.term) ->
- CicNotationPt.pattern_variable ->
- CicNotationPt.pattern_variable
-
-val strip_attributes: CicNotationPt.term -> CicNotationPt.term
-
- (** @return the list of proper (i.e. non recursive) IdRef of a term *)
-val get_idrefs: CicNotationPt.term -> string list
-
- (** generalization of List.combine to n lists *)
-val ncombine: 'a list list -> 'a list list
-
-val string_of_literal: CicNotationPt.literal -> string
-
-val dress: sep:'a -> 'a list -> 'a list
-val dressn: sep:'a list -> 'a list -> 'a list
-
-val boxify: CicNotationPt.term list -> CicNotationPt.term
-val group: CicNotationPt.term list -> CicNotationPt.term
-val ungroup: CicNotationPt.term list -> CicNotationPt.term list
-
-val find_appl_pattern_uris:
- CicNotationPt.cic_appl_pattern ->
- [`Uri of UriManager.uri | `NRef of NReference.reference] list
-
-val find_branch:
- CicNotationPt.term -> CicNotationPt.term
-
-val cic_name_of_name: CicNotationPt.term -> Cic.name
-val name_of_cic_name: Cic.name -> CicNotationPt.term
-
- (** Symbol/Numbers instances *)
-
-val freshen_term: CicNotationPt.term -> CicNotationPt.term
-val freshen_obj: CicNotationPt.term CicNotationPt.obj -> CicNotationPt.term CicNotationPt.obj
-
- (** Notation id handling *)
-
-type notation_id
-
-val fresh_id: unit -> notation_id
-
open Printf
-module Ast = CicNotationPt
+module Ast = NotationPt
module Obj = LibraryObjects
let debug = false
uri: (Cic.id, UriManager.uri) Hashtbl.t;
}
-let destroy_nat annterm =
- let is_zero = function
- | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let is_succ = function
- | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let rec aux acc = function
- | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
- | t when is_zero t -> Some acc
- | _ -> None in
- aux 0 annterm
-
(* persistent state *)
let initial_level2_patterns32 () = Hashtbl.create 211
in
let rec add_lambda t n =
if n > 0 then
- let name = CicNotationUtil.fresh_name () in
+ let name = NotationUtil.fresh_name () in
Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
else
val add_interpretation:
string -> (* id / description *)
- string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
- CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
+ string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
+ NotationPt.cic_appl_pattern -> (* level 3 pattern *)
interpretation_id
(** @raise Interpretation_not_found *)
val lookup_interpretations:
?sorted:bool -> string -> (* symbol *)
- (string * CicNotationPt.argument_pattern list *
- CicNotationPt.cic_appl_pattern) list
+ (string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern) list
exception Interpretation_not_found
mk_implicit:(bool -> 'term) ->
term_of_uri : (UriManager.uri -> 'term) ->
term_of_nref : (NReference.reference -> 'term) ->
- (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
+ (string * 'term) list -> NotationPt.cic_appl_pattern ->
'term
val push: unit -> unit
val find_level2_patterns32:
int ->
string * string *
- CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern
+ NotationPt.argument_pattern list * NotationPt.cic_appl_pattern
val add_load_patterns32:
- ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit
+ ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit
val init: unit -> unit
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+module Ast = NotationPt
+
+type value =
+ | TermValue of Ast.term
+ | StringValue of string
+ | NumValue of string
+ | OptValue of value option
+ | ListValue of value list
+
+type value_type =
+ | TermType of int
+ | StringType
+ | NumType
+ | OptType of value_type
+ | ListType of value_type
+
+exception Value_not_found of string
+exception Type_mismatch of string * value_type
+
+type declaration = string * value_type
+type binding = string * (value_type * value)
+type t = binding list
+
+let lookup env name =
+ try
+ List.assoc name env
+ with Not_found -> raise (Value_not_found name)
+
+let lookup_value env name =
+ try
+ snd (List.assoc name env)
+ with Not_found -> raise (Value_not_found name)
+
+let remove_name env name = List.remove_assoc name env
+
+let remove_names env names =
+ List.filter (fun name, _ -> not (List.mem name names)) env
+
+let lookup_term env name =
+ match lookup env name with
+ | _, TermValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_num env name =
+ match lookup env name with
+ | _, NumValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_string env name =
+ match lookup env name with
+ | _, StringValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_opt env name =
+ match lookup env name with
+ | _, OptValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_list env name =
+ match lookup env name with
+ | _, ListValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
+let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
+let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
+let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
+let opt_declaration (n, ty) = (n, OptType ty)
+let list_declaration (n, ty) = (n, ListType ty)
+
+let declaration_of_var = function
+ | Ast.NumVar s -> s, NumType
+ | Ast.IdentVar s -> s, StringType
+ | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l
+ | _ -> assert false
+
+let value_of_term = function
+ | Ast.Num (s, _) -> NumValue s
+ | Ast.Ident (s, None) -> StringValue s
+ | t -> TermValue t
+
+let term_of_value = function
+ | NumValue s -> Ast.Num (s, 0)
+ | StringValue s -> Ast.Ident (s, None)
+ | TermValue t -> t
+ | _ -> assert false (* TO BE UNDERSTOOD *)
+
+let rec well_typed ty value =
+ match ty, value with
+ | TermType _, TermValue _
+ | StringType, StringValue _
+ | OptType _, OptValue None
+ | NumType, NumValue _ -> true
+ | OptType ty', OptValue (Some value') -> well_typed ty' value'
+ | ListType ty', ListValue vl ->
+ List.for_all (fun value' -> well_typed ty' value') vl
+ | _ -> false
+
+let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
+let declarations_of_term p =
+ List.map declaration_of_var (NotationUtil.variables_of_term p)
+
+let rec combine decls values =
+ match decls, values with
+ | [], [] -> []
+ | (name, ty) :: decls, v :: values ->
+ (name, (ty, v)) :: (combine decls values)
+ | _ -> assert false
+
+let coalesce_env declarations env_list =
+ let env0 = List.map list_binding_of_name declarations in
+ let grow_env_entry env n v =
+ List.map
+ (function
+ | (n', (ty, ListValue vl)) as entry ->
+ if n' = n then n', (ty, ListValue (v :: vl)) else entry
+ | _ -> assert false)
+ env
+ in
+ let grow_env env_i env =
+ List.fold_left
+ (fun env (n, (_, v)) -> grow_env_entry env n v)
+ env env_i
+ in
+ List.fold_right grow_env env_list env0
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(** {2 Types} *)
+
+type value =
+ | TermValue of NotationPt.term
+ | StringValue of string
+ | NumValue of string
+ | OptValue of value option
+ | ListValue of value list
+
+type value_type =
+ | TermType of int (* the level of the expected term *)
+ | StringType
+ | NumType
+ | OptType of value_type
+ | ListType of value_type
+
+ (** looked up value not found in environment *)
+exception Value_not_found of string
+
+ (** looked up value has the wrong type
+ * parameters are value name and value type in environment *)
+exception Type_mismatch of string * value_type
+
+type declaration = string * value_type
+type binding = string * (value_type * value)
+type t = binding list
+
+val declaration_of_var: NotationPt.pattern_variable -> declaration
+val value_of_term: NotationPt.term -> value
+val term_of_value: value -> NotationPt.term
+val well_typed: value_type -> value -> bool
+
+val declarations_of_env: t -> declaration list
+val declarations_of_term: NotationPt.term -> declaration list
+val combine: declaration list -> value list -> t (** @raise Invalid_argument *)
+
+(** {2 Environment lookup} *)
+
+val lookup_value: t -> string -> value (** @raise Value_not_found *)
+
+(** lookup_* functions below may raise Value_not_found and Type_mismatch *)
+
+val lookup_term: t -> string -> NotationPt.term
+val lookup_string: t -> string -> string
+val lookup_num: t -> string -> string
+val lookup_opt: t -> string -> value option
+val lookup_list: t -> string -> value list
+
+val remove_name: t -> string -> t
+val remove_names: t -> string list -> t
+
+(** {2 Bindings mangling} *)
+
+val opt_binding_some: binding -> binding (* v -> Some v *)
+val opt_binding_none: binding -> binding (* v -> None *)
+
+val opt_binding_of_name: declaration -> binding (* None binding *)
+val list_binding_of_name: declaration -> binding (* [] binding *)
+
+val opt_declaration: declaration -> declaration (* t -> OptType t *)
+val list_declaration: declaration -> declaration (* t -> ListType t *)
+
+(** given a list of environments bindings a set of names n_1, ..., n_k, returns
+ * a single environment where n_i is bound to the list of values bound in the
+ * starting environments *)
+val coalesce_env: declaration list -> t list -> t
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+module Ast = NotationPt
+module Env = NotationEnv
+
+ (* when set to true debugging information, not in sync with input syntax, will
+ * 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 = false
+
+let pp_binder = function
+ | `Lambda -> "lambda"
+ | `Pi -> "Pi"
+ | `Exists -> "exists"
+ | `Forall -> "forall"
+
+let pp_literal =
+ if debug_printing then
+ (function (* debugging version *)
+ | `Symbol s -> sprintf "symbol(%s)" s
+ | `Keyword s -> sprintf "keyword(%s)" s
+ | `Number s -> sprintf "number(%s)" s)
+ else
+ (function
+ | `Symbol s
+ | `Keyword s
+ | `Number s -> s)
+
+let pp_pos =
+ function
+(* `None -> "`None" *)
+ | `Left -> "`Left"
+ | `Right -> "`Right"
+ | `Inner -> "`Inner"
+
+let pp_attribute =
+ function
+ | `IdRef id -> sprintf "x(%s)" id
+ | `XmlAttrs attrs ->
+ sprintf "X(%s)"
+ (String.concat ";"
+ (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
+ | `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
+ | Ast.AttributedTerm (attr, term) when debug_printing ->
+ sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term)
+ | Ast.AttributedTerm (`Raw text, _) -> text
+ | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
+ | Ast.Appl terms ->
+ sprintf "%s" (String.concat " " (List.map pp_term terms))
+ | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
+ sprintf "%s \\to %s"
+ (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 pp_term var)
+ (pp_term ~pp_parens:true body)
+ | Ast.Case (term, indtype, typ, patterns) ->
+ sprintf "match %s%s%s with %s"
+ (pp_term term)
+ (match indtype with
+ | None -> ""
+ | Some (ty, href_opt) ->
+ sprintf " in %s%s" ty
+ (match debug_printing, href_opt with
+ | true, Some uri ->
+ sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ | _ -> ""))
+ (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,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 rec get_guard i = function
+ | [] -> (*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 `JustOne
+ | 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 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"
+ (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (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.NRef nref -> NReference.string_of_reference nref
+ | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
+ | Ast.Ident (name, Some substs)
+ | Ast.Uri (name, Some substs) ->
+ sprintf "%s \\subst [%s]" name (pp_substs substs)
+ | Ast.Implicit `Vector -> "…"
+ | Ast.Implicit `JustOne -> "?"
+ | Ast.Implicit (`Tagged name) -> "?"^name
+ | Ast.Meta (index, substs) ->
+ sprintf "%d[%s]" index
+ (String.concat "; "
+ (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 -> "%"
+
+ | Ast.Literal l -> pp_literal l
+ | Ast.Layout l -> pp_layout l
+ | Ast.Magic m -> pp_magic m
+ | Ast.Variable v -> pp_variable v
+ in
+ match pp_parens, t with
+ | false, _
+ | true, Ast.Implicit _
+ | true, Ast.UserInput
+ | true, Ast.Sort _
+ | true, Ast.Ident (_, Some [])
+ | true, Ast.Ident (_, None) -> t_pp
+ | _ -> sprintf "(%s)" t_pp
+
+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 =
+ 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_box_spec (kind, spacing, indent) =
+ let int_of_bool b = if b then 1 else 0 in
+ let kind_string =
+ match kind with
+ Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV"
+ in
+ sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
+
+and pp_layout = function
+ | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
+ | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
+ | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
+ | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2)
+ | 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)
+ | Ast.Break -> "\\BREAK"
+(* | Space -> "\\SPACE" *)
+ | Ast.Box (box_spec, terms) ->
+ sprintf "\\%s [%s]" (pp_box_spec box_spec)
+ (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) ->
+ sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | Ast.List1 (t, sep_opt) ->
+ sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | Ast.Opt t -> sprintf "opt %s" (pp_term t)
+ | Ast.Fold (kind, p_base, names, p_rec) ->
+ let acc = match names with acc :: _ -> acc | _ -> assert false in
+ sprintf "fold %s %s rec %s %s"
+ (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec)
+ | Ast.Default (p_some, p_none) ->
+ sprintf "default %s %s" (pp_term p_some) (pp_term p_none)
+ | Ast.If (p_test, p_true, p_false) ->
+ sprintf "if %s then %s else %s"
+ (pp_term p_test) (pp_term p_true) (pp_term p_false)
+ | Ast.Fail -> "fail"
+
+and pp_fold_kind = function
+ | `Left -> "left"
+ | `Right -> "right"
+
+and pp_sep_opt = function
+ | None -> ""
+ | Some sep -> sprintf " sep %s" (pp_literal sep)
+
+and pp_variable = function
+ | Ast.NumVar s -> "number " ^ s
+ | Ast.IdentVar s -> "ident " ^ 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
+
+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 pp_term = function
+ | [] -> ""
+ | 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"
+ | `Remark -> "remark"
+ | `Theorem -> "theorem"
+ | `Variant -> "variant"
+ | `Axiom -> "axiom"
+
+let pp_fields pp_term fields =
+ (if fields <> [] then "\n" else "") ^
+ String.concat ";\n"
+ (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)
+
+let pp_obj pp_term = function
+ | Ast.Inductive (params, types) ->
+ let pp_constructors constructors =
+ String.concat "\n"
+ (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
+ constructors)
+ in
+ let pp_type (name, _, typ, constructors) =
+ sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
+ (pp_constructors constructors)
+ in
+ (match types with
+ | [] -> assert false
+ | (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 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 "<<pretty printing of mutual definitions not implemented yet>>"
+ | Ast.Theorem (flavour, name, typ, body,_) ->
+ sprintf "%s %s:\n %s\n%s"
+ (pp_flavour flavour)
+ name
+ (pp_term typ)
+ (match body with
+ | None -> ""
+ | Some body -> "\\def\n " ^ pp_term body)
+ | Ast.Record (params,name,ty,fields) ->
+ "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)
+ | Env.StringValue s -> sprintf "\"%s\"" s
+ | Env.NumValue n -> n
+ | Env.OptValue (Some v) -> "Some " ^ pp_value v
+ | Env.OptValue None -> "None"
+ | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
+
+let rec pp_value_type =
+ function
+ | Env.TermType l -> "Term "^string_of_int l
+ | Env.StringType -> "String"
+ | Env.NumType -> "Number"
+ | Env.OptType t -> "Maybe " ^ pp_value_type t
+ | Env.ListType l -> "List " ^ pp_value_type l
+
+let pp_env env =
+ String.concat "; "
+ (List.map
+ (fun (name, (ty, value)) ->
+ sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
+ 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.ApplPattern aps ->
+ sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(** ZACK
+ * This module does not print terms and object properly, it has been created
+ * mainly for debugging reason. There is no guarantee that printed strings are
+ * re-parsable. Moreover, actually there is no way at all to proper print
+ * objects in a way that is re-parsable.
+ *
+ * TODO the proper implementation of a pp_obj function like the one below should
+ * be as follows. Change its type to
+ * pp_obj: NotationPt.obj -> NotationPres.markup
+ * and parametrize it over a function with the following type
+ * pp_term: NotationPt.term -> NotationPres.markup
+ * The obtained markup can then be printed using CicNotationPres.print_xml or
+ * BoxPp.render_to_string(s)
+ *)
+
+val pp_term: NotationPt.term -> string
+val pp_obj: ('term -> string) -> 'term NotationPt.obj -> string
+
+val pp_env: NotationEnv.t -> string
+val pp_value: NotationEnv.value -> string
+val pp_value_type: NotationEnv.value_type -> string
+
+val pp_pos: NotationPt.child_pos -> string
+val pp_attribute: NotationPt.term_attribute -> string
+
+val pp_cic_appl_pattern: NotationPt.cic_appl_pattern -> string
+
+ (** non re-entrant change of pp_term function above *)
+val set_pp_term: (NotationPt.term -> string) -> unit
+
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+(** CIC Notation Parse Tree *)
+
+type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
+type induction_kind = [ `Inductive | `CoInductive ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
+CicUniv.universe | `NType of string |`NCProp of string]
+type fold_kind = [ `Left | `Right ]
+
+type location = Stdpp.location
+let fail floc msg =
+ let (x, y) = HExtlib.loc_of_floc floc in
+ failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
+
+type href = UriManager.uri
+
+type child_pos = [ `Left | `Right | `Inner ]
+
+type term_attribute =
+ [ `Loc of location (* source file location *)
+ | `IdRef of string (* ACic pointer *)
+ | `Level of int
+ | `XmlAttrs of (string option * string * string) list
+ (* list of XML attributes: namespace, name, value *)
+ | `Raw of string (* unparsed version *)
+ ]
+
+type literal =
+ [ `Symbol of string
+ | `Keyword of string
+ | `Number of string
+ ]
+
+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 = 6
+
+type term =
+ (* CIC AST *)
+
+ | AttributedTerm of term_attribute * term
+
+ | Appl of term list
+ | 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 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.
+ * Some [] -> user has given an empty explicit substitution list
+ * None -> user has given no explicit substitution list *)
+ | Implicit of [`Vector | `JustOne | `Tagged of string]
+ | Meta of int * meta_subst list
+ | Num of string * int (* literal, instance *)
+ | Sort of sort_kind
+ | Symbol of string * int (* canonical name, instance *)
+
+ | UserInput (* place holder for user input, used by MatitaConsole, not to be
+ used elsewhere *)
+ | Uri of string * subst list option (* as Ident, for long names *)
+ | NRef of NReference.reference
+
+ | NCic of NCic.term
+
+ (* Syntax pattern extensions *)
+
+ | Literal of literal
+ | Layout of layout_pattern
+
+ | Magic of magic_term
+ | Variable of pattern_variable
+
+ (* name, type. First component must be Ident or Variable (FreshVar _) *)
+
+and meta_subst = term option
+and subst = string * term
+and case_pattern =
+ Pattern of string * href option * term capture_variable list
+ | Wildcard
+
+and box_kind = H | V | HV | HOV
+and box_spec = box_kind * bool * bool (* kind, spacing, indent *)
+
+and layout_pattern =
+ | Sub of term * term
+ | Sup of term * term
+ | Below of term * term
+ | Above of term * term
+ | Frac of term * term
+ | Over of term * term
+ | Atop of term * term
+ | InfRule of term * term * term
+(* | array of term * literal option * literal option
+ |+ column separator, row separator +| *)
+ | Maction of term list
+ | Sqrt of term
+ | Root of term * term (* argument, index *)
+ | Break
+ | Box of box_spec * term list
+ | Group of term list
+ | Mstyle of (string * string) list * term list
+ | Mpadded of (string * string) list * term list
+
+and magic_term =
+ (* level 1 magics *)
+ | List0 of term * literal option (* pattern, separator *)
+ | List1 of term * literal option (* pattern, separator *)
+ | Opt of term
+
+ (* level 2 magics *)
+ | Fold of fold_kind * term * string list * term
+ (* base case pattern, recursive case bound names, recursive case pattern *)
+ | Default of term * term (* "some" case pattern, "none" case pattern *)
+ | Fail
+ | If of term * term * term (* test, pattern if true, pattern if false *)
+
+and term_level = Self of int | Level of int
+
+and pattern_variable =
+ (* level 1 and 2 variables *)
+ | NumVar of string
+ | IdentVar of string
+ | TermVar of string * term_level
+
+ (* level 1 variables *)
+ | Ascription of term * string
+
+ (* level 2 variables *)
+ | FreshVar of string
+
+type argument_pattern =
+ | IdentArg of int * string (* eta-depth, name *)
+
+type cic_appl_pattern =
+ | UriPattern of UriManager.uri
+ | NRefPattern of NReference.reference
+ | VarPattern of string
+ | ImplicitPattern
+ | ApplPattern of cic_appl_pattern list
+
+ (** <name, inductive/coinductive, type, constructor list>
+ * true means inductive, false coinductive *)
+type 'term inductive_type = string * bool * 'term * (string * 'term) 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 * NCic.def_pragma
+ (** flavour, name, type, body
+ * - name is absent when an unnamed theorem is being proved, tipically in
+ * interactive usage
+ * - body is present when its given along with the command, otherwise it
+ * will be given in proof editing mode using the tactical language,
+ * unless the flavour is an Axiom
+ *)
+ | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
+ (** left parameters, name, type, fields *)
+
+(** {2 Standard precedences} *)
+
+let let_in_prec = 10
+let binder_prec = 20
+let apply_prec = 70
+let simple_prec = 90
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+module Ast = NotationPt
+
+let visit_ast ?(special_k = fun _ -> assert false)
+ ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x)
+ ?(map_case_outtype=
+ fun k x -> match x with None -> None | Some x -> Some (k x))
+ k
+=
+ let rec aux = function
+ | Ast.Appl terms -> Ast.Appl (List.map k terms)
+ | Ast.Binder (kind, var, body) ->
+ Ast.Binder (kind, aux_capture_variable var, k body)
+ | Ast.Case (term, indtype, typ, patterns) ->
+ Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ,
+ aux_patterns map_xref_option patterns)
+ | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
+ | Ast.LetIn (var, t1, t3) ->
+ Ast.LetIn (aux_capture_variable var, k t1, k t3)
+ | Ast.LetRec (kind, definitions, term) ->
+ let definitions =
+ List.map
+ (fun (params, var, ty, decrno) ->
+ List.map aux_capture_variable params, aux_capture_variable var,
+ k ty, decrno)
+ definitions
+ in
+ Ast.LetRec (kind, definitions, k term)
+ | Ast.Ident (name, Some substs) ->
+ Ast.Ident (name, Some (aux_substs substs))
+ | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
+ | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
+ | (Ast.AttributedTerm _
+ | Ast.Layout _
+ | Ast.Literal _
+ | Ast.Magic _
+ | Ast.Variable _) as t -> special_k t
+ | (Ast.Ident _
+ | Ast.NRef _
+ | Ast.NCic _
+ | Ast.Implicit _
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.Uri _
+ | Ast.UserInput) as t -> t
+ and aux_opt = function
+ | None -> None
+ | Some term -> Some (k term)
+ and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
+ and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns
+ and aux_pattern k_xref =
+ function
+ Ast.Pattern (head, hrefs, vars), term ->
+ Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
+ | Ast.Wildcard, term -> Ast.Wildcard, k term
+ and aux_subst (name, term) = (name, k term)
+ and aux_substs substs = List.map aux_subst substs
+ in
+ aux
+
+let visit_layout k = function
+ | Ast.Sub (t1, t2) -> Ast.Sub (k t1, k t2)
+ | Ast.Sup (t1, t2) -> Ast.Sup (k t1, k t2)
+ | Ast.Below (t1, t2) -> Ast.Below (k t1, k t2)
+ | Ast.Above (t1, t2) -> Ast.Above (k t1, k t2)
+ | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
+ | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
+ | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+ | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
+ | Ast.Sqrt t -> Ast.Sqrt (k t)
+ | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
+ | Ast.Break -> Ast.Break
+ | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
+ | Ast.Group terms -> Ast.Group (List.map k terms)
+ | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
+ | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+ | Ast.Maction terms -> Ast.Maction (List.map k terms)
+
+let visit_magic k = function
+ | Ast.List0 (t, l) -> Ast.List0 (k t, l)
+ | Ast.List1 (t, l) -> Ast.List1 (k t, l)
+ | Ast.Opt t -> Ast.Opt (k t)
+ | Ast.Fold (kind, t1, names, t2) -> Ast.Fold (kind, k t1, names, k t2)
+ | Ast.Default (t1, t2) -> Ast.Default (k t1, k t2)
+ | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3)
+ | Ast.Fail -> Ast.Fail
+
+let visit_variable k = function
+ | Ast.NumVar _
+ | Ast.IdentVar _
+ | Ast.TermVar _
+ | Ast.FreshVar _ as t -> t
+ | Ast.Ascription (t, s) -> Ast.Ascription (k t, s)
+
+let variables_of_term t =
+ let rec vars = ref [] in
+ let add_variable v =
+ if List.mem v !vars then ()
+ else vars := v :: !vars
+ in
+ let rec aux = function
+ | Ast.Magic m -> Ast.Magic (visit_magic aux m)
+ | Ast.Layout l -> Ast.Layout (visit_layout aux l)
+ | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | Ast.Literal _ as t -> t
+ | Ast.AttributedTerm (_, t) -> aux t
+ | t -> visit_ast aux t
+ and aux_variable = function
+ | (Ast.NumVar _
+ | Ast.IdentVar _
+ | Ast.TermVar _) as t ->
+ add_variable t ;
+ t
+ | Ast.FreshVar _ as t -> t
+ | Ast.Ascription _ -> assert false
+ in
+ ignore (aux t) ;
+ !vars
+
+let names_of_term t =
+ let aux = function
+ | Ast.NumVar s
+ | Ast.IdentVar s
+ | Ast.TermVar (s,_) -> s
+ | _ -> assert false
+ in
+ List.map aux (variables_of_term t)
+
+let keywords_of_term t =
+ let rec keywords = ref [] in
+ let add_keyword k = keywords := k :: !keywords in
+ let rec aux = function
+ | Ast.AttributedTerm (_, t) -> aux t
+ | Ast.Layout l -> Ast.Layout (visit_layout aux l)
+ | Ast.Literal (`Keyword k) as t ->
+ add_keyword k;
+ t
+ | Ast.Literal _ as t -> t
+ | Ast.Magic m -> Ast.Magic (visit_magic aux m)
+ | Ast.Variable _ as v -> v
+ | t -> visit_ast aux t
+ in
+ ignore (aux t) ;
+ !keywords
+
+let rec strip_attributes t =
+ let special_k = function
+ | Ast.AttributedTerm (_, term) -> strip_attributes term
+ | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m)
+ | Ast.Variable _ as t -> t
+ | t -> assert false
+ in
+ visit_ast ~special_k strip_attributes t
+
+let rec get_idrefs =
+ function
+ | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
+ | Ast.AttributedTerm (_, t) -> get_idrefs t
+ | _ -> []
+
+let meta_names_of_term term =
+ let rec names = ref [] in
+ let add_name n =
+ if List.mem n !names then ()
+ else names := n :: !names
+ in
+ let rec aux = function
+ | Ast.AttributedTerm (_, term) -> aux term
+ | Ast.Appl terms -> List.iter aux terms
+ | Ast.Binder (_, _, body) -> aux body
+ | Ast.Case (term, indty, outty_opt, patterns) ->
+ aux term ;
+ aux_opt outty_opt ;
+ List.iter aux_branch patterns
+ | Ast.LetIn (_, t1, t3) ->
+ aux t1 ;
+ aux t3
+ | Ast.LetRec (_, definitions, body) ->
+ List.iter aux_definition definitions ;
+ aux body
+ | Ast.Uri (_, Some substs) -> aux_substs substs
+ | Ast.Ident (_, Some substs) -> aux_substs substs
+ | Ast.Meta (_, substs) -> aux_meta_substs substs
+
+ | Ast.Implicit _
+ | Ast.Ident _
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.Uri _
+ | Ast.UserInput -> ()
+
+ | Ast.Magic magic -> aux_magic magic
+ | Ast.Variable var -> aux_variable var
+
+ | _ -> assert false
+ and aux_opt = function
+ | Some term -> aux term
+ | None -> ()
+ and aux_capture_var (_, ty_opt) = aux_opt ty_opt
+ and aux_branch (pattern, term) =
+ aux_pattern pattern ;
+ aux term
+ and aux_pattern =
+ function
+ Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+ | Ast.Wildcard -> ()
+ and aux_definition (params, var, term, decrno) =
+ List.iter aux_capture_var params ;
+ aux_capture_var var ;
+ aux term
+ and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
+ and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
+ and aux_variable = function
+ | Ast.NumVar name -> add_name name
+ | Ast.IdentVar name -> add_name name
+ | Ast.TermVar (name,_) -> add_name name
+ | Ast.FreshVar _ -> ()
+ | Ast.Ascription _ -> assert false
+ and aux_magic = function
+ | Ast.Default (t1, t2)
+ | Ast.Fold (_, t1, _, t2) ->
+ aux t1 ;
+ aux t2
+ | Ast.If (t1, t2, t3) ->
+ aux t1 ;
+ aux t2 ;
+ aux t3
+ | Ast.Fail -> ()
+ | _ -> assert false
+ in
+ aux term ;
+ !names
+
+let rectangular matrix =
+ let columns = Array.length matrix.(0) in
+ try
+ Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix;
+ true
+ with Exit -> false
+
+let ncombine ll =
+ let matrix = Array.of_list (List.map Array.of_list ll) in
+ assert (rectangular matrix);
+ let rows = Array.length matrix in
+ let columns = Array.length matrix.(0) in
+ let lists = ref [] in
+ for j = 0 to columns - 1 do
+ let l = ref [] in
+ for i = 0 to rows - 1 do
+ l := matrix.(i).(j) :: !l
+ done;
+ lists := List.rev !l :: !lists
+ done;
+ List.rev !lists
+
+let string_of_literal = function
+ | `Symbol s
+ | `Keyword s
+ | `Number s -> s
+
+let boxify = function
+ | [ a ] -> a
+ | l -> Ast.Layout (Ast.Box ((Ast.H, false, false), l))
+
+let unboxify = function
+ | Ast.Layout (Ast.Box ((Ast.H, false, false), [ a ])) -> a
+ | l -> l
+
+let group = function
+ | [ a ] -> a
+ | l -> Ast.Layout (Ast.Group l)
+
+let ungroup =
+ let rec aux acc =
+ function
+ [] -> List.rev acc
+ | Ast.Layout (Ast.Group terms) :: terms' -> aux acc (terms @ terms')
+ | term :: terms -> aux (term :: acc) terms
+ in
+ aux []
+
+let dress ~sep:sauce =
+ let rec aux =
+ function
+ | [] -> []
+ | [hd] -> [hd]
+ | hd :: tl -> hd :: sauce :: aux tl
+ in
+ aux
+
+let dressn ~sep:sauces =
+ let rec aux =
+ function
+ | [] -> []
+ | [hd] -> [hd]
+ | hd :: tl -> hd :: sauces @ aux tl
+ in
+ aux
+
+let find_appl_pattern_uris ap =
+ let rec aux acc =
+ function
+ | Ast.UriPattern uri -> `Uri uri :: acc
+ | Ast.NRefPattern nref -> `NRef nref :: acc
+ | Ast.ImplicitPattern
+ | Ast.VarPattern _ -> acc
+ | Ast.ApplPattern apl -> List.fold_left aux acc apl
+ in
+ let uris = aux [] ap in
+ let cmp u1 u2 =
+ match u1,u2 with
+ `Uri u1, `Uri u2 -> UriManager.compare u1 u2
+ | `NRef r1, `NRef r2 -> NReference.compare r1 r2
+ | `Uri _,`NRef _ -> -1
+ | `NRef _, `Uri _ -> 1
+ in
+ HExtlib.list_uniq (List.fast_sort cmp uris)
+
+let rec find_branch =
+ function
+ Ast.Magic (Ast.If (_, Ast.Magic Ast.Fail, t)) -> find_branch t
+ | Ast.Magic (Ast.If (_, t, _)) -> find_branch t
+ | t -> t
+
+let cic_name_of_name = function
+ | Ast.Ident ("_", None) -> Cic.Anonymous
+ | Ast.Ident (name, None) -> Cic.Name name
+ | _ -> assert false
+
+let name_of_cic_name =
+(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *)
+ (* ZACK why we used to generate dummy xrefs? *)
+ let add_dummy_xref t = t in
+ function
+ | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None))
+ | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None))
+
+let fresh_index = ref ~-1
+
+type notation_id = int
+
+let fresh_id () =
+ incr fresh_index;
+ !fresh_index
+
+ (* TODO ensure that names generated by fresh_var do not clash with user's *)
+ (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
+
+let rec freshen_term ?(index = ref 0) term =
+ let freshen_term = freshen_term ~index in
+ let fresh_instance () = incr index; !index in
+ let special_k = function
+ | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, freshen_term t)
+ | Ast.Layout l -> Ast.Layout (visit_layout freshen_term l)
+ | Ast.Magic m -> Ast.Magic (visit_magic freshen_term m)
+ | Ast.Variable v -> Ast.Variable (visit_variable freshen_term v)
+ | Ast.Literal _ as t -> t
+ | _ -> assert false
+ in
+ match term with
+ | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
+ | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
+ | t -> visit_ast ~special_k freshen_term t
+
+let freshen_obj obj =
+ let index = ref 0 in
+ let freshen_term = freshen_term ~index in
+ let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
+ let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
+ let freshen_capture_variables =
+ List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
+ in
+ match obj with
+ | NotationPt.Inductive (params, indtypes) ->
+ let indtypes =
+ List.map
+ (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
+ indtypes
+ in
+ NotationPt.Inductive (freshen_capture_variables params, indtypes)
+ | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+ let ty_opt =
+ match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
+ in
+ NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+ | NotationPt.Record (params, n, ty, fields) ->
+ NotationPt.Record (freshen_capture_variables params, n,
+ freshen_term ty, freshen_name_ty_b fields)
+
+let freshen_term = freshen_term ?index:None
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val fresh_name: unit -> string
+
+val variables_of_term: NotationPt.term -> NotationPt.pattern_variable list
+val names_of_term: NotationPt.term -> string list
+
+ (** extract all keywords (i.e. string literals) from a level 1 pattern *)
+val keywords_of_term: NotationPt.term -> string list
+
+val visit_ast:
+ ?special_k:(NotationPt.term -> NotationPt.term) ->
+ ?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
+ ?map_case_indty:(NotationPt.case_indtype option ->
+ NotationPt.case_indtype option) ->
+ ?map_case_outtype:((NotationPt.term -> NotationPt.term) ->
+ NotationPt.term option -> NotationPt.term
+ option) ->
+ (NotationPt.term -> NotationPt.term) ->
+ NotationPt.term ->
+ NotationPt.term
+
+val visit_layout:
+ (NotationPt.term -> NotationPt.term) ->
+ NotationPt.layout_pattern ->
+ NotationPt.layout_pattern
+
+val visit_magic:
+ (NotationPt.term -> NotationPt.term) ->
+ NotationPt.magic_term ->
+ NotationPt.magic_term
+
+val visit_variable:
+ (NotationPt.term -> NotationPt.term) ->
+ NotationPt.pattern_variable ->
+ NotationPt.pattern_variable
+
+val strip_attributes: NotationPt.term -> NotationPt.term
+
+ (** @return the list of proper (i.e. non recursive) IdRef of a term *)
+val get_idrefs: NotationPt.term -> string list
+
+ (** generalization of List.combine to n lists *)
+val ncombine: 'a list list -> 'a list list
+
+val string_of_literal: NotationPt.literal -> string
+
+val dress: sep:'a -> 'a list -> 'a list
+val dressn: sep:'a list -> 'a list -> 'a list
+
+val boxify: NotationPt.term list -> NotationPt.term
+val group: NotationPt.term list -> NotationPt.term
+val ungroup: NotationPt.term list -> NotationPt.term list
+
+val find_appl_pattern_uris:
+ NotationPt.cic_appl_pattern ->
+ [`Uri of UriManager.uri | `NRef of NReference.reference] list
+
+val find_branch:
+ NotationPt.term -> NotationPt.term
+
+val cic_name_of_name: NotationPt.term -> Cic.name
+val name_of_cic_name: Cic.name -> NotationPt.term
+
+ (** Symbol/Numbers instances *)
+
+val freshen_term: NotationPt.term -> NotationPt.term
+val freshen_obj: NotationPt.term NotationPt.obj -> NotationPt.term NotationPt.obj
+
+ (** Notation id handling *)
+
+type notation_id
+
+val fresh_id: unit -> notation_id
+
open Printf
-module Ast = CicNotationPt
-module Env = CicNotationEnv
+module Ast = NotationPt
+module Env = NotationEnv
exception Parse_error of string
exception Level_not_found of int
| Env of (string * Env.value_type) list
let make_action action bindings =
- let rec aux (vl : CicNotationEnv.t) =
+ let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
(fun (v:'a list) ->
aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
| Env _ :: tl ->
- Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
+ Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl)
(* LUCA: DEFCON 3 END *)
in
aux [] (List.rev bindings)
| Ast.Magic m -> aux_magic m
| Ast.Variable v -> aux_variable v
| t ->
- prerr_endline (CicNotationPp.pp_term t);
+ prerr_endline (NotationPp.pp_term t);
assert false
and aux_literal =
function
match magic with
| Ast.Opt p ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
- let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
+ let action (env_opt : NotationEnv.t option) (loc : Ast.location) =
match env_opt with
| Some env -> List.map Env.opt_binding_some env
| None -> List.map Env.opt_binding_of_name p_names
| Ast.List0 (p, _)
| Ast.List1 (p, _) ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
- let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
- CicNotationEnv.coalesce_env p_names env_list
+ let action (env_list : NotationEnv.t list) (loc : Ast.location) =
+ NotationEnv.coalesce_env p_names env_list
in
let gram_of_list s =
match magic with
let p_bindings, p_atoms = List.split (aux p) in
let p_names = flatten_opt p_bindings in
let action =
- make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
+ make_action (fun (env : NotationEnv.t) (loc : Ast.location) -> env)
p_bindings
in
p_bindings, p_atoms, p_names, action
let initial_owned_keywords () = Hashtbl.create 23
let owned_keywords = ref (initial_owned_keywords ())
-type checked_l1_pattern = CL1P of CicNotationPt.term * int
+type checked_l1_pattern = CL1P of NotationPt.term * int
let check_l1_pattern level1_pattern pponly level associativity =
let variables = ref 0 in
raise (Parse_error ("You can not specify an associative notation " ^
"at level "^string_of_int min_precedence ^ "; increase it"));
let cp = aux level1_pattern in
-(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *)
+(* prerr_endline ("checked_pattern: " ^ NotationPp.pp_term cp); *)
if !variables <> 2 && associativity <> Gramext.NonA then
raise (Parse_error ("Exactly 2 variables must be specified in an "^
"associative notation"));
Some (*Gramext.NonA*) Gramext.NonA,
[ p_atoms,
(make_action
- (fun (env: CicNotationEnv.t) (loc: Ast.location) ->
+ (fun (env: NotationEnv.t) (loc: Ast.location) ->
(action env loc))
p_bindings) ]]]
in
- let keywords = CicNotationUtil.keywords_of_term level1_pattern in
+ let keywords = NotationUtil.keywords_of_term level1_pattern in
let rule_id = p_atoms in
List.iter CicNotationLexer.add_level2_ast_keyword keywords;
Hashtbl.add !owned_keywords rule_id keywords; (* keywords may be [] *)
GLOBAL: level1_pattern;
level1_pattern: [
- [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ]
+ [ p = l1_pattern; EOI -> fun l -> NotationUtil.boxify (p l) ]
];
l1_pattern: [
[ p = LIST1 l1_simple_pattern ->
| "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
- CicNotationUtil.group (x l)) m)))
+ NotationUtil.group (x l)) m)))
| LPAREN; p = l1_pattern; RPAREN ->
- return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
+ return_term_of_level loc (fun l -> NotationUtil.group (p l))
]
| "simple" NONA
[ i = IDENT ->
let rec find_arg name n = function
| [] ->
Ast.fail loc (sprintf "Argument %s not found"
- (CicNotationPp.pp_term name))
+ (NotationPp.pp_term name))
| (l,_) :: tl ->
(match position_of name 0 l with
| None, len -> find_arg name (n + len) tl
exception Parse_error of string
exception Level_not_found of int
-type checked_l1_pattern = private CL1P of CicNotationPt.term * int
+type checked_l1_pattern = private CL1P of NotationPt.term * int
(** {2 Parsing functions} *)
(** concrete syntax pattern: notation level 1, the
* integer is the precedence *)
-val parse_level1_pattern: int -> Ulexing.lexbuf -> CicNotationPt.term
+val parse_level1_pattern: int -> Ulexing.lexbuf -> NotationPt.term
(** AST pattern: notation level 2 *)
-val parse_level2_ast: Ulexing.lexbuf -> CicNotationPt.term
-val parse_level2_meta: Ulexing.lexbuf -> CicNotationPt.term
+val parse_level2_ast: Ulexing.lexbuf -> NotationPt.term
+val parse_level2_meta: Ulexing.lexbuf -> NotationPt.term
(** {2 Grammar extension} *)
val compare_rule_id : rule_id -> rule_id -> int
val check_l1_pattern: (* level1_pattern, pponly, precedence, assoc *)
- CicNotationPt.term -> bool -> int -> Gramext.g_assoc -> checked_l1_pattern
+ NotationPt.term -> bool -> int -> Gramext.g_assoc -> checked_l1_pattern
val extend:
checked_l1_pattern ->
- (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) ->
+ (NotationEnv.t -> NotationPt.location -> NotationPt.term) ->
rule_id
val delete: rule_id -> unit
val level2_ast_grammar: unit -> Grammar.g
-val term : unit -> CicNotationPt.term Grammar.Entry.e
+val term : unit -> NotationPt.term Grammar.Entry.e
val let_defs : unit ->
- (CicNotationPt.term CicNotationPt.capture_variable list * CicNotationPt.term CicNotationPt.capture_variable * CicNotationPt.term * int) list
+ (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list
Grammar.Entry.e
val protected_binder_vars : unit ->
- (CicNotationPt.term list * CicNotationPt.term option) Grammar.Entry.e
+ (NotationPt.term list * NotationPt.term option) Grammar.Entry.e
-val parse_term: Ulexing.lexbuf -> CicNotationPt.term
+val parse_term: Ulexing.lexbuf -> NotationPt.term
(** {2 Debugging} *)
open Printf
-module Ast = CicNotationPt
+module Ast = NotationPt
module Mpres = Mpresentation
type mathml_markup = boxml_markup Mpres.mpres
let kind, spacing, indent = spec in
let dress children =
if spacing then
- CicNotationUtil.dress small_skip children
+ NotationUtil.dress small_skip children
else
children
in
let substs' =
box_of mathonly (A.H, false, false) []
(open_brace
- :: (CicNotationUtil.dress semicolon
+ :: (NotationUtil.dress semicolon
(List.map
(fun (name, t) ->
box_of mathonly (A.H, false, false) [] [
let local_context l =
box_of mathonly (A.H, false, false) []
([ Mpres.Mtext ([], "[") ] @
- (CicNotationUtil.dress (Mpres.Mtext ([], ";"))
+ (NotationUtil.dress (Mpres.Mtext ([], ";"))
(List.map
(function
| None -> Mpres.Mtext ([], "_")
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
| t ->
- prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
+ prerr_endline ("unexpected ast: " ^ NotationPp.pp_term t);
assert false
and aux_attributes xmlattrs mathonly xref prec t =
let reset = ref false in
then ((*prerr_endline "reset";*)t')
else add_parens child_prec prec t')
in
-(* prerr_endline (CicNotationPp.pp_term t); *)
+(* prerr_endline (NotationPp.pp_term t); *)
aux_attribute t
and aux_literal xmlattrs xref prec l =
let attrs = make_href xmlattrs xref in
| A.Box ((_, spacing, _) as kind, terms) ->
let children =
aux_children mathonly spacing xref prec
- (CicNotationUtil.ungroup terms)
+ (NotationUtil.ungroup terms)
in
box_of mathonly kind attrs children
| A.Mstyle (l,terms) ->
(List.map (fun (k,v) -> None,k,v) l,
box_of mathonly (A.H, false, false) attrs
(aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)))
+ (NotationUtil.ungroup terms)))
| A.Mpadded (l,terms) ->
Mpres.Mpadded
(List.map (fun (k,v) -> None,k,v) l,
box_of mathonly (A.H, false, false) attrs
(aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)))
+ (NotationUtil.ungroup terms)))
| A.Maction alternatives ->
toggle_action (List.map invoke_reinit alternatives)
| A.Group terms ->
let children =
aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)
+ (NotationUtil.ungroup terms)
in
box_of mathonly (A.H, false, false) attrs children
| A.Break -> assert false (* TODO? *)
* @param ids_to_uris mapping id -> uri for hyperlinking
* @param prec precedence level *)
val render:
- lookup_uri:(Cic.id -> string option) -> ?prec:int -> CicNotationPt.term ->
+ lookup_uri:(Cic.id -> string option) -> ?prec:int -> NotationPt.term ->
markup
(** level 0 -> xml stream *)
(* |+* level 1 -> xml stream
* @param ids_to_uris +|
val render_to_boxml:
- (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t *)
+ (Cic.id, string) Hashtbl.t -> NotationPt.term -> Xml.token Stream.t *)
val print_box: boxml_markup -> Xml.token Stream.t
val print_mpres: mathml_markup -> Xml.token Stream.t
let name = match d.Content.def_name with Some x -> x|_->assert false in
let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
let ty = d.Content.def_type in
- let module P = CicNotationPt in
+ let module P = NotationPt in
let rec split_pi i t =
if i <= 1 then
match t with
let ncontent2pres0
?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
- (id,params,metasenv,obj : CicNotationPt.term Content.cobj)
+ (id,params,metasenv,obj : NotationPt.term Content.cobj)
=
match obj with
| `Def (Content.Const, thesis, `Proof p) ->
val ncontent2pres:
?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool ->
ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t ->
- CicNotationPt.term Content.cobj ->
+ NotationPt.term Content.cobj ->
CicNotationPres.boxml_markup
open Printf
-module Ast = CicNotationPt
-module Env = CicNotationEnv
-module Pp = CicNotationPp
-module Util = CicNotationUtil
+module Ast = NotationPt
+module Env = NotationEnv
+module Pp = NotationPp
+module Util = NotationUtil
let get_tag term0 =
let subterms = ref [] in
Ast.Implicit `JustOne
in
let rec aux t =
- CicNotationUtil.visit_ast
+ NotationUtil.visit_ast
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
| _ -> PatternMatcher.Constructor
let tag_of_pattern = get_tag
let tag_of_term t = get_tag t
- let string_of_term = CicNotationPp.pp_term
- let string_of_pattern = CicNotationPp.pp_term
+ let string_of_term = NotationPp.pp_term
+ let string_of_pattern = NotationPp.pp_term
end
module M = PatternMatcher.Matcher (Pattern21)
sig
(** @param l2_patterns level 2 (AST) patterns *)
val compiler :
- (CicNotationPt.term * int) list ->
- (CicNotationPt.term ->
- (CicNotationEnv.t * CicNotationPt.term list * int) option)
+ (NotationPt.term * int) list ->
+ (NotationPt.term ->
+ (NotationEnv.t * NotationPt.term list * int) option)
end
val nsequent2pres :
ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t ->
- subst:NCic.substitution -> CicNotationPt.term Content.conjecture ->
+ subst:NCic.substitution -> NotationPt.term Content.conjecture ->
CicNotationPres.boxml_markup
open Printf
-module Ast = CicNotationPt
-module Env = CicNotationEnv
+module Ast = NotationPt
+module Env = NotationEnv
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
in
add_level_info Ast.apply_prec
- (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
+ (hovbox true true (NotationUtil.dress break (aux_args 70 ts)))
| Ast.Binder (binder_kind, (id, ty), body) ->
add_level_info Ast.binder_prec
(hvbox false true
| Ast.Uri (_, None) | Ast.Uri (_, Some [])
| Ast.Literal _
| Ast.UserInput as leaf -> leaf
- | t -> CicNotationUtil.visit_ast ~special_k k t
+ | t -> NotationUtil.visit_ast ~special_k k t
and aux_sort sort_kind = xml_of_sort sort_kind
and aux_ty = function
| None -> builtin_symbol "?"
and special_k = function
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
| t ->
- prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t);
+ prerr_endline ("unexpected special: " ^ NotationPp.pp_term t);
assert false
in
aux t
function
Ast.AttributedTerm (attr, t) ->
Ast.AttributedTerm (attr, subst_singleton pos env t)
- | t -> CicNotationUtil.group (subst pos env t)
+ | t -> NotationUtil.group (subst pos env t)
and subst pos env = function
| Ast.AttributedTerm (attr, t) ->
-(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
+(* prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *)
subst pos env t
| Ast.Variable var ->
- let name, expected_ty = CicNotationEnv.declaration_of_var var in
+ let name, expected_ty = NotationEnv.declaration_of_var var in
let ty, value =
try
List.assoc name env
prerr_endline ("name " ^ name ^ " not found in environment");
assert false
in
- assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
+ assert (NotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
- if not (CicNotationEnv.well_typed expected_ty value) then
+ if not (NotationEnv.well_typed expected_ty value) then
begin
prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration");
assert false
end;
- let value = CicNotationEnv.term_of_value value in
+ let value = NotationEnv.term_of_value value in
let value =
match expected_ty with
| Env.TermType l -> Ast.AttributedTerm (`Level l,value)
| `Keyword k -> [ add_keyword_attrs t ]
| _ -> [ t ])
| Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
- | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ]
+ | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
- let rec_decls = CicNotationEnv.declarations_of_term p in
+ let rec_decls = NotationEnv.declarations_of_term p in
let rec_values =
- List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
+ List.map (fun (n, _) -> NotationEnv.lookup_list env n) rec_decls
in
- let values = CicNotationUtil.ncombine rec_values in
+ let values = NotationUtil.ncombine rec_values in
let sep =
match sep_opt with
| None -> []
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->
- let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list (CicNotationUtil.group (subst pos env p) :: acc)
+ let env = NotationEnv.combine rec_decls value_set in
+ instantiate_list (NotationUtil.group (subst pos env p) :: acc)
[]
| value_set :: tl ->
- let env = CicNotationEnv.combine rec_decls value_set in
+ let env = NotationEnv.combine rec_decls value_set in
let terms = subst pos env p in
- instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
+ instantiate_list (NotationUtil.group (terms @ sep) :: acc) tl
in
if values = [] then []
else [hovbox false false (instantiate_list [] values)]
| Ast.Opt p ->
- let opt_decls = CicNotationEnv.declarations_of_term p in
+ let opt_decls = NotationEnv.declarations_of_term p in
let env =
let rec build_env = function
| [] -> []
| (name, ty) :: tl ->
(* assumption: if one of the value is None then all are *)
- (match CicNotationEnv.lookup_opt env name with
+ (match NotationEnv.lookup_opt env name with
| None -> raise Exit
| Some v -> (name, (ty, v)) :: build_env tl)
in
| Ast.Box (kind, tl) ->
let tl' = subst_children pos env tl in
Ast.Box (kind, List.concat tl')
- | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
+ | l -> NotationUtil.visit_layout (subst_singleton pos env) l
and subst_children pos env =
function
| [] -> []
let rec pp_ast1 term =
let rec pp_value = function
- | CicNotationEnv.NumValue _ as v -> v
- | CicNotationEnv.StringValue _ as v -> v
-(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
- | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
- | CicNotationEnv.OptValue None as v -> v
- | CicNotationEnv.OptValue (Some v) ->
- CicNotationEnv.OptValue (Some (pp_value v))
- | CicNotationEnv.ListValue vl ->
- CicNotationEnv.ListValue (List.map pp_value vl)
+ | NotationEnv.NumValue _ as v -> v
+ | NotationEnv.StringValue _ as v -> v
+(* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *)
+ | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 t)
+ | NotationEnv.OptValue None as v -> v
+ | NotationEnv.OptValue (Some v) ->
+ NotationEnv.OptValue (Some (pp_value v))
+ | NotationEnv.ListValue vl ->
+ NotationEnv.ListValue (List.map pp_value vl)
in
let ast_env_of_env env =
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
-(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *)
match term with
| Ast.AttributedTerm (attrs, term') ->
Ast.AttributedTerm (attrs, pp_ast1 term')
| None -> pp_ast0 term pp_ast1
| Some (env, ctors, pid) ->
let idrefs =
- List.flatten (List.map CicNotationUtil.get_idrefs ctors)
+ List.flatten (List.map NotationUtil.get_idrefs ctors)
in
let l1 =
try
let pp_ast ast =
debug_print (lazy "pp_ast <-");
let ast' = pp_ast1 ast in
- debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
+ debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast'));
ast'
exception Pretty_printer_not_found
let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
let id = fresh_id () in
let l1' = add_level_info precedence (fill_pos_info l1) in
- let l2' = CicNotationUtil.strip_attributes l2 in
+ let l2' = NotationUtil.strip_attributes l2 in
Hashtbl.add !level1_patterns21 id l1';
pattern21_matrix := (l2', id) :: !pattern21_matrix;
load_patterns21 !pattern21_matrix;
aux [] env
let instantiate_level2 env term =
-(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *)
+(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
try
List.assoc n !fresh_env
with Not_found ->
- let new_name = CicNotationUtil.fresh_name () in
+ let new_name = NotationUtil.fresh_name () in
fresh_env := (n, new_name) :: !fresh_env;
new_name
in
let rec aux env term =
-(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
+(* prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
match term with
| Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
| Ast.Ascription (term, name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
- let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
- let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
+ let some_pattern_names = NotationUtil.names_of_term some_pattern in
+ let none_pattern_names = NotationUtil.names_of_term none_pattern in
let opt_names =
List.filter
(fun name -> not (List.mem name none_pattern_names))
| _ ->
prerr_endline (sprintf
"lookup of %s in env %s did not return an optional value"
- name (CicNotationPp.pp_env env));
+ name (NotationPp.pp_env env));
assert false))
| Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
List.filter ((<>) acc_name)
- (CicNotationUtil.names_of_term rec_pattern)
+ (NotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
List.filter ((<>) acc_name)
- (CicNotationUtil.names_of_term rec_pattern)
+ (NotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
in
instantiate_fold_right env)
| Ast.If (_, p_true, p_false) as t ->
- aux env (CicNotationUtil.find_branch (Ast.Magic t))
+ aux env (NotationUtil.find_branch (Ast.Magic t))
| Ast.Fail -> assert false
| _ -> assert false
in
type pretty_printer_id
val add_pretty_printer:
- CicNotationPt.term -> (* level 2 pattern *)
+ NotationPt.term -> (* level 2 pattern *)
CicNotationParser.checked_l1_pattern ->
pretty_printer_id
(** {2 content -> pres} *)
-val pp_ast: CicNotationPt.term -> CicNotationPt.term
+val pp_ast: NotationPt.term -> NotationPt.term
(** {2 pres -> content} *)
(** fills a term pattern instantiating variable magics *)
val instantiate_level2:
- CicNotationEnv.t -> CicNotationPt.term ->
- CicNotationPt.term
+ NotationEnv.t -> NotationPt.term ->
+ NotationPt.term
val push: unit -> unit
val pop: unit -> unit
open DisambiguateTypes
open UriManager
-module Ast = CicNotationPt
+module Ast = NotationPt
(* the integer is an offset to be added to each location *)
exception Ambiguous_input
val find_in_context: string -> string option list -> int
val domain_of_term: context:
- string option list -> CicNotationPt.term -> domain
+ string option list -> NotationPt.term -> domain
val domain_of_obj:
- context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
+ context:string option list -> NotationPt.term NotationPt.obj -> domain
val disambiguate_thing:
context:'context ->
'lazy_term option * ('ident * 'term) list * 'term option
type npattern =
- CicNotationPt.term option * (string * CicNotationPt.term) list * CicNotationPt.term option
+ NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option
type 'lazy_term reduction =
[ `Normalize
| `Auto of 'term auto_params ]
type ntactic =
- | NApply of loc * CicNotationPt.term
- | NSmartApply of loc * CicNotationPt.term
- | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list
- | NCases of loc * CicNotationPt.term * npattern
+ | NApply of loc * NotationPt.term
+ | NSmartApply of loc * NotationPt.term
+ | NAssert of loc * ((string * [`Decl of NotationPt.term | `Def of NotationPt.term * NotationPt.term]) list * NotationPt.term) list
+ | NCases of loc * NotationPt.term * npattern
| NCase1 of loc * string
- | NChange of loc * npattern * CicNotationPt.term
- | NConstructor of loc * int option * CicNotationPt.term list
- | NCut of loc * CicNotationPt.term
-(* | NDiscriminate of loc * CicNotationPt.term
- | NSubst of loc * CicNotationPt.term *)
+ | NChange of loc * npattern * NotationPt.term
+ | NConstructor of loc * int option * NotationPt.term list
+ | NCut of loc * NotationPt.term
+(* | NDiscriminate of loc * NotationPt.term
+ | NSubst of loc * NotationPt.term *)
| NDestruct of loc * string list option * string list
- | NElim of loc * CicNotationPt.term * npattern
+ | NElim of loc * NotationPt.term * npattern
| NGeneralize of loc * npattern
| NId of loc
| NIntro of loc * string
| NIntros of loc * string list
- | NInversion of loc * CicNotationPt.term * npattern
- | NLApply of loc * CicNotationPt.term
- | NLetIn of loc * npattern * CicNotationPt.term * string
+ | NInversion of loc * NotationPt.term * npattern
+ | NLApply of loc * NotationPt.term
+ | NLetIn of loc * npattern * NotationPt.term * string
| NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
- | NRewrite of loc * direction * CicNotationPt.term * npattern
- | NAuto of loc * CicNotationPt.term auto_params
+ | NRewrite of loc * direction * NotationPt.term * npattern
+ | NAuto of loc * NotationPt.term auto_params
| NDot of loc
| NSemicolon of loc
| NBranch of loc
(* URI or base-uri, parameters *)
type nmacro =
- | NCheck of loc * CicNotationPt.term
+ | NCheck of loc * NotationPt.term
| Screenshot of loc * string
- | NAutoInteractive of loc * CicNotationPt.term auto_params
+ | NAutoInteractive of loc * NotationPt.term auto_params
| NIntroGuess of loc
(** To be increased each time the command type below changes, used for "safe"
| Qed of loc
type ncommand =
- | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
- | NObj of loc * CicNotationPt.term CicNotationPt.obj
- | NDiscriminator of loc * CicNotationPt.term
- | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option
+ | UnificationHint of loc * NotationPt.term * int (* term, precedence *)
+ | NObj of loc * NotationPt.term NotationPt.obj
+ | NDiscriminator of loc * NotationPt.term
+ | NInverter of loc * string * NotationPt.term * bool list option * NotationPt.term option
| NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NCoercion of loc * string *
- CicNotationPt.term * CicNotationPt.term *
- (string * CicNotationPt.term) * CicNotationPt.term
+ NotationPt.term * NotationPt.term *
+ (string * NotationPt.term) * NotationPt.term
| NQed of loc
type punctuation_tactical =
;;
let rec pp_ntactic ~map_unicode_to_tex =
- let term_pp = CicNotationPp.pp_term in
+ let term_pp = NotationPp.pp_term in
let lazy_term_pp = fun _ -> assert false in
let pp_tactic_pattern =
pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
- | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NApply (_,t) -> "napply " ^ NotationPp.pp_term t
| NSmartApply (_,t) -> "fixme"
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NAuto (_,(Some l,flgs)) ->
"nautobatch" ^ " by " ^
- (String.concat "," (List.map CicNotationPp.pp_term l)) ^
+ (String.concat "," (List.map NotationPp.pp_term l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
- | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+ | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NConstructor (_,None,l) -> "@ " ^
- String.concat " " (List.map CicNotationPp.pp_term l)
+ String.concat " " (List.map NotationPp.pp_term l)
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
- String.concat " " (List.map CicNotationPp.pp_term l)
+ String.concat " " (List.map NotationPp.pp_term l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
- " with " ^ CicNotationPp.pp_term wwhat
- | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
-(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
- | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
+ " with " ^ NotationPp.pp_term wwhat
+ | NCut (_,t) -> "ncut " ^ NotationPp.pp_term t
+(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t
+ | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *)
| NDestruct (_,dom,skip) -> "ndestruct ..."
- | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
+ | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
- | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+ | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^
assert false ^ " " ^ assert false
- | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
+ | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
(match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
- " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
+ " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
| NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
| NDot _ -> "##."
| NSemicolon _ -> "##;"
"(" ^ s ^ ")"
let pp_nmacro = function
- | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term)
+ | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term term)
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
let pp_ncommand ~obj_pp = function
| UnificationHint (_,t, n) ->
- "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t
| NDiscriminator (_,_)
| NInverter (_,_,_,_,_)
| NUnivConstraint (_) -> "not supported"
try
let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm None status [] [] []
- ("",0,CicNotationPt.Ident (name,None)) in
+ ("",0,NotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
let status, nuris =
NCicCoercDeclaration.
val eval_ncoercion:
#GrafiteTypes.status as 'status ->
string ->
- CicNotationPt.term ->
- CicNotationPt.term ->
- string * CicNotationPt.term ->
- CicNotationPt.term -> 'status * [> `New of NUri.uri list ]
+ NotationPt.term ->
+ NotationPt.term ->
+ string * NotationPt.term ->
+ NotationPt.term -> 'status * [> `New of NUri.uri list ]
(* for records, the term is the projection, already refined, while the
* first integer is the number of left params and the second integer is
exception BaseUriNotSetYet
type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
+ (NotationPt.term, NotationPt.term,
+ NotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactic
type lazy_tactic =
type pattern =
- CicNotationPt.term Disambiguate.disambiguator_input option *
+ NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
in
let name =
match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | CicNotationPt.Inductive _ -> assert false
+ | NotationPt.Inductive (_,(name,_,_,_)::_)
+ | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Inductive _ -> assert false
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
exception BaseUriNotSetYet
type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
+ (NotationPt.term, NotationPt.term,
+ NotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactic
type lazy_tactic =
val disambiguate_command:
LexiconEngine.status as 'status ->
?baseuri:string ->
- ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+ ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
'status * (Cic.term,Cic.obj) GrafiteAst.command
val disambiguate_nterm :
NCic.term option ->
(#NEstatus.status as 'status) ->
NCic.context -> NCic.metasenv -> NCic.substitution ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
+ NotationPt.term Disambiguate.disambiguator_input ->
NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
#NEstatus.status as 'status ->
?baseuri:string ->
- (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+ (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
'status * NCic.obj
type pattern =
- CicNotationPt.term Disambiguate.disambiguator_input option *
+ NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
val disambiguate_npattern:
(* $Id$ *)
-module N = CicNotationPt
+module N = NotationPt
module G = GrafiteAst
module L = LexiconAst
module LE = LexiconEngine
| N.Implicit _ -> false
| N.UserInput -> true
| _ -> raise (Invalid_argument "malformed target parameter list 1")) l
- | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
+ | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ]
];
direction: [
[ SYMBOL ">" -> `LeftToRight
| IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
let urify = function
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+ | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
| _ -> raise (Failure "only a Type[…] sort can be constrained")
in
| LNone of GrafiteAst.loc
type ast_statement =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.term CicNotationPt.obj, string)
+ (NotationPt.term, NotationPt.term,
+ NotationPt.term GrafiteAst.reduction,
+ NotationPt.term NotationPt.obj, string)
GrafiteAst.statement
exception NoInclusionPerformed of string (* full path *)
let process_stream istream =
let char_count = ref 0 in
- let module P = CicNotationPt in
+ let module P = NotationPt in
let module G = GrafiteAst in
let status =
ref
| None -> ()
| Some id ->
prerr_endline "removing last notation rule ...";
- CicNotationParser.delete id) *)
+ NotationParser.delete id) *)
| G.Executable (_, G.Macro (_, G.Check (_, t))) ->
- prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t));
+ prerr_endline (sprintf "ast: %s" (NotationPp.pp_term t));
let t' = TermContentPres.pp_ast t in
prerr_endline (sprintf "rendered ast: %s"
- (CicNotationPp.pp_term t'));
+ (NotationPp.pp_term t'));
let tbl = Hashtbl.create 0 in
dump_xml t' tbl "out.xml"
| statement ->
GrafiteAstPp.pp_statement
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- ~term_pp:CicNotationPp.pp_term
+ ~term_pp:NotationPp.pp_term
~lazy_term_pp:(fun _ -> "_lazy_term_here_")
~obj_pp:(fun _ -> "_obj_here_")
statement)
let id =
CicNotationParser.extend l1
(fun env loc ->
- CicNotationPt.AttributedTerm
+ NotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
rule_id := [ RuleId id ];
Hashtbl.add !rule_ids_to_items id item
| Include of loc * string * inclusion_mode * string (* _,buri,_,path *)
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
- | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
- int * CicNotationPt.term
+ | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc *
+ int * NotationPt.term
(* direction, l1 pattern, associativity, precedence, l2 pattern *)
| Interpretation of loc *
- string * (string * CicNotationPt.argument_pattern list) *
- CicNotationPt.cic_appl_pattern
+ string * (string * NotationPt.argument_pattern list) *
+ NotationPt.cic_appl_pattern
(* description (i.e. id), symbol, arg pattern, appl pattern *)
(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
+let magic = magic + 10000 * NotationPt.magic
let description_of_alias =
function
open LexiconAst
-let pp_l1_pattern = CicNotationPp.pp_term
-let pp_l2_pattern = CicNotationPp.pp_term
+let pp_l1_pattern = NotationPp.pp_term
+let pp_l2_pattern = NotationPp.pp_term
let pp_alias = function
| Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
let pp_precedence i = sprintf "with precedence %d" i
let pp_argument_pattern = function
- | CicNotationPt.IdentArg (eta_depth, name) ->
+ | NotationPt.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in
for i = 1 to eta_depth do
Buffer.add_string eta_buf "\\eta."
sprintf "interpretation \"%s\" '%s %s = %s."
dsc symbol
(String.concat " " (List.map pp_argument_pattern arg_patterns))
- (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
+ (NotationPp.pp_cic_appl_pattern cic_appl_pattern)
let pp_dir_opt = function
| None -> ""
| L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
let rec disambiguate =
function
- CicNotationPt.ApplPattern l ->
- CicNotationPt.ApplPattern (List.map disambiguate l)
- | CicNotationPt.VarPattern id
+ NotationPt.ApplPattern l ->
+ NotationPt.ApplPattern (List.map disambiguate l)
+ | NotationPt.VarPattern id
when not
(List.exists
- (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
+ (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
->
let item = DisambiguateTypes.Id id in
begin try
match DisambiguateTypes.Environment.find item status.aliases with
L.Ident_alias (_, uri) ->
(try
- CicNotationPt.NRefPattern
+ NotationPt.NRefPattern
(NReference.reference_of_string uri)
with
NReference.IllFormedReference _ ->
- CicNotationPt.UriPattern (UriManager.uri_of_string uri))
+ NotationPt.UriPattern (UriManager.uri_of_string uri))
| _ -> assert false
with Not_found ->
prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
| LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
let rec aux =
function
- | CicNotationPt.UriPattern uri ->
- CicNotationPt.UriPattern (rehash_uri uri)
- | CicNotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
+ | NotationPt.UriPattern uri ->
+ NotationPt.UriPattern (rehash_uri uri)
+ | NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
let uri = NCicLibrary.refresh_uri uri in
- CicNotationPt.NRefPattern (NReference.reference_of_spec uri spec)
- | CicNotationPt.ApplPattern args ->
- CicNotationPt.ApplPattern (List.map aux args)
- | CicNotationPt.VarPattern _
- | CicNotationPt.ImplicitPattern as pat -> pat
+ NotationPt.NRefPattern (NReference.reference_of_spec uri spec)
+ | NotationPt.ApplPattern args ->
+ NotationPt.ApplPattern (List.map aux args)
+ | NotationPt.VarPattern _
+ | NotationPt.ImplicitPattern as pat -> pat
in
let appl_pattern = aux cic_appl_pattern in
LexiconAst.Interpretation (loc, dsc, args, appl_pattern)
open Printf
-module Ast = CicNotationPt
+module Ast = NotationPt
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(* CODICE c&p da NCicPp *)
let nast_of_cic0 status
~(idref:
- ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+ ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
~output_type ~metasenv ~subst k ~context =
function
| NCic.Rel n ->
in
let rec add_lambda t n =
if n > 0 then
- let name = CicNotationUtil.fresh_name () in
+ let name = NotationUtil.fresh_name () in
Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
else
idref
~reference:
(match term with NCic.Const nref -> nref | _ -> assert false)
- (CicNotationPt.Ident ("dummy",None))
+ (NotationPt.Ident ("dummy",None))
in
match attrterm with
Ast.AttributedTerm (`IdRef id, _) -> id
^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast = ast_of_acic1 ~output_type term_info annterm in
- debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
+ debug_print (lazy ("ast_of_acic -> " ^ NotationPp.pp_term ast));
ast, term_info.uri
let fresh_id =
val add_interpretation:
string -> (* id / description *)
- string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
- CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
+ string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
+ NotationPt.cic_appl_pattern -> (* level 3 pattern *)
interpretation_id
(** @raise Interpretation_not_found *)
val lookup_interpretations:
string -> (* symbol *)
- (string * CicNotationPt.argument_pattern list *
- CicNotationPt.cic_appl_pattern) list
+ (string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern) list
exception Interpretation_not_found
val ast_of_acic:
output_type:[`Pattern|`Term] ->
- (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
+ (Cic.id, NotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
Cic.annterm -> (* acic *)
- CicNotationPt.term (* ast *)
+ NotationPt.term (* ast *)
* (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *)
(** {2 content -> acic} *)
mk_appl:('term list -> 'term) ->
mk_implicit:(bool -> 'term) ->
term_of_uri : (UriManager.uri -> 'term) ->
- (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
+ (string * 'term) list -> NotationPt.cic_appl_pattern ->
'term
val push: unit -> unit
val nast_of_cic :
output_type:[`Pattern | `Term ] ->
subst:NCic.substitution -> context:NCic.context -> NCic.term ->
- CicNotationPt.term
+ NotationPt.term
*)
type id = string
val nmap_sequent:
#NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
int * NCic.conjecture ->
- CicNotationPt.term Content.conjecture *
+ NotationPt.term Content.conjecture *
(id, NReference.reference) Hashtbl.t (* id -> reference *)
val nmap_obj:
#NCicCoercion.status -> NCic.obj ->
- CicNotationPt.term Content.cobj *
+ NotationPt.term Content.cobj *
(id, NReference.reference) Hashtbl.t (* id -> reference *)
(* $Id: acic2astMatcher.ml 9271 2008-11-28 18:28:58Z fguidi $ *)
-module Ast = CicNotationPt
-module Util = CicNotationUtil
+module Ast = NotationPt
+module Util = NotationUtil
let reference_of_oxuri = ref (fun _ -> assert false);;
let set_reference_of_oxuri f = reference_of_oxuri := f;;
type pattern_t = Ast.cic_appl_pattern
type term_t = NCic.term
- let string_of_pattern = CicNotationPp.pp_cic_appl_pattern
+ let string_of_pattern = NotationPp.pp_cic_appl_pattern
let string_of_term t =
(*CSC: ??? *)
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
sig
(** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *)
val compiler :
- (CicNotationPt.cic_appl_pattern * int) list ->
+ (NotationPt.cic_appl_pattern * int) list ->
(NCic.term ->
((string * NCic.term) list * NCic.term list * int) option)
end
(fun cic_args ->
let env',rest =
let names =
- List.map (function CicNotationPt.IdentArg (_, name) -> name) args
+ List.map (function NotationPt.IdentArg (_, name) -> name) args
in
let rec combine_with_rest l1 l2 =
match l1,l2 with
mk_implicit: (bool -> 'term) ->
term_of_uri: (UriManager.uri -> 'term) ->
term_of_nref: (NReference.reference -> 'term) ->
- string * CicNotationPt.argument_pattern list *
- CicNotationPt.cic_appl_pattern ->
+ string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern ->
'term codomain_item
open DisambiguateTypes
open UriManager
-module Ast = CicNotationPt
+module Ast = NotationPt
module NRef = NReference
let debug_print s = prerr_endline (Lazy.force s);;
assert (uri = None);
let rec aux ~localize loc context = function
- | CicNotationPt.AttributedTerm (`Loc loc, term) ->
+ | NotationPt.AttributedTerm (`Loc loc, term) ->
let res = aux ~localize loc context term in
if localize then
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
- | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- | CicNotationPt.Appl (CicNotationPt.Appl inner :: args) ->
- aux ~localize loc context (CicNotationPt.Appl (inner @ args))
- | CicNotationPt.Appl
- (CicNotationPt.AttributedTerm (att,(CicNotationPt.Appl inner))::args)->
+ | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
+ | NotationPt.Appl (NotationPt.Appl inner :: args) ->
+ aux ~localize loc context (NotationPt.Appl (inner @ args))
+ | NotationPt.Appl
+ (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
aux ~localize loc context
- (CicNotationPt.AttributedTerm (att,CicNotationPt.Appl (inner @ args)))
- | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
+ (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+ | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
- | CicNotationPt.Appl terms ->
+ | NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
- | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
+ | NotationPt.Binder (binder_kind, (var, typ), body) ->
let cic_type = aux_option ~localize loc context `Type typ in
let cic_name = cic_name_of_name var in
let cic_body = aux ~localize loc (cic_name :: context) body in
| `Exists ->
Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
(`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
- | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
+ | NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context `Term outtype in
let do_branch ((_, _, args), term) =
function
0 -> term
| n ->
- CicNotationPt.Binder
- (`Lambda, (CicNotationPt.Ident ("_", None), None),
+ NotationPt.Binder
+ (`Lambda, (NotationPt.Ident ("_", None), None),
mk_lambdas (n - 1))
in
(("wildcard",None,[]),
let branches = sort branches cl in
NCic.Match (indtype_ref, cic_outtype, cic_term,
(List.map do_branch branches))
- | CicNotationPt.Cast (t1, t2) ->
+ | NotationPt.Cast (t1, t2) ->
let cic_t1 = aux ~localize loc context t1 in
let cic_t2 = aux ~localize loc context t2 in
NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1)
- | CicNotationPt.LetIn ((name, typ), def, body) ->
+ | NotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = cic_name_of_name name in
let cic_typ =
in
let cic_body = aux ~localize loc (cic_name :: context) body in
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
- | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
- | CicNotationPt.Ident _
- | CicNotationPt.Uri _
- | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.Ident (name, subst) ->
+ | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
+ | NotationPt.Ident _
+ | NotationPt.Uri _
+ | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | NotationPt.Ident (name, subst) ->
assert (subst = None);
(try
NCic.Rel (find_in_context name context)
try NCic.Const (List.assoc name obj_context)
with Not_found ->
Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
- | CicNotationPt.Uri (uri, subst) ->
+ | NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
with NRef.IllFormedReference _ ->
- CicNotationPt.fail loc "Ill formed reference")
- | CicNotationPt.NRef nref -> NCic.Const nref
- | CicNotationPt.NCic t ->
+ NotationPt.fail loc "Ill formed reference")
+ | NotationPt.NRef nref -> NCic.Const nref
+ | NotationPt.NCic t ->
let context = (* to make metas_of_term happy *)
List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
assert(NCicUntrusted.metas_of_term [] context t = []); t
- | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
- | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
- | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
- | CicNotationPt.UserInput -> NCic.Implicit `Hole
- | CicNotationPt.Num (num, i) ->
+ | NotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
+ | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
+ | NotationPt.UserInput -> NCic.Implicit `Hole
+ | NotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
- | CicNotationPt.Meta (index, subst) ->
+ | NotationPt.Meta (index, subst) ->
let cic_subst =
List.map
(function None -> assert false| Some t -> aux ~localize loc context t)
subst
in
NCic.Meta (index, (0, NCic.Ctx cic_subst))
- | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
- | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
+ | NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
+ | NotationPt.Sort `Set -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
- | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
+ | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
- | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
+ | NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
- | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
+ | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
- | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
+ | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
- | CicNotationPt.Symbol (symbol, instance) ->
+ | NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
- | CicNotationPt.Variable _
- | CicNotationPt.Magic _
- | CicNotationPt.Layout _
- | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
+ | NotationPt.Variable _
+ | NotationPt.Magic _
+ | NotationPt.Layout _
+ | NotationPt.Literal _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> NCic.Implicit annotation
- | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) ->
+ | Some (NotationPt.AttributedTerm (`Loc loc, term)) ->
let res = aux_option ~localize loc context annotation (Some term) in
if localize then
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
- | Some (CicNotationPt.AttributedTerm (_, term)) ->
+ | Some (NotationPt.AttributedTerm (_, term)) ->
aux_option ~localize loc context annotation (Some term)
- | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
- | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | Some NotationPt.Implicit `JustOne -> NCic.Implicit annotation
+ | Some NotationPt.Implicit `Vector -> NCic.Implicit `Vector
| Some term -> aux ~localize loc context term
in
(fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
+ | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
- | CicNotationPt.LetRec (kind, defs, _) ->
+ | NotationPt.LetRec (kind, defs, _) ->
let inductive = kind = `Inductive in
let _,obj_context =
List.fold_left
let add_binders kind t =
List.fold_right
(fun var t ->
- CicNotationPt.Binder (kind, var, t)) params t
+ NotationPt.Binder (kind, var, t)) params t
in
let cic_body =
interpretate_term
in
let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
- | CicNotationPt.Inductive (params,tyl) ->
+ | NotationPt.Inductive (params,tyl) ->
let context,params =
let context,res =
List.fold_left
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit `JustOne
+ None -> NotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =
let attrs = `Provided, `Regular in
uri, height, [], [],
NCic.Inductive (inductive,leftno,tyl,attrs)
- | CicNotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields) ->
let context,params =
let context,res =
List.fold_left
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit `JustOne
+ None -> NotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:CicNotationUtil.freshen_term
+ ~freshen_thing:NotationUtil.freshen_term
~context ~metasenv ~initial_ugraph:() ~aliases
~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~universe ~uri:None ~pp_thing:NotationPp.pp_term
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:CicNotationUtil.freshen_obj
+ ~freshen_thing:NotationUtil.freshen_obj
~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~pp_thing:(NotationPp.pp_obj NotationPp.pp_term)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj ~mk_choice)
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
'alias list) ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
+ NotationPt.term Disambiguate.disambiguator_input ->
((DisambiguateTypes.domain_item * 'alias) list *
NCic.metasenv *
NCic.substitution *
DisambiguateTypes.Environment.key ->
'alias list) ->
uri:NUri.uri ->
- string * int * CicNotationPt.term CicNotationPt.obj ->
+ string * int * NotationPt.term NotationPt.obj ->
((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
NCic.substitution * NCic.obj)
list * bool
-val disambiguate_path: CicNotationPt.term -> NCic.term
+val disambiguate_path: NotationPt.term -> NCic.term
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- CicNotationPt.Ident (id,None)
+ NotationPt.Ident (id,None)
;;
(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
function
[] -> assert false
| [x] -> x
- | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2)
- | l -> CicNotationPt.Appl l
+ | NotationPt.Appl l1 :: l2 -> NotationPt.Appl (l1 @ l2)
+ | l -> NotationPt.Appl l
;;
let mk_elim uri leftno it (outsort,suffix) pragma =
let rec_arg = mk_id (fresh_name ()) in
let p_ty =
List.fold_right
- (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
- (CicNotationPt.Binder
+ (fun name res -> NotationPt.Binder (`Forall,(name,None),res)) args
+ (NotationPt.Binder
(`Forall,
(rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))),
- CicNotationPt.Sort outsort)) in
+ NotationPt.Sort outsort)) in
let args = args @ [rec_arg] in
let k_names = List.map (function _,name,_ -> name_of_k name) cl in
let final_params =
name, Some (
List.fold_right
(fun id res ->
- CicNotationPt.Binder (`Lambda,(id,None),res))
+ NotationPt.Binder (`Lambda,(id,None),res))
abs
- (CicNotationPt.Appl
+ (NotationPt.Appl
(rec_name ::
params @
[p_name] @
k_names @
- List.map (fun _ -> CicNotationPt.Implicit `JustOne)
+ List.map (fun _ -> NotationPt.Implicit `JustOne)
(List.tl args) @
[mk_appl (name::abs)])))
| _ -> mk_id name,None
) cargs in
let cargs,recursive_args = List.split cargs_and_recursive_args in
let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
- CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
+ NotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
mk_appl (name_of_k name :: cargs @ recursive_args)
) cl
in
- let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let bo = NotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
let recno = List.length final_params in
let where = recno - 1 in
let res =
- CicNotationPt.LetRec (`Inductive,
+ NotationPt.LetRec (`Inductive,
[final_params, (rec_name,ty), bo, where], rec_name)
in
(*
(BoxPp.render_to_string
~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false)
- 80 (CicNotationPres.render (fun _ -> None)
+ 80 (NotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));
prerr_endline "#####";
let cobj = ("xxx", [], None, `Joint {
def_term = bo;
def_type =
List.fold_right
- (fun x t -> CicNotationPt.Binder(`Forall,x,t))
+ (fun x t -> NotationPt.Binder(`Forall,x,t))
final_params cty
}
];
prerr_endline (
(BoxPp.render_to_string ~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false) 80
- (CicNotationPres.mpres_of_box boxml)));
+ (NotationPres.mpres_of_box boxml)));
*)
- CicNotationPt.Theorem
+ NotationPt.Theorem
(`Definition,srec_name,
- CicNotationPt.Implicit `JustOne,Some res,pragma)
+ NotationPt.Implicit `JustOne,Some res,pragma)
;;
let ast_of_sort s =
function
[] -> assert false
| [t] -> t
- | l -> CicNotationPt.Appl l
+ | l -> NotationPt.Appl l
;;
let rec count_prods = function NCic.Prod (_,_,t) -> 1 + count_prods t | _ -> 0;;
function
NCic.Rel i -> List.nth rels (i - 1)
| NCic.Const _ as t ->
- CicNotationPt.Ident
+ NotationPt.Ident
(NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
- | NCic.Sort s -> CicNotationPt.Sort (fst (ast_of_sort s))
+ | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
| NCic.Meta _
| NCic.Implicit _ -> assert false
- | NCic.Appl l -> CicNotationPt.Appl (List.map (pp rels) l)
+ | NCic.Appl l -> NotationPt.Appl (List.map (pp rels) l)
| NCic.Prod (n,s,t) ->
let n = mk_id n in
- CicNotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t)
+ NotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t)
| NCic.Lambda (n,s,t) ->
let n = mk_id n in
- CicNotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t)
+ NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t)
| NCic.LetIn (n,s,ty,t) ->
let n = mk_id n in
- CicNotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t)
+ NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t)
| NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
let name = NUri.name_of_uri uri in
let case_indty = Some (name, None) in
List.map2
(fun (_, name, ty) pat ->
let capture_variables,rhs = eat_branch leftno rels ty pat in
- CicNotationPt.Pattern (name, None, capture_variables), rhs
+ NotationPt.Pattern (name, None, capture_variables), rhs
) constructors patterns
with Invalid_argument _ -> assert false
in
- CicNotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns)
+ NotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns)
;;
let mk_projection leftno tyname consname consty (projname,_,_) i =
let arg = mk_id "xxx" in
let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
let bvar = mk_id "yyy" in
- let underscore = CicNotationPt.Ident ("_",None),None in
+ let underscore = NotationPt.Ident ("_",None),None in
let bvars =
HExtlib.mk_list underscore i @ [bvar,None] @
HExtlib.mk_list underscore (argsno - i -1) in
- let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in
+ let branch = NotationPt.Pattern (consname,None,bvars), bvar in
let projs,outtype = nth_prod [] i ty in
let rels =
List.map
(fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs
@ names in
let outtype = pp rels outtype in
- let outtype= CicNotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
- [arg, Some arg_ty], CicNotationPt.Case (arg,None,Some outtype,[branch])
+ let outtype= NotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
+ [arg, Some arg_ty], NotationPt.Case (arg,None,Some outtype,[branch])
| _,NCic.Prod (name,_,t) ->
let name = mk_id name in
let params,body = aux (name::names) t (leftno - 1) in
let params,bo = aux [] consty leftno in
let pprojname = mk_id projname in
let res =
- CicNotationPt.LetRec (`Inductive,
+ NotationPt.LetRec (`Inductive,
[params, (pprojname,None), bo, leftno], pprojname) in
(* prerr_endline
(BoxPp.render_to_string
~map_unicode_to_tex:false
(function x::_ -> x | _ -> assert false)
- 80 (CicNotationPres.render (fun _ -> None)
+ 80 (NotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
- CicNotationPt.Theorem
- (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection)
+ NotationPt.Theorem
+ (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
;;
let mk_projections (_,_,_,_,obj) =
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
-val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
+val mk_elims: NCic.obj -> NotationPt.term NotationPt.obj list
+val mk_projections: NCic.obj -> NotationPt.term NotationPt.obj list
val ast_of_sort :
NCic.sort -> [> `NCProp of string | `NType of string | `Prop ] * string
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- CicNotationPt.Ident (id,None)
+ NotationPt.Ident (id,None)
;;
let rec mk_prods l t =
match l with
[] -> t
- | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
+ | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
let mk_appl =
function
[] -> assert false
| [x] -> x
- | l -> CicNotationPt.Appl l
+ | l -> NotationPt.Appl l
;;
let rec iter f n acc =
let _,_,t_k = List.nth cl consno in
List.length (arg_list nleft t_k) ;;
-let default_pattern = "",0,(None,[],Some CicNotationPt.UserInput);;
+let default_pattern = "",0,(None,[],Some NotationPt.UserInput);;
(* returns the discrimination = injection+contradiction principle *)
let mk_eq tys ts us es n =
if use_jmeq then
mk_appl [mk_id "jmeq";
- CicNotationPt.Implicit `JustOne; List.nth ts n;
- CicNotationPt.Implicit `JustOne; List.nth us n]
+ NotationPt.Implicit `JustOne; List.nth ts n;
+ NotationPt.Implicit `JustOne; List.nth us n]
else
(* eqty = Tn u0 e0...un-1 en-1 *)
let eqty = mk_appl
let tys = List.map
(fun x -> iter
(fun i acc ->
- CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
- CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
+ NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
+ NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
acc))) (x-1)
- (CicNotationPt.Implicit (`Tagged ("T" ^ (string_of_int x)))))
+ (NotationPt.Implicit (`Tagged ("T" ^ (string_of_int x)))))
(HExtlib.list_seq 0 nargs) in
let tys = tys @
[iter (fun i acc ->
- CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
- CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
+ NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
+ NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
acc))) (nargs-1)
- (mk_appl [mk_id "eq"; CicNotationPt.Implicit `JustOne;
+ (mk_appl [mk_id "eq"; NotationPt.Implicit `JustOne;
mk_appl (mk_id (kname it i)::
List.map (fun x -> mk_id ("x" ^string_of_int x))
(HExtlib.list_seq 0 (List.length ts)));
mk_appl (mk_id (kname it j)::us)])]
in
- (** CicNotationPt.Binder (`Lambda, (mk_id "e",
+ (** NotationPt.Binder (`Lambda, (mk_id "e",
Some (mk_appl
[mk_id "eq";
- CicNotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
mk_appl (mk_id (kname it i)::ts);
mk_appl (mk_id (kname it j)::us)])),
let ts = ts @ [mk_id "e"] in
let refl2 = mk_appl
[mk_id "refl";
- CicNotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
mk_appl (mk_id (kname it j)::us)] in
let us = us @ [refl2] in *)
- CicNotationPt.Binder (`Forall, (mk_id "P", Some (CicNotationPt.Sort (`NType "1") )),
+ NotationPt.Binder (`Forall, (mk_id "P", Some (NotationPt.Sort (`NType "1") )),
if i = j then
- CicNotationPt.Binder (`Forall, (mk_id "_",
+ NotationPt.Binder (`Forall, (mk_id "_",
Some (iter (fun i acc ->
- CicNotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc))
+ NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc))
(nargs-1)
- (** (CicNotationPt.Binder (`Forall, (mk_id "_",
+ (** (NotationPt.Binder (`Forall, (mk_id "_",
Some (mk_eq tys ts us es nargs)),*)
(mk_id "P"))), mk_id "P")
else mk_id "P")
in
- let inner i ts = CicNotationPt.Case
+ let inner i ts = NotationPt.Case
(mk_id "y",None,
- (*Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None),
- CicNotationPt.Binder (`Forall, (mk_id "_", Some
- (mk_appl [mk_id "eq";CicNotationPt.Implicit
- `JustOne;(*CicNotationPt.Implicit `JustOne*)
+ (*Some (NotationPt.Binder (`Lambda, (mk_id "y",None),
+ NotationPt.Binder (`Forall, (mk_id "_", Some
+ (mk_appl [mk_id "eq";NotationPt.Implicit
+ `JustOne;(*NotationPt.Implicit `JustOne*)
mk_appl (mk_id (kname it i)::ts);mk_id "y"])),
- CicNotationPt.Implicit `JustOne )))*)
+ NotationPt.Implicit `JustOne )))*)
None,
List.map
(fun j ->
(nargs_kty - 1) [] in
let nones =
iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
- CicNotationPt.Pattern (kname it j,
+ NotationPt.Pattern (kname it j,
None,
List.combine us nones),
branch i j ts us)
(HExtlib.list_seq 0 (List.length cl)))
in
- let outer = CicNotationPt.Case
+ let outer = NotationPt.Case
(mk_id "x",None,
None ,
List.map
(nargs_kty - 1) [] in
let nones =
iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
- CicNotationPt.Pattern (kname it i,
+ NotationPt.Pattern (kname it i,
None,
List.combine ts nones),
inner i ts)
(HExtlib.list_seq 0 (List.length cl))) in
- let principle = CicNotationPt.Binder (`Lambda, (mk_id "x", Some xyty),
- CicNotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer))
+ let principle = NotationPt.Binder (`Lambda, (mk_id "x", Some xyty),
+ NotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer))
in
- pp (lazy ("discriminator = " ^ (CicNotationPp.pp_term principle)));
+ pp (lazy ("discriminator = " ^ (NotationPp.pp_term principle)));
status, principle
;;
NTactics.block_tac (
[(fun status ->
let status, discr = mk_discriminator it ~use_jmeq leftno xyty status in
- let cut_term = mk_prods params (CicNotationPt.Binder (`Forall, (mk_id "x",
+ let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x",
Some xyty),
- CicNotationPt.Binder (`Forall, (mk_id "y", Some xyty),
- CicNotationPt.Binder (`Forall, (mk_id "e",
- Some (mk_appl [mk_id "eq";CicNotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),
+ NotationPt.Binder (`Forall, (mk_id "y", Some xyty),
+ NotationPt.Binder (`Forall, (mk_id "e",
+ Some (mk_appl [mk_id "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),
mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in
- let status = print_tac (lazy ("cut_term = "^ CicNotationPp.pp_term cut_term)) status in
+ let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term cut_term)) status in
NTactics.cut_tac ("",0, cut_term)
status);
NTactics.branch_tac;
print_tac (lazy "ci sono 3");
NTactics.intro_tac "#discriminate";
NTactics.apply_tac ("",0,mk_appl ([mk_id "#discriminate"]@
- HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length params + 2) @
+ HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length params + 2) @
[mk_id eq_name ]));
NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern;
NTactics.clear_tac ["#discriminate"];
else
let gen_tac x =
NTactics.generalize_tac
- ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
NTactics.block_tac ((List.map gen_tac names_to_gen)@
[NTactics.clear_tac names_to_gen;
NTactics.rewrite_tac ~dir
let names_to_gen = names_to_gen @ [eq_name] in
let gen_tac x =
NTactics.generalize_tac
- ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
NTactics.block_tac ((List.map gen_tac names_to_gen)@
[NTactics.clear_tac names_to_gen;
NTactics.apply_tac ("",0, mk_appl [streicher_id;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne]);
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne]);
NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern] @
(let names_to_intro =
let names_to_gen = names_to_gen @ [eq_name] in
let gen_tac x =
NTactics.generalize_tac
- ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
NTactics.block_tac ((List.map gen_tac names_to_gen)@
[NTactics.clear_tac names_to_gen;
NTactics.apply_tac ("",0, mk_appl [streicher_id;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne]);
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne]);
NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern] @
(let names_to_intro =
let names_to_gen = names_to_gen (* @ [eq_name]*) in
let gen_tac x =
NTactics.generalize_tac
- ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
let gen_eq = NTactics.generalize_tac
~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- mk_id eq_name]),[], Some CicNotationPt.UserInput)) in
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ mk_id eq_name]),[], Some NotationPt.UserInput)) in
NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq::
[NTactics.clear_tac names_to_gen;
NTactics.try_tac (NTactics.clear_tac [eq_name]);
NTactics.apply_tac ("",0, mk_appl [streicher_id;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne;
- CicNotationPt.Implicit `JustOne]);
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne]);
NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern] @
(let names_to_intro = List.rev names_to_gen in
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- CicNotationPt.Ident (id,None)
+ NotationPt.Ident (id,None)
;;
let rec split_arity ~subst context te =
function
[] -> assert false
| [x] -> x
- | l -> CicNotationPt.Appl l
+ | l -> NotationPt.Appl l
;;
let rec mk_prods l t =
match l with
[] -> t
- | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
+ | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
let rec mk_arrows ?(pattern=false) xs ys selection target =
[],[],[] -> target
| false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
| true :: l,x::xs,y::ys ->
- CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then CicNotationPt.Implicit `JustOne else mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+ NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])),
mk_arrows ~pattern xs ys l target)
| _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
;;
let outsort, suffix = NCicElim.ast_of_sort outsort in
let theorem =
mk_prods xs
- (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
- mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs)))))
+ (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (NotationPt.Sort outsort))),
+ mk_prods hyplist (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs)))))
in
let status, theorem =
GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
- CicNotationPt.Theorem
+ NotationPt.Theorem
(`Theorem,name,theorem,
- Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let rs = List.map (fun x -> mk_id x) rs in
mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
- let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
+ let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
-CicNotationPt.Implicit (`Tagged "end"));
- CicNotationPt.Implicit (`Tagged "cut")] in
+NotationPt.Implicit (`Tagged "end"));
+ NotationPt.Implicit (`Tagged "cut")] in
let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
let where =
"",0,(None,[],
Some (
mk_arrows ~pattern:true
- (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys))
- (HExtlib.mk_list CicNotationPt.UserInput (List.length ys))
- selection CicNotationPt.UserInput)) in
+ (HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length ys))
+ (HExtlib.mk_list NotationPt.UserInput (List.length ys))
+ selection NotationPt.UserInput)) in
let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
let status =
NTactics.block_tac
= fun o -> (self#set_estatus o)#set_obj o#obj
end
-type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_term = NotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
let pp_tac_status status =
method set_pstatus: #g_pstatus -> 'self
end
-type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_term = NotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
type cic_term
open Continuationals.Stack
open NTacStatus
-module Ast = CicNotationPt
+module Ast = NotationPt
let id_tac status = status ;;
let print_tac print_status message status =
open Continuationals.Stack
open NTacStatus
-module Ast = CicNotationPt
+module Ast = NotationPt
(* ======================= statistics ========================= *)
Pervasives.compare (relevance v1) (relevance v2) in
let l = List.sort vcompare l in
let vstring (a,v)=
- CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
+ NotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
(string_of_float (relevance v)) ^
"; uses = " ^ (string_of_int !(v.uses)) ^
"; nom = " ^ (string_of_int !(v.nominations)) in
let is_a_fact_ast status subst metasenv ctx cand =
debug_print ~depth:0
- (lazy ("------- checking " ^ CicNotationPp.pp_term cand));
+ (lazy ("------- checking " ^ NotationPp.pp_term cand));
let status, t = disambiguate status ctx ("",0,cand) None in
let status,t = term_of_cic_term status t ctx in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
let add_to_trace ~depth cache t =
match t with
| Ast.NRef _ ->
- debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t));
+ debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term t));
{cache with trace = t::cache.trace}
| Ast.NCic _ (* local candidate *)
| _ -> (*not an application *) cache
let pptrace tr =
(lazy ("Proof Trace: " ^ (String.concat ";"
- (List.map CicNotationPp.pp_term tr))))
+ (List.map NotationPp.pp_term tr))))
(* not used
let remove_from_trace cache t =
match t with
List.sort (fun (a,_) (b,_) -> a - b) candidates in
let candidates = List.map snd candidates in
debug_print (lazy ("candidates =\n" ^ (String.concat "\n"
- (List.map CicNotationPp.pp_term candidates))));
+ (List.map NotationPp.pp_term candidates))));
candidates
let sort_new_elems l =
let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
try
- debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
+ debug_print ~depth (lazy ("try " ^ NotationPp.pp_term t));
let status =
if smart= 0 then NTactics.apply_tac ("",0,t) status
else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
(lazy ("(re)considering goal " ^
(string_of_int g) ^" : "^ppterm status gty));
debug_print (~depth:depth)
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
+ (lazy ("Case: " ^ NotationPp.pp_term t));
let depth,cache =
if t=Ast.Ident("__whd",None) ||
t=Ast.Ident("__intros",None)
val auto_tac:
params:(NTacStatus.tactic_term list option * (string * string) list) ->
- ?trace_ref:CicNotationPt.term list ref ->
+ ?trace_ref:NotationPt.term list ref ->
's NTacStatus.tactic
val keys_of_type:
?do_heavy_checks:bool ->
GrafiteTypes.status ->
string * int *
- ((CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
+ ((NotationPt.term, NotationPt.term,
+ NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
GrafiteAst.statement) ->
(GrafiteTypes.status *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
GrafiteTypes.status ->
Ulexing.lexbuf ->
(GrafiteTypes.status ->
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
+ (NotationPt.term, NotationPt.term,
+ NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string)
GrafiteAst.statement -> unit) ->
(GrafiteTypes.status *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
let current_proof_uri = BuildTimeConf.current_proof_uri
type term_source =
- [ `Ast of CicNotationPt.term
+ [ `Ast of NotationPt.term
| `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `String of string
]
;;
let pp_eager_statement_ast =
- GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
None status ctx menv subst (parsed_text,parsed_text_length,
- CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
| thms ->
String.concat ", "
(HExtlib.filter_map (function
- | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | NotationPt.NRef r -> Some (NCicPp.r2s true r)
| _ -> None)
thms)
in
let pp_ast_statement grafite_status stm =
let stm = GrafiteAstPp.pp_statement
~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
- ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj
- CicNotationPp.pp_term) stm
+ ~term_pp:NotationPp.pp_term
+ ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj
+ NotationPp.pp_term) stm
in
let stm = Pcre.replace ~rex:slash_n_RE stm in
let stm =
let floc = H.dummy_floc in
let nl_ast = G.Comment (floc, G.Note (floc, "")) in
let pp_statement stm =
- GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- ~lazy_term_pp:CicNotationPp.pp_term
- ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
+ ~lazy_term_pp:NotationPp.pp_term
+ ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
in
let pp_lexicon = LexiconAstPp.pp_command in
let och = open_out f in
projects / helm.git / commitdiff