+++ /dev/null
-requires="helm-library helm-ng_kernel"
-version="0.0.1"
-archive(byte)="acic_content.cma"
-archive(native)="acic_content.cmxa"
--- /dev/null
+requires="helm-library helm-ng_kernel"
+version="0.0.1"
+archive(byte)="content.cma"
+archive(native)="content.cmxa"
-requires="helm-acic_content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
+requires="helm-content helm-ng_cic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
version="0.0.1"
archive(byte)="content_pres.cma"
archive(native)="content_pres.cmxa"
-requires="helm-acic_content"
+requires="helm-content"
version="0.0.1"
archive(byte)="disambiguation.cma"
archive(native)="disambiguation.cmxa"
-requires="helm-cic helm-acic_content helm-ng_kernel"
+requires="helm-cic helm-content helm-ng_kernel"
version="0.0.1"
archive(byte)="grafite.cma"
archive(native)="grafite.cmxa"
-requires="helm-library helm-acic_content helm-ng_refiner"
+requires="helm-library helm-content helm-ng_refiner"
version="0.0.1"
archive(byte)="ng_cic_content.cma"
archive(native)="ng_cic_content.cmxa"
-requires="helm-acic_content helm-ng_refiner helm-disambiguation"
+requires="helm-content helm-ng_refiner helm-disambiguation"
version="0.0.1"
archive(byte)="ng_disambiguation.cma"
archive(native)="ng_disambiguation.cmxa"
cic \
library \
ng_kernel \
- acic_content \
+ content \
grafite \
disambiguation \
ng_kernel \
+++ /dev/null
-content.cmi:
-cicNotationUtil.cmi: cicNotationPt.cmo
-cicNotationEnv.cmi: cicNotationPt.cmo
-cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
-termAcicContent.cmi: cicNotationPt.cmo
-cicNotationPt.cmo:
-cicNotationPt.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
-termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \
- termAcicContent.cmi
-termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
- termAcicContent.cmi
+++ /dev/null
-content.cmi:
-cicNotationUtil.cmi: cicNotationPt.cmx
-cicNotationEnv.cmi: cicNotationPt.cmx
-cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
-termAcicContent.cmi: cicNotationPt.cmx
-cicNotationPt.cmo:
-cicNotationPt.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
-termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationPp.cmi \
- termAcicContent.cmi
-termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
- termAcicContent.cmi
+++ /dev/null
-PACKAGE = acic_content
-PREDICATES =
-
-INTERFACE_FILES = \
- content.mli \
- cicNotationUtil.mli \
- cicNotationEnv.mli \
- cicNotationPp.mli \
- termAcicContent.mli \
- $(NULL)
-IMPLEMENTATION_FILES = \
- cicNotationPt.ml \
- $(INTERFACE_FILES:%.mli=%.ml)
-
-include ../../Makefile.defs
-include ../Makefile.common
+++ /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
-
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-(**************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti <asperti@cs.unibo.it> *)
-(* 16/6/2003 *)
-(* *)
-(**************************************************************************)
-
-(* $Id$ *)
-
-type id = string;;
-type joint_recursion_kind =
- [ `Recursive of int list
- | `CoRecursive
- | `Inductive of int (* paramsno *)
- | `CoInductive of int (* paramsno *)
- ]
-;;
-
-type var_or_const = Var | Const;;
-
-type 'term declaration =
- { dec_name : string option;
- dec_id : id ;
- dec_inductive : bool;
- dec_aref : string;
- dec_type : 'term
- }
-;;
-
-type 'term definition =
- { def_name : string option;
- def_id : id ;
- def_aref : string ;
- def_term : 'term ;
- def_type : 'term
- }
-;;
-
-type 'term inductive =
- { inductive_id : id ;
- inductive_name : string;
- inductive_kind : bool;
- inductive_type : 'term;
- inductive_constructors : 'term declaration list
- }
-;;
-
-type 'term decl_context_element =
- [ `Declaration of 'term declaration
- | `Hypothesis of 'term declaration
- ]
-;;
-
-type ('term,'proof) def_context_element =
- [ `Proof of 'proof
- | `Definition of 'term definition
- ]
-;;
-
-type ('term,'proof) in_joint_context_element =
- [ `Inductive of 'term inductive
- | 'term decl_context_element
- | ('term,'proof) def_context_element
- ]
-;;
-
-type ('term,'proof) joint =
- { joint_id : id ;
- joint_kind : joint_recursion_kind ;
- joint_defs : ('term,'proof) in_joint_context_element list
- }
-;;
-
-type ('term,'proof) joint_context_element =
- [ `Joint of ('term,'proof) joint ]
-;;
-
-type 'term proof =
- { proof_name : string option;
- proof_id : id ;
- proof_context : 'term in_proof_context_element list ;
- proof_apply_context: 'term proof list;
- proof_conclude : 'term conclude_item
- }
-
-and 'term in_proof_context_element =
- [ 'term decl_context_element
- | ('term,'term proof) def_context_element
- | ('term,'term proof) joint_context_element
- ]
-
-and 'term conclude_item =
- { conclude_id : id;
- conclude_aref : string;
- conclude_method : string;
- conclude_args : ('term arg) list ;
- conclude_conclusion : 'term option
- }
-
-and 'term arg =
- Aux of string
- | Premise of premise
- | Lemma of lemma
- | Term of bool * 'term
- | ArgProof of 'term proof
- | ArgMethod of string (* ???? *)
-
-and premise =
- { premise_id: id;
- premise_xref : string ;
- premise_binder : string option;
- premise_n : int option;
- }
-
-and lemma =
- { lemma_id: id;
- lemma_name: string;
- lemma_uri: string
- }
-
-;;
-
-type 'term conjecture = id * int * 'term context * 'term
-
-and 'term context = 'term hypothesis list
-
-and 'term hypothesis =
- ['term decl_context_element | ('term,'term proof) def_context_element ] option
-;;
-
-type 'term in_object_context_element =
- [ `Decl of var_or_const * 'term decl_context_element
- | `Def of var_or_const * 'term * ('term,'term proof) def_context_element
- | ('term,'term proof) joint_context_element
- ]
-;;
-
-type 'term cobj =
- id * (* id *)
- UriManager.uri list * (* params *)
- 'term conjecture list option * (* optional metasenv *)
- 'term in_object_context_element (* actual object *)
-;;
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
-type id = string;;
-type joint_recursion_kind =
- [ `Recursive of int list (* decreasing arguments *)
- | `CoRecursive
- | `Inductive of int (* paramsno *)
- | `CoInductive of int (* paramsno *)
- ]
-;;
-
-type var_or_const = Var | Const;;
-
-type 'term declaration =
- { dec_name : string option;
- dec_id : id ;
- dec_inductive : bool;
- dec_aref : string;
- dec_type : 'term
- }
-;;
-
-type 'term definition =
- { def_name : string option;
- def_id : id ;
- def_aref : string ;
- def_term : 'term ;
- def_type : 'term
- }
-;;
-
-type 'term inductive =
- { inductive_id : id ;
- inductive_name : string;
- inductive_kind : bool;
- inductive_type : 'term;
- inductive_constructors : 'term declaration list
- }
-;;
-
-type 'term decl_context_element =
- [ `Declaration of 'term declaration
- | `Hypothesis of 'term declaration
- ]
-;;
-
-type ('term,'proof) def_context_element =
- [ `Proof of 'proof
- | `Definition of 'term definition
- ]
-;;
-
-type ('term,'proof) in_joint_context_element =
- [ `Inductive of 'term inductive
- | 'term decl_context_element
- | ('term,'proof) def_context_element
- ]
-;;
-
-type ('term,'proof) joint =
- { joint_id : id ;
- joint_kind : joint_recursion_kind ;
- joint_defs : ('term,'proof) in_joint_context_element list
- }
-;;
-
-type ('term,'proof) joint_context_element =
- [ `Joint of ('term,'proof) joint ]
-;;
-
-type 'term proof =
- { proof_name : string option;
- proof_id : id ;
- proof_context : 'term in_proof_context_element list ;
- proof_apply_context: 'term proof list;
- proof_conclude : 'term conclude_item
- }
-
-and 'term in_proof_context_element =
- [ 'term decl_context_element
- | ('term,'term proof) def_context_element
- | ('term,'term proof) joint_context_element
- ]
-
-and 'term conclude_item =
- { conclude_id : id;
- conclude_aref : string;
- conclude_method : string;
- conclude_args : ('term arg) list ;
- conclude_conclusion : 'term option
- }
-
-and 'term arg =
- Aux of string
- | Premise of premise
- | Lemma of lemma
- | Term of bool * 'term (* inferrable, term *)
- | ArgProof of 'term proof
- | ArgMethod of string (* ???? *)
-
-and premise =
- { premise_id: id;
- premise_xref : string ;
- premise_binder : string option;
- premise_n : int option;
- }
-
-and lemma =
- { lemma_id: id;
- lemma_name : string;
- lemma_uri: string
- }
-;;
-
-type 'term conjecture = id * int * 'term context * 'term
-
-and 'term context = 'term hypothesis list
-
-and 'term hypothesis =
- ['term decl_context_element | ('term,'term proof) def_context_element ] option
-;;
-
-type 'term in_object_context_element =
- [ `Decl of var_or_const * 'term decl_context_element
- | `Def of var_or_const * 'term * ('term,'term proof) def_context_element
- | ('term,'term proof) joint_context_element
- ]
-;;
-
-type 'term cobj =
- id * (* id *)
- UriManager.uri list * (* params *)
- 'term conjecture list option * (* optional metasenv *)
- 'term in_object_context_element (* actual object *)
-;;
+++ /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$ *)
-
-open Printf
-
-module Ast = CicNotationPt
-module Obj = LibraryObjects
-
-let debug = false
-let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-
-type interpretation_id = int
-
-let idref id t = Ast.AttributedTerm (`IdRef id, t)
-
-type term_info =
- { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
- 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
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-let pattern32_matrix = ref []
-let counter = ref ~-1
-let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;;
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old ->
- stack := old;
- counter := ocounter;
- level2_patterns32 := olevel2_patterns32;
- interpretations := ointerpretations;
- pattern32_matrix := opattern32_matrix
-;;
-
-let add_idrefs =
- List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
-
-let instantiate32 term_info idrefs env symbol args =
- let rec instantiate_arg = function
- | Ast.IdentArg (n, name) ->
- let t =
- try List.assoc name env
- with Not_found -> prerr_endline ("name not found in env: "^name);
- assert false
- in
- let rec count_lambda = function
- | Ast.AttributedTerm (_, t) -> count_lambda t
- | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
- | _ -> 0
- in
- let rec add_lambda t n =
- if n > 0 then
- let name = CicNotationUtil.fresh_name () in
- Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
- Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
- else
- t
- in
- add_lambda t (n - count_lambda t)
- in
- let head =
- let symbol = Ast.Symbol (symbol, 0) in
- add_idrefs idrefs symbol
- in
- if args = [] then head
- else Ast.Appl (head :: List.map instantiate_arg args)
-
-let load_patterns32s = ref [];;
-
-let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;;
-let fresh_id =
- fun () ->
- incr counter;
- !counter
-
-let add_interpretation dsc (symbol, args) appl_pattern =
- let id = fresh_id () in
- Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
- pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s;
- (try
- let ids = Hashtbl.find !interpretations symbol in
- ids := id :: !ids
- with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
- id
-
-let get_all_interpretations () =
- List.map
- (function (_, _, id) ->
- let (dsc, _, _, _) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- (id, dsc))
- !pattern32_matrix
-
-let get_active_interpretations () =
- HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
- !pattern32_matrix
-
-let set_active_interpretations ids =
- let pattern32_matrix' =
- List.map
- (function
- | (_, ap, id) when List.mem id ids -> (true, ap, id)
- | (_, ap, id) -> (false, ap, id))
- !pattern32_matrix
- in
- pattern32_matrix := pattern32_matrix';
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
-
-exception Interpretation_not_found
-
-let lookup_interpretations ?(sorted=true) symbol =
- try
- let raw =
- List.map (
- fun id ->
- let (dsc, _, args, appl_pattern) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- dsc, args, appl_pattern
- )
- !(Hashtbl.find !interpretations symbol)
- in
- if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
- else raw
- with Not_found -> raise Interpretation_not_found
-
-let remove_interpretation id =
- (try
- let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
- let ids = Hashtbl.find !interpretations symbol in
- ids := List.filter ((<>) id) !ids;
- Hashtbl.remove !level2_patterns32 id;
- with Not_found -> raise Interpretation_not_found);
- pattern32_matrix :=
- List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
- List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
-
-let init () = List.iter (fun f -> f []) !load_patterns32s
-
-let instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern
-=
- let lookup name =
- try List.assoc name env
- with Not_found ->
- prerr_endline (sprintf "Name %s not found" name);
- assert false
- in
- let rec aux = function
- | Ast.UriPattern uri -> term_of_uri uri
- | Ast.NRefPattern nref -> term_of_nref nref
- | Ast.ImplicitPattern -> mk_implicit false
- | Ast.VarPattern name -> lookup name
- | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
- in
- aux appl_pattern
-
+++ /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/
- *)
-
-
- (** {2 Persistant state handling} *)
-
-type interpretation_id
-
-val add_interpretation:
- string -> (* id / description *)
- string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
- CicNotationPt.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
-
-exception Interpretation_not_found
-
- (** @raise Interpretation_not_found *)
-val remove_interpretation: interpretation_id -> unit
-
- (** {3 Interpretations toggling} *)
-
-val get_all_interpretations: unit -> (interpretation_id * string) list
-val get_active_interpretations: unit -> interpretation_id list
-val set_active_interpretations: interpretation_id list -> unit
-
- (** {2 content -> acic} *)
-
- (** @param env environment from argument_pattern to cic terms
- * @param pat cic_appl_pattern *)
-val instantiate_appl_pattern:
- mk_appl:('term list -> 'term) ->
- mk_implicit:(bool -> 'term) ->
- term_of_uri : (UriManager.uri -> 'term) ->
- term_of_nref : (NReference.reference -> 'term) ->
- (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
- 'term
-
-val push: unit -> unit
-val pop: unit -> unit
-
-(* for Matita NG *)
-val find_level2_patterns32:
- int ->
- string * string *
- CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern
-
-val add_load_patterns32:
- ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit
-val init: unit -> unit
--- /dev/null
+content.cmi:
+cicNotationUtil.cmi: cicNotationPt.cmo
+cicNotationEnv.cmi: cicNotationPt.cmo
+cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
+interpretations.cmi: cicNotationPt.cmo
+cicNotationPt.cmo:
+cicNotationPt.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
--- /dev/null
+content.cmi:
+cicNotationUtil.cmi: cicNotationPt.cmx
+cicNotationEnv.cmi: cicNotationPt.cmx
+cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
+interpretations.cmi: cicNotationPt.cmx
+cicNotationPt.cmo:
+cicNotationPt.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
--- /dev/null
+PACKAGE = content
+PREDICATES =
+
+INTERFACE_FILES = \
+ content.mli \
+ cicNotationUtil.mli \
+ cicNotationEnv.mli \
+ cicNotationPp.mli \
+ interpretations.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ cicNotationPt.ml \
+ $(INTERFACE_FILES:%.mli=%.ml)
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /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
+
--- /dev/null
+(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
+ *)
+
+(**************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Andrea Asperti <asperti@cs.unibo.it> *)
+(* 16/6/2003 *)
+(* *)
+(**************************************************************************)
+
+(* $Id$ *)
+
+type id = string;;
+type joint_recursion_kind =
+ [ `Recursive of int list
+ | `CoRecursive
+ | `Inductive of int (* paramsno *)
+ | `CoInductive of int (* paramsno *)
+ ]
+;;
+
+type var_or_const = Var | Const;;
+
+type 'term declaration =
+ { dec_name : string option;
+ dec_id : id ;
+ dec_inductive : bool;
+ dec_aref : string;
+ dec_type : 'term
+ }
+;;
+
+type 'term definition =
+ { def_name : string option;
+ def_id : id ;
+ def_aref : string ;
+ def_term : 'term ;
+ def_type : 'term
+ }
+;;
+
+type 'term inductive =
+ { inductive_id : id ;
+ inductive_name : string;
+ inductive_kind : bool;
+ inductive_type : 'term;
+ inductive_constructors : 'term declaration list
+ }
+;;
+
+type 'term decl_context_element =
+ [ `Declaration of 'term declaration
+ | `Hypothesis of 'term declaration
+ ]
+;;
+
+type ('term,'proof) def_context_element =
+ [ `Proof of 'proof
+ | `Definition of 'term definition
+ ]
+;;
+
+type ('term,'proof) in_joint_context_element =
+ [ `Inductive of 'term inductive
+ | 'term decl_context_element
+ | ('term,'proof) def_context_element
+ ]
+;;
+
+type ('term,'proof) joint =
+ { joint_id : id ;
+ joint_kind : joint_recursion_kind ;
+ joint_defs : ('term,'proof) in_joint_context_element list
+ }
+;;
+
+type ('term,'proof) joint_context_element =
+ [ `Joint of ('term,'proof) joint ]
+;;
+
+type 'term proof =
+ { proof_name : string option;
+ proof_id : id ;
+ proof_context : 'term in_proof_context_element list ;
+ proof_apply_context: 'term proof list;
+ proof_conclude : 'term conclude_item
+ }
+
+and 'term in_proof_context_element =
+ [ 'term decl_context_element
+ | ('term,'term proof) def_context_element
+ | ('term,'term proof) joint_context_element
+ ]
+
+and 'term conclude_item =
+ { conclude_id : id;
+ conclude_aref : string;
+ conclude_method : string;
+ conclude_args : ('term arg) list ;
+ conclude_conclusion : 'term option
+ }
+
+and 'term arg =
+ Aux of string
+ | Premise of premise
+ | Lemma of lemma
+ | Term of bool * 'term
+ | ArgProof of 'term proof
+ | ArgMethod of string (* ???? *)
+
+and premise =
+ { premise_id: id;
+ premise_xref : string ;
+ premise_binder : string option;
+ premise_n : int option;
+ }
+
+and lemma =
+ { lemma_id: id;
+ lemma_name: string;
+ lemma_uri: string
+ }
+
+;;
+
+type 'term conjecture = id * int * 'term context * 'term
+
+and 'term context = 'term hypothesis list
+
+and 'term hypothesis =
+ ['term decl_context_element | ('term,'term proof) def_context_element ] option
+;;
+
+type 'term in_object_context_element =
+ [ `Decl of var_or_const * 'term decl_context_element
+ | `Def of var_or_const * 'term * ('term,'term proof) def_context_element
+ | ('term,'term proof) joint_context_element
+ ]
+;;
+
+type 'term cobj =
+ id * (* id *)
+ UriManager.uri list * (* params *)
+ 'term conjecture list option * (* optional metasenv *)
+ 'term in_object_context_element (* actual object *)
+;;
--- /dev/null
+(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
+ *)
+
+type id = string;;
+type joint_recursion_kind =
+ [ `Recursive of int list (* decreasing arguments *)
+ | `CoRecursive
+ | `Inductive of int (* paramsno *)
+ | `CoInductive of int (* paramsno *)
+ ]
+;;
+
+type var_or_const = Var | Const;;
+
+type 'term declaration =
+ { dec_name : string option;
+ dec_id : id ;
+ dec_inductive : bool;
+ dec_aref : string;
+ dec_type : 'term
+ }
+;;
+
+type 'term definition =
+ { def_name : string option;
+ def_id : id ;
+ def_aref : string ;
+ def_term : 'term ;
+ def_type : 'term
+ }
+;;
+
+type 'term inductive =
+ { inductive_id : id ;
+ inductive_name : string;
+ inductive_kind : bool;
+ inductive_type : 'term;
+ inductive_constructors : 'term declaration list
+ }
+;;
+
+type 'term decl_context_element =
+ [ `Declaration of 'term declaration
+ | `Hypothesis of 'term declaration
+ ]
+;;
+
+type ('term,'proof) def_context_element =
+ [ `Proof of 'proof
+ | `Definition of 'term definition
+ ]
+;;
+
+type ('term,'proof) in_joint_context_element =
+ [ `Inductive of 'term inductive
+ | 'term decl_context_element
+ | ('term,'proof) def_context_element
+ ]
+;;
+
+type ('term,'proof) joint =
+ { joint_id : id ;
+ joint_kind : joint_recursion_kind ;
+ joint_defs : ('term,'proof) in_joint_context_element list
+ }
+;;
+
+type ('term,'proof) joint_context_element =
+ [ `Joint of ('term,'proof) joint ]
+;;
+
+type 'term proof =
+ { proof_name : string option;
+ proof_id : id ;
+ proof_context : 'term in_proof_context_element list ;
+ proof_apply_context: 'term proof list;
+ proof_conclude : 'term conclude_item
+ }
+
+and 'term in_proof_context_element =
+ [ 'term decl_context_element
+ | ('term,'term proof) def_context_element
+ | ('term,'term proof) joint_context_element
+ ]
+
+and 'term conclude_item =
+ { conclude_id : id;
+ conclude_aref : string;
+ conclude_method : string;
+ conclude_args : ('term arg) list ;
+ conclude_conclusion : 'term option
+ }
+
+and 'term arg =
+ Aux of string
+ | Premise of premise
+ | Lemma of lemma
+ | Term of bool * 'term (* inferrable, term *)
+ | ArgProof of 'term proof
+ | ArgMethod of string (* ???? *)
+
+and premise =
+ { premise_id: id;
+ premise_xref : string ;
+ premise_binder : string option;
+ premise_n : int option;
+ }
+
+and lemma =
+ { lemma_id: id;
+ lemma_name : string;
+ lemma_uri: string
+ }
+;;
+
+type 'term conjecture = id * int * 'term context * 'term
+
+and 'term context = 'term hypothesis list
+
+and 'term hypothesis =
+ ['term decl_context_element | ('term,'term proof) def_context_element ] option
+;;
+
+type 'term in_object_context_element =
+ [ `Decl of var_or_const * 'term decl_context_element
+ | `Def of var_or_const * 'term * ('term,'term proof) def_context_element
+ | ('term,'term proof) joint_context_element
+ ]
+;;
+
+type 'term cobj =
+ id * (* id *)
+ UriManager.uri list * (* params *)
+ 'term conjecture list option * (* optional metasenv *)
+ 'term in_object_context_element (* actual object *)
+;;
--- /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$ *)
+
+open Printf
+
+module Ast = CicNotationPt
+module Obj = LibraryObjects
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+type interpretation_id = int
+
+let idref id t = Ast.AttributedTerm (`IdRef id, t)
+
+type term_info =
+ { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
+ 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
+let initial_interpretations () = Hashtbl.create 211
+
+let level2_patterns32 = ref (initial_level2_patterns32 ())
+(* symb -> id list ref *)
+let interpretations = ref (initial_interpretations ())
+let pattern32_matrix = ref []
+let counter = ref ~-1
+let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;;
+
+let stack = ref []
+
+let push () =
+ stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack;
+ counter := ~-1;
+ level2_patterns32 := initial_level2_patterns32 ();
+ interpretations := initial_interpretations ();
+ pattern32_matrix := []
+;;
+
+let pop () =
+ match !stack with
+ [] -> assert false
+ | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old ->
+ stack := old;
+ counter := ocounter;
+ level2_patterns32 := olevel2_patterns32;
+ interpretations := ointerpretations;
+ pattern32_matrix := opattern32_matrix
+;;
+
+let add_idrefs =
+ List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+
+let instantiate32 term_info idrefs env symbol args =
+ let rec instantiate_arg = function
+ | Ast.IdentArg (n, name) ->
+ let t =
+ try List.assoc name env
+ with Not_found -> prerr_endline ("name not found in env: "^name);
+ assert false
+ in
+ let rec count_lambda = function
+ | Ast.AttributedTerm (_, t) -> count_lambda t
+ | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
+ | _ -> 0
+ in
+ let rec add_lambda t n =
+ if n > 0 then
+ let name = CicNotationUtil.fresh_name () in
+ Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
+ Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
+ else
+ t
+ in
+ add_lambda t (n - count_lambda t)
+ in
+ let head =
+ let symbol = Ast.Symbol (symbol, 0) in
+ add_idrefs idrefs symbol
+ in
+ if args = [] then head
+ else Ast.Appl (head :: List.map instantiate_arg args)
+
+let load_patterns32s = ref [];;
+
+let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;;
+let fresh_id =
+ fun () ->
+ incr counter;
+ !counter
+
+let add_interpretation dsc (symbol, args) appl_pattern =
+ let id = fresh_id () in
+ Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
+ pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
+ List.iter (fun f -> f !pattern32_matrix) !load_patterns32s;
+ (try
+ let ids = Hashtbl.find !interpretations symbol in
+ ids := id :: !ids
+ with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
+ id
+
+let get_all_interpretations () =
+ List.map
+ (function (_, _, id) ->
+ let (dsc, _, _, _) =
+ try
+ Hashtbl.find !level2_patterns32 id
+ with Not_found -> assert false
+ in
+ (id, dsc))
+ !pattern32_matrix
+
+let get_active_interpretations () =
+ HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
+ !pattern32_matrix
+
+let set_active_interpretations ids =
+ let pattern32_matrix' =
+ List.map
+ (function
+ | (_, ap, id) when List.mem id ids -> (true, ap, id)
+ | (_, ap, id) -> (false, ap, id))
+ !pattern32_matrix
+ in
+ pattern32_matrix := pattern32_matrix';
+ List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
+
+exception Interpretation_not_found
+
+let lookup_interpretations ?(sorted=true) symbol =
+ try
+ let raw =
+ List.map (
+ fun id ->
+ let (dsc, _, args, appl_pattern) =
+ try
+ Hashtbl.find !level2_patterns32 id
+ with Not_found -> assert false
+ in
+ dsc, args, appl_pattern
+ )
+ !(Hashtbl.find !interpretations symbol)
+ in
+ if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+ else raw
+ with Not_found -> raise Interpretation_not_found
+
+let remove_interpretation id =
+ (try
+ let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
+ let ids = Hashtbl.find !interpretations symbol in
+ ids := List.filter ((<>) id) !ids;
+ Hashtbl.remove !level2_patterns32 id;
+ with Not_found -> raise Interpretation_not_found);
+ pattern32_matrix :=
+ List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
+ List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
+
+let init () = List.iter (fun f -> f []) !load_patterns32s
+
+let instantiate_appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern
+=
+ let lookup name =
+ try List.assoc name env
+ with Not_found ->
+ prerr_endline (sprintf "Name %s not found" name);
+ assert false
+ in
+ let rec aux = function
+ | Ast.UriPattern uri -> term_of_uri uri
+ | Ast.NRefPattern nref -> term_of_nref nref
+ | Ast.ImplicitPattern -> mk_implicit false
+ | Ast.VarPattern name -> lookup name
+ | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
+ in
+ aux appl_pattern
+
--- /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/
+ *)
+
+
+ (** {2 Persistant state handling} *)
+
+type interpretation_id
+
+val add_interpretation:
+ string -> (* id / description *)
+ string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
+ CicNotationPt.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
+
+exception Interpretation_not_found
+
+ (** @raise Interpretation_not_found *)
+val remove_interpretation: interpretation_id -> unit
+
+ (** {3 Interpretations toggling} *)
+
+val get_all_interpretations: unit -> (interpretation_id * string) list
+val get_active_interpretations: unit -> interpretation_id list
+val set_active_interpretations: interpretation_id list -> unit
+
+ (** {2 content -> cic} *)
+
+ (** @param env environment from argument_pattern to cic terms
+ * @param pat cic_appl_pattern *)
+val instantiate_appl_pattern:
+ mk_appl:('term list -> 'term) ->
+ mk_implicit:(bool -> 'term) ->
+ term_of_uri : (UriManager.uri -> 'term) ->
+ term_of_nref : (NReference.reference -> 'term) ->
+ (string * 'term) list -> CicNotationPt.cic_appl_pattern ->
+ 'term
+
+val push: unit -> unit
+val pop: unit -> unit
+
+(* for Matita NG *)
+val find_level2_patterns32:
+ int ->
+ string * string *
+ CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern
+
+val add_load_patterns32:
+ ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit
+val init: unit -> unit
type notation_id =
| RuleId of CicNotationParser.rule_id
- | InterpretationId of TermAcicContent.interpretation_id
+ | InterpretationId of Interpretations.interpretation_id
| PrettyPrinterId of TermContentPres.pretty_printer_id
let compare_notation_id x y =
in
!rule_id @ pp_id
| Interpretation (loc, dsc, l2, l3) ->
- let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
+ let interp_id = Interpretations.add_interpretation dsc l2 l3 in
[InterpretationId interp_id]
| st -> []
RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
!parser_ref_counter item
| PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
- | InterpretationId id -> TermAcicContent.remove_interpretation id
+ | InterpretationId id -> Interpretations.remove_interpretation id
let get_all_notations () =
List.map
(fun (interp_id, dsc) ->
InterpretationId interp_id, "interpretation: " ^ dsc)
- (TermAcicContent.get_all_interpretations ())
+ (Interpretations.get_all_interpretations ())
let get_active_notations () =
List.map (fun id -> InterpretationId id)
- (TermAcicContent.get_active_interpretations ())
+ (Interpretations.get_active_interpretations ())
let set_active_notations ids =
let interp_ids =
(function InterpretationId interp_id -> Some interp_id | _ -> None)
ids
in
- TermAcicContent.set_active_interpretations interp_ids
+ Interpretations.set_active_interpretations interp_ids
let history = ref [];;
parser_ref_counter := initial_parser_ref_counter ();
rule_ids_to_items := initial_rule_ids_to_items ();
TermContentPres.push ();
- TermAcicContent.push ();
+ Interpretations.push ();
CicNotationParser.push ()
;;
let pop () =
TermContentPres.pop ();
- TermAcicContent.pop ();
+ Interpretations.pop ();
CicNotationParser.pop ();
match !history with
| [] -> assert false
in
let _, symbol, args, _ =
try
- TermAcicContent.find_level2_patterns32 pid
+ Interpretations.find_level2_patterns32 pid
with Not_found -> assert false
in
let ast = instantiate32 idrefs env symbol args in
in
set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
in
- TermAcicContent.add_load_patterns32 load_patterns32;
- TermAcicContent.init ()
+ Interpretations.add_load_patterns32 load_patterns32;
+ Interpretations.init ()
;;
(*
"The notation " ^ dsc ^ " expects more arguments")))
in
let combined =
- TermAcicContent.instantiate_appl_pattern
+ Interpretations.instantiate_appl_pattern
~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern
in
match rest with
| _::_ -> mk_appl (combined::rest))
let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc =
- let interpretations = TermAcicContent.lookup_interpretations ~sorted:false symbol in
+ let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in
try
mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref
(List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
- with TermAcicContent.Interpretation_not_found | Not_found ->
+ with Interpretations.Interpretation_not_found | Not_found ->
raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc
projects / helm.git / commitdiff