Commit 51181014 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

acg-data added as alternative signature and lexicon implementations

parent ece24d3b
......@@ -301,7 +301,7 @@ on `(hostname || uname -n) 2>/dev/null | sed 1q`
"
# Files that config.status was made for.
config_files=" ./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/scripting/Makefile"
config_files=" ./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/acg-data/Makefile src/scripting/Makefile"
ac_cs_usage="\
\`$as_me' instantiates files from templates according to the
......@@ -418,6 +418,7 @@ do
"src/logic/Makefile") CONFIG_FILES="$CONFIG_FILES src/logic/Makefile" ;;
"src/grammars/Makefile") CONFIG_FILES="$CONFIG_FILES src/grammars/Makefile" ;;
"src/lambda/Makefile") CONFIG_FILES="$CONFIG_FILES src/lambda/Makefile" ;;
"src/acg-data/Makefile") CONFIG_FILES="$CONFIG_FILES src/acg-data/Makefile" ;;
"src/scripting/Makefile") CONFIG_FILES="$CONFIG_FILES src/scripting/Makefile" ;;
*) { { echo "$as_me:$LINENO: error: invalid argument: $ac_config_target" >&5
......
......@@ -124,7 +124,7 @@ AC_SUBST(OCAMLP4_LOC)
AC_SUBST(SET_MAKE)
AC_CONFIG_FILES([./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/scripting/Makefile])
AC_CONFIG_FILES([./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/acg-data/Makefile src/scripting/Makefile])
AC_PROG_MAKE_SET
......
......@@ -2134,7 +2134,7 @@ echo "${ECHO_T}Compilation will be done with the $OCAML09WARNINGS option" >&6; }
ac_config_files="$ac_config_files ./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/scripting/Makefile"
ac_config_files="$ac_config_files ./Makefile config/Makefile src/Makefile.master src/Makefile.common src/Makefile src/utils/Makefile src/logic/Makefile src/grammars/Makefile src/lambda/Makefile src/acg-data/Makefile src/scripting/Makefile"
{ echo "$as_me:$LINENO: checking whether ${MAKE-make} sets \$(MAKE)" >&5
......@@ -2744,6 +2744,7 @@ do
"src/logic/Makefile") CONFIG_FILES="$CONFIG_FILES src/logic/Makefile" ;;
"src/grammars/Makefile") CONFIG_FILES="$CONFIG_FILES src/grammars/Makefile" ;;
"src/lambda/Makefile") CONFIG_FILES="$CONFIG_FILES src/lambda/Makefile" ;;
"src/acg-data/Makefile") CONFIG_FILES="$CONFIG_FILES src/acg-data/Makefile" ;;
"src/scripting/Makefile") CONFIG_FILES="$CONFIG_FILES src/scripting/Makefile" ;;
*) { { echo "$as_me:$LINENO: error: invalid argument: $ac_config_target" >&5
......
PHONY: test
SUBDIRS= utils logic grammars lambda
SUBDIRS= utils logic grammars acg-data scripting lambda
test:
$(foreach dir,$(SUBDIRS),$(MAKE) -r -S -C $(dir) byte;)
......
PHONY: test
SUBDIRS= utils logic grammars lambda
SUBDIRS= utils logic grammars acg-data scripting lambda
test:
$(foreach dir,$(SUBDIRS),$(MAKE) -r -S -C $(dir) byte;)
......
###############################################
# #
# Makefile for directories with no executable #
# #
###############################################
include ../Makefile.master
###############################
# #
# Set the following variables #
# #
###############################
# Used libraries
LIBS += dyp.cma str.cma
# The corresponding directories
# (if not in the main ocaml lib directory,
# ex. -I +campl4
LIBDIR = -I +dypgen -I +camlp4
# Directories to which the current source files depend on
PREVIOUS_DIRS = ../utils ../logic ../grammars
# Source files in the right order of dependance
ML = signature.ml lexicon.ml
EXE_SOURCES = test.ml
####################################
# #
# End of the configuration section #
# #
####################################
include ../Makefile.common
open Abstract_syntax
open Lambda
open Signature
module Make (Sg:Interface.Signature_sig with type term = Lambda.term and type stype = Lambda.stype) =
struct
exception Duplicate_type_interpretation
exception Duplicate_constant_interpretation
(* exception Not_yet_interpreted_value*)
exception Missing_interpretation of string
module Dico = Utils.StringMap
module Signature=Sg
type signature = Sg.t
type interpretation =
| Type of (Abstract_syntax.location * Lambda.stype )
| Constant of (Abstract_syntax.location * Lambda.term )
let interpretation_to_string i sg = match i with
| Type (_,t) -> Printf.sprintf "\t%s" (Lambda.type_to_string t (Sg.id_to_string sg))
| Constant (_,c) -> Printf.sprintf "\t%s" (Lambda.term_to_string c (Sg.id_to_string sg))
type t = {name:string*Abstract_syntax.location;
dico:interpretation Dico.t;
abstract_sig:Sg.t;
object_sig:Sg.t;}
let name {name=n}=n
let get_sig {abstract_sig=abs;object_sig=obj} = abs,obj
let empty name ~abs ~obj = {name=name;dico=Dico.empty;abstract_sig=abs;object_sig=obj}
let emit_missing_inter lex lst =
let lex_name,loc = name lex in
let abs_name,_ = Sg.name lex.abstract_sig in
raise (Error.Error (Error.Lexicon_error (Error.Missing_interpretations(lex_name,abs_name,lst),loc)))
let rec interpret_type abs_ty ({abstract_sig=abs_sg;dico=dico} as lex) =
match abs_ty with
| Lambda.Atom i ->
(let _,abs_ty_as_str = Sg.id_to_string abs_sg i in
try
match Dico.find abs_ty_as_str dico with
| Type (_,obj_ty) -> obj_ty
| Constant _ -> failwith "Bug"
with
| Not_found -> emit_missing_inter lex [abs_ty_as_str])
| Lambda.DAtom i -> interpret_type (Sg.unfold_type_definition i abs_sg) lex
| Lambda.LFun (ty1,ty2) -> Lambda.LFun (interpret_type ty1 lex,interpret_type ty2 lex)
| Lambda.Fun (ty1,ty2) -> Lambda.Fun (interpret_type ty1 lex,interpret_type ty2 lex)
| _ -> failwith "Not yet implemented"
let rec interpret_term abs_t ({abstract_sig=abs_sg;dico=dico} as lex) =
match abs_t with
| (Lambda.Var i| Lambda.LVar i) -> abs_t
| Lambda.Const i ->
(let _,abs_term_as_str = Sg.id_to_string abs_sg i in
try
match Dico.find abs_term_as_str dico with
| Constant (_,obj_t) -> obj_t
| Type _ -> failwith "Bug"
with
| Not_found -> emit_missing_inter lex [abs_term_as_str] )
| Lambda.DConst i ->
interpret_term (Sg.unfold_term_definition i abs_sg) lex
| Lambda.Abs(x,t) -> Lambda.Abs(x,interpret_term t lex)
| Lambda.LAbs(x,t) -> Lambda.LAbs(x,interpret_term t lex)
| Lambda.App(t,u) -> Lambda.App(interpret_term t lex,interpret_term u lex)
| _ -> failwith "Not yet implemented"
let interpret t ty lex =
let t_interpretation = (interpret_term t lex) in
(* let () = Printf.printf "Going_to_normalize:\t%s\n%!" (Lambda.term_to_string t_interpretation (Sg.id_to_string lex.object_sig)) in*)
Lambda.normalize ~id_to_term:(fun i -> Sg.unfold_term_definition i lex.object_sig) t_interpretation,interpret_type ty lex
let insert e ({dico=d} as lex) = match e with
| Abstract_syntax.Type (id,loc,ty) -> {lex with dico=Dico.add id (Type (loc,Sg.convert_type ty lex.object_sig)) d}
| Abstract_syntax.Constant (id,loc,t) -> {lex with dico=Dico.add id (Constant (loc,Sg.typecheck t (interpret_type (Sg.type_of_constant id lex.abstract_sig) lex) lex.object_sig)) d}
let to_string {name=n,_;dico=d;abstract_sig=abs_sg;object_sig=obj_sg} =
Printf.sprintf
"lexicon %s(%s): %s =\n%send"
n
(fst (Sg.name abs_sg))
(fst (Sg.name obj_sg))
(match
Dico.fold
(fun k i -> function
| None -> Some (Printf.sprintf "\t%s := %s;" k (interpretation_to_string i obj_sg))
| Some a -> Some (Printf.sprintf "%s\n\t%s := %s;" a k (interpretation_to_string i obj_sg)))
d
None with
| None -> ""
| Some s -> Printf.sprintf "%s\n" s)
let check ({dico=d;abstract_sig=abs} as lex) =
let missing_interpretations =
Signature.fold
(fun e acc ->
match Sg.is_declared e abs with
| Some s ->
(try
let _ = Utils.StringMap.find s d in
acc
with
| Not_found -> s::acc)
| None -> acc
)
[]
abs in
match missing_interpretations with
| [] -> ()
| lst -> emit_missing_inter lex lst
let compose lex1 lex2 n =
{name=n;
dico =
Dico.fold
(fun key inter acc ->
match inter with
| Type (l,stype) -> Dico.add key (Type (l,interpret_type stype lex1)) acc
| Constant (l,t) -> Dico.add key (Constant (l,Lambda.normalize ~id_to_term:(fun i -> Sg.unfold_term_definition i lex1.object_sig) (interpret_term t lex1))) acc)
lex2.dico
Dico.empty;
abstract_sig = lex2.abstract_sig;
object_sig=lex1.object_sig}
end
module Sylvain_lexicon = Make (Sylvains_signature)
open Signature
module Sylvain_lexicon : Interface.Lexicon_sig
This diff is collapsed.
open Abstract_syntax
open Lambda
type sig_entry =
| Type_declaration of string * int * Lambda.kind
| Type_definition of string * int * Lambda.kind * Lambda.stype
| Term_declaration of string * int * Abstract_syntax.syntactic_behavior * Lambda.stype
| Term_definition of string * int * Abstract_syntax.syntactic_behavior * Lambda.stype * Lambda.term
module Sylvains_signature : Interface.Signature_sig
with
type term = Lambda.term
and type stype = Lambda.stype
and type entry = sig_entry
module Sg = Signature.Sylvains_signature
(*module Lex = Syntactic_data_structures.Abstract_lex*)
module Lex = Lexicon.Sylvain_lexicon
module Test = Interactive.Make(Lex)
let () = Test.main ()
......@@ -21,7 +21,7 @@ LIBS += dyp.cma str.cma
LIBDIR = -I +dypgen -I +camlp4
# Directories to which the current source files depend on
PREVIOUS_DIRS = ../utils ../logic ../grammars ../lambda.sylvain
PREVIOUS_DIRS = ../utils ../logic ../grammars ../acg-data
# Source files in the right order of dependance
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment