Restrict the effects of nl_lexicon to de-linearization of abstract -> and...

Restrict the effects of nl_lexicon to de-linearization of abstract -> and abstract lambda only. Fixes #12

src/acg-data/acg_lexicon.ml

@@ -32,7 +32,23 @@ struct
   exception Duplicate_constant_interpretation
   exception Missing_interpretation of string
 
-  module Dico = Utils.StringMap
+  (*  module Dico = Utils.StringMap *)
+  type kind =
+    | Type
+    | Cst
+
+  module Pair =
+    struct
+      type t = string * kind
+      let compare (s,k) (s',k') =
+        match k,k' with
+        | Type , Cst -> -1
+        | Cst , Type -> 1
+        | _ , _ -> String.compare s s'
+    end
+
+  module Dico = Map.Make(Pair)
+                  
   module Signature=Sg
 
 
@@ -120,7 +136,7 @@ struct
      build = Interpret (abs,obj);
      timestamp = Unix.time ()}
 
-  let interpret_linear_arrow_as_non_linear {non_linear_interpretation} = non_linear_interpretation
+  (*  let interpret_linear_arrow_as_non_linear {non_linear_interpretation} = non_linear_interpretation *)
 
   let emit_missing_inter lex lst =
     let lex_name,loc = name lex in
@@ -131,29 +147,41 @@ struct
     match abs_ty with
     | Lambda.Atom i -> 
        (let abs_ty_as_str = Sg.type_to_string abs_ty abs_sg in
-	match Dico.find abs_ty_as_str dico with
+	match Dico.find (abs_ty_as_str,Type) dico with
 	| Type (_,obj_ty) -> Sg.expand_type obj_ty lex.object_sig
 	| Constant _ -> failwith "Bug"
         | exception 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.LFun (ty1,ty2) ->
+       if lex.non_linear_interpretation then
+         Lambda.Fun (interpret_type ty1 lex,interpret_type ty2 lex)
+       else
+         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 -> abs_t
-    | Lambda.LVar i -> abs_t
+    | Lambda.Var _ -> abs_t
+    | Lambda.LVar i -> 
+       if lex.non_linear_interpretation then
+         Lambda.Var i
+       else
+         abs_t
     | Lambda.Const i -> 
        (let abs_term_as_str = Sg.term_to_string abs_t abs_sg in
-	match Dico.find abs_term_as_str dico with
+	match Dico.find (abs_term_as_str,Cst) dico with
 	| Constant (_,obj_t) -> obj_t
 	| Type _ -> failwith "Bug"
         | exception 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.LAbs(x,t) -> 
+       if lex.non_linear_interpretation then
+         Lambda.Abs(x,interpret_term t lex)
+       else
+         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"
     
@@ -161,9 +189,6 @@ struct
     let t_interpretation = interpret_term t lex in
     let t_interpretation = Lambda.normalize ~id_to_term:(fun i -> Sg.unfold_term_definition i lex.object_sig) t_interpretation in
     let ty_interpretation = interpret_type ty lex in
-    if lex.non_linear_interpretation then
-      Lambda.unlinearize_term t_interpretation,Lambda.unlinearize_type ty_interpretation
-    else
       t_interpretation,ty_interpretation
 
   module Reduction=Reduction.Make(Sg)
@@ -175,8 +200,7 @@ struct
     let eta_long_term = 
       Sg.eta_long_form 
 	interpreted_term
-	(*	interpreted_type *)
-	(if interpret_linear_arrow_as_non_linear lex then Lambda.unlinearize_type interpreted_type else interpreted_type)
+	interpreted_type 
 	lex.object_sig in
     Log.info (fun m -> m "term: %s:%s" (Sg.term_to_string interpreted_term lex.object_sig) (Sg.type_to_string interpreted_type lex.object_sig));
     Log.info (fun m -> m "eta-long form: %s" (Sg.term_to_string eta_long_term lex.object_sig));
@@ -219,29 +243,11 @@ struct
   let insert e ({dico=d} as lex) = match e with
     | Abstract_syntax.Type (id,loc,ty) ->
        let interpreted_type = Sg.convert_type ty lex.object_sig in
-       let interpreted_type =
-	 if lex.non_linear_interpretation then
-	   Lambda.unlinearize_type interpreted_type 
-	 else
-	   interpreted_type in
-       {lex with dico=Dico.add id (Type (loc,interpreted_type)) d}
+       {lex with dico=Dico.add (id,Type) (Type (loc,interpreted_type)) d}
     | Abstract_syntax.Constant (id,loc,t) ->
        let abs_type=Sg.expand_type (Sg.type_of_constant id lex.abstract_sig) lex.abstract_sig in
-       let interpreted_type = 
-	 if lex.non_linear_interpretation then
-	   interpret_type (Lambda.unlinearize_type abs_type) lex
-	 else 
-	   interpret_type abs_type lex in
-       let t = 
-	 if lex.non_linear_interpretation then
-	   Abstract_syntax.unlinearize_term t
-	 else
-	   t in	
-       let unfold i = 
-	 if lex.non_linear_interpretation then
-	   Lambda.unlinearize_term (Sg.unfold_term_definition i lex.object_sig)
-	 else
-	   Sg.unfold_term_definition i lex.object_sig in	
+       let interpreted_type = interpret_type abs_type lex in
+       let unfold i = Sg.unfold_term_definition i lex.object_sig in	
        let interpreted_term = 
 	 Lambda.normalize
 	   ~id_to_term:unfold
@@ -249,11 +255,11 @@ struct
        let prog = match lex.datalog_prog with
 	 | None -> None
 	 | Some p ->
-	    let duplicated_entry = Dico.mem id d in
+	    let duplicated_entry = Dico.mem (id,Cst) d in
 	    let new_prog= add_rule_for_cst_in_prog id duplicated_entry abs_type (Signature.expand_term interpreted_term lex.object_sig) lex p in
 	    Some new_prog in
        {lex with
-	 dico=Dico.add id (Constant (loc,interpreted_term)) d;
+	 dico=Dico.add (id,Cst) (Constant (loc,interpreted_term)) d;
 	 datalog_prog =prog}
 	
   let rebuild_prog lex =
@@ -262,14 +268,14 @@ struct
     | Some _ ->
       let new_prog=
 	Dico.fold
-	  (fun key inter acc ->
+	  (fun (id,_) inter acc ->
 	    match inter with
 	    | Type (l,stype) -> acc
 	    | Constant (l,t) -> 
 	      add_rule_for_cst_in_prog
-		key
+		id
 		false (* When rebuilding, no risk of dublicated interpretations *)
-		(Sg.expand_type (Sg.type_of_constant key lex.abstract_sig) lex.abstract_sig) 
+		(Sg.expand_type (Sg.type_of_constant id lex.abstract_sig) lex.abstract_sig) 
 		t
 		lex
 		acc)
@@ -362,7 +368,7 @@ struct
       (fst (Sg.name obj_sg))
       (match 
 	  Dico.fold
-	    (fun k i -> function
+	    (fun (k,_) i -> function
 	    | None -> Some (Printf.sprintf "\t%s := %s;" k (interpretation_to_string k (fun id -> interpret_type (Sg.type_of_constant id abs_sg) lex) i obj_sg))
 	    | Some a -> Some (Printf.sprintf "%s\n\t%s := %s;" a k (interpretation_to_string k (fun id -> interpret_type (Sg.type_of_constant id abs_sg) lex) i obj_sg)))
 	    d
@@ -384,14 +390,19 @@ struct
       Signature.fold
 	(fun e acc ->
 	   match Sg.is_declared e abs with
-	     | Some s ->
-		 (try
-		    let _ = Dico.find s d in
-		      acc
-		  with
-		    | Not_found -> s::acc) 
-	     | None -> acc
-	)
+	   | Some s ->
+              (match Sg.entry_to_data e with
+               | Sg.Type _ ->
+                  if Dico.mem (s,Type) d then
+                    acc
+                  else
+                    s::acc
+               | Sg.Term _ ->
+                  if Dico.mem (s,Cst) d then
+                    acc
+                  else
+                    s::acc)
+	   | None -> acc)
 	[]
 	abs in
       match missing_interpretations with
@@ -435,7 +446,7 @@ struct
        abstract_sig = lex2.abstract_sig;
        object_sig=lex1.object_sig;
        datalog_prog=lex2.datalog_prog;
-       non_linear_interpretation=(interpret_linear_arrow_as_non_linear lex1) || (interpret_linear_arrow_as_non_linear lex2);
+       non_linear_interpretation=(lex1.non_linear_interpretation) || (lex2.non_linear_interpretation);
        build = Compose (lex1,lex2);
        timestamp = Unix.time ()} in
     rebuild_prog temp_lex

src/acg-data/interface.ml

@@ -67,8 +67,7 @@ sig
   val type_of_constant : string -> t -> stype
   val typecheck : Abstract_syntax.term -> stype -> t -> term
   val fold : (entry -> 'a -> 'a) -> 'a -> t -> 'a
-  (* REVIEW: Commented out because of still missing impl. *)
-  (*  val extract : entry -> t -> data *)
+  val entry_to_data : entry -> data 
   val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
   val is_declared : entry -> t -> string option
   val eta_long_form : term -> stype -> t -> term
@@ -112,6 +111,5 @@ sig
   val program_to_log : Logs.src -> Logs.level -> t -> unit
   val query_to_buffer : Signature.term -> Signature.stype -> t -> Buffer.t
   val query_to_log : Logs.src -> Logs.level -> Signature.term -> Signature.stype -> t -> unit
-  val interpret_linear_arrow_as_non_linear : t -> bool
   val update : t -> (string -> data) -> t
 end

src/acg-data/interface.mli

@@ -177,10 +177,9 @@ sig
       have been inserted. *)
   val fold : (entry -> 'a -> 'a) -> 'a -> t -> 'a
 
-  (** [extract e sig] returns a data depending of the content of the
-      entry [e] *)
-  (* REVIEW: Commented out because of still missing impl. *)
-  (* val extract : entry -> t -> data *)
+  (** [entry_to_data e] returns a data depending of the content of
+      the entry [e] in the signature [sig]*)
+  val entry_to_data : entry -> data 
 
   (** [get_binder_argument_functionnal_type s sg] returns [None] if
       the constant [s] is not defined in [sg] as a binder (that is
@@ -301,13 +300,6 @@ module type Lexicon_sig =
   the [level] level.*)
   val query_to_log : Logs.src -> Logs.level -> Signature.term -> Signature.stype -> t -> unit
 
-                                                                    
-  (** [interpret_linear_arrow_as_non_linear lex] returns [True] if
-  [lex] has been defined as a non-linear lexicon, i.e., a lexicon that
-  interprets all arrows (and lambdas) as non-linear ones. It returns
-  [False] otherwise.*)
-  val interpret_linear_arrow_as_non_linear : t -> bool
-
   val update : t -> (string -> data) -> t
 
 end

src/acg-data/signature.ml

@@ -125,7 +125,8 @@ struct
   let rec convert_type ty ({types=syms} as sg) = 
     match ty with
       | Abstract_syntax.Type_atom (s,l,args) -> find_atomic_type s sg
-      | Abstract_syntax.Linear_arrow (ty1,ty2,l) -> Lambda.LFun (convert_type ty1 sg,convert_type ty2 sg)
+      | Abstract_syntax.Linear_arrow (ty1,ty2,l) ->
+           Lambda.LFun (convert_type ty1 sg,convert_type ty2 sg)
       | Abstract_syntax.Arrow (ty1,ty2,l) -> Lambda.Fun (convert_type ty1 sg,convert_type ty2 sg)
 
   let abstract_on_dependent_types lst sg=
@@ -411,7 +412,7 @@ struct
   let is_2nd_order {is_2nd_order} = is_2nd_order
 
 
-  let extract e s = 
+  let entry_to_data e = 
     match e with 
     | Type_declaration (_,id,_) -> Type(Lambda.Atom id)
     | Type_definition (_,_,_,stype) -> Type stype

src/data/JLM-acg-examples/Makefile

 #ACGC=acgc
 BUILD_PATH=../../../_build/default/src/
 ACGC=$(BUILD_PATH)/grammars/acgc.exe
-ACG=$(BUILD_PATH)/scripting/acg.exe
+#ACG=$(BUILD_PATH)/scripting/acg.exe
 
 .PHONY: default clean all archive
 

src/data/JLM-acg-examples/jlm-cotag.acg

@@ -241,7 +241,7 @@ nl_lexicon CoTAG_sem(CoTAG):low_logic=
     L_Paul := proper_noun paul;
     L_Mary := proper_noun mary;
 
-    L_who := lambda P. WHO P;
+    L_who := Lambda P. WHO P;
 
     L_sleeps := intransitive_verb sleep;
     L_barks := intransitive_verb bark;

src/grammars/TODO.parser_bugs

@@ -11,3 +11,5 @@
 + [X] to indicate new dependencies (menhir, logs...)
 + [ ] to document syntax extensions for infix operators, precedence of the latter over application. Highest precedence for prefix operators
 * TODO What about lexicon composition when one lexicon at least is non-linear?
+* TODO Add debug flag (+ flag for log sources?)
+* TODO Change command line parsing to use Cmd

src/grammars/lex_parser.mly

+%{
+    type kind =
+      | Both
+      | Type
+      | Term
+%}
+
 %token <Logic.Abstract_syntax.Abstract_syntax.location> COLON_EQUAL
 %start <AcgData.Environment.Environment.Lexicon.t -> AcgData.Environment.Environment.t -> AcgData.Environment.Environment.Lexicon.t > lex_entry_eoi
                                                           
@@ -17,28 +24,55 @@
     fun lex e ->
     let abs,obj = Environment.Lexicon.get_sig lex in
     let id,loc = t in
-    if fst (Environment.Signature1.is_constant id obj) then
-      let term = Abstract_syntax.Const t in
-      List.fold_left
-        (fun acc (id,l) ->
-          match Environment.Signature1.is_constant id abs,Environment.Signature1.is_type id abs with
-          | (true,_),false -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,loc,term)) acc
-          | (false,_), _ -> emit_parse_error (Error.Unknown_constant id) l
-          | (true,_), true -> failwith (Printf.sprintf "Bug: should not happen. \"%s\" should not be both a type and a term" id))
-        lex
-        cst
-    else if Environment.Signature1.is_type id obj then
-      let stype = Abstract_syntax.Type_atom (id,loc,[]) in
-      List.fold_left
-        (fun acc (id,l) ->
-          match Environment.Signature1.is_constant id abs,Environment.Signature1.is_type id abs with
-          | (false,_),true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,loc,stype)) acc
-          | _,false -> emit_parse_error (Error.Unknown_type id) l
-          | (true,_), true -> failwith (Printf.sprintf "Bug: should not happen. \"%s\" should not be both a type and a term" id))
-        lex
-        cst
-    else raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),loc))))    
-  }
+    match fst (Environment.Signature1.is_constant id obj), Environment.Signature1.is_type id obj with
+    | true,false ->
+       let term = Abstract_syntax.Const t in
+       List.fold_left
+         (fun acc (id,l) ->
+           match Environment.Signature1.is_constant id abs with
+           | true,_ -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc
+           | false,_ -> emit_parse_error (Error.Unknown_constant id) l)
+         lex
+         cst
+    | false,true ->
+       let stype = Abstract_syntax.Type_atom (id,loc,[]) in
+       List.fold_left
+         (fun acc (id,l) ->
+           match Environment.Signature1.is_type id abs with
+           | true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc
+           | false -> emit_parse_error (Error.Unknown_type id) l)
+         lex
+         cst
+    | true,true ->
+       let term = Abstract_syntax.Const t in
+       let stype = Abstract_syntax.Type_atom (id,loc,[]) in
+       let kind =
+         List.fold_left
+           (fun acc (id,l) ->
+             match acc,(fst (Environment.Signature1.is_constant id abs)),Environment.Signature1.is_type id abs with
+             | Both,false,true -> Type
+             | Both,true,false -> Term
+             | Both,true,true -> Both
+             | Type,_,true -> Type
+             | Type,_,false -> emit_parse_error (Error.Unknown_type id) l
+             | Term,true,_ -> Term
+             | Term,false,_ -> emit_parse_error (Error.Unknown_constant id) l
+             | _,false,false -> raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),l)))))
+           Both
+           cst in
+       List.fold_left
+         (fun acc (id,l) ->
+           match kind with
+           | Type -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc
+           | Term -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc
+           | Both ->
+              let acc' = Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc in
+              Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc')
+         lex
+         cst
+    | false,false -> raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),loc))))    
+           }
+
 | cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=not_atomic_term
   {
     fun lex e ->

src/grammars/term_parser.mly

@@ -253,11 +253,14 @@
                                                     vars in                                   
                                    let t',loc',ws' = t type_env sg warnings in
                                    let n_loc = new_loc binder loc' in
-                                   ((List.fold_left
-                                       (fun acc (var,loc) ->
-                                        (fun t -> acc (abs (var,loc,t) Abstract_syntax.Non_linear)))
-                                      (fun x -> x)
-                                      vars)
+                                   ((fst (List.fold_left
+                                       (fun (acc,first_var) (var,loc) ->
+                                         if first_var then
+                                           (fun t -> acc (abs (var,n_loc,t) Abstract_syntax.Non_linear)),false
+                                         else
+                                           (fun t -> acc (abs (var,loc,t) Abstract_syntax.Non_linear)),false)
+                                       ((fun x -> x),true)
+                                       vars))
                                       t'),
                                    n_loc,
                                    ws'}
@@ -271,11 +274,14 @@
                                                         vars in                                   
                                        let t',loc',ws' = t type_env sg warnings in
                                        let n_loc = new_loc binder loc' in
-                                       ((List.fold_left
-                                           (fun acc (var,loc) ->
-                                             (fun t -> acc (abs (var,loc,t) Abstract_syntax.Linear)))
-                                           (fun x -> x)
-                                           vars)
+                                       ((fst (List.fold_left
+                                           (fun (acc,first_var) (var,loc) ->
+                                             if first_var then
+                                               (fun t -> acc (abs (var,n_loc,t) Abstract_syntax.Linear)),false
+                                             else
+                                               (fun t -> acc (abs (var,loc,t) Abstract_syntax.Linear)),false )
+                                           ((fun x -> x),true)
+                                           vars))
                                           t'),
                                        n_loc,
                                        ws' }
@@ -299,11 +305,14 @@
                                       let n_loc = new_loc loc loc' in
                                       Abstract_syntax.App
                                         (Const (binder,loc),
-                                         (List.fold_left
-                                            (fun acc (var,loc) ->
-                                              (fun t -> acc (abs (var,loc,t) linearity )))
-                                            (fun x -> x)
-                                            vars)
+                                         (fst (List.fold_left
+                                            (fun (acc,first_var) (var,loc) ->
+                                              if first_var then
+                                                (fun t -> acc (abs (var,n_loc,t) linearity )),false
+                                              else
+                                                (fun t -> acc (abs (var,loc,t) linearity )),false)
+                                            ((fun x -> x),true)
+                                            vars))
                                            t',
                                          n_loc),
                                       n_loc,

src/logic/lambda.ml

@@ -75,7 +75,9 @@ module Lambda =
 
     type consts = int -> Abstract_syntax.syntactic_behavior * string
 
-
+    let env_to_string e =
+      Utils.string_of_list ", " (fun (i,s) -> Printf.sprintf "%d:%s" i s) e
+                                                                
     let rec generate_var_name x (l_env, env) =
       if List.exists (fun (_,s) -> x=s) (l_env @ env) then
 	generate_var_name (Printf.sprintf "%s'" x) (l_env, env)
@@ -211,7 +213,7 @@ module Lambda =
        let rec term_to_string_aux t paren l_level level (l_env,env) =
 	 match t with
 	   | Var i -> Utils.fformat fmter "@[%s@]" (List.assoc (level - 1  - i) env)
-	   | LVar i ->Utils.fformat fmter "@[%s@]" (List.assoc (l_level - 1  - i) l_env)
+	   | LVar i -> Utils.fformat fmter "@[%s@]" (List.assoc (l_level - 1  - i) l_env)
 	   | Const i -> 
 	     let _,x = id_to_sym i in
 	     Utils.fformat fmter "@[%s@]" x

src/logic/lambda.mli

@@ -68,6 +68,8 @@ sig
   type env = (int * string) list
   type consts = int -> Abstract_syntax.syntactic_behavior * string
 
+  val env_to_string :  env -> string
+
   val generate_var_name : string -> env * env -> string
   val unfold_labs : env -> int -> env * env -> term -> env * int * term
   val unfold_abs : env -> int -> env * env -> term -> env * int * term

src/scripting/show.ml

@@ -30,6 +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 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
@@ -257,6 +258,7 @@ 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
       term_to_diagram_in config obj_sig obj_term in
 
     let abs_term_tree = render_term_graph 0 0 ([], [])