From: Stefano Zacchiroli Date: Wed, 4 Feb 2004 09:42:12 +0000 (+0000) Subject: moved Ast in cic_transformations/ X-Git-Tag: V_0_2_3~80 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a428a96ac2d7aa38be075f7139aa06c5b7019b3;p=helm.git moved Ast in cic_transformations/ --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli deleted file mode 100644 index 849d10285..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli +++ /dev/null @@ -1,115 +0,0 @@ - - (* when an 'ident option is None, the default is to apply the tactic - to the current goal *) - -type reduction_kind = [ `Reduce | `Simpl | `Whd ] - -type 'term pattern = - | Pattern of 'term - -type location = int * int - -type ('term, 'ident) tactic = - | LocatedTactic of location * ('term, 'ident) tactic - - | Absurd - | Apply of 'term - | Assumption - | Change of 'term * 'term * 'ident option (* what, with what, where *) - | Change_pattern of 'term pattern * 'term * 'ident option - (* what, with what, where *) - | Contradiction - | Cut of 'term - | Decompose of 'ident * 'ident list (* which hypothesis, which principles *) - | Discriminate of 'ident - | Elim of 'term * 'term option (* what to elim, which principle to use *) - | ElimType of 'term - | Exact of 'term - | Exists - | Fold of reduction_kind * 'term - | Fourier - | Injection of 'ident - | Intros of int option - | Left - | LetIn of 'term * 'ident (* TODO clashes with term below *) - | Named_intros of 'ident list - | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) - | Reflexivity - | Replace of 'term * 'term (* what, with what *) - | Replace_pattern of 'term pattern * 'term - | RewriteLeft of 'term * 'ident option - | RewriteRight of 'term * 'ident option - | Right - | Ring - | Split - | Symmetry - | Transitivity of 'term - -type 'tactic tactical = - | LocatedTactical of location * 'tactic tactical - - | Fail - | For of int * 'tactic tactical - | IdTac - | Repeat of 'tactic tactical - | Seq of 'tactic tactical list (* sequential composition *) - | Tactic of 'tactic - | Then of 'tactic tactical * 'tactic tactical list - | Tries of 'tactic tactical list - (* try a sequence of tacticals until one succeeds, fail otherwise *) - | Try of 'tactic tactical (* try a tactical and mask failures *) - -type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] -type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type | `CProp ] - -type term_attribute = - [ `Loc of location (* source file location *) - | `IdRef of string (* ACic pointer *) - ] - -type term = - | AttributedTerm of term_attribute * term - - | Appl of term list - | Appl_symbol of string * int * term list (* literal, instance, args *) - | Binder of binder_kind * capture_variable * term (* kind, name, body *) - | Case of term * string * term option * (case_pattern * term) list - (* what to match, inductive type, out type, list *) - | LetIn of capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (capture_variable * term * int) list * term - (* (name, body, decreasing argument) list, where *) - | Ident of string * subst list (* literal, substitutions *) - | Meta of int * meta_subst list - | Num of string * int (* literal, instance *) - | Sort of sort_kind - -and capture_variable = Cic.name * term option (* name, type *) -and meta_subst = term option -and subst = string * term -and case_pattern = string * capture_variable list - -(* -type cexpr = - | Symbol of string option * string * (subst option) * string option - (* h:xref, name, subst, definitionURL *) - | LocalVar of string option * string (* h:xref, name *) - | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) - | Num of string option * string (* h:xref, value *) - | Appl of string option * cexpr list (* h:xref, args *) - | Binder of string option *string * decl * cexpr - (* h:xref, name, decl, body *) - | Letin of string option * def * cexpr (* h:xref, def, body *) - | Letrec of string option * def list * cexpr (* h:xref, def list, body *) - | Case of string option * cexpr * ((string * cexpr) list) - (* h:xref, case_expr, named-pattern list *) -and - decl = string * cexpr (* name, type *) -and - def = string * cexpr (* name, body *) -and - subst = (UriManager.uri * cexpr) list -and - meta_subst = cexpr option list -*) - diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml deleted file mode 100644 index 411159b2f..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml +++ /dev/null @@ -1,90 +0,0 @@ -(* Copyright (C) 2004, 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/ - *) - -open CicTextualParser2Ast -open Printf - -let pp_binder = function - | `Lambda -> "lambda" - | `Pi -> "pi" - | `Exists -> "exists" - | `Forall -> "forall" - -let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s -let rec pp_capture_variable = function - | name, None -> pp_name name - | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")" -and pp_term = function - | AttributedTerm (_, term) -> pp_term term - - | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | Appl_symbol (symbol, _, terms) -> - sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms)) - | Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) - (pp_term body) - | Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" - (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) - (pp_term term) (pp_patterns patterns) - | LetIn (var, t1, t2) -> - sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) - (pp_term t2) - | LetRec (kind, definitions, term) -> - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " - (List.map - (fun (var, body, _) -> - sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) - definitions)) - (pp_term term) - | Ident (name, []) -> name - | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs) - | Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Num (num, _) -> num - | Sort `Set -> "Set" - | Sort `Prop -> "Prop" - | Sort `Type -> "Type" - | Sort `CProp -> "CProp" - -and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) -and pp_substs substs = String.concat "; " (List.map pp_subst substs) - -and pp_pattern ((head, vars), term) = - sprintf "%s -> %s" - (match vars with - | [] -> head - | _ -> - sprintf "(%s %s)" head - (String.concat " " (List.map pp_capture_variable vars))) - (pp_term term) - -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) - diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli deleted file mode 100644 index 555e3272c..000000000 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* Copyright (C) 2004, 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 pp_term: CicTextualParser2Ast.term -> string