Commit 4a19f6fd authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

nl_lexicon now restricts the non linear interpretation to the interpretation...

nl_lexicon now restricts the non linear interpretation to the interpretation of -> and lambda at the abstract level. It is the user's responsability to have Lambda's and => in the lexicon and in the object signature when required. Fixes #12
parent ce862d1a
......@@ -136,7 +136,8 @@ struct
build = Interpret (abs,obj);
timestamp = Unix.time ()}
(* let interpret_linear_arrow_as_non_linear {non_linear_interpretation} = non_linear_interpretation *)
let is_linear {non_linear_interpretation} = not non_linear_interpretation
let emit_missing_inter lex lst =
let lex_name,loc = name lex in
......
......@@ -95,6 +95,7 @@ sig
val get_dependencies : t -> dependency
val empty : (string*Abstract_syntax.location) -> ?non_linear:bool -> abs:signature -> obj:signature -> t
val is_linear : t -> bool
val name : t -> (string*Abstract_syntax.location)
val insert : Abstract_syntax.lex_entry -> t -> t
val to_string : t -> string
......
......@@ -241,6 +241,9 @@ module type Lexicon_sig =
(** [empty name] returns the empty lexicon of name [name] *)
val empty : (string*Abstract_syntax.location) -> ?non_linear:bool -> abs:signature -> obj:signature -> t
(** [is_linear l] returns [true] if the lexicon [l] is linear, and [false] otherwise *)
val is_linear : t -> bool
(** [name l] returns the name of the lexicon [l] and the location of its definition *)
val name : t -> (string*Abstract_syntax.location)
......
......@@ -30,7 +30,7 @@ module Lambda_show (T : Show_text_sig) = struct
((l_env, env) : env * env)
(id_to_sym : consts)
: diagram * bool =
let () = Printf.fprintf stderr "Linear env: %s\nNon linear env: %s\n" (env_to_string l_env) (env_to_string env) in
(* let () = Printf.fprintf stderr "Linear env: %s\nNon linear env: %s\n" (env_to_string l_env) (env_to_string env) in *)
let recurse t l_level level (l_env,env) =
recur_fn t l_level level (l_env,env) id_to_sym in
let d, b = match t with
......@@ -174,29 +174,30 @@ module Make (E : Environment_sig)
Tree.T (t, List.map (term_to_graph sg) children)
let rec render_term_graph (l_level : int) (level : int)
let rec render_term_graph ?(non_linear=false) (l_level : int) (level : int)
(l_env, env : env * env)
(render_term : term -> int -> int -> env * env -> diagram)
((Tree.T (term, children)) : term tree)
: diagram tree =
let render_children_in l_level level (l_env, env) =
List.map (render_term_graph l_level level (l_env, env) render_term) children in
List.map (render_term_graph ~non_linear l_level level (l_env, env) render_term) children in
let children_d = match term with
| Abs (x, _) ->
let x' = generate_var_name x (l_env, env) in
let env' = (level, x') :: env in
let level' = level + 1 in
| Abs (x, _)
| LAbs (x, _) when non_linear ->
let x' = generate_var_name x (l_env, env) in
let env' = (level, x') :: env in
let level' = level + 1 in
render_children_in l_level level' (l_env, env')
| LAbs (x, _) ->
let x' = generate_var_name x (l_env, env) in
let l_env' = (l_level, x') :: l_env in
let l_level' = l_level + 1 in
render_children_in l_level' level (l_env', env)
let x' = generate_var_name x (l_env, env) in
let l_env' = (l_level, x') :: l_env in
let l_level' = l_level + 1 in
render_children_in l_level' level (l_env', env)
| _ ->
render_children_in l_level level (l_env, env) in
render_children_in l_level level (l_env, env) in
Tree.T (render_term term l_level level (l_env, env), children_d)
......@@ -258,23 +259,28 @@ module Make (E : Environment_sig)
let render_obj_term lex abs_term =
let obj_sig = object_sig lex in
let obj_term = interpret_term abs_term lex in
let () = Printf.fprintf stderr "Interpretation '% s:= %s'\n%!" (raw_to_string abs_term) (raw_to_string obj_term) in
(* let () = Printf.fprintf stderr "Interpretation '% s:= %s'\n%!" (raw_to_string abs_term) (raw_to_string obj_term) in *)
term_to_diagram_in config obj_sig obj_term in
let abs_term_tree = render_term_graph 0 0 ([], [])
render_abs_term
term_graph in
(* let () = Printf.fprintf stderr ">>>>>>> Abstract term rendering was successful <<<<<<<<<<<<<<<<<<\n%!" in *)
let last_abs_term_graph =
if abs_terms_differ then
term_to_graph abs_sig expanded_abs_term
else
term_graph in
let obj_term_trees = List.map (fun lex ->
render_term_graph 0 0 ([], [])
(render_obj_term lex)
last_abs_term_graph)
lexs in
(* let () = Printf.fprintf stderr ">>>>>>> Entering object term trees <<<<<<<<<<<<<<<<<<\n%!" in *)
let obj_term_trees = List.map
(fun lex ->
render_term_graph ~non_linear:(not (E.Lexicon.is_linear lex)) 0 0 ([], [])
(render_obj_term lex)
last_abs_term_graph)
lexs in
let trees =
if abs_terms_differ then
......
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