From: Andrea Asperti Date: Fri, 8 Oct 2010 09:01:00 +0000 (+0000) Subject: - acic_content ==> content X-Git-Tag: make_still_working~2793 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git - acic_content ==> content - termAcicContent ==> interpretations --- diff --git a/matita/components/METAS/meta.helm-acic_content.src b/matita/components/METAS/meta.helm-acic_content.src deleted file mode 100644 index 0013afa41..000000000 --- a/matita/components/METAS/meta.helm-acic_content.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-library helm-ng_kernel" -version="0.0.1" -archive(byte)="acic_content.cma" -archive(native)="acic_content.cmxa" diff --git a/matita/components/METAS/meta.helm-content.src b/matita/components/METAS/meta.helm-content.src new file mode 100644 index 000000000..6973a54d9 --- /dev/null +++ b/matita/components/METAS/meta.helm-content.src @@ -0,0 +1,4 @@ +requires="helm-library helm-ng_kernel" +version="0.0.1" +archive(byte)="content.cma" +archive(native)="content.cmxa" diff --git a/matita/components/METAS/meta.helm-content_pres.src b/matita/components/METAS/meta.helm-content_pres.src index 74b1b23c9..8db3fca82 100644 --- a/matita/components/METAS/meta.helm-content_pres.src +++ b/matita/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -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" diff --git a/matita/components/METAS/meta.helm-disambiguation.src b/matita/components/METAS/meta.helm-disambiguation.src index 706f6dd12..6c286ea71 100644 --- a/matita/components/METAS/meta.helm-disambiguation.src +++ b/matita/components/METAS/meta.helm-disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-acic_content" +requires="helm-content" version="0.0.1" archive(byte)="disambiguation.cma" archive(native)="disambiguation.cmxa" diff --git a/matita/components/METAS/meta.helm-grafite.src b/matita/components/METAS/meta.helm-grafite.src index 46a6fb338..f45beff90 100644 --- a/matita/components/METAS/meta.helm-grafite.src +++ b/matita/components/METAS/meta.helm-grafite.src @@ -1,4 +1,4 @@ -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" diff --git a/matita/components/METAS/meta.helm-ng_cic_content.src b/matita/components/METAS/meta.helm-ng_cic_content.src index 4823c8bc6..a2c08e135 100644 --- a/matita/components/METAS/meta.helm-ng_cic_content.src +++ b/matita/components/METAS/meta.helm-ng_cic_content.src @@ -1,4 +1,4 @@ -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" diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src index 7910e8dff..84eeab3fe 100644 --- a/matita/components/METAS/meta.helm-ng_disambiguation.src +++ b/matita/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -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" diff --git a/matita/components/Makefile b/matita/components/Makefile index 6b248d0e6..86fc08c69 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -19,7 +19,7 @@ MODULES = \ cic \ library \ ng_kernel \ - acic_content \ + content \ grafite \ disambiguation \ ng_kernel \ diff --git a/matita/components/acic_content/.depend b/matita/components/acic_content/.depend deleted file mode 100644 index e8b9a6135..000000000 --- a/matita/components/acic_content/.depend +++ /dev/null @@ -1,19 +0,0 @@ -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 diff --git a/matita/components/acic_content/.depend.opt b/matita/components/acic_content/.depend.opt deleted file mode 100644 index a679f7253..000000000 --- a/matita/components/acic_content/.depend.opt +++ /dev/null @@ -1,19 +0,0 @@ -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 diff --git a/matita/components/acic_content/Makefile b/matita/components/acic_content/Makefile deleted file mode 100644 index 119aaaa73..000000000 --- a/matita/components/acic_content/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -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 diff --git a/matita/components/acic_content/cicNotationEnv.ml b/matita/components/acic_content/cicNotationEnv.ml deleted file mode 100644 index 5b4190eb8..000000000 --- a/matita/components/acic_content/cicNotationEnv.ml +++ /dev/null @@ -1,153 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/cicNotationEnv.mli b/matita/components/acic_content/cicNotationEnv.mli deleted file mode 100644 index aa937d00c..000000000 --- a/matita/components/acic_content/cicNotationEnv.mli +++ /dev/null @@ -1,92 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/cicNotationPp.ml b/matita/components/acic_content/cicNotationPp.ml deleted file mode 100644 index f94891375..000000000 --- a/matita/components/acic_content/cicNotationPp.ml +++ /dev/null @@ -1,371 +0,0 @@ -(* 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 "<>" - | 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)) - diff --git a/matita/components/acic_content/cicNotationPp.mli b/matita/components/acic_content/cicNotationPp.mli deleted file mode 100644 index d883ddfc6..000000000 --- a/matita/components/acic_content/cicNotationPp.mli +++ /dev/null @@ -1,55 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/cicNotationPt.ml b/matita/components/acic_content/cicNotationPt.ml deleted file mode 100644 index 731a2ba74..000000000 --- a/matita/components/acic_content/cicNotationPt.ml +++ /dev/null @@ -1,199 +0,0 @@ -(* 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, 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 - - (** - * 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 - diff --git a/matita/components/acic_content/cicNotationUtil.ml b/matita/components/acic_content/cicNotationUtil.ml deleted file mode 100644 index 7eccd7901..000000000 --- a/matita/components/acic_content/cicNotationUtil.ml +++ /dev/null @@ -1,420 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/cicNotationUtil.mli b/matita/components/acic_content/cicNotationUtil.mli deleted file mode 100644 index 77350a2ac..000000000 --- a/matita/components/acic_content/cicNotationUtil.mli +++ /dev/null @@ -1,98 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/content.ml b/matita/components/acic_content/content.ml deleted file mode 100644 index 1e4cc88af..000000000 --- a/matita/components/acic_content/content.ml +++ /dev/null @@ -1,170 +0,0 @@ -(* 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 *) -(* 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 *) -;; diff --git a/matita/components/acic_content/content.mli b/matita/components/acic_content/content.mli deleted file mode 100644 index 229d30749..000000000 --- a/matita/components/acic_content/content.mli +++ /dev/null @@ -1,158 +0,0 @@ -(* 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 *) -;; diff --git a/matita/components/acic_content/termAcicContent.ml b/matita/components/acic_content/termAcicContent.ml deleted file mode 100644 index 599a0704e..000000000 --- a/matita/components/acic_content/termAcicContent.ml +++ /dev/null @@ -1,221 +0,0 @@ -(* 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 - diff --git a/matita/components/acic_content/termAcicContent.mli b/matita/components/acic_content/termAcicContent.mli deleted file mode 100644 index f7ac8ccc6..000000000 --- a/matita/components/acic_content/termAcicContent.mli +++ /dev/null @@ -1,77 +0,0 @@ -(* 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 diff --git a/matita/components/content/.depend b/matita/components/content/.depend new file mode 100644 index 000000000..50d486b4f --- /dev/null +++ b/matita/components/content/.depend @@ -0,0 +1,19 @@ +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 diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt new file mode 100644 index 000000000..9af10948d --- /dev/null +++ b/matita/components/content/.depend.opt @@ -0,0 +1,19 @@ +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 diff --git a/matita/components/content/Makefile b/matita/components/content/Makefile new file mode 100644 index 000000000..2f1a3896a --- /dev/null +++ b/matita/components/content/Makefile @@ -0,0 +1,16 @@ +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 diff --git a/matita/components/content/cicNotationEnv.ml b/matita/components/content/cicNotationEnv.ml new file mode 100644 index 000000000..5b4190eb8 --- /dev/null +++ b/matita/components/content/cicNotationEnv.ml @@ -0,0 +1,153 @@ +(* 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 + diff --git a/matita/components/content/cicNotationEnv.mli b/matita/components/content/cicNotationEnv.mli new file mode 100644 index 000000000..aa937d00c --- /dev/null +++ b/matita/components/content/cicNotationEnv.mli @@ -0,0 +1,92 @@ +(* 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 + diff --git a/matita/components/content/cicNotationPp.ml b/matita/components/content/cicNotationPp.ml new file mode 100644 index 000000000..f94891375 --- /dev/null +++ b/matita/components/content/cicNotationPp.ml @@ -0,0 +1,371 @@ +(* 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 "<>" + | 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)) + diff --git a/matita/components/content/cicNotationPp.mli b/matita/components/content/cicNotationPp.mli new file mode 100644 index 000000000..d883ddfc6 --- /dev/null +++ b/matita/components/content/cicNotationPp.mli @@ -0,0 +1,55 @@ +(* 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 + diff --git a/matita/components/content/cicNotationPt.ml b/matita/components/content/cicNotationPt.ml new file mode 100644 index 000000000..731a2ba74 --- /dev/null +++ b/matita/components/content/cicNotationPt.ml @@ -0,0 +1,199 @@ +(* 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, 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 + + (** + * 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 + diff --git a/matita/components/content/cicNotationUtil.ml b/matita/components/content/cicNotationUtil.ml new file mode 100644 index 000000000..7eccd7901 --- /dev/null +++ b/matita/components/content/cicNotationUtil.ml @@ -0,0 +1,420 @@ +(* 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 + diff --git a/matita/components/content/cicNotationUtil.mli b/matita/components/content/cicNotationUtil.mli new file mode 100644 index 000000000..77350a2ac --- /dev/null +++ b/matita/components/content/cicNotationUtil.mli @@ -0,0 +1,98 @@ +(* 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 + diff --git a/matita/components/content/content.ml b/matita/components/content/content.ml new file mode 100644 index 000000000..1e4cc88af --- /dev/null +++ b/matita/components/content/content.ml @@ -0,0 +1,170 @@ +(* 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 *) +(* 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 *) +;; diff --git a/matita/components/content/content.mli b/matita/components/content/content.mli new file mode 100644 index 000000000..229d30749 --- /dev/null +++ b/matita/components/content/content.mli @@ -0,0 +1,158 @@ +(* 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 *) +;; diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml new file mode 100644 index 000000000..599a0704e --- /dev/null +++ b/matita/components/content/interpretations.ml @@ -0,0 +1,221 @@ +(* 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 + diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli new file mode 100644 index 000000000..259a7b1ac --- /dev/null +++ b/matita/components/content/interpretations.mli @@ -0,0 +1,77 @@ +(* 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 diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml index ebc9463ee..7351596fa 100644 --- a/matita/components/lexicon/cicNotation.ml +++ b/matita/components/lexicon/cicNotation.ml @@ -29,7 +29,7 @@ open LexiconAst 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 = @@ -77,7 +77,7 @@ let process_notation st = 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 -> [] @@ -90,17 +90,17 @@ let remove_notation = function 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 = @@ -108,7 +108,7 @@ let set_active_notations 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 [];; @@ -117,13 +117,13 @@ let push () = 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 diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index 26d7e98fb..b8d474cc2 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -322,7 +322,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = 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 @@ -335,8 +335,8 @@ let load_patterns32 t = 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 () ;; (* diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 6d4d63b70..3da5f9baa 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -74,7 +74,7 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl "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 @@ -82,11 +82,11 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl | _::_ -> 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