(* * ENIAM_LCGparser, a parser for Logical Categorial Grammar formalism * Copyright (C) 2016-2017 Wojciech Jaworski <wjaworski atSPAMfree mimuw dot edu dot pl> * Copyright (C) 2016-2017 Institute of Computer Science Polish Academy of Sciences * * This library is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * This library is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. * * You should have received a copy of the GNU Lesser General Public License * along with this program. If not, see <http://www.gnu.org/licenses/>. *) open Xstd open ENIAM_LCGtypes (* let references = ref [0,Ref 0] let next_reference = ref 0 let make_reference sem = let r = !next_reference in references := (r,sem) :: !references; incr next_reference; r *) let new_variable_ref = ref 0 let get_new_variable () = incr new_variable_ref; "x" ^ (string_of_int (!new_variable_ref)) let rec unify v1 v2 = function AVar a,Atom t -> if v2=a then Atom t else failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a)) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (Atom t))) | Atom s,AVar a -> if v1=a then Atom s else failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (Atom s)) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a))) | AVar a,With lt -> if v2=a then With lt else failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a)) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (With lt))) | With ls,AVar a -> if v1=a then With ls else failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (With ls)) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a))) | AVar a,t -> failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a)) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 t)) | t,AVar a -> failwith ("unify AVar: " ^ v1 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 t) ^ " " ^ v2 ^ "=" ^ (ENIAM_LCGstringOf.internal_grammar_symbol 0 (AVar a))) | Zero, t -> t | t, Zero -> t | With ls, With lt -> let ls = Xlist.map ls (function Atom s -> s | _ -> failwith "unify: With") in let lt = Xlist.map lt (function Atom s -> s | _ -> failwith "unify: With") in let set = StringSet.of_list lt in let l = Xlist.fold ls [] (fun l s -> if StringSet.mem set s then s :: l else l) in (match l with [] -> raise Not_found | [s] -> Atom s | l -> With(Xlist.map l (fun s -> Atom s))) | Atom s, t -> unify v1 v2 (With[Atom s],t) | s, Atom t -> unify v1 v2 (s,With[Atom t]) | _,_ -> failwith "unify" (*let unify_fv afv bfv = StringMap.fold afv bfv (fun bfv v g -> let g2 = try StringMap.find bfv v with Not_found -> Zero in StringMap.add bfv v (unify v v (g,g2))) *) let find_fv fv v = try StringMap.find fv v with Not_found -> failwith ("find_fv: "^ v) let add_fv = StringMap.add let mem_fv = StringMap.mem let remove_fv = StringMap.remove let is_empty_fv = StringMap.is_empty let empty_fv = StringMap.empty let fold_fv = StringMap.fold let string_of_fv fv = let l = StringMap.fold fv [] (fun l v (t,e) -> (e ^ ": " ^ v ^ ":=" ^ ENIAM_LCGstringOf.internal_grammar_symbol 0 t) :: l) in String.concat "," (List.sort compare l) let rec infer s = function Zero -> true | Atom t -> t = s | With l -> Xlist.fold l false (fun b t -> b || (infer s t)) | AVar _ -> failwith "infer" | Top -> failwith "infer" let make_variant = function [] -> failwith "make_variant" | [t] -> t | l -> (* let e = get_variant_label () in *) let l,_ = Xlist.fold l ([],1) (fun (l,i) -> function t -> (string_of_int i,t) :: l, i+1) in Variant("",l) let make_subst e = function Zero -> Dot | Atom t -> Val t | With l -> (* let e = get_variant_label () in *) let l,_ = Xlist.fold l ([],1) (fun (l,i) -> function Atom t -> (string_of_int i,Val t) :: l, i+1 | _ -> failwith "make_subst 1") in Variant(e,List.rev l) | AVar a -> SubstVar a | _ -> failwith "make_subst 2" let internal_deduce_matching afv bfv sem = function (* maczowany term * argument funktora *) Atom s, Atom t -> if s = t then [afv,bfv,sem] else [] | Atom s, Top -> [afv,bfv,sem] | Zero, Atom t -> [afv,bfv,sem] | Zero, Top -> [afv,bfv,sem] | AVar a, Atom t -> let g,e = find_fv afv a in let l = if infer t g then [add_fv afv a (Atom t,e),bfv,sem] else [] in (* Printf.printf "AVar,Atom: [%s] '%s' [%s] '%s' -> %d\n%!" (string_of_fv afv) (ENIAM_LCGstringOf.internal_grammar_symbol 1 (AVar a)) (string_of_fv bfv) (ENIAM_LCGstringOf.internal_grammar_symbol 1 (Atom t)) (Xlist.size l); *) l | AVar a, Top -> [afv,bfv,sem] | Zero, AVar b -> (*print_endline "idm";*)[afv,bfv,sem] | Atom s, AVar b -> let g,e = find_fv bfv b in if infer s g then [afv, add_fv bfv b (Atom s,e),sem] else [] | AVar a, AVar b -> let ga,ea = find_fv afv a in let gb,eb = find_fv bfv b in (try let subst = (*print_endline "internal_deduce_matching";*)unify a b (ga,gb) in [add_fv afv a (AVar b,eb), add_fv bfv b (subst,eb),sem] with Not_found -> []) | Top, Top -> [afv,bfv,sem] | Top, _ -> [] | s,t -> failwith ("internal_deduce_matching pattern: " ^ ENIAM_LCGstringOf.internal_grammar_symbol 1 s ^ " " ^ ENIAM_LCGstringOf.internal_grammar_symbol 1 t) let rec imp_selector s dir fv in_sem d = function Maybe t -> if d = Both || d = dir then let x = get_new_variable () in let y = get_new_variable () in [fv,Imp(s,dir,Maybe t),t,Lambda(x,Lambda(y,App(in_sem,Insert(Apply(Var x),Var y))))] else [] | t -> if d = Both || d = dir then [fv,s,t,in_sem] else [] let rec impset_selector s dir fv in_sem rev = function [],_ -> [] | (d,Maybe t) :: l,i -> (* print_endline "impset_selector Maybe"; *) (if d = Both || d = dir then let x = get_new_variable () in let y = get_new_variable () in let s = if rev = [] && l = [] then s else ImpSet(s,List.rev rev @ l) in [fv,Imp(s,dir,Maybe t),t,Lambda(x,Lambda(y,App(LambdaRot(i,in_sem),Insert(Apply(Var x),Var y))))] else []) @ (impset_selector s dir fv in_sem ((d,Maybe t) :: rev) (l,i+1)) | (d,t) :: l,i -> (* print_endline "impset_selector"; *) (if d = Both || d = dir then let s = if rev = [] && l = [] then s else ImpSet(s,List.rev rev @ l) in [fv,s,t,LambdaRot(i,in_sem)] else []) @ (impset_selector s dir fv in_sem ((d,t) :: rev) (l,i+1)) let rec deduce_tensor afv bfv rev_sems = function [] -> [afv,bfv,List.rev rev_sems] | (s,(t,v)) :: tensor_elems -> let l = internal_deduce_matching afv bfv v (s,t) in (* Printf.printf "deduce_tensor: [%s] '%s' [%s] '%s' -> %d\n%!" (string_of_fv afv) (ENIAM_LCGstringOf.internal_grammar_symbol_prime s) (string_of_fv bfv) (ENIAM_LCGstringOf.internal_grammar_symbol_prime t) (Xlist.size l); *) Xlist.fold l [] (fun found (afv,bfv,sem) -> (deduce_tensor afv bfv (sem :: rev_sems) tensor_elems) @ found) let rec deduce_matching afv bfv in_sem = function (* maczowany term * argument funktora *) (* | Plus l, t -> (* zakładam, że afv jest pusty *) let x = get_new_variable () in let found = Xlist.multiply_list (Xlist.map l (fun s -> Xlist.map (deduce_matching afv bfv (Var x) (s,t)) (fun (afv,bfv,sem) -> if not (is_empty_fv afv) then failwith "deduce_matching: is_empty_fv afv" else bfv,sem))) in Xlist.fold found [] (fun found l -> try let bfv = Xlist.fold (List.tl l) (fst (List.hd l)) (fun bfv (frame_bfv,_) -> unify_fv bfv frame_bfv) in let sem = Case(in_sem,(Xlist.map l (fun (_,sem) -> x,sem))) in (empty_fv,bfv,sem) :: found with Not_found -> found)*) | s, Plus l -> (* istotne jest by prawy plus byl po lewym *) fst (Xlist.fold l ([],1) (fun (found,i) t -> Xlist.map (deduce_matching afv bfv in_sem (s,t)) (fun (afv,bfv,sem) -> afv,bfv,Inj(i,sem)) @ found, i+1)) (* | Star s, Star t -> let x = get_new_variable () in Xlist.map (deduce_matching afv bfv (Var x) (s,t)) (fun (afv,bfv,sem) -> afv,bfv,Map(in_sem,Lambda(x,sem)))*) | Star _, _ -> [] | _, Star _ -> [] | WithVar(v,g,e,s),t -> Xlist.map (deduce_matching (add_fv afv v (g,e)) bfv (ProjVar(v,in_sem)) (s,t)) (fun (afv,bfv,sem) -> let g,e = find_fv afv v in remove_fv afv v,bfv,Subst(sem,v,make_subst e g)) | One, Maybe _ -> [afv,bfv,Empty in_sem] | One, One -> [afv,bfv,in_sem] | One, _ -> [] | _, One -> [] | _, Maybe _ -> [] | Imp(psi,d,phi), Imp(tau,dir,sigma) -> (List.flatten (Xlist.map (deduce_optarg in_sem phi) (fun sem -> deduce_matching afv bfv sem (psi,Imp(tau,dir,sigma))))) @ let l = imp_selector psi dir afv in_sem d phi in List.flatten (Xlist.map l (fun (afv,psi,phi,sem) -> let x = get_new_variable () in let l = List.flatten (Xlist.map (deduce_matching bfv afv (Var x) (sigma,phi)) (fun (bfv,afv,p) -> deduce_matching afv bfv (App(sem,p)) (psi,tau))) in Xlist.map l (fun (afv,bfv,sem) -> afv,bfv,Lambda(x,sem)))) | ImpSet(psi,phi_list), Imp(tau,dir,sigma) -> (List.flatten (Xlist.map (deduce_optargs in_sem phi_list) (fun sem -> deduce_matching afv bfv sem (psi,Imp(tau,dir,sigma))))) @ let l = impset_selector psi dir afv in_sem [] (phi_list,1) in List.flatten (Xlist.map l (fun (afv,psi,phi,sem) -> let x = get_new_variable () in let l = List.flatten (Xlist.map (deduce_matching bfv afv (Var x) (sigma,phi)) (fun (bfv,afv,p) -> deduce_matching afv bfv (App(sem,p)) (psi,tau))) in Xlist.map l (fun (afv,bfv,sem) -> afv,bfv,Lambda(x,sem)))) | Imp(s,d,s2), t -> List.flatten (Xlist.map (deduce_optarg in_sem s2) (fun sem -> deduce_matching afv bfv sem (s,t))) | ImpSet(s,l), t -> List.flatten (Xlist.map (deduce_optargs in_sem l) (fun sem -> deduce_matching afv bfv sem (s,t))) | _, Imp(s,d,s2) -> [] | Tensor l1, Tensor l2 -> (* Printf.printf "Tensor: [%s] '%s' [%s] '%s'\n%!" (string_of_fv afv) (ENIAM_LCGstringOf.grammar_symbol 1 (Tensor l1)) (string_of_fv bfv) (ENIAM_LCGstringOf.grammar_symbol 1 (Tensor l2)); *) if Xlist.size l1 <> Xlist.size l2 then [] else ( let dots = Xlist.map (List.tl l1) (fun _ -> Dot) in (* let variables = Xlist.map l2 (fun _ -> get_new_variable ()) in *) (* let variables2 = Xlist.map variables (fun v -> Var v) in *) let sem_substs_list = deduce_tensor afv bfv [] (List.combine l1 (List.combine l2 (in_sem :: dots)(*variables2*))) in let l = Xlist.map sem_substs_list (fun (afv,bfv,sems) -> let sem = List.hd sems(*LetIn(variables,in_sem,Tuple sems)*) in afv,bfv,sem) in l) | Tensor _, _ -> [] | _, Tensor _ -> [] | s,t -> failwith ("deduce_matching: " ^ ENIAM_LCGstringOf.grammar_symbol 1 s ^ " " ^ ENIAM_LCGstringOf.grammar_symbol 1 t) and deduce_optarg in_sem t = let l = deduce_matching empty_fv empty_fv (Dot(*Triple(Dot,Dot,Dot)*)) (One,t) in match l with [] -> [] | [_,_,sem] -> [App(in_sem, sem)] | l -> (*print_endline ("deduce_optarg: " ^ ENIAM_LCGstringOf.grammar_symbol 0 t ^ " " ^ String.concat " " (Xlist.map l (fun (_,_,sem) -> ENIAM_LCGstringOf.linear_term 0 sem)));*) failwith "deduce_optarg" and deduce_optargs sem l = (* print_endline "deduce_optargs"; *) let b,sems = Xlist.fold (List.rev l) (true,[]) (fun (b,sems) (_,t) -> if not b then b,[] else let l = deduce_matching empty_fv empty_fv (Dot(*Triple(Dot,Dot,Dot)*)) (One,t) in if l = [] then false,[] else b,((List.hd l) :: sems)) in if b then [Xlist.fold sems sem (fun sem (_,_,s) -> App(LambdaRot(1,sem),s))] else [] let make_forward sem l = (* FIXME: po co jest ta procedura? *) (* print_endline "make_forward 1"; *) let l,sem,_ = Xlist.fold l ([],sem,1) (fun (l,sem,i) -> function Forward,t -> (Forward,t) :: l,sem,i+1 | Both,t -> (Forward,t) :: l,sem,i+1 | Backward,t -> (* print_endline "make_forward 2"; *) let res = deduce_matching empty_fv empty_fv Dot (One,t) in (* Printf.printf "make_forward 3 |res|=%d\n%!" (Xlist.size res); *) if res = [] then raise Not_found else let _,_,res = List.hd res in l, App(LambdaRot(i,sem),res), i) in (* print_endline "make_forward 3"; *) List.rev l, sem let rec deduce_imp dir afv in_sem = function Tensor _ -> [] | Star _ -> [] | Plus _ -> [] | WithVar(v,g,e,s) -> (*print_endline "deduce_imp WithVar";*) deduce_imp dir (add_fv afv v (g,e)) (ProjVar(v,in_sem)) s | Imp(s,d,t) -> (* print_endline "deduce_imp Imp"; *) (List.flatten (Xlist.map (deduce_optarg in_sem t) (fun sem -> deduce_imp dir afv sem s))) @ (imp_selector s dir afv in_sem d t) | ImpSet(s,l) -> (* print_endline "deduce_imp ImpSet 1"; *) let (l2,in_sem2),b = if dir = Backward then (l,in_sem),true else try make_forward in_sem l,true with Not_found -> ([],Dot),false in (* print_endline "deduce_imp ImpSet 2"; *) if b then (List.flatten (Xlist.map (deduce_optargs in_sem l) (fun sem -> deduce_imp dir afv sem s))) @ (impset_selector s dir afv in_sem2 [] (l2,1)) else [] | s -> failwith ("deduce_imp: " ^ ENIAM_LCGstringOf.grammar_symbol 1 s) let rec deduce_app references dir (funct,funct_sem) args = (* Printf.printf "deduce_app 1: '%s' [%s]\n%!" (ENIAM_LCGstringOf.grammar_symbol 1 funct) (String.concat "; " (Xlist.map args (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))); *) let x = List.flatten (Xlist.map (deduce_imp dir empty_fv funct_sem funct) (fun (fv,psi,phi,funct_sem) -> (* print_endline "deduce_app 2"; *) let l = Xlist.fold args [] (fun l (arg,arg_sem) -> let res = deduce_matching empty_fv fv arg_sem (arg,phi) in (* Printf.printf "deduce_matching: '%s' '%s' -> %d\n%!" (ENIAM_LCGstringOf.grammar_symbol 1 arg) (ENIAM_LCGstringOf.grammar_symbol 1 phi) (Xlist.size res); *) res @ l) in let map = Xlist.fold l StringMap.empty (fun map (afv,bfv,sem) -> if not (is_empty_fv afv) then failwith "deduce_app" else StringMap.add_inc map (string_of_fv bfv) (bfv,[sem]) (fun (fv,sems) -> fv, sem :: sems)) in StringMap.fold map [] (fun l _ (bfv,sems) -> let reference = ExtArray.add references (App(funct_sem,make_variant sems)) in (fold_fv bfv (psi,Ref reference) (fun (t,sem) v (g,e) -> WithVar(v,g,e,t), VariantVar(v,sem))) :: l))) in (* print_endline "deduce_app 3"; *) x let rec make_uniq fv n v = if n = 1 then if mem_fv fv v then make_uniq fv (n+1) v else v else if mem_fv fv (v ^ string_of_int n) then make_uniq fv (n+1) v else v ^ string_of_int n let internal_comp_substitute afv bfv arg_sem l = function AVar v -> let g,e = find_fv afv v in (match g with Atom _ -> remove_fv afv v, bfv, Subst(arg_sem,v,make_subst e g), g :: l | AVar _ -> remove_fv afv v, bfv, Subst(arg_sem,v,make_subst e g), g :: l | Top -> failwith "internal_comp_substitute" | _ -> let w = make_uniq bfv 1 v in remove_fv afv v, add_fv bfv w (g,e), Subst(arg_sem,v,make_subst e (AVar w)), AVar w :: l) | t -> afv,bfv,arg_sem,t :: l let comp_substitute afv bfv arg_sem = function Tensor l -> let afv,bfv,arg_sem,l = Xlist.fold l (afv,bfv,arg_sem,[]) (fun (afv,bfv,arg_sem,l) t -> internal_comp_substitute afv bfv arg_sem l t) in let arg_sem = fold_fv afv arg_sem (fun arg_sem v (g,e) -> Subst(arg_sem,v,make_subst e g)) in bfv,Tensor(List.rev l),arg_sem | t -> failwith ("comp_substitute: " ^ ENIAM_LCGstringOf.grammar_symbol 0 t) let rec deduce_comp references dir_funct dir_arg (funct,funct_sem) args = (* Printf.printf "deduce_app 1: '%s' [%s]\n%!" (ENIAM_LCGstringOf.grammar_symbol 1 funct) (String.concat "; " (Xlist.map args (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))); *) let x = List.flatten (Xlist.map (deduce_imp dir_funct empty_fv funct_sem funct) (fun (fv,psi,phi,funct_sem) -> (* print_endline "deduce_app 2"; *) let l = Xlist.fold args [] (fun l (arg,arg_sem) -> Xlist.fold (deduce_imp dir_arg empty_fv arg_sem arg) l (fun l (arg_fv,arg_psi,arg_phi,arg_sem) -> (* let avars = get_avars arg_phi in *) let x = get_new_variable () in let res = deduce_matching arg_fv fv (App(arg_sem,Var x)) (arg_psi,phi) in Xlist.fold res l (fun l (afv,bfv,arg_sem) -> let bfv,arg_phi,arg_sem = comp_substitute afv bfv arg_sem arg_phi in (bfv,Imp(psi,dir_arg,arg_phi),Lambda(x,App(funct_sem,arg_sem))) :: l))) in Xlist.fold l [] (fun l (bfv,t,sem) -> let reference = ExtArray.add references sem in (fold_fv bfv (t,Ref reference) (fun (t,sem) v (g,e) -> WithVar(v,g,e,t), VariantVar(v,sem))) :: l))) in (* print_endline "deduce_app 3"; *) x (*let rec forward_application = function (Bracket(lf,false,funct),sem), (Bracket(false,rf,arg),arg_sem) -> Xlist.map (deduce_app Forward (funct,sem) (arg,arg_sem)) (fun (t,sem) -> Bracket(lf,rf,t), LCGreductions.linear_term_beta_reduction2 sem) | (Bracket(lf,true,funct),sem), (Bracket(true,true,arg),arg_sem) -> Xlist.map (deduce_app Forward (funct,sem) (arg,arg_sem)) (fun (t,sem) -> Bracket(lf,true,t), LCGreductions.linear_term_beta_reduction2 sem) | (BracketSet(Forward),_), (Bracket(false,rf,arg),arg_sem) -> [Bracket(true,rf,arg),arg_sem] | ((x,_),(y,_)) -> (*Printf.printf "forward_application: '%s' '%s'\n%!" (ENIAM_LCGstringOf.grammar_symbol_prime x) (ENIAM_LCGstringOf.grammar_symbol_prime y);*) [] let rec backward_application = function (Bracket(lf,false,arg),arg_sem), (Bracket(false,rf,funct),sem) -> Xlist.map (deduce_app Backward (funct,sem) (arg,arg_sem)) (fun (t,sem) -> Bracket(lf,rf,t), LCGreductions.linear_term_beta_reduction2 sem) | (Bracket(true,true,arg),arg_sem), (Bracket(true,rf,funct),sem) -> Xlist.map (deduce_app Backward (funct,sem) (arg,arg_sem)) (fun (t,sem) -> Bracket(true,rf,t), LCGreductions.linear_term_beta_reduction2 sem) | (Bracket(lf,false,arg),arg_sem), (BracketSet(Backward),_) -> [Bracket(lf,true,arg),arg_sem] | _ -> []*) let forward_application references functs args = Xlist.fold functs [] (fun l -> function Bracket(lf,false,funct),sem -> let argst,argsf = Xlist.fold args ([],[]) (fun (argst,argsf) -> function Bracket(false,true,arg),arg_sem -> (arg,arg_sem) :: argst, argsf | Bracket(false,false,arg),arg_sem -> argst, (arg,arg_sem) :: argsf | _ -> argst,argsf) in let l = Xlist.fold (deduce_app references Forward (funct,sem) argst) l (fun l (t,sem) -> (Bracket(lf,true,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) in Xlist.fold (deduce_app references Forward (funct,sem) argsf) l (fun l (t,sem) -> (Bracket(lf,false,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | Bracket(lf,true,funct),sem -> let args = Xlist.fold args [] (fun args -> function Bracket(true,true,arg),arg_sem -> (arg,arg_sem) :: args | _ -> args) in Xlist.fold (deduce_app references Forward (funct,sem) args) l (fun l (t,sem) -> (Bracket(lf,true,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | BracketSet(Forward),_ -> Xlist.fold args l (fun l -> function Bracket(false,rf,arg),arg_sem -> (Bracket(true,rf,arg),arg_sem) :: l | _ -> l) | _ -> l) let forward_application_conll references functs args = Xlist.fold functs [] (fun l -> function Bracket(_,_,funct),sem -> let args = Xlist.fold args [] (fun args -> function Bracket(_,_,arg),arg_sem -> (arg,arg_sem) :: args | _ -> args) in Xlist.fold (deduce_app references Forward (funct,sem) args) l (fun l (t,sem) -> (Bracket(false,false,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | _ -> l) let forward_cross_composition references functs args = Xlist.fold functs [] (fun l -> function Bracket(lf,false,funct),sem -> let argst,argsf = Xlist.fold args ([],[]) (fun (argst,argsf) -> function Bracket(false,true,arg),arg_sem -> (arg,arg_sem) :: argst, argsf | Bracket(false,false,arg),arg_sem -> argst, (arg,arg_sem) :: argsf | _ -> argst,argsf) in let l = Xlist.fold (deduce_comp references Forward Backward (funct,sem) argst) l (fun l (t,sem) -> (Bracket(lf,true,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) in Xlist.fold (deduce_comp references Forward Backward (funct,sem) argsf) l (fun l (t,sem) -> (Bracket(lf,false,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | _ -> l) let backward_application references args functs = (* Printf.printf "backward_application: [%s] [%s]\n%!" (String.concat "; " (Xlist.map args (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))) (String.concat "; " (Xlist.map functs (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))); *) Xlist.fold functs [] (fun l -> function Bracket(false,rf,funct),sem -> let argst,argsf = Xlist.fold args ([],[]) (fun (argst,argsf) -> function Bracket(true,false,arg),arg_sem -> (arg,arg_sem) :: argst, argsf | Bracket(false,false,arg),arg_sem -> argst, (arg,arg_sem) :: argsf | _ -> argst,argsf) in let l = Xlist.fold (deduce_app references Backward (funct,sem) argst) l (fun l (t,sem) -> (Bracket(true,rf,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) in Xlist.fold (deduce_app references Backward (funct,sem) argsf) l (fun l (t,sem) -> (Bracket(false,rf,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | Bracket(true,rf,funct),sem -> let args = Xlist.fold args [] (fun args -> function Bracket(true,true,arg),arg_sem -> (arg,arg_sem) :: args | _ -> args) in Xlist.fold (deduce_app references Backward (funct,sem) args) l (fun l (t,sem) -> (Bracket(true,rf,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | BracketSet(Backward),_ -> (*print_endline "tt";*) Xlist.fold args l (fun l -> function Bracket(lf,false,arg),arg_sem -> (Bracket(lf,true,arg),arg_sem) :: l | _ -> l) | _ -> l) let backward_application_conll references args functs = (* Printf.printf "backward_application: [%s] [%s]\n%!" (String.concat "; " (Xlist.map args (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))) (String.concat "; " (Xlist.map functs (fun (arg,_) -> "'" ^ ENIAM_LCGstringOf.grammar_symbol 1 arg ^ "'"))); *) Xlist.fold functs [] (fun l -> function Bracket(_,_,funct),sem -> let args = Xlist.fold args [] (fun args -> function Bracket(_,_,arg),arg_sem -> (arg,arg_sem) :: args | _ -> args) in Xlist.fold (deduce_app references Backward (funct,sem) args) l (fun l (t,sem) -> (Bracket(false,false,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | _ -> l) let backward_cross_composition references args functs = Xlist.fold functs [] (fun l -> function Bracket(false,rf,funct),sem -> let argst,argsf = Xlist.fold args ([],[]) (fun (argst,argsf) -> function Bracket(true,false,arg),arg_sem -> (arg,arg_sem) :: argst, argsf | Bracket(false,false,arg),arg_sem -> argst, (arg,arg_sem) :: argsf | _ -> argst,argsf) in let l = Xlist.fold (deduce_comp references Backward Forward (funct,sem) argst) l (fun l (t,sem) -> (Bracket(true,rf,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) in Xlist.fold (deduce_comp references Backward Forward (funct,sem) argsf) l (fun l (t,sem) -> (Bracket(false,rf,t), (*LCGreductions.linear_term_beta_reduction2*) sem) :: l) | _ -> l) (* FIXME: błąd przy redukcji "Jan chce iść spać" *) let rules = [ backward_application; forward_application; (*backward_cross_composition; forward_cross_composition;*) ] let rec flatten_functor2 l seml = function Imp(s,d,t),Lambda(v,sem) -> flatten_functor2 ((d,t) :: l) (v :: seml) (s,sem) | ImpSet(s,l2),LambdaSet(vl,sem) -> flatten_functor2 (l2 @ l) (vl @ seml) (s,sem) | s,sem -> if l = [] then s,sem else ImpSet(s,l),LambdaSet(seml,sem) let rec flatten_functor = function Bracket(lf,rf,s),t -> let s,t = flatten_functor (s,t) in Bracket(lf,rf,s),t | WithVar(v,g,e,s), VariantVar(x,t) -> let s,t = flatten_functor (s,t) in WithVar(v,g,e,s), VariantVar(x,t) | t -> flatten_functor2 [] [] t let rec set_x_type = function Bracket(lf,rf,s),t -> let s,t = set_x_type (s,t) in Bracket(lf,rf,s),t | WithVar(v,g,e,s), t -> let s,t = set_x_type (s,t) in WithVar(v,g,e,s), t | Imp(s,d,t),sem -> let s,sem = set_x_type (s,sem) in Imp(s,d,t),sem | ImpSet(s,l2),sem -> let s,sem = set_x_type (s,sem) in ImpSet(s,l2),sem | Tensor s,sem -> Tensor[Atom "X"],sem | t,_ -> failwith ("set_x_type: " ^ ENIAM_LCGstringOf.grammar_symbol_prime t)