Commit 2904be8c authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

By default now generate the realize.svg output

parent 4a1f13ae
......@@ -32,7 +32,7 @@ prefix = @prefix@
exec_prefix = @exec_prefix@
ACG_DIR=src/scripting
ACGC_DIR=src/acg-data
ACGC_DIR=src/grammars
DATA_DIR=@datarootdir@/acgtk
......
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
VERSION="1.2-20150528"
VERSION="1.2-20150529"
AC_INIT([ACG DTK],[$VERSION],[sylvain.pogodalla@loria.fr])
......@@ -187,7 +187,8 @@ AC_MSG_CHECKING([for $OCAMLC version])
AC_MSG_RESULT([$OCAMLC version is $OCAML_VERSION])
# Check whether the caml version checker is provided
ML_CHECK_FILE=config/ml_check.ml
DIR=$( cd "$( dirname "$0" )" && pwd )
ML_CHECK_FILE=$DIR/config/ml_check.ml
AC_CHECK_FILE($ML_CHECK_FILE,,AC_MSG_ERROR(Cannot check versions))
# check that this version is at least the one we need
......
......@@ -3215,7 +3215,8 @@ $as_echo_n "checking for $OCAMLC version... " >&6; }
$as_echo "$OCAMLC version is $OCAML_VERSION" >&6; }
# Check whether the caml version checker is provided
ML_CHECK_FILE=config/ml_check.ml
DIR=$( cd "$( dirname "$0" )" && pwd )
ML_CHECK_FILE=$DIR/config/ml_check.ml
as_ac_File=`$as_echo "ac_cv_file_$ML_CHECK_FILE" | $as_tr_sh`
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ML_CHECK_FILE" >&5
$as_echo_n "checking for $ML_CHECK_FILE... " >&6; }
......
archive: "http://calligramme.loria.fr/acg/software/acg-1.1-20150506.tar.gz"
checksum: "2bb5e2cb41c3b2439ea7eb268c111fb8"
archive: "http://calligramme.loria.fr/acg/software/acg-1.2-20150529.tar.gz"
checksum: "129a3d11907d7688172ba35f36709b54"
......@@ -21,10 +21,10 @@
#SUBDIRS= utils logic grammars acg-data scripting lambda datalog
#SUBDIRS= utils logic grammars acg-data scripting datalog reduction s_datalog
SUBDIRS= utils logic datalog.prover grammars acg-data scripting datalog.solver
SUBDIRS= utils logic datalog.prover acg-data grammars scripting datalog.solver
ACG_DIR=scripting
ACGC_DIR=acg-data
ACGC_DIR=grammars
acg acg.opt:
$(MAKE) -r -S -C $(ACG_DIR) $@
......
......@@ -26,21 +26,21 @@ include ../Makefile.master
###############################
# Used libraries
LIBS += dyp.cma str.cma ANSITerminal.cma
LIBS += dyp.cma str.cma
# The corresponding directories
# (if not in the main ocaml lib directory,
# ex. -I +campl4
LIBDIR += @DYPGEN_INCLUDE@ @ANSITerminal_INCLUDE@
LIBDIR += @DYPGEN_INCLUDE@
# Directories to which the current source files depend on
PREVIOUS_DIRS = ../utils ../logic ../grammars ../datalog.prover
PREVIOUS_DIRS = ../utils ../logic ../datalog.prover
# Source files in the right order of dependance
ML = type_system.ml signature.ml reduction.ml acg_lexicon.ml
ML = error.ml type_system.ml interface.ml signature.ml reduction.ml acg_lexicon.ml
EXE_SOURCES = acgc.ml
EXE_SOURCES =
####################################
# #
......
......@@ -452,4 +452,4 @@ struct
end
module Sylvain_lexicon = Make (Sylvains_signature)
module Data_Lexicon = Make (Data_Signature)
......@@ -19,4 +19,7 @@
open Signature
module Sylvain_lexicon : Interface.Lexicon_sig with type Signature.term=Lambda.Lambda.term and type Signature.stype=Lambda.Lambda.stype
module Data_Lexicon : Interface.Lexicon_sig
with
type Signature.term=Lambda.Lambda.term
and type Signature.stype=Lambda.Lambda.stype
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 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 Sg = Signature.Sylvains_signature
(*module Lex = Syntactic_data_structures.Abstract_lex*)
module Lex = Acg_lexicon.Sylvain_lexicon
module Test = Interactive.Make(Lex)
Test.main ()
......@@ -441,6 +441,6 @@ module Table = Table.Make_table(struct let b = 10 end)
end
*)
module Sylvains_signature = Make(Tries.Tries)(Table)
module Data_Signature = Make(Tries.Tries)(Table)
......@@ -20,14 +20,16 @@
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
module Data_Signature : Interface.Signature_sig
with
type term = Lambda.term
and type stype = Lambda.stype
......
......@@ -26,21 +26,21 @@ include ../Makefile.master
###############################
# Used libraries
LIBS += dyp.cma str.cma
LIBS += dyp.cma str.cma ANSITerminal.cma
# The corresponding directories
# (if not in the main ocaml lib directory,
# ex. -I +campl4
LIBDIR += @DYPGEN_INCLUDE@
LIBDIR += @DYPGEN_INCLUDE@ @ANSITerminal_INCLUDE@
# Directories to which the current source files depend on
PREVIOUS_DIRS = ../utils ../logic
PREVIOUS_DIRS = ../utils ../logic ../datalog.prover ../acg-data
# Source files in the right order of dependance
#ML = error.ml interface.ml environment.ml entry.ml syntactic_data_structures.ml acg_token.ml data_lexer.ml data_parser.ml interactive.ml
ML = error.ml interface.ml environment.ml entry.ml acg_token.ml data_lexer.ml data_parser.ml interactive.ml
ML = environment.ml entry.ml acg_token.ml data_lexer.ml data_parser.ml
EXE_SOURCES =
EXE_SOURCES = acgc.ml
DYP = data_parser.dyp
CAMLLEX = data_lexer.mll
......@@ -69,14 +69,14 @@ include ../Makefile.common
# @OCAMLLEX@ $<
data_parser.ml: ../utils/utils.cmi acg_token.cmi \
data_lexer.cmi error.cmi environment.cmi entry.cmi \
data_lexer.cmi ../acg-data/error.cmi environment.cmi entry.cmi \
../logic/abstract_syntax.cmi
data_parser.cmo: ../utils/utils.cmi acg_token.cmi \
data_lexer.cmo error.cmi environment.cmi entry.cmi \
data_lexer.cmo ../acg-data/error.cmi environment.cmi entry.cmi \
../logic/abstract_syntax.cmi data_parser.cmi
data_parser.cmx: ../utils/utils.cmx acg_token.cmx \
data_lexer.cmx error.cmx environment.cmx entry.cmx \
data_lexer.cmx ../acg-data/error.cmx environment.cmx entry.cmx \
../logic/abstract_syntax.cmx data_parser.cmi
data_parser.ml: ../utils/utils.cmi acg_token.cmi \
......@@ -98,4 +98,4 @@ truc : $(filter-out essai_sylvain.cmo,$(CMO)) example_dispatch.cmo essai_sylvai
echo $^
example_dispatch.cmo : PP=-pp "@OCAMLP4@ pa_r.cmo pa_rp.cmo pr_dump.cmo pa_extend.cmo"
example_dispatch.cmx : PP=-pp "@OCAMLP4@ pa_r.cmo pa_rp.cmo pr_dump.cmo pa_extend.cmo"
\ No newline at end of file
example_dispatch.cmx : PP=-pp "@OCAMLP4@ pa_r.cmo pa_rp.cmo pr_dump.cmo pa_extend.cmo"
(**************************************************************************)
(* *)
(* ACG development toolkit *)
(* *)
(* Copyright 2008 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 Lex = Acg_lexicon.Data_Lexicon *)
(*module Test = Interactive.Make(Lex)
Test.main ()
*)
(*module Actual_env = Environment.Make(Lex) *)
module Actual_env = Environment.Environment
module Sg=Actual_env.Signature1
type return_status = Failure | Success of ((string option) * Actual_env.t)
(* The pair is meant to keep the name of the current parsing file,
and the build environment *)
(*module Actual_parser = Data_parser.Make(Actual_env) *)
module Actual_parser = Data_parser.Parser
let resize_terminal () =
let () = Utils.sterm_set_size () in
Utils.term_set_size ()
let empty_env = Actual_env.empty
let interactive = ref false
let dirs = ref [""]
let output_name = ref None
let return_status = ref (Success (None,empty_env))
let initialize name =
let () = output_name := Some name in
return_status := Success (!output_name,empty_env)
let options =
[
("-version", Arg.Unit (fun () -> Printf.printf "%s\n" Version.version;exit 0), Format.sprintf "@[@,@[<hov 10>@[Prints@ the@ version@ number@]@]@]");
("-o", Arg.String initialize, Format.sprintf "@[-o file_name@, @[<hv 9>@[sets@ the@ name@ of@ the@ ouput@ file@ to@ \"file_name\".@ The@ default@ is@ to@ use@ the@ base@ name@ (with@ no@ extension)@ of@ the@ first@ file@ argument@ with@ the@ suffix@ \".acgo\"@]@]@]");
("-i", Arg.Set interactive , Format.sprintf "@[@,@[<5>Enters@ the@ interaction@ loop@ to@ parse@ terms@ according@ to@ signatures@]@]");
("-I", Arg.String (fun dir -> dirs := (!dirs)@[dir]) , Format.sprintf "@[@[-I dir@, @[<15>@[sets@ dir@ as@ a@ directory@ in@ which@ file@ arguments@ can@ be@ looked@ for@]@]@]@]")
]
let usg_msg = Format.sprintf "@[usage:\n@[\t%s [options] file1 file2 ...@]@, @[This@ command@ parse@ the@ files@ which@ are@ supposed@ to@ be@ files@ containing@ acg@ signatures@ or@ lexicons@,@ either@ as@ source@ files@ (the_file.acg)@ or@ object@ files@ (the_file.acgo).@ If@ all@ the@ parses@ are@ successful@,@ a@ binary@ containing@ all@ the@ acg@ signatures@ and@ lexicons@ is@ created.@ Its@ default@ name@ is@ \"filen.acgo\"@ where@ filen.acg@ is@ the@ last@ acg@ source@ file@ of@ the@ list@ (see@ option@ -o).@ Files@ should@ have@ a@ suffix@ \".acg\"@ or@ \".acgo\".@]@]@]" Sys.executable_name
let parse_term sg =
let t = ref None in
let rec parse_rec = function
| true ->
let () = Printf.printf "Enter a term: " in
let term_string = read_line () in
(match Actual_parser.parse_term term_string sg with
| None -> parse_rec true
| Some ta -> let () = t:= (Some ta) in false )
| false -> false in
let () =
while (parse_rec true) do
()
done in
match !t with
| Some u -> u
| _ -> failwith "Strange..."
type file_type = Source | Object | Neither
let parse filename dirs status =
match status with
| Failure -> Failure
| Success (name,env) ->
let file_type =
match Filename.check_suffix filename ".acg" with
| true -> Source
| false ->
(match Filename.check_suffix filename ".acgo" with
| true -> Object
| false -> Neither) in
match file_type with
| Neither ->
let () = Printf.fprintf stderr "File name's suffixes should be \".acg\" or \".acgo\". The name \"%s\" has not this suffix.\n" filename in
Failure
| Source ->
let basename=Filename.basename filename in
let name_wo_suffix = Filename.chop_suffix basename ".acg" in
begin
match Actual_parser.parse_data filename dirs env with
| None -> Failure
| Some e -> Success ((Some (Printf.sprintf "%s.acgo" name_wo_suffix)),e)
end
| Object ->
let new_env = Actual_env.read filename dirs in
match new_env with
| None -> Failure
| Some n_e -> Success (name,Actual_env.append env n_e)
let term_parsing i env =
if not i then
()
else
let n = Actual_env.sig_number env in
let m = Actual_env.lex_number env in
let available_data =
Utils.string_of_list
"\n"
(fun x -> x)
(Actual_env.fold
(fun d a ->
match d with
| Actual_env.Signature sg -> (Printf.sprintf "\tSignature\t%s" (fst (Actual_env.Signature1.name sg)))::a
| Actual_env.Lexicon lx -> (Printf.sprintf "\tLexicon\t\t%s" (fst (Actual_env.Lexicon.name lx)))::a)
[]
env) in
let chosen_sig=Actual_env.choose_signature env in
let chosen_sig_name_loaded =
match chosen_sig with
| None -> ""
| Some s -> Printf.sprintf "Signature \"%s\" loaded." (fst (Sg.name s)) in
if (n+m=0) || (not i)
then
()
else
try
let () = if (n=1)&&(m=0) then Printf.printf "%s\n" chosen_sig_name_loaded else () in
while true do
try
let () = Printf.printf "Available data:\n%s\n" available_data in
let entry =
match n,chosen_sig with
| 1, Some s -> Actual_env.Signature s
| _,_ ->
let () = Printf.printf "Enter a name: " in
let sig_string = read_line () in
Actual_env.get sig_string env in
match entry with
| Actual_env.Signature sg -> ignore (parse_term sg)
| Actual_env.Lexicon lex ->
let abs,obj=Actual_env.Lexicon.get_sig lex in
let t,ty = parse_term abs in
let t',ty'=Actual_env.Lexicon.interpret t ty lex in
Printf.printf
"Interpreted as:\n%s : %s\n"
(Actual_env.Signature1.term_to_string t' obj)
(Actual_env.Signature1.type_to_string ty' obj)
with
| Actual_env.Signature_not_found sig_name -> Printf.printf "No such signature in %s\n" sig_name
done
with
| End_of_file -> let () = print_newline () in ()
let output_env name env =
let () = Actual_env.write name env in
Printf.printf "Output written on: \"%s\"\n%!" name
let main () =
let () = resize_terminal () in
let anon_fun file =
return_status := parse file !dirs !return_status in
let () = Arg.parse options anon_fun usg_msg in
match !return_status with
| Failure -> 1
| Success (name,env) ->
match name with
| None ->
let () = Printf.fprintf stderr "No ouput file is produced\nPlease specify an output file.\n%!"
in 0
| Some n ->
let () = output_env n env in
let () = term_parsing !interactive env in
0
let _ = main ()
......@@ -22,6 +22,7 @@
open Abstract_syntax
open Dyp
open Environment
module Env = Utils.StringSet
......@@ -29,14 +30,14 @@
type token=Acg_token.Token.t
open Acg_token.Token
module Make (E:Environment.Environment_sig) =
(* module Make (E:Environment.Environment_sig) = *)
module Parser =
struct
type local_data =
| Signature of E.Signature1.t
| Abs_and_obj of (E.Signature1.t * E.Signature1.t)
| Env of E.t
| Signature of Environment.Signature1.t
| Abs_and_obj of (Environment.Signature1.t * Environment.Signature1.t)
| Env of Environment.t
}
......@@ -138,7 +139,7 @@
let get_env_value = function
| None -> E.empty
| None -> Environment.empty
| Some (Env e) -> e
| Some (Abs_and_obj _) -> failwith "Bug: looking for an env while abs_obj is the current local data"
| Some (Signature _) -> failwith "Bug: looking for an env while signature is the current local data"
......@@ -179,10 +180,10 @@ EOI
<(string*Abstract_syntax.location)> SYMBOL
/*
%start <E.t> data
%start <E.Signature1.t -> E.Signature1.t> sig_entry
%start <E.Lexicon.t -> E.Lexicon.t> lex_entry
%start <(E.Signature1.term*E.Signature1.stype)> term_alone
%start <Environment.t> data
%start <Environment.Signature1.t -> Environment.Signature1.t> sig_entry
%start <Environment.Lexicon.t -> Environment.Lexicon.t> lex_entry
%start <(Environment.Signature1.term*Environment.Signature1.stype)> term_alone
*/
/* optional types for entry points are removed due to a bug in dypgen 20090430 */
......@@ -205,8 +206,8 @@ EOI
data:
| EOI {get_env_value dyp.last_local_data}
| signature<s> ...@{s,[Local_data (Some (Env (E.insert ~override:dyp.global_data (E.Signature s) ~to_be_dumped:true (get_env_value dyp.last_local_data))))]} data<d> {d}
| lexicon<l> ...@{let () = E.Lexicon.check l in l,[Local_data (Some (Env (E.insert ~override:dyp.global_data (E.Lexicon l) ~to_be_dumped:true (get_env_value dyp.last_local_data))))]} data<d> {d}
| signature<s> ...@{s,[Local_data (Some (Env (Environment.insert ~override:dyp.global_data (Environment.Signature s) ~to_be_dumped:true (get_env_value dyp.last_local_data))))]} data<d> {d}
| lexicon<l> ...@{let () = Environment.Lexicon.check l in l,[Local_data (Some (Env (Environment.insert ~override:dyp.global_data (Environment.Lexicon l) ~to_be_dumped:true (get_env_value dyp.last_local_data))))]} data<d> {d}
signature :
| SIG_OPEN sig_ident EQUAL sig_entries {$4}
......@@ -223,14 +224,14 @@ EOI
let env = get_env_value dyp.last_local_data in
let signature =
try
E.get_signature name env
Environment.get_signature name env
with
| E.Signature_not_found _ -> raise Dyp.Giveup in
| Environment.Signature_not_found _ -> raise Dyp.Giveup in
signature,[Local_data (Some (Signature (signature)))]}
sig_entries {$5}
sig_ident :
| IDENT<n> @{n,[Local_data (Some (Signature (E.Signature1.empty n)))]}
| IDENT<n> @{n,[Local_data (Some (Signature (Environment.Signature1.empty n)))]}
lexicon :
| LEX_OPEN lex_opening<l> EQUAL lex_entries<e> {e (l~non_linear:false)}
......@@ -243,19 +244,19 @@ lexicon_composition :
fun name ->
try
let env=get_env_value dyp.last_local_data in
let l1 = E.get_lexicon name1 env in
E.Lexicon.compose l1 (l ("__NO__NAME__",(Lexing.dummy_pos,Lexing.dummy_pos))) ( name)
let l1 = Environment.get_lexicon name1 env in
Environment.Lexicon.compose l1 (l ("__NO__NAME__",(Lexing.dummy_pos,Lexing.dummy_pos))) ( name)
with
| E.Lexicon_not_found _ ->
| Environment.Lexicon_not_found _ ->
emit_parse_error (Error.No_such_signature name1) loc}
| LPAREN lexicon_composition<c> RPAREN {c}
composition_argument:
| IDENT<name,loc> {fun res_name->
try
E.get_lexicon name (get_env_value dyp.last_local_data)
Environment.get_lexicon name (get_env_value dyp.last_local_data)
with
| E.Lexicon_not_found _ ->
| Environment.Lexicon_not_found _ ->
emit_parse_error (Error.No_such_signature name) loc}
| lexicon_composition<c> {c}
......@@ -265,16 +266,16 @@ composition_argument:
let env = get_env_value dyp.last_local_data in
let abs =
try
E.get_signature abs_name env
Environment.get_signature abs_name env
with
| E.Signature_not_found _ -> emit_parse_error (Error.No_such_signature abs_name) abs_loc in
| Environment.Signature_not_found _ -> emit_parse_error (Error.No_such_signature abs_name) abs_loc in
let obj =
try
E.get_signature obj_name env
Environment.get_signature obj_name env
with
| E.Signature_not_found _ -> emit_parse_error (Error.No_such_signature obj_name) obj_loc in
| Environment.Signature_not_found _ -> emit_parse_error (Error.No_such_signature obj_name) obj_loc in
let lex = fun ~non_linear ->
E.Lexicon.empty name ~abs:abs ~obj:obj ~non_linear:non_linear in
Environment.Lexicon.empty name ~abs:abs ~obj:obj ~non_linear:non_linear in
lex,[Local_data (Some (Abs_and_obj (abs,obj)))]}
sig_entries :
......@@ -302,9 +303,9 @@ sig_entries :
List.fold_left
(fun acc id ->
try
E.Signature1.add_entry (Abstract_syntax.Type_decl (fst id,snd id,(Abstract_syntax.K []))) acc
Environment.Signature1.add_entry (Abstract_syntax.Type_decl (fst id,snd id,(Abstract_syntax.K []))) acc
with
| E.Signature1.Duplicate_type_definition ->
| Environment.Signature1.Duplicate_type_definition ->
let pos1,pos2= snd id in
emit_parse_error (Error.Duplicated_type (fst id)) (pos1,pos2))
s
......@@ -320,9 +321,9 @@ sig_entries :
fun s ->
let new_sig =
try
E.Signature1.add_entry (Abstract_syntax.Type_def (fst $1,snd $1,fst ($3 s),Abstract_syntax.K [])) s
Environment.Signature1.add_entry (Abstract_syntax.Type_def (fst $1,snd $1,fst ($3 s),Abstract_syntax.K [])) s
with
| E.Signature1.Duplicate_type_definition ->
| Environment.Signature1.Duplicate_type_definition ->
let pos1,pos2= snd $1 in
emit_parse_error (Error.Duplicated_type (fst $1)) (pos1,pos2) in
new_sig}
......@@ -355,7 +356,7 @@ sig_entries :
atomic_type :
| IDENT {fun sg ->
let id,((pos1,pos2) as l) = $1 in
match E.Signature1.is_type id sg with
match Environment.Signature1.is_type id sg with
| true -> Abstract_syntax.Type_atom (id,l,[]),l
| false -> emit_parse_error (Error.Unknown_type id) (pos1,pos2)} atom_type
| LPAREN type_expression RPAREN {fun sg -> fst ($2 sg),new_loc $1 $3} atom_type
......@@ -368,9 +369,9 @@ sig_entries :
(fun acc (id,kind,loc) ->
try
let ty = fst ($3 s) in
E.Signature1.add_entry (Abstract_syntax.Term_decl (id,kind,loc,ty)) acc
Environment.Signature1.add_entry (Abstract_syntax.Term_decl (id,kind,loc,ty)) acc
with
| E.Signature1.Duplicate_term_definition ->
| Environment.Signature1.Duplicate_term_definition ->
let pos1,pos2= loc in
emit_parse_error (Error.Duplicated_term id) (pos1,pos2))
s
......@@ -396,17 +397,17 @@ sig_entries :
let new_sig =
try
let term_value,ws = $3 Env.empty [] in
let new_sig2 = E.Signature1.add_entry (Abstract_syntax.Term_def (id,k,l,term_value,fst ($5 s))) s in
let new_sig2 = Environment.Signature1.add_entry (Abstract_syntax.Term_def (id,k,l,term_value,fst ($5 s))) s in
(match ws with
| [] -> new_sig2
| lst -> E.Signature1.add_warnings ws new_sig2) with
| E.Signature1.Duplicate_term_definition ->
| lst -> Environment.Signature1.add_warnings ws new_sig2) with
| Environment.Signature1.Duplicate_term_definition ->
emit_parse_error (Error.Duplicated_term id) (fst l,snd l) in
new_sig}
term_alone :
| term<t> COLON type_expression<ty> EOI {let sg = (get_sig_value dyp.last_local_data) in
E.Signature1.convert_term (fst (t Env.empty [])) (fst (ty sg)) sg }
Environment.Signature1.convert_term (fst (t Env.empty [])) (fst (ty sg)) sg }
heterogenous_term_and_type :
......@@ -424,9 +425,9 @@ sig_entries :
fun env ws -> reset_location $1 (multiple_abs env ws Abstract_syntax.Non_linear $2 $4 (fun x -> x))} binder
| IDENT<b> idents<ids> DOT ...{let sg = get_sig_value dyp.last_local_data in
let binder,((p1,p2) as l) = b in
match E.Signature1.is_constant binder sg with
match Environment.Signature1.is_constant binder sg with
| true,Some Abstract_syntax.Binder -> (
match E.Signature1.get_binder_argument_functional_type binder sg with
match Environment.Signature1.get_binder_argument_functional_type binder sg with
| None -> failwith "Binder of non functional type"
| Some k -> k)
| _ -> emit_parse_error (Error.Binder_expected binder) (p1,p2) }<lin>
......@@ -436,7 +437,7 @@ sig_entries :
| application(<=app) {$1} app
| atomic_term(<=atom)<arg1> SYMBOL<sym> ...{let id,((pos1,pos2) as l) = sym in
let sg = get_sig_value dyp.last_local_data in
match E.Signature1.is_constant id sg with
match Environment.Signature1.is_constant id sg with
| true,Some (Abstract_syntax.Infix) -> Error.unset_infix ()
| true,_ -> raise Dyp.Giveup
| _ -> emit_parse_error (Error.Unknown_constant id) (pos1,pos2)}
......@@ -449,7 +450,7 @@ sig_entries :
atomic_term :
| IDENT {let id,l=$1 in
let s = get_sig_value dyp.last_local_data in
let is_constant,_ = E.Signature1.is_constant id s in
let is_constant,_ = Environment.Signature1.is_constant id s in
fun env ws ->
match Env.mem id env,is_constant with
| true,false -> Abstract_syntax.Var (id,l),ws
......@@ -459,7 +460,7 @@ sig_entries :
| LPAREN term RPAREN {$2} atom
| SYMBOL<sym> ...{let sg = get_sig_value dyp.last_local_data in
let id,((pos1,pos2) as l) = sym in
match E.Signature1.is_constant id sg with
match Environment.Signature1.is_constant id sg with
| true,Some (Abstract_syntax.Prefix) -> ()
| true,_ -> let () = Error.set_infix sym in
raise Dyp.Giveup
......@@ -493,7 +494,7 @@ sig_entries :
let kind =
List.fold_left
(fun k (id,loc) ->
match k,fst (E.Signature1.is_constant id abs),E.Signature1.is_type id abs with
match k,fst (Environment.Signature1.is_constant id abs),Environment.Signature1.is_type id abs with
| (Nothing|Cst|Both),true,false -> Cst
| (Nothing|Both),true,true -> Both
| Cst,true,_ -> Cst
......@@ -509,7 +510,7 @@ sig_entries :
fun lex ->
let term = fst (t Env.empty []) in
List.fold_left
(fun acc (id,loc) -> E.Lexicon.insert (Abstract_syntax.Constant (id,loc,term)) acc)
(fun acc (id,loc) -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,loc,term)) acc)
lex
ids
with
......@@ -520,7 +521,7 @@ sig_entries :
let kind =
List.fold_left
(fun k (id,loc) ->
match k,fst (E.Signature1.is_constant id abs),E.Signature1.is_type id abs with