From 29d132244b797aaaa79319d81e0be4edf05ba7ae Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:04:31 +0000 Subject: [PATCH] - added pack/unpack over AST of terms - created cicAst.mli (it was missing) - added syntax for URIs --- helm/ocaml/cic_transformations/cicAst.ml | 40 ++++++----- helm/ocaml/cic_transformations/cicAst.mli | 82 +++++++++++++++++++++++ 2 files changed, 101 insertions(+), 21 deletions(-) create mode 100644 helm/ocaml/cic_transformations/cicAst.mli diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml index cb65c2497..399181372 100644 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -23,12 +23,8 @@ * http://helm.cs.unibo.it/ *) -(** {2 Parsing related types} *) - type location = Lexing.position * Lexing.position - (* maps old style (i.e. <= 3.07) lexer location to new style location, padding - * with dummy values where needed *) let floc_of_loc (loc_begin, loc_end) = let floc_begin = { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; @@ -37,49 +33,51 @@ let floc_of_loc (loc_begin, loc_end) = let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in (floc_begin, floc_end) - (* the other way round *) let loc_of_floc = function | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> (loc_begin, loc_end) let dummy_floc = floc_of_loc (-1, -1) -(** {2 Cic Ast} *) - 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 *) + [ `Loc of location + | `IdRef of string ] type term = | AttributedTerm of term_attribute * term | Appl of term list - | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Binder of binder_kind * capture_variable * term | Case of term * string option * term option * (case_pattern * term) list - (* what to match, inductive type, out type, list *) - | LetIn of capture_variable * term * term (* name, body, where *) + | LetIn of capture_variable * term * term | LetRec of induction_kind * (capture_variable * term * int) list * term - (* (name, body, decreasing argument) 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 | Meta of int * meta_subst list - | Num of string * int (* literal, instance *) + | Num of string * int | Sort of sort_kind - | Symbol of string * int (* canonical name, instance *) + | Symbol of string * int - | UserInput (* place holder for user input, used by MatitaConsole, not to be - used elsewhere *) + | UserInput + | Uri of string * subst list option -and capture_variable = Cic.name * term option (* name, type *) +and capture_variable = Cic.name * term option and meta_subst = term option and subst = string * term and case_pattern = string * capture_variable list +let pack asts = + List.fold_right + (fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc)) + asts (Sort `Type) + +let rec unpack = function + | Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast] + | Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt + | _ -> assert false + diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli new file mode 100644 index 000000000..8abd4f3c9 --- /dev/null +++ b/helm/ocaml/cic_transformations/cicAst.mli @@ -0,0 +1,82 @@ +(* 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/ + *) + +(** {2 Parsing related types} *) + +type location = Lexing.position * Lexing.position + + (** maps old style (i.e. <= 3.07) lexer location to new style location, + * padding with dummy values where needed *) +val floc_of_loc: int * int -> location + + (* the other way round *) +val loc_of_floc: location -> int * int + + (* dummy location *) +val dummy_floc: location + +(** {2 Cic Ast} *) + +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 + | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Case of term * string option * 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 option + (* literal, substitutions. + * Some [] -> user has given an empty explicit substitution list + * None -> user has given no explicit substitution list *) + | Implicit + | 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 *) + +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 + +val pack: term list -> term +val unpack: term -> term list + -- 2.39.2