Skip to content

A
ACGtk
Commit 83f28f68 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files
Options

Removed useless directories

parent 283cb5e0
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 5365 deletions
src/grammars.old/Makefile.in deleted 100644 → 0
View file @ 283cb5e0
##########################################################################
# #
# ACG development toolkit #
# #
# Copyright 2008 INRIA #
# #
# More information on "http://acg.gforge.loria.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 #
# #
##########################################################################
include ../Makefile.master
###############################
# #
# Set the following variables #
# #
###############################
# Used libraries
LIBS += gramlib.cma
# The corresponding directories
# (if not in the main ocaml lib directory,
# ex. -I +campl4
LIBDIR = -I +camlp4
# Directories to which the current source files depend on
PREVIOUS_DIRS = ../utils ../lambda
# Source files in the right order of dependance
ML = base_grammar.ml abstract_syntax.ml syntax.ml term_grammar.ml signature_grammar.ml lexicon_grammar.ml parser.ml
EXE_SOURCES = test.ml
####################################
# #
# End of the configuration section #
# #
####################################
include ../Makefile.common
src/grammars.old/abstract_syntax.ml deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)
(* More information on "http://acg.gforge.loria.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 *)
(* *)
(**************************************************************************)
open Printf
open Tries
module Abstract_sig =
struct
type location = Token.flocation
type symbol =
| Prefix of string
| Infix of string
| Outfix of string*string
| Binder of string
type term =
| Id of string * location
(** I f the term is either a constant or a variable (not to
determine it during parsing) *)
| Symbol of symbol * location
| Abs of string * term * location
(** If the term is a intuitionistic abstraction *)
| LAbs of string * term * location
(** If the term is a linear abstraction *)
| App of term * term * location
(** If the term is an application *)
type type_def =
| Type_atom of string * location * term list
(** If the type is atomic *)
| 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 *)
let is_atomic_term = function
| Id _ -> true
| _ -> false
let extract_term_location = function
| Id (_,l) -> l
| Symbol (_,l) -> l
| Abs (_,_,l) -> l
| LAbs (_,_,l) -> l
| App (_,_,l) -> l
let extract_type_location = function
| Type_atom (_,l,_) -> l
| Linear_arrow (_,_,l) -> l
| Arrow (_,_,l) -> l
| Dep (_,_,l) -> l
| Type_Abs (_,l) -> l
let rec term_to_string = function
| Id (s,_) -> s
| Symbol (Prefix s,_) -> s
| Symbol (Infix s,_) -> s
| Symbol (Outfix(s1,s2),_) -> s1^s2
| Symbol (Binder s,_) -> s
| Abs (s,t,_) ->
let vars,u=unfold_abs [s] t in
sprintf
"Lambda %s. %s"
(Utils.string_of_list " " (fun x -> x) (List.rev vars))
(term_to_string u)
| LAbs (s,t,_) ->
let vars,u=unfold_labs [s] t in
sprintf
"lambda %s. %s"
(Utils.string_of_list " " (fun x -> x) (List.rev vars))
(term_to_string u)
| App (t1,t2,_) ->
sprintf
"(%s %s)"
(term_to_string t1)
(term_to_string t2)
and unfold_abs acc = function
| Abs (s,t,_) -> unfold_abs (s::acc) t
| t -> acc,t
and unfold_labs acc = function
| LAbs (s,t,_) -> unfold_labs (s::acc) t
| t -> acc,t
and unfold_app acc = function
| App (t1,t2,_) -> unfold_app (t2::acc) t1
| t -> acc,t
let rec is_atomic_type = function
| Type_atom _ -> true
| Dep (_,t,_) -> is_atomic_type t
| _ -> false
let is_arrow = function
| Arrow _ -> true
| Linear_arrow _ -> true
| _ -> false
let rec type_def_to_string = function
| Type_atom (s,_,terms) ->
(match terms with
[] -> s
| _ -> sprintf "%s %s" s (Utils.string_of_list " " (fun x -> sprintf "(%s)" (term_to_string x)) terms))
| Linear_arrow (t1,t2,_) ->
let arrows,u = unfold_linear_arrow [t1] t2 in
let u_string = if (is_atomic_type u)||(is_arrow u) then type_def_to_string u else sprintf "(%s)" (type_def_to_string u) in
sprintf
"%s -> %s"
(Utils.string_of_list
" -> "
(fun x -> if is_atomic_type x then type_def_to_string x else sprintf "(%s)" (type_def_to_string x))
(List.rev arrows))
u_string
| Arrow (t1,t2,_) ->
let arrows,u = unfold_arrow [t1] t2 in
let u_string = if (is_atomic_type u)||(is_arrow u) then type_def_to_string u else sprintf "(%s)" (type_def_to_string u) in
sprintf
"%s => %s"
(Utils.string_of_list
" => "
(fun x -> if (is_atomic_type x) then type_def_to_string x else sprintf "(%s)" (type_def_to_string x))
(List.rev arrows))
u_string
| Dep ((s,_,ty1),ty2,_) ->
let deps,u = unfold_dep [(s,ty1)] ty2 in
sprintf
"(%s) %s"
(Utils.string_of_list ", " (fun (id,t) -> sprintf "%s:%s" id (type_def_to_string t)) (List.rev deps))
(if is_atomic_type u
then
type_def_to_string u
else
sprintf "(%s)" (type_def_to_string u))
| Type_Abs ((s,_,ty),_) ->
let abs,u = unfold_type_abs [s] ty in
sprintf
"lambda %s.(%s)"
(Utils.string_of_list " " (fun x -> x) (List.rev abs))
(type_def_to_string ty)
and unfold_linear_arrow acc = function
| Linear_arrow (t1,t2,_) -> unfold_linear_arrow (t1::acc) t2
| t -> acc,t
and unfold_arrow acc = function
| Arrow (t1,t2,_) -> unfold_arrow (t1::acc) t2
| t -> acc,t
and unfold_dep acc = function
| Dep ((s,_,t),t2,_) -> unfold_dep ((s,t)::acc) t2
| t -> acc,t
and unfold_type_abs acc = function
| Type_Abs ((s,_,t),_) -> unfold_type_abs (s::acc) t
| t -> acc,t
type kind = K of type_def list
type t = Signature of string * sig_content
and sig_content = sig_entry list
and sig_entry =
| Type_decl of (string * location * kind)
| Term_decl of (string * location * type_def)
let empty s = Signature (s,[])
let insert_type_decl id types loc (Signature (name,content)) =
Signature (name,(Type_decl (id,loc,K types))::content)
let insert_term_decl id ty loc (Signature (name,content)) =
Signature (name,(Term_decl (id,loc,ty))::content)
let to_string (Signature (name,dec)) =
sprintf
"signature %s = \n%s\nend"
name
(Utils.string_of_list
"\n"
(function
| Type_decl (id,_,K types) ->
(match types
with [] -> sprintf "\t%s: type;" id
| _ -> sprintf "\t%s: (%s)type;" id (Utils.string_of_list "," type_def_to_string types))
| Term_decl (id,_,t) -> sprintf "\t%s: %s;" id (type_def_to_string t))
dec)
end
module Abstract_lexicon =
struct
type term = Abstract_sig.term
type type_def = Abstract_sig.type_def
type location = Abstract_sig.location
(*
type t = Lexicon of string * string * string * lex_content
and lex_content = lex_assignment list
and lex_assignment =
| Type_assgt of string * location * type_def
| Const_assgt of string * location * term
let empty name abs_sg obg_sg = Lexicon (name,abs_sg,obg_sg,[])
let insert_type_assgt id ty loc (Lexicon(name,abs_sg,obg_sg,lst)) =
Lexicon (name,abs_sg,obg_sg,(Type_assgt (id,loc,ty))::lst)
let insert_const_assgt id cst loc (Lexicon(name,abs_sg,obg_sg,lst)) =
Lexicon (name,abs_sg,obg_sg,(Const_assgt (id,loc,cst))::lst)
*)
type t = Lexicon of string * string * string * lex_content
and lex_content = lex_assignment Tries.t
and lex_assignment =
| Type_assgt of string * location * type_def
| Const_assgt of string * location * term
let empty name abs_sg obg_sg = Lexicon (name,abs_sg,obg_sg,Tries.empty)
let insert_type_assgt id ty loc (Lexicon(name,abs_sg,obg_sg,tr)) =
Lexicon (name,abs_sg,obg_sg,Tries.insert id (Type_assgt (id,loc,ty)) tr)
let insert_const_assgt id cst loc (Lexicon(name,abs_sg,obg_sg,tr)) =
Lexicon (name,abs_sg,obg_sg,Tries.insert id (Const_assgt (id,loc,cst)) tr)
let to_string (Lexicon (name,abs_sg,obg_sg,tr)) =
sprintf
"lexicon %s(%s): %s = \n%s\nend"
name
abs_sg
obg_sg
(Utils.string_of_list
"\n"
(function
| Type_assgt (id,_,ty) -> sprintf "\t%s:= %s;" id (Abstract_sig.type_def_to_string ty)
| Const_assgt (id,_,t) -> sprintf "\t%s:= %s;" id (Abstract_sig.term_to_string t))
(Tries.content tr))
end
src/grammars.old/abstract_syntax.mli deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)
(* More information on "http://acg.gforge.loria.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 *)
(* *)
(**************************************************************************)
open Tries
(** This modules implements the abstract syntax and the build function for the signatures *)
module Abstract_sig :
sig
(** The type of location in the signature files *)
type location = Token.flocation
(** The type of terms provided by the parser. Note their is no
distinction between variables and constants, as we require this to
be made by the signature *)
type symbol =
| Prefix of string
| Infix of string
| Outfix of string*string
| Binder of string
type term =
| Id of string * location
(** If the term is either a constant or a variable (not to
determine it during parsing) *)
| Symbol of symbol * location
(** If the term is a symbol *)
| Abs of string * term * location
(** If the term is a intuitionistic abstraction *)
| LAbs of string * term * location
(** If the term is a linear abstraction *)
| App of term * term * location
(** If the term is an application *)
(** The type of types as found in the signature files *)
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 *)
(** The type of kinds as found in the signature files *)
type kind = K of type_def list
(** The type of the signature as abstract object *)
type t = Signature of string * sig_content (** The first string is the name of the signature *)
and sig_content = sig_entry list
and 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 and the last parameter is its kind *)
| Term_decl of (string * 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 *)
(** [empty name] returns the empty signature of name [name] *)
val empty : string -> t
(** [insert_type_decl id types loc sig] returns a signature where
the type [id] has been added as type depending of [types] to the
signature [sig] *)
val insert_type_decl : string -> type_def list -> location -> t -> t
(** [insert_term_decl id type loc sig] returns a signature where the
constant [id] of type [type] has been added to the signature [sig]
*)
val insert_term_decl : string -> type_def -> location -> t -> t
(** [to_string sg] returns a string describing the signature
[sg]. Should be parsable *)
val to_string : t -> string
(** [term_to_string t] returns a string describing the term [t]. *)
val term_to_string : term -> string
(** [type_def_to_string t ] returns a string describing the type definition [t] *)
val type_def_to_string : type_def -> string
(** [extract_term_location t] returns the location of the term [t]. *)
val extract_term_location : term -> Token.flocation
(** [extract_type_location t] returns the location of the type definiton [t]. *)
val extract_type_location : type_def -> Token.flocation
end
module Abstract_lexicon :
sig
(** The type of location in the signature files *)
type location = Token.flocation
(** The type of terms provided by the parser. Note their is no
distinction between variables and constants, as we require this to
be made by the signature *)
type term = Abstract_sig.term
(** The type of types as found in the signature files *)
type type_def = Abstract_sig.type_def
(** The type of the signature as abstract object *)
type t = Lexicon of string * string * string * lex_content
(** The first string is the name of the lexicon, the second is the
name of the abstract signature and the last one is the name of the
object signature *)
and lex_content = lex_assignment Tries.t
and lex_assignment =
| Type_assgt of string * location * type_def
(** The first parameter of type [string] is the name of the
abstract type, the second parameter is the place where it is
defined, and the third parameter is its realization as type in
the object signature *)
| Const_assgt of string * location * term
(** The first parameter of type [string] is the name of the
abstract constant, the second parameter is the place where it
is defined, and the third parameter is its realization as term
in the object signature *)
(** [empty name abs_sig obj_sig] returns the empty lexicon of name
[name] from the abstract signature [abs_sig] to the object signature
[obj_sig] *)
val empty : string -> string -> string -> t
(** [insert_type_assgt id type loc lex] returns a lexicon where the
type [id] has been assigned the type [type] at place [loc] to the
lexicon [lex] *)
val insert_type_assgt : string -> type_def -> location -> t -> t
(** [insert_cst_assgt id t loc lex] returns a lexicon where the
constant [id] has been assigned the term [t] at place [loc] to the
lexicon [lex] *)
val insert_const_assgt : string -> term -> location -> t -> t
(** [to_string sg] returns a string describing the signature. Should
be parsable *)
val to_string : t -> string
end
src/grammars.old/base_grammar.ml deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)
(* More information on "http://acg.gforge.loria.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 Base_grammar =
struct
module type Base_grammar =
sig
include Grammar.S with type te = Token.t
exception Parse_Error of string
val luident : string Entry.e
val luident_loc : (string*Token.flocation) Entry.e
val symbol : string list Entry.e
end
module Make(G:Grammar.S with type te = Token.t) =
struct
include G
exception Parse_Error of string
exception Stop
let luident = G.Entry.create "identifier"
let luident_loc = G.Entry.create "identifier"
let symbol =
let rec symbol_parser strm =
match Stream.peek strm with
| Some ("",s) when (s <> ":") && (s <> ".") -> let () = Stream.junk strm in
s::(try
symbol_parser strm
with
| Stream.Failure -> [])
| _ -> raise Stream.Failure in
G.Entry.of_parser "symbol" symbol_parser
GEXTEND G
luident :
[ [ x = UIDENT -> x
| x = LIDENT -> x ] ];
luident_loc :
[ [ x = UIDENT -> x,loc
| x = LIDENT -> x,loc ] ];
END
end
end
src/grammars.old/base_grammar.mli deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)
(* More information on "http://acg.gforge.loria.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 *)
(* *)
(**************************************************************************)
(** This modules implements the basic grammar that is used for the
parsong of signtures and lexicon *)
module Base_grammar :
sig
(** The requirement for a grammar to be basic. *)
module type Base_grammar =
sig
(** A special entry, useful when we don't want to distinguish upper
and lower identiders *)
include Grammar.S with type te = Token.t
exception Parse_Error of string
val luident : string Entry.e
val luident_loc : (string*Token.flocation) Entry.e
val symbol : string list Entry.e
end
(** A module that implements a basic grammar *)
module Make (G:Grammar.S with type te = Token.t) : Base_grammar
end
src/grammars.old/lexicon_grammar.ml deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)
(* More information on "http://acg.gforge.loria.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 *)
(* *)
(**************************************************************************)
open Environment
open Abstract_syntax
open Signature_grammar
open Signature
module Lexicon_grammar =
struct
module type Lexicon_grammar =
sig
include Signature_grammar.Signature_grammar
val lexicon : (Environment.t -> Abstract_lexicon.t) Entry.e
end
module Make(Gram:Signature_grammar.Signature_grammar) =
struct
include Gram
let lexicons = Gram.Entry.create "lexicon list"
let lexicon = Gram.Entry.create "lexicon"
let insert_id id assgt sg loc =
try
match assgt with
| Gram.Const t when Signature.is_a_cst id sg ->
(fun lex -> Abstract_lexicon.insert_const_assgt id t loc lex),assgt
| Gram.Type t when Signature.is_a_type id sg ->
(fun lex -> Abstract_lexicon.insert_type_assgt id t loc lex), assgt
| _ -> Stdpp.raise_with_loc loc (Parse_Error "Mixing type and constants or neither type or constant")
with
| Signature.Not_found -> Stdpp.raise_with_loc loc (Parse_Error (Printf.sprintf "No constant or type \"%s\" in abstract signature" id))
GEXTEND Gram
GLOBAL: lexicons lexicon ;
lexicons :
[ [ lexicons=LIST1 lexicon ; EOI -> lexicons ]];
lexicon :
[ [ "lexicon" ; name = UIDENT ; "(" ; abs_sg_name = UIDENT ; ")" ; ":" ; obj_sg_name = UIDENT ; "=" ; dec=lexicon_declaration ->
(fun env ->
let abs_sg =
try
Environment.get_signature abs_sg_name env
with
| Environment.Error s -> Stdpp.raise_with_loc loc (Parse_Error s) in
let obj_sg =
try Environment.get_signature obj_sg_name env
with
| Environment.Error s -> Stdpp.raise_with_loc loc (Parse_Error s) in
(dec (abs_sg,obj_sg)) (Abstract_lexicon.empty name abs_sg_name obj_sg_name))]];
lexicon_declaration :
[ [ "end" -> (fun sgs lex -> lex)
| e=lexicon_entry ; ";" ; "end" -> (fun sgs -> fst (e sgs))
| e=lexicon_entry ; "end" -> (fun sgs -> fst (e sgs))
| e=lexicon_entry ; ";" ; dec=lexicon_declaration -> (fun sgs -> (fun lex -> (dec sgs) ( (fst (e sgs)) lex))) ] ];
lexicon_entry :
[ [
x = Gram.luident ; ":=" ; e=Gram.entry -> (fun (a_sg,o_sg) -> insert_id x (e o_sg) a_sg loc)
| x = Gram.luident ; "," ; e= lexicon_entry ->
(fun (a_sg,o_sg) ->
let new_lex_f,assgt = e (a_sg,o_sg) in
(fun lex ->
let new_lex,_ = insert_id x assgt a_sg loc in
new_lex_f (new_lex lex)),assgt) ] ];
END
let parse file env =
List.map
(fun lex_f -> lex_f env)
(Utils.new_parse_file file (fun x -> Gram.Entry.parse lexicons (Gram.parsable x)) (fun x -> Parse_Error x))
end
end
src/grammars.old/lexicon_grammar.mli deleted 100644 → 0
View file @ 283cb5e0
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 INRIA *)
(* *)