package acgtk

You can search for identifiers within the package.

in-package search v0.2.0

Abstract Categorial Grammar development toolkit

Install

Dune Dependency

acg.loria.fr Readme Changelog CeCILL-1.0+ License Edit opam file Versions (2)

Authors

S

Sylvain Pogodalla

Maintainers

S

sylvain.pogodalla@inria.fr

Sources

acgtk-1.5.3.tar.gz

sha256=2743321ae4cc97400856eb503a876cbcbd08435ebc750276399a97481d001d41

md5=04c1e14f98e2c8fd966ef7ef30b38323

doc/src/acgtkLib.logic/abstract_syntax.ml.html

Source file `abstract_syntax.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
(*                  Copyright 2008-2021 INRIA                             *)
(*                                                                        *)
(*  More information on "http://acg.gforge.inria.fr/"                     *)
(*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *)
(*  Authors: see the AUTHORS file                                         *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*  $Rev::                              $:  Revision of last commit       *)
(*  $Author::                           $:  Author of last commit         *)
(*  $Date::                             $:  Date of last commit           *)
(*                                                                        *)
(**************************************************************************)

module Abstract_syntax =
struct

  type location = Lexing.position*Lexing.position

  (** The type of the kind of associativity for infix operators *)
  type associativity =
    | Left
    | Right
    | NonAss

  (** The type of the syntactic behaviour of constants defined in
      the signature *)    
  type syntactic_behavior =
    | Default 
    | Prefix 
    | Infix of associativity * float
    (* the float indicates precedence in the total order of infix
    operators *)
    | Binder

  type abstraction =
    | Linear
    | Non_linear
	

  type term =
    | Var of (string * location)
	(** If the term is variable (bound by a binder)*)
    | Const of (string * location)
	(** If the term is a constant (not bound by a binder) *)
    | Abs of (string * location * term * location)
	(** If the term is a intuitionistic abstraction *)
    | LAbs of (string * location * term * location)
	(** If the term is a linear abstraction *)
    | App of (term * term * location)
	(** If the term is an application *)	

  let rec unlinearize_term = function
    | Var _ as v -> v
    | Const _ as c -> c
    | Abs (x,loc,t,loc') -> Abs (x,loc,unlinearize_term t,loc')
    | LAbs (x,loc,t,loc') -> Abs (x,loc,unlinearize_term t,loc')
    | App (t,u,loc) -> App (unlinearize_term t,unlinearize_term u,loc)

  type type_def =
    | Type_atom of (string * location * term list)
	(** If the type is atomic. The third parameter is the terms to
	    which the type is applied in case of a dependent type. The
	    list is empty if the type does not depend on any type *)
    | Linear_arrow of (type_def * type_def * location)
	(** If the type is described with a linear abstraction *)
    | Arrow of (type_def * type_def * location)
	(** If the type is described with a intuitionistic abstraction
	*)
(*    | Dep of (string * location * type_def) * type_def * location
	(** If the type is a dependent type *)
    | Type_Abs of (string * location * type_def)  * location
	(** If the type is a dependent type build with an abstraction *) *)



  type sig_entry = 
    | Type_decl of (string * location * kind )
	(** The first parameter ([string]) is the name of the type,
	    the second parameter is the place in the file where it was
	    defined *)
    | Type_def of (string * location * type_def * kind)
	(** Tthe first parameter ([string]) is the name of the defined type,
	    the second parameter is the place in the file where it was
	    defined and the last parameter is its value *)
    | Term_decl of (string * syntactic_behavior * location * type_def)
	(** The first parameter ([string]) is the name of the constant,
	    the second parameter is the place in the file where it was
	    defined and the last parameter is its type *)
    | Term_def of (string * syntactic_behavior * location * term * type_def)
	(** The first parameter ([string]) is the name of the constant,
	    the second parameter is the place in the file where it was
	    defined and the last parameter is its value *)
  and kind = K of type_def list
    
  type lex_entry = 
    | Type of (string*location * type_def)
    | Constant of (string*location * term)
end