ptree.mli 3.67 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25

(*s Parse trees. *)

type loc = Loc.position

(*s Logical expressions (for both terms and predicates) *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26 27
type real_constant = Term.real_constant
type constant = Term.constant
28

29 30 31
type pp_quant =
  | PPforall | PPexists

32
type pp_infix = 
33
  | PPand | PPor | PPimplies | PPiff 
34 35

type pp_prefix = 
36
  | PPnot
37

38 39 40 41
type ident = { id : string; id_loc : loc }

type qualid =
  | Qident of ident
42
  | Qdot of qualid * ident
43

44 45 46
type pty =
  | PPTtyvar of ident
  | PPTtyapp of pty list * qualid
47

Andrei Paskevich's avatar
Andrei Paskevich committed
48 49 50 51 52 53 54 55 56
type pattern =
  { pat_loc : loc; pat_desc : pat_desc }

and pat_desc =
  | PPpwild
  | PPpvar of ident
  | PPpapp of qualid * pattern list
  | PPpas of pattern * ident

57 58 59
type uquant =
  ident list * pty

60 61 62 63
type lexpr = 
  { pp_loc : loc; pp_desc : pp_desc }

and pp_desc =
64 65
  | PPvar of qualid
  | PPapp of qualid * lexpr list
66 67 68 69 70 71
  | PPtrue
  | PPfalse
  | PPconst of constant
  | PPinfix of lexpr * pp_infix * lexpr
  | PPprefix of pp_prefix * lexpr
  | PPif of lexpr * lexpr * lexpr
72
  | PPquant of pp_quant * uquant list * lexpr list list * lexpr
73
  | PPnamed of string * lexpr
74
  | PPlet of ident * lexpr * lexpr
75
(*  | PPeps of ident * lexpr *)
Andrei Paskevich's avatar
Andrei Paskevich committed
76
  | PPmatch of lexpr * (pattern * lexpr) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
  | PPcast of lexpr * pty
78 79 80 81

(*s Declarations. *)

type plogic_type =
82
  | PPredicate of pty list
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
83
  | PFunction  of pty list * pty
84

85 86
type imp_exp =
  | Import | Export | Nothing
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87

88
type use = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
89 90
  use_theory  : qualid;
  use_as      : ident option;
91
  use_imp_exp : imp_exp;
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
92 93
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94 95
type clone_subst = {
  ts_subst : (qualid * qualid) list;
96
  ls_subst : (qualid * qualid) list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97 98
}

99 100 101 102
type param = ident option * pty

type type_def = 
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
103
  | TDalias     of pty
104 105 106
  | TDalgebraic of (loc * ident * param list) list

type type_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
107 108
  td_loc    : loc;
  td_ident  : ident;
109
  td_params : ident list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
110
  td_def    : type_def;
111 112 113
}

type logic_decl = { 
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
114 115
  ld_loc    : loc;
  ld_ident  : ident;
116
  ld_params : param list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
117 118
  ld_type   : pty option;
  ld_def    : lexpr option;
119 120
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121 122 123
type prop_kind =
  | Kaxiom | Klemma | Kgoal

124 125 126
type decl = 
  | TypeDecl of loc * type_decl list
  | Logic of loc * logic_decl list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
  | Prop of loc * prop_kind * ident * lexpr
128
  | Inductive_def of loc * ident * pty list * (ident * lexpr) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
129
  | UseClone of loc * use * clone_subst option
130
  | Namespace of loc * ident * decl list
131 132

type theory = {
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133 134
  pt_loc  : loc;
  pt_name : ident;
135
  pt_decl : decl list;
136 137 138
}

type logic_file = theory list
139