[Toss-devel-svn] SF.net SVN: toss:[1733] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1733] trunk/Toss
|
From: <luk...@us...> - 2012-06-25 14:30:33
|
Revision: 1733
http://toss.svn.sourceforge.net/toss/?rev=1733&view=rev
Author: lukstafi
Date: 2012-06-25 14:30:21 +0000 (Mon, 25 Jun 2012)
Log Message:
-----------
New Speagram step 2: doing inference online during parsing. For clean intermediate step, removed dealing with types from rewriting, apart from preserving them on rewritten subterms.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Term/BuiltinLang.ml
trunk/Toss/Term/Coding.ml
trunk/Toss/Term/Coding.mli
trunk/Toss/Term/ParseArc.ml
trunk/Toss/Term/ParseArc.mli
trunk/Toss/Term/ParseArcTest.ml
trunk/Toss/Term/Rewriting.ml
trunk/Toss/Term/SyntaxDef.ml
trunk/Toss/Term/SyntaxDef.mli
trunk/Toss/Term/TRS.ml
trunk/Toss/Term/TRS.mli
trunk/Toss/Term/TRSTest.ml
trunk/Toss/Term/Term.ml
trunk/Toss/Term/Term.mli
trunk/Toss/Term/TermTest.ml
trunk/Toss/Term/tests/short_checks.log
trunk/Toss/Term/tests/short_checks.trs
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Formula/Aux.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -203,6 +203,11 @@
in
List.rev (maps_f [] l)
+let rec find_some f = function
+ | [] -> raise Not_found
+ | a::l ->
+ match f a with None -> find_some f l | Some r -> r
+
let map_reduce mapf redf red0 l =
match List.sort (fun x y -> compare (fst x) (fst y))
(List.map mapf l) with
@@ -707,6 +712,15 @@
true
with Not_found -> false
+let array_iter2 f a b =
+ let len = Array.length a in
+ if len <> Array.length b then
+ raise (Invalid_argument "Aux.array_iter2")
+ else
+ for i = 0 to len - 1 do
+ f (Array.unsafe_get a i) (Array.unsafe_get b i)
+ done
+
let array_replace array i elem =
let a = Array.copy array in a.(i) <- elem; a
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Formula/Aux.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -62,6 +62,8 @@
(** Map a list filtering out some elements. *)
val map_some : ('a -> 'b option) -> 'a list -> 'b list
+(** Find the first non-None element. Raise [Not_found] if none exists. *)
+val find_some : ('a -> 'b option) -> 'a list -> 'b
(** Map elements into key-value pairs, and fold values with the same
key. Uses {!List.fold_left}, therefore reverses the order. The
@@ -288,6 +290,11 @@
arrays are of different lengths. *)
val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
+(** Iterate an action over all elements of two arrays
+ pointwise. Raises [Invalid_argument "Aux.array_iter2"] if
+ arrays are of different lengths. *)
+val array_iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
+
(** Return a copy of [array] with the [i]th element replaced by [elem]. *)
val array_replace : 'a array -> int -> 'a -> 'a array
Modified: trunk/Toss/Term/BuiltinLang.ml
===================================================================
--- trunk/Toss/Term/BuiltinLang.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/BuiltinLang.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -293,7 +293,7 @@
let preprocess_sd = SDfun ([Str "#"; Str "#"; Str "#";
- Tp (Var ("p",0,top_type_term,[||]))], Var ("q",0,top_type_term,[||]))
+ Tp (Var ("p",0,top_type_term,[||]))], Var ("p",0,top_type_term,[||]))
let preprocess_name = name_of_sd preprocess_sd
Modified: trunk/Toss/Term/Coding.ml
===================================================================
--- trunk/Toss/Term/Coding.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/Coding.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -296,13 +296,36 @@
(* --- Term matching and substitutions --- *)
+(* Including supertypes.
let rec matches dict = function
- | (Term (n1, _, a1), Term (n2, _, a2)) when n1=n2 && (length a1 = length a2)->
+ | (Term (n1, t1, a1), Term (n2, t2, a2))
+ when n1=n2 && (length t1 = length t2) && (length a1 = length a2)->
+ Aux.array_for_all2 (fun u v -> matches dict (u, v)) t1 t2 &&
Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
- | (Var (n1, d1, _, a1), Var (n2, d2, _, a2))
+ | (Var (n1, d1, t1, a1), Var (n2, d2, t2, a2))
when n1 = n2 && d1 = d2 && length a1 = length a2 ->
+ matches dict (t1, t2) &&
+ Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
+ | (Var (n1, d1, t1, [||]), te) ->
+ (try
+ let arg = List.assoc n1 (!dict) in
+ let coded_arg = fn_apply d1 code_term arg in
+ te = coded_arg
+ with Not_found ->
+ let decoded_te = fn_apply d1 decode_term te in
+ (dict := (n1, decoded_te) :: (!dict); true)
+ )
+ | _ -> false
+*)
+(* Ignoring supertypes. *)
+let rec matches dict = function
+ | (Term (n1, _, a1), Term (n2, _, a2))
+ when n1=n2 && (length a1 = length a2)->
Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
- | (Var (n1, d1, _, [||]), te) ->
+ | (Var (n1, d1, _, a1), Var (n2, d2, _, a2))
+ when n1 = n2 && d1 = d2 && length a1 = length a2 ->
+ Aux.array_for_all2 (fun u v -> matches dict (u, v)) a1 a2
+ | (Var (n1, d1, t1, [||]), te) ->
(try
let arg = List.assoc n1 (!dict) in
let coded_arg = fn_apply d1 code_term arg in
@@ -313,27 +336,50 @@
)
| _ -> false
-
-(* Application of term substitutions (only flat functional substitutes). *)
+(* Application of term substitutions (only flat functional
+ substitutes). Ignoring supertypes. *)
let rec apply_s substs = function
| Var (n, d, _, [||]) as t ->
(* FIXME: why we don't apply substitutions recursively, as below? *)
(try (fn_apply d code_term (List.assoc n substs)) with Not_found -> t)
- | Term (n, tp, a) -> Term (n, map (apply_s substs) tp, map (apply_s substs) a)
+ | Term (n, tp, a) -> Term (n, tp, map (apply_s substs) a)
| Var (n, deg, t, a) ->
try (
let raw_result =
match (List.assoc n substs) with
| Term (name, tps, [||]) ->
- Term (name, map (apply_s substs) tps, map (apply_s substs) a)
+ Term (name, tps, map (apply_s substs) a)
| Var (name, d, ty, [||]) ->
- Var (name, d, apply_s substs ty, map (apply_s substs) a)
+ Var (name, d, ty, map (apply_s substs) a)
| _ -> failwith "functional substitution of non-flat term" in
fn_apply deg code_term raw_result
)
with Not_found -> Var (n, deg, t, map (apply_s substs) a)
+(* Application of term substitutions (only flat functional
+ substitutes). Including supertypes. *)
+let rec apply_st substs = function
+ | Var (n, d, t, [||]) ->
+ (* FIXME: why we don't apply substitutions recursively, as below? *)
+ (try (fn_apply d code_term (List.assoc n substs))
+ with Not_found -> Var (n, d, apply_st substs t, [||]))
+ | Term (n, tp, a) ->
+ Term (n, map (apply_st substs) tp, map (apply_st substs) a)
+ | Var (n, deg, t, a) ->
+ try (
+ let raw_result =
+ match (List.assoc n substs) with
+ | Term (name, tps, [||]) ->
+ Term (name, map (apply_st substs) tps, map (apply_st substs) a)
+ | Var (name, d, ty, [||]) ->
+ Var (name, d, apply_st substs ty, map (apply_st substs) a)
+ | _ -> failwith "functional substitution of non-flat term" in
+ fn_apply deg code_term raw_result
+ )
+ with Not_found ->
+ Var (n, deg, apply_st substs t, map (apply_st substs) a)
+
(* --- Nice Term display based on Syntax Definitions --- *)
let is_some = function Some _ -> true | None -> false
@@ -351,7 +397,21 @@
let args = List.map display_term (Array.to_list a) in
display_sd (split_sdef_name n) args
+let rec display_term_bracketed = function
+ | te when is_some (decode_string_opt te) ->
+ "\"" ^ (decode_string te) ^ "\""
+ | te when is_some (decode_list_opt (fun x -> x) te) ->
+ let str_list = List.map display_term_bracketed
+ (decode_list (fun x -> x) te) in
+ "["^ (String.concat ", " str_list) ^ "]"
+ | Term (n, _, a) ->
+ let args = List.map display_term_bracketed (Array.to_list a) in
+ display_sd_bracketed (split_sdef_name n) args
+ | Var (n, _, _, a) ->
+ let args = List.map display_term_bracketed (Array.to_list a) in
+ display_sd_bracketed (split_sdef_name n) args
+
(* --- Display terms and types as XML --- *)
let rec display_type_xml = function
@@ -405,18 +465,30 @@
(match (decode_term_opt term) with None -> ""
| Some te -> "@T " ^ (term_to_string te))
| Var (v, d, t, [||]) ->
+ (try
"@V [" ^ v ^ " @: " ^ (type_to_string t) ^
" @: "^ string_of_int (d) ^ " ]"
+ with exn -> Printf.printf "Nontype: %s\n%!"(term_to_string t);
+ raise exn)
| Var (v, d, t, a) ->
+ (try
"@V [" ^ v ^ " @: " ^ (type_to_string t) ^
" @: "^ string_of_int (d) ^ " ] (" ^
(term_array_to_string a) ^ " )"
- (* FIXME: we should print types!!! *)
- | Term (n, tp, [||]) -> n ^ "[ @: " ^ type_array_to_string tp ^ "]"
+ with exn -> Printf.printf "Nontype: %s\n%!"(term_to_string t);
+ raise exn)
+ (* FIXME: we should print types!!! *)
+ | Term (n, tp, [||]) ->
+ (try
+ n ^ "[ @: " ^ type_array_to_string tp ^ "]"
+ with exn -> Printf.printf "Nontype: %s\n%!"(term_to_string tp.(0));
+ raise exn)
| Term (n, tp, a) ->
- n ^ "[ @: " ^ type_array_to_string tp ^ "] (" ^ (term_array_to_string a) ^ " )"
+ (try
+ n ^ "[ @: " ^ type_array_to_string tp ^ "] (" ^ (term_array_to_string a) ^ " )"
+ with exn -> Printf.printf "Nontype: %s\n%!"(term_to_string tp.(0));
+ raise exn)
-
(* Parser for terms. *)
let rec parse_term = function
| (Delim "@`") :: rest ->
Modified: trunk/Toss/Term/Coding.mli
===================================================================
--- trunk/Toss/Term/Coding.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/Coding.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -63,12 +63,18 @@
(** {2 Term Matching} *)
val matches : (string * term) list ref -> term * term -> bool
+(** Application of term substitutions (only flat functional
+ substitutes). Ignoring supertypes. *)
val apply_s : (string * term) list -> term -> term
+(** Application of term substitutions (only flat functional
+ substitutes). Including supertypes. *)
+val apply_st : (string * term) list -> term -> term
(** {2 Term Display, printing and parsing} *)
val display_term : term -> string
+val display_term_bracketed : term -> string
val display_type_xml : term -> string
val display_term_xml : term -> string
Modified: trunk/Toss/Term/ParseArc.ml
===================================================================
--- trunk/Toss/Term/ParseArc.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/ParseArc.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -7,172 +7,189 @@
(* The type of elements created during parsing.
- Tokens come just from lexer and terms are created during parsing.
- Type is kept together with each term not to recalculate it too often. *)
+ Tokens come just from lexer and terms are created during parsing.
+ [term] does not have [substitution] applied. *)
type parser_elem =
| Token of string
- | Typed_term of term * term
+ | PTerm of term * substitution * int (* From [parsed_elems], [cstrn]
+ and [endpos] of {!parser_arc}. *)
(* Print a parser elem. *)
let elem_str = function
| Token s -> "Tok " ^ s
- | Typed_term (tp, te) ->
- "Te " ^ (Coding.term_to_string te) ^ " : " ^ (type_to_string tp)
+ | PTerm (te, subst, endpos) -> (* FIXME perhaps *)
+ "Te " ^ Coding.term_to_string te
-(* The type of incomplete arcs that appear during parsing;
- The last field is the position where the arc begins
- and the elements on the list are in reverse order
- and the field after the syntax definition is the
- unique name generated for this syntax def. *)
-type parser_arc = Arc of syntax_def * string * parser_elem list * int
+(* Incomplete arcs that appear during parsing. [parsed_elems] do not have
+ [cstrn] applied. *)
+type parser_arc = {
+ sd_n : string; (* The parsed definition's unique name. *)
+ sd_res : sdef_result; (* Its supertypes and whether it's
+ a variable. *)
+ rem_elems : syntax_elem list; (* Its remaining elements. *)
+ parsed_elems : parser_elem list; (* Useful elements parsed so far in
+ rev. order (all will be arguments). *)
+ spos : int; (* Start position of the arc. *)
+ endpos : int; (* The current end position of the
+ arc. FIXME: unnecessary? *)
+ cstrn : substitution; (* Constraint for the arc. *)
+}
-
(* --- Extending and closing arcs --- *)
-exception NOT_EXTENDED
-exception NOT_CLOSED
+(* This function takes a parser element and an arc and extends the arc
+ if the next free position in the arc matches the given
+ element. Maching means equality for tokens and inference constraint
+ satisfaction for terms. Throws NOT_EXTENDED if it was impossible
+ to extend the arc.
-(* Checking if a given parser element matches the given position in a syntax
- definition. Maching means equality for tokens and unification possibility
- when a typed term is put against a type. When a typed term is put against
- a constant string in syntax definition then it does not match and if a token
- is put agains a type then it matches only if its type is the string type. *)
-let matches_position elem sd i =
- let sel = syntax_elems_of_sd sd in
- let sd_elem =
- if (length sel < i) then None else Some (nth sel (i-1)) in
- match (sd_elem, elem) with
- | (None, _) -> false
- | (Some (Str s), Token t) -> s = t
- | (Some (Str s), Typed_term (_,te)) -> false
- | (Some (Tp ty), Token tk) -> ty = BuiltinLang.string_tp
- | (Some (Tp ty), Typed_term (t, _)) ->
- let (ty, t as tp) = suffix 0 ty, suffix 1 t in
- try let _ = mgu [] [tp] in true
- with UNIFY -> false
+ When a term is put against a constant string in syntax definition
+ then it does not match and if a token is put against a term then it
+ matches only if it is a string type. Parsing can be seen as
+ performing "algorithm W" style type inference.
+ Note that the remaining elements were originally generated from a
+ syntax definition by freshening the s.d.'s variables. *)
+let extend_arc elem arc =
+ match arc.rem_elems, elem with
+ | [], _ -> None
+ | Str s::rem_elems, Token t ->
+ if s = t
+ then Some {arc with rem_elems; endpos = arc.endpos + 1}
+ else None
+ | Str s::_, PTerm _ -> None
+ | Tp ty::rem_elems, Token tk ->
+ if ty = BuiltinLang.string_tp
+ then Some
+ {arc with rem_elems; endpos = arc.endpos + 1;
+ parsed_elems = elem::arc.parsed_elems}
+ else None
+ | Tp ty::rem_elems, PTerm (t, t_cstrn, t_endpos) ->
+ (* For now (first-order mgu) we assume single type. *)
+ let pty = type_of t in
+ try
+ (* Purely an optimization step. *)
+ precheck_eq ty pty;
+ (*let ty = Term.apply_sb arc.cstrn ty in
+ let pty = Term.apply_sb t_cstrn pty in
+ precheck_eq ty pty;*)
+ (* Combine the constraints so far, and extend them to cover
+ the new parsed element. *)
+ let cstrn = combine_mgu_sb t_cstrn arc.cstrn in
+ let cstrn =
+ mgu cstrn [apply_sb cstrn pty, apply_sb cstrn ty] in
+ Some
+ {arc with rem_elems; parsed_elems = elem::arc.parsed_elems;
+ endpos = t_endpos; cstrn}
+ with UNIFY -> None
-(* This function takes a parser element and an arc and extends
- the arc if the next free position in the syntax definition
- of the arc matches the given element.
- Throws NOT_EXTENDED if it was impossible to extend the arc. *)
-let extend_arc elem = function
- | Arc (sd, n, l, p) ->
- if matches_position elem sd ((length l) + 1) then
- Arc (sd, n, (elem :: l), p)
- else raise NOT_EXTENDED
-
-
(* Extends all the arcs in the given list that can be extended
and removes all other arcs. *)
let extend_arc_list elem arcs =
- let extend_elem arc = try [extend_arc elem arc] with NOT_EXTENDED -> [] in
- flatten (map extend_elem arcs)
+ Aux.map_some (extend_arc elem) arcs
-(* Divides arcs into complete and incomplete looking at the length
- of the syntax definition input list and the list of parsed elements.
- In other words the arc is complete if nothing can be added to it. *)
-let divide_arcs arcs =
- let is_complete = function
- | Arc (SDtype i, _, l, _) -> length i = length l
- | Arc (SDfun (i, _), _, l, _) -> length i = length l
- | Arc (SDvar (i, _), _, l, _) -> length i = length l in
- (filter is_complete arcs, filter (fun a -> not (is_complete a)) arcs)
+(* Divides arcs into completed and incompleted (the arc is completed if
+ nothing can be added to it). *)
+let completed_arcs arcs =
+ List.partition (fun arc -> arc.rem_elems = []) arcs
-(* Closes an arc, also when an arc is full generates a term
- from it so as the syntax definition prescribes and returns this
- element together with the starting position of the arc.
- It is checked if the generated term is well-typed and
- the type is computetd and kept in the resulting parser element.
- Type declarations are given as a list of pairs that gives
- for each term symbol the type of that symbol.
- Throws NOT_CLOSED if closing fails. *)
-let match_of_tok = function
- | (Str _, _) -> []
- | (Tp _, Token s) -> [Coding.code_string s]
- | (Tp _, Typed_term (_, te)) -> [te]
-
-let close_arc type_decls = function
- | Arc (sd, n, l, spos) when (length l = length (syntax_elems_of_sd sd)) ->
- let elems = syntax_elems_of_sd sd in
- let args = flatten (map match_of_tok (combine elems (rev l))) in
- let res_term = (match sd with
- | SDtype _ ->
+(* Closes an arc when it is completed: returns the corresponding term
+ parser element together with the starting position of the arc. *)
+let close_arc arc =
+ let match_of_tok = function
+ | Token s -> Coding.code_string s
+ | PTerm (t,_,_) -> t in (* t_cstrn is part of arc.cstrn *)
+ if arc.rem_elems <> [] then None else
+ let args = rev_map match_of_tok arc.parsed_elems in
+ let res_term = match arc.sd_res with
+ | SD_Term ty when ty = toplevel_type ->
Term (BuiltinLang.term_type_cons_name, [|BuiltinLang.term_type_tp|],
- [|Coding.code_string n;
+ [|Coding.code_string arc.sd_n;
Coding.code_list
[|BuiltinLang.list_tp BuiltinLang.term_type_tp|]
(fun x -> x) args|])
- | SDfun (_,tp) -> Term (n, [|tp|], Array.of_list args)
- | SDvar (_, _) ->
- (match sd_type sd with
- | None -> failwith "variable syntax definition w/o type"
- | Some (ty) -> Var (n, 0, ty, Array.of_list args) )
- ) in
- (try
- let typ = type_of_term type_decls res_term in
- (Typed_term (typ, res_term), spos)
- with NOT_WELL_TYPED _ ->
- raise NOT_CLOSED)
- | _ -> raise NOT_CLOSED
+ | SD_Term tp -> Term (arc.sd_n, tp, Array.of_list args)
+ | SD_Var tp -> Var (arc.sd_n, 0, tp, Array.of_list args) in
+ (* Note that [arc.cstrn] is not applied to [res_term]. *)
+ Some (PTerm (res_term, arc.cstrn, arc.endpos), arc.spos)
-(* Closes all arcs from the given list that can be closed
- and returns the elements together with starting positions. *)
-let close_arc_list type_decls arcs =
- let close_a a = try [close_arc type_decls a] with NOT_CLOSED -> [] in
- flatten (map close_a arcs)
+(* --- Parsing by adding arcs --- *)
+let fresh_suffix = ref 0
+let reset_fresh_count () = fresh_suffix := 0
+let create_arc sdef sd_n spos =
+ let freshen = List.map
+ (function Str _ as e -> e | Tp t -> Tp (suffix !fresh_suffix t)) in
+ let elems, sd_res =
+ match sdef with
+ | SDtype elems -> incr fresh_suffix;
+ freshen elems, SD_Term toplevel_type
+ | SDfun (elems, ty) -> incr fresh_suffix;
+ freshen elems, SD_Term [|suffix !fresh_suffix ty|]
+ | SDvar (elems, ty) ->
+ (* Do not freshen variable types or their argument types --
+ variables are not polymorphic! *)
+ elems, SD_Var ty in
+ {
+ sd_n; spos; sd_res;
+ rem_elems = elems;
+ parsed_elems = [];
+ endpos = spos;
+ cstrn = empty_sb;
+ }
-(* --- Parsing by adding arcs --- *)
-
-(* Parsing proceeds by going from left to right through the list
+(* TODO: clean-up the description.
+ Parsing proceeds by going from left to right through the list
of tokens and extending the incomplete arcs for each position.
We have our constant set of syntax definitions and in each step
we have a list of incomplete arcs ending in all up to this position
and the new parser elements (starting with just the next token).
We gather the secured incomplete arcs for the next position by doing this:
(1) extend all incomplete arcs (also assuming that each syntax definition
- is a new incomplete arc with empty list of parser elems) ending in
- this position with the new token,
+ is a new incomplete arc with empty list of parser elems) ending in
+ this position with the new token,
(2) secure the arcs that were extended and are still incomplete for the
- next step and close all complete arcs generating new parser elems
+ next step and close all complete arcs generating new parser elems
(3) for each new generated parser element look where its arc was
- starting and try extend all incomplete arcs ending there with
- the new element; repeat recursively until no new elements are generated.
- WARINNG: at the end we need to return also the elements. *)
-let rec extend type_decls sdefs arcs_to pos elem =
- let arcs = (map (fun (sd, n) -> Arc (sd,n,[],pos)) sdefs)@ arcs_to.(pos-1) in
- let (complete_arcs, ready_arcs) = divide_arcs (extend_arc_list elem arcs) in
- let new_els = close_arc_list type_decls complete_arcs in
- let res = map (fun (e, s) -> extend type_decls sdefs arcs_to s e) new_els in
+ starting and try extend all incomplete arcs ending there with
+ the new element; repeat recursively until no new elements are generated.
+ WARINNG: at the end we need to return also the elements. *)
+let rec extend sdefs arcs_to pos elem =
+ let arcs =
+ map (fun (n, sd) -> create_arc sd n pos) sdefs @ arcs_to.(pos-1) in
+ let compl_arcs, ready_arcs =
+ completed_arcs (extend_arc_list elem arcs) in
+ let new_els = Aux.map_some close_arc compl_arcs in
+ let res = map (fun (e, spos) -> extend sdefs arcs_to spos e) new_els in
let (res_arcs, res_elems) = List.split ((ready_arcs, new_els) :: res) in
(flatten res_arcs, flatten res_elems)
-let parse_elems type_decls sdefs elems =
+let parse_elems sdefs elems =
let len = length elems in
let arcs_to = Array.make (len + 1) [] in
let parsed_elems = Array.make (len + 1) [] in
let rec update i = if i > len then () else
- let (arcs_i,el_i) = extend type_decls sdefs arcs_to i (nth elems (i-1)) in
+ let (arcs_i,el_i) = extend sdefs arcs_to i (nth elems (i-1)) in
( arcs_to.(i) <- arcs_i; parsed_elems.(i) <- el_i; update (i+1) ) in
- ( update 1; (arcs_to, parsed_elems) )
+ update 1;
+ (arcs_to, parsed_elems)
-let parse_to_array type_decls sdefs_original strs =
+let parse_to_array sdefs_original strs =
let possible_tok = function Tp _ -> true | Str s -> mem s strs in
let possible_sd sd = for_all possible_tok (syntax_elems_of_sd sd) in
- let sdefs = filter (fun (sd, s) -> possible_sd sd) sdefs_original in
- snd (parse_elems type_decls sdefs (map (fun s -> Token s) strs))
+ let sdefs = filter (fun (n, sd) -> possible_sd sd) sdefs_original in
+ snd (parse_elems sdefs (map (fun s -> Token s) strs))
-let parse type_decls sdefs strs =
- let parsed = (parse_to_array type_decls sdefs strs).(length strs) in
- fst (List.split (filter (fun (_, start) -> start = 1) parsed))
+let parse sdefs strs =
+ let parsed = (parse_to_array sdefs strs).(length strs) in
+ map fst (filter (fun (_, start) -> start = 1) parsed)
(* --- Input splitting --- *)
@@ -244,3 +261,12 @@
let res = first_down (split_string_all split_delims_str) in
LOG 1 "%s" (String.concat " " res);
res
+
+(* --- Final parsing --- *)
+let parse_with_sdefs sdefs str =
+ let type_of_pe = function Token _ -> None
+ | PTerm (te, cstrn, _) ->
+ let result = apply_sb cstrn te in
+ Some result in
+ let elems = parse sdefs (split_input_string str) in
+ Aux.map_some type_of_pe elems
Modified: trunk/Toss/Term/ParseArc.mli
===================================================================
--- trunk/Toss/Term/ParseArc.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/ParseArc.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -4,34 +4,52 @@
open Term
open SyntaxDef
-(** Elements used in the parser. *)
+(** The type of elements created during parsing. Tokens come just
+ from lexer and terms are created during parsing. [term] does not
+ have [substitution] applied. *)
type parser_elem =
| Token of string
- | Typed_term of term * Term.term
+ | PTerm of term * substitution * int (** From [parsed_elems], [cstrn]
+ and [endpos] of {!parser_arc}. *)
(** Print a parser elem. *)
val elem_str : parser_elem -> string
-(** Arcs built by the parser. *)
-type parser_arc = Arc of syntax_def * string * parser_elem list * int
+(** Reset the variable suffix count. *)
+val reset_fresh_count : unit -> unit
+(** Incomplete arcs that appear during parsing. [parsed_elems] do not have
+ [cstrn] applied. *)
+type parser_arc = {
+ sd_n : string; (** The parsed definition's unique name. *)
+ sd_res : sdef_result; (** Its supertypes and whether it's
+ a variable. *)
+ rem_elems : syntax_elem list; (** Its remaining elements. *)
+ parsed_elems : parser_elem list; (** Useful elements parsed so far in
+ rev. order (all will be arguments). *)
+ spos : int; (** Start position of the arc. *)
+ endpos : int; (** The current end position of the arc. *)
+ cstrn : substitution; (** Constraint for the arc. *)
+}
+
(** {2 Parsing, done by adding arcs} *)
+val create_arc : syntax_def -> string -> int -> parser_arc
+
(** Extends all the arcs in the given list that can be extended
and removes all other arcs. *)
val extend_arc_list : parser_elem -> parser_arc list -> parser_arc list
-(** Closes all arcs from the given list that can be closed
- and returns the elements together with starting positions. *)
-val close_arc_list : (string, term) Hashtbl.t ->
- parser_arc list -> (parser_elem * int) list
+(** Closes an arc when it is completed: returns the corresponding term
+ parser element together with the starting position of the arc. *)
+val close_arc : parser_arc -> (parser_elem * int) option
+val parse_to_array :
+ (string * syntax_def) list -> string list -> (parser_elem * int) list array
-val parse_to_array : (string, term) Hashtbl.t ->
- (syntax_def * string) list -> string list -> (parser_elem * int) list array
+val parse : (string * syntax_def) list -> string list -> parser_elem list
-val parse : (string, term) Hashtbl.t -> (syntax_def * string) list ->
- string list -> parser_elem list
+val split_input_string : string -> string list
-val split_input_string : string -> string list
+val parse_with_sdefs : (string * syntax_def) list -> string -> term list
Modified: trunk/Toss/Term/ParseArcTest.ml
===================================================================
--- trunk/Toss/Term/ParseArcTest.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/ParseArcTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -20,25 +20,25 @@
let var_x_a_sd = SDvar ([Str "x"], Var ("a",0,top_type_term,[||])) in
let sdefs = [list_cons_sd; list_nil_sd;
boolean_true_sd; boolean_false_sd; var_x_a_sd] in
- let arcs = List.map (fun sd -> Arc (sd, (name_of_sd sd), [], 0)) sdefs in
+ let arcs = List.map (fun sd -> create_arc sd (name_of_sd sd) 0) sdefs in
let var_arc = extend_arc_list (Token "x") arcs in
- let var_closed = fst (List.hd (close_arc_list tps var_arc)) in
- elem_eq "Te @V [Vx @: @? a @: 0 ] : @? a" var_closed;
+ let var_closed = fst (Aux.find_some close_arc var_arc) in
+ elem_eq "Te @V [Vx @: @? a @: 0 ]" var_closed;
let nil_part_arcs = extend_arc_list (Token "[") arcs in
let nil_arc = extend_arc_list (Token "]") nil_part_arcs in
- let nil_closed = fst (List.hd (close_arc_list tps nil_arc)) in
- elem_eq "Te @L[] : T\\?_list (@? a._.5)" nil_closed;
+ let nil_closed = fst (Aux.find_some close_arc nil_arc) in
+ elem_eq "Te @L[]" nil_closed;
let cons_part1_arc = extend_arc_list var_closed arcs in
let cons_part2_arc = extend_arc_list (Token ",") cons_part1_arc in
let cons_arc = extend_arc_list nil_closed cons_part2_arc in
- let cons_closed = fst (List.hd (close_arc_list tps cons_arc)) in
- elem_eq "Te @L[@V [Vx @: @? a @: 0 ]] : T\\?_list (@? a._.6)" cons_closed;
+ let cons_closed = fst (Aux.find_some close_arc cons_arc) in
+ elem_eq "Te @L[@V [Vx @: @? a @: 0 ]]" cons_closed;
let cons_bad_arc = extend_arc_list var_closed cons_part2_arc in
- let cons_bad_closed = close_arc_list tps cons_bad_arc in
+ let cons_bad_closed = Aux.map_some close_arc cons_bad_arc in
assert_equal ~printer:(fun x -> "empty list test") [] cons_bad_closed;
);
@@ -56,16 +56,17 @@
let var_x_a_sd = SDvar ([Str "x"], Var ("a",0,top_type_term,[||])) in
let sdefs_basic = [list_cons_sd; list_nil_sd;
boolean_true_sd; boolean_false_sd; var_x_a_sd] in
- let sdefs = List.map (fun sd -> (sd, name_of_sd sd)) sdefs_basic in
+ let sdefs = List.map (fun sd -> (name_of_sd sd, sd)) sdefs_basic in
let parse_test res l =
- let ls = String.concat ", " (List.map elem_str (parse tps sdefs l)) in
+ let ls = String.concat ", " (List.map elem_str (parse sdefs l)) in
assert_equal ~printer:(fun x -> x) res ls in
- parse_test "Te @V [Vx @: @? a @: 0 ] : @? a" ["x"];
- parse_test "Te @L[@V [Vx @: @? a @: 0 ]] : T\\?_list (@? a._.6)"
+ parse_test "Te @V [Vx @: @? a @: 0 ]" ["x"];
+ parse_test "Te @L[@V [Vx @: @? a @: 0 ]]"
["x"; ","; "["; "]"];
parse_test "" ["x"; ","; "x"];
- parse_test ("Te @L[@V [Vx @: @? a @: 0 ], @V [Vx @: @? a @: 0 ]] : " ^
- "T\\?_list (@? a._.7)") ["x"; ","; "x"; ","; "["; "]"];
+ parse_test
+ ("Te @L[@V [Vx @: @? a @: 0 ], @V [Vx @: @? a @: 0 ]]")
+ ["x"; ","; "x"; ","; "["; "]"];
);
Modified: trunk/Toss/Term/Rewriting.ml
===================================================================
--- trunk/Toss/Term/Rewriting.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/Rewriting.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -33,10 +33,15 @@
(* --- Rewriting with Clash Detection --- *)
+(* For now, rewriting ignores supertypes, which is fast for
+ manipulating only arguments at the bottom level of hierarchy (but
+ reduces the flexibility of "Hierarchical Terms" to providing
+ subtypes for parsing). *)
+
exception NO_MATCH
(* Checking match returning lists to substitute for and detecting clash.
- In documentation this is described as STEP 1.
+ In documentation this is described as STEP 1. (FIXME: docs)
We assume that the rewrite rules are correct and therefore have no
functions on the left side, but we do not check it dynamically here. *)
let check_clash_match (term1, term2) =
@@ -49,7 +54,7 @@
Aux.array_fold_left2 update (false, []) a1 a2
| (Term (n1, _, _), Term (n2, _, [||])) when (n1 = n2) ->
raise NO_MATCH (* used cons vs. functional cons *)
- | (Term (n1, _, a1), Term (n2, _, a2)) when (n1 = n2) ->
+ | (Term (n1, _, _), Term (n2, _, _)) when (n1 = n2) ->
(*Printf.printf "check_clash_match: [1] %s(%d) %s(%d): %a -- %a\n"
n1 (Array.length a1) n2 (Array.length a2)
(Aux.array_fprint (fun o t->output_string o (Coding.term_to_string t))) a1
@@ -75,10 +80,12 @@
raise NO_MATCH (* non-0-arg fun and functional term *)
| _ -> failwith "rewriting not this function"
-(* Merging substitutions according to variable names. *)
+(* Merging substitutions according to variable names. FIXME: perhaps
+ use [Term.combine_mgu_sb], otherwise streamline. *)
let merge_substs substs =
let merged_substs = Aux.collect substs in
- let mkcm b = if List.length b <> 1 then failwith "cm" else snd (List.hd b) in
+ let mkcm b = (* if List.length b <> 1 then failwith "cm" else *)
+ snd (List.hd b) in
let make_cm (a, b) = (false, (a, mkcm b)) in
let (clashes, substs) = List.split (map make_cm merged_substs) in
(exists (fun x -> x) clashes, substs)
@@ -91,7 +98,23 @@
let (clash, substs) = check_clash_match (left, term) in
if clash then term else
let (merge_clash, merged_substs) = merge_substs substs in
- if merge_clash then term else Coding.apply_s merged_substs right
+ if merge_clash then term
+ else
+ let result = Coding.apply_s merged_substs right in
+ (* For now, we copy over the supertypes fro the original, as
+ the old rewriting ignores supertypes. *)
+ match term, result with
+ | Term (_, oldtys, _), Term (n, _, args) ->
+ Term (n, oldtys, args)
+ | Var (_, _, oldty, _), Term (n, _, args) ->
+ Term (n, [|oldty|], args)
+ | Var (_, _, oldty, _), Var (n, d, _, args) ->
+ Var (n, d, oldty, args)
+ | Term (_, [|oldty|], _), Var (n, d, _, args) ->
+ Var (n, d, oldty, args)
+ (* failwith "apply_check_clash: rewriting non-var with var" *)
+ | Term _, Var (n, d, _, args) ->
+ Var (n, d, term, args)
(* The final rewrite function that takes care of function names in terms. *)
let rewrite (Rules (rules)) term =
Modified: trunk/Toss/Term/SyntaxDef.ml
===================================================================
--- trunk/Toss/Term/SyntaxDef.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/SyntaxDef.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -16,6 +16,11 @@
| SDfun of syntax_elem list * term
| SDvar of syntax_elem list * term
+(* Supertypes and whether we define a variable. Minor current and
+ perhaps bigger future use. *)
+type sdef_result =
+ | SD_Term of term array
+ | SD_Var of term
(* --- Basic functions for Syntax Definitions, generating names --- *)
@@ -92,7 +97,7 @@
let func_sd_of_sd sd =
let change = function Tp _ -> [Str "{"; Str "}"] | x -> [x] in
let oldelems = (syntax_elems_of_sd sd) in
- let nelems = List.flatten (List.map change oldelems) in
+ let nelems = Aux.concat_map change oldelems in
let (sels, ty) =
if nelems = oldelems then
(Str "{" :: nelems @ [Str "}"], sd_type sd)
@@ -206,7 +211,31 @@
let display_sd syntax args =
display_sd_full syntax (List.map (fun x -> (x, None)) args)
+let rec display_sd_full_bracketed syntax args =
+ let are_common_type c1 c2 = ((Aux.is_digit c1) && (Aux.is_digit c2)) ||
+ ((not (Aux.is_alphanum c1 || c1 = ')' || c1 = ']')) &&
+ (not (Aux.is_alphanum c2 || c2 = '(' || c2 = '['))) ||
+ ((c1 ='(') && (Aux.is_alphanum c2)) || ((c2=')') && (Aux.is_alphanum c1)) ||
+ ((c1 ='[') && (Aux.is_alphanum c2)) || ((c2=']') && (Aux.is_alphanum c1)) ||
+ ((c1 = '(') && (c2 = ')')) || ((c1 = '[') && (c2 = ']')) in
+ let put_space s1 s2 =
+ if (s1 = "" || s2 = "") then s1 ^ s2 else
+ if s2.[0] = ' ' then s1 ^ s2 else
+ if (are_common_type (s1.[(String.length s1) - 1]) (s2.[0])) then
+ s1 ^ s2
+ else s1 ^ " " ^ s2 in
+ match (syntax, args) with
+ | ([], []) -> ""
+ | (Some s :: xs, a) -> put_space s (display_sd_full_bracketed xs a)
+ | (None :: xs, []) -> " {} " ^ (display_sd_full_bracketed xs [])
+ | (None :: xs, (n, _) :: aas) -> "{" ^ n ^"} "^ (display_sd_full_bracketed xs aas)
+ | ([], a) -> " ("^ (String.concat ", " (List.map (fun (s, _) -> s) a)) ^")"
+
+let display_sd_bracketed syntax args =
+ display_sd_full_bracketed syntax (List.map (fun x -> (x, None)) args)
+
+
(* --- Printing Syntax Definitions and Types in our syntax --- *)
let split_sdef_name n =
@@ -347,7 +376,7 @@
String.concat "" (List.map xslt_for_se sels)
-let xslt_template_for_sd_name (sd, name) =
+let xslt_template_for_sd_name (name, sd) =
try
"<xsl:template match=\"*[@class='" ^ make_xml_compatible (name) ^
"']\">" ^ xslt_content_for_sel (syntax_elems_of_sd sd) ^ "</xsl:template>"
Modified: trunk/Toss/Term/SyntaxDef.mli
===================================================================
--- trunk/Toss/Term/SyntaxDef.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/SyntaxDef.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -12,7 +12,13 @@
| SDfun of syntax_elem list * Term.term
| SDvar of syntax_elem list * Term.term
+(** Supertypes and whether we define a variable. Minor current and
+ perhaps bigger future use. *)
+type sdef_result =
+ | SD_Term of Term.term array
+ | SD_Var of Term.term
+
(** {2 Basic functions on Syntax Definitions, generating names} *)
val syntax_elems_of_sd : syntax_def -> syntax_elem list
@@ -29,6 +35,7 @@
val split_sd_name : string -> string option list
val display_sd : string option list -> string list -> string
+val display_sd_bracketed : string option list -> string list -> string
(** {2 Pretty printing Types and Syntax Definitions} *)
@@ -51,4 +58,4 @@
(** {2 XSLT output for Syntax Definitions with names} *)
val make_xml_compatible : string -> string
-val print_xslt : string -> (syntax_def * string) list -> string
+val print_xslt : string -> (string * syntax_def) list -> string
Modified: trunk/Toss/Term/TRS.ml
===================================================================
--- trunk/Toss/Term/TRS.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/TRS.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -13,7 +13,7 @@
names, type declarations, rewrite rules and list of all used names.
For now it also has list of loaded file names to prevent double-loading. *)
type trs = {
- sdefs : (syntax_def * string) list; (* Syntax definitions *)
+ sdefs : (string * syntax_def) list; (* Syntax definitions *)
types : (string, term) Hashtbl.t; (* Types *)
mem : (term TermHashtbl.t); (* Memory used by normalisation *)
rrules : (string, Rewriting.rrules_set) Hashtbl.t; (* Rewriting rules *)
@@ -37,7 +37,7 @@
let tds = match sd_type sd with
| None -> sys.hist
| Some t -> (Hashtbl.add sys.types n t; (n, t) :: sys.hist) in
- let add_sdefs = map (fun sd -> (sd, n)) (sd :: (func_sd_of_sd sd)) in
+ let add_sdefs = map (fun sd -> (n, sd)) (sd :: (func_sd_of_sd sd)) in
{ sys with
sdefs = add_sdefs @ sys.sdefs;
mem = TermHashtbl.create 512;
@@ -68,7 +68,8 @@
let update_on_close_context_term te sys =
match te with
| Term (n, _, [||]) when n = close_context_name ->
- let nsds = filter (function (SDvar _, _) -> false | _-> true) sys.sdefs in
+ reset_fresh_count ();
+ let nsds = filter (function (_, SDvar _) -> false | _-> true) sys.sdefs in
{ sys with sdefs = nsds }
| _ -> sys
@@ -161,9 +162,9 @@
let get_funs_of_sys = get_elems_of_sys 'F'
let get_types_of_sys sys =
- let classes = filter (function (SDtype _, _) -> true | _-> false) sys.sdefs in
+ let classes = filter (function (_,SDtype _) -> true | _-> false) sys.sdefs in
let get_tys sels = filter (function Tp _ -> true | _ -> false) sels in
- let td_of_sd (sd, n) = (n, length (get_tys (syntax_elems_of_sd sd))) in
+ let td_of_sd (n, sd) = (n, length (get_tys (syntax_elems_of_sd sd))) in
map td_of_sd classes
@@ -201,10 +202,7 @@
(* Parse a string using the given system. *)
let parse_with_sys sys str =
- let elems = parse sys.types sys.sdefs (split_input_string str) in
- let type_of_pe = function Token _ -> []
- | Typed_term (_, te) -> [te] in
- flatten (map type_of_pe elems)
+ parse_with_sdefs sys.sdefs str
let is_better sys te1 te2 =
let query = Term (preferred_to_name,[|ternary_truth_value_tp|],
@@ -249,7 +247,7 @@
remove_bracket_duplicates best
let terms_info verb ts =
- let disp t = (display_term t) ^
+ let disp t = (display_term_bracketed t) ^
" [" ^ (term_to_string (normalise_brackets t)) ^ "]" in
if (length ts > 1) then
"Disambiguate " ^ (string_of_int (length ts)) ^ " terms\n" ^
@@ -387,7 +385,10 @@
let path = decode_load_cmd k te in
msg ("Loaded state " ^ path ^ ".") ""
| (te, _) ->
- let ty = type_of_term tydecls te in
+ (* FIXME: at step 4 the "types" will get displayed properly *)
+ let ty = match te with
+ | Var (_, _, ty, _) -> ty
+ | Term (_, tys, _) -> tys.(0) in
if xml_out then
"<trs-result>\n" ^
(display_term_xml te) ^ "\n\n" ^ (display_type_xml ty) ^
@@ -405,7 +406,8 @@
raise (FAILED_PARSE_OR_EXN msg))
| [x] ->
(* FIXME *)
- let te = normalise_with_sys s (Term (preprocess_name, [|Var ("q",0,top_type_term,[||])|], [|x|])) in (
+ let te = normalise_with_sys s
+ (Term (preprocess_name, types_of x, [|x|])) in (
match te with
| Term (te_name, _, [|a|]) when te_name = exception_name ->
let msg = "TRS EXCEPTION:\n" ^ (display_term a) ^ "\n" in
Modified: trunk/Toss/Term/TRS.mli
===================================================================
--- trunk/Toss/Term/TRS.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/TRS.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -5,7 +5,7 @@
type trs
(** Get syntax definitions from a TRS. *)
-val syntax_defs_of_sys : trs -> (syntax_def * string) list
+val syntax_defs_of_sys : trs -> (string * syntax_def) list
(** Get set values (chronologically) from a TRS. *)
val set_vals_of_sys : trs -> (string * Term.term * Term.term) list
Modified: trunk/Toss/Term/TRSTest.ml
===================================================================
--- trunk/Toss/Term/TRSTest.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/TRSTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -19,13 +19,14 @@
let proc sys s =
let o = ref "" in
let print_o str = o := !o ^ str ^ "\n" in
+ ParseArc.reset_fresh_count ();
let (sys1, _, m) = process_with_system "" false sys s false print_o
in (sys1, m, !o) in
let s1 = "function ''new'' syntax definition as syntax definition" in
let (sys1, m, _) = proc (basic_system ()) s1 in
assert_equal ~printer:(fun x->x) "New function \"new\" X_1 declared.\n" m;
let (_, m, _) = proc sys1 "[]" in
- assert_equal ~printer:(fun x -> x) "Result: {[] as ?a._.5 list}" m;
+ assert_equal ~printer:(fun x -> x) "Result: {[] as ?a._.4 list}" m;
);
"simple parsing" >::
@@ -97,7 +98,7 @@
);
if (not (!grammar_path = "")) then (
let grammar_str =
- let sys_sdefs = fst (List.split (syntax_defs_of_sys !sys)) in
+ let sys_sdefs = List.map snd (syntax_defs_of_sys !sys) in
print_grammar (flat_grammar_of_sd_list (sys_sdefs)) in
AuxIO.output_file ~fname:!grammar_path grammar_str
);
Modified: trunk/Toss/Term/Term.ml
===================================================================
--- trunk/Toss/Term/Term.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/Term.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -192,21 +192,48 @@
Thanks to F. Baader and T. Nipkow for the book "Term Rewriting and
all That" where the algorithm is explained and similar code is
- given. *)
+ given.
+ When doing first-order operations, we cannot check for
+ well-formedness of substitution, i.e. "typecheck" the
+ variables. *)
+
(* Just an alias for term types substitutions. *)
type substitution = (string * term) list
+let empty_sb = []
+
(* Exists funciton for arrays. *)
let exists f ar = Aux.array_existsi (fun _ e -> f e) ar
+let assoc_sb = List.assoc
+
(* Application of substitutions. *)
-let rec apply subst tp =
+let rec apply_sb subst tp =
match tp with
- | Var (n, _, _, _) as var ->
- (try List.assoc n subst with Not_found -> var)
- | Term (n, t, a) -> Term (n, map (apply subst) t, map (apply subst) a)
+ | Var (n, d, ty, [||]) ->
+ (try List.assoc n subst with Not_found ->
+ Var (n, d, apply_sb subst ty, [||]))
+ | Var (n, d, ty, a) ->
+ (try
+ match List.assoc n subst with
+ | Term (name, tps, [||]) ->
+ Term (name, tps, map (apply_sb subst) a)
+ | Var (name, d, ty, [||]) ->
+ Var (name, d, ty, map (apply_sb subst) a)
+ | _ -> failwith
+ "apply_sb: functional substitution of non-flat term"
+ with Not_found ->
+ Var (n, d, apply_sb subst ty, map (apply_sb subst) a))
+ | Term (n, t, a) ->
+ Term (n, map (apply_sb subst) t, map (apply_sb subst) a)
+let compose_sb s1 s2 =
+ let rec aux = function
+ | [] -> s1
+ | (x, t)::tl -> (x, apply_sb s1 t) :: aux tl in
+ aux s2
+
exception UNIFY
(* The combine function makes a list of pairs from a pair of arrays. *)
@@ -218,6 +245,21 @@
| [] -> raise UNIFY
| hd::tl -> try f hd with UNIFY -> find_unify f tl
+let rec precheck_eq te1 te2 =
+ match te1, te2 with
+ | Term (_, t1, a1), Term (_, t2, a2)
+ when Array.length t1 <> Array.length t2 ||
+ Array.length a1 <> Array.length a2 -> raise UNIFY
+ | Term (n1, t1, a1), Term (n2, t2, a2) when n1 == n2 ->
+ Aux.array_iter2 precheck_eq t1 t2;
+ Aux.array_iter2 precheck_eq a1 a2
+ | Term (n1, t1, a1), Term (n2, t2, a2) when n1 <> n2 ->
+ raise UNIFY
+ | Term (n1, t1, a1), Term (n2, t2, a2) (*when n1 = n2*) ->
+ Aux.array_iter2 precheck_eq t1 t2;
+ Aux.array_iter2 precheck_eq a1 a2
+ | _ -> () (* variable on either side *)
+
(** Returns the matching: [eq_match [] (p,q)] is a well-formed
substitution [r] such that [r(p)=q]. *)
let rec eq_match subst = function
@@ -233,10 +275,7 @@
(try if List.assoc v subst = tp then eq_match subst tps
else raise UNIFY
with Not_found ->
- let subst = (v,tp)::subst in
- let subst = find_unify (eq_match subst)
- (List.map (fun t' -> [t, t']) (tp::to_list t')) in
- eq_match subst tps)
+ eq_match ((v,tp)::subst) tps)
(* for higher-order variable, we do a head-term matching *)
| (Var (v, _, t, a), (Var (_, _, t', a') as tp)) :: tps ->
(try if List.assoc v subst = tp then eq_match subst tps
@@ -248,10 +287,8 @@
(try if List.assoc v subst = tp then eq_match subst tps
else raise UNIFY
with Not_found ->
- let subst = (v,tp)::subst in
- let subst = find_unify (eq_match subst)
- (List.map (fun t' -> [t, t']) (tp::to_list t')) in
- eq_match subst (combine a a' @ tps))
+ (* *)
+ eq_match ((v,tp)::subst) (combine a a' @ tps))
| (_, (Var _)) :: _ -> raise UNIFY
| (Term (f, t, a), Term (g, t', a')) :: tps ->
if f = g
@@ -272,18 +309,12 @@
| (t,t')::tps when t = t' -> mgu subst tps
| (Var (v, _, t, [||]), (Var (_, _, t', _) as tp)) :: tps ->
elim v tp ((t,t') :: tps) subst
- | (Var (v, _, t, [||]), (Term (_, t', _) as tp)) :: tps ->
- (* checking one level of [tp ISA var] *)
- let subst = find_unify (mgu subst)
- (List.map (fun t' -> [t, t']) (tp::to_list t')) in
+ | (Var (v, _, _, [||]), (Term _ as tp)) :: tps ->
elim v tp tps subst
(* for higher-order variable, we do a head-term matching *)
| (Var (v, _, t, a), (Var (_, _, t', a') as tp)) :: tps ->
elim v tp ((t,t') :: combine a a' @ tps) subst
- | (Var (v, _, t, a), (Term (_, t', a') as tp)) :: tps ->
- (* checking one level of [tp ISA var] *)
- let subst = find_unify (mgu subst)
- (List.map (fun t' -> [t, t']) (tp::to_list t')) in
+ | (Var (v, _, _, a), (Term (_, _, a') as tp)) :: tps ->
elim v tp (combine a a' @ tps) subst
| (tp, (Var _ as var)) :: tps -> mgu subst ((var, tp) :: tps)
(* [top_type_term] can be bound to a variable, but otherwise we let
@@ -297,11 +328,27 @@
(* occurs check is only needed if we want to avoid cyclic terms *)
if occurs v tp then raise UNIFY
else
- let app = apply [v, tp] in
+ let app = apply_sb [v, tp] in
let new_tps = List.map (fun (t1,t2) -> app t1, app t2) tps in
let new_subst = (v, tp) :: List.map (fun (n, ty) -> n, app ty) subst in
mgu new_subst new_tps
+let combine_mgu_sb s1 s2 =
+ let eqs, s1 =
+ Aux.partition_map (fun (x, t) ->
+ try Aux.Left (List.assoc x s2, t)
+ with Not_found -> Aux.Right (x, apply_sb s2 t)) s1 in
+ let sb = compose_sb s1 s2 in
+ mgu sb eqs
+
+let type_of = function
+ | Var (_, _, t, _) -> t
+ | Term (_, supt, _) -> supt.(0)
+
+let types_of = function
+ | Var (_, _, t, _) -> [|t|]
+ | Term (_, supt, _) -> supt
+
(** {2 ISA relation operations.} *)
(** Result of comparing two symbols w.r.t. the ISA relation in a
@@ -347,6 +394,7 @@
| Term (n, tp, a) when tp = toplevel_type ->
if (length a = 0) then n else
n ^ " (" ^ (type_array_to_string a) ^ ")"
+ | t when t = top_type_term -> "@U"
| _ -> failwith "non-type term in type_to_string"
@@ -355,7 +403,8 @@
let split_to_list str =
let split_space s = Aux.split_spaces s in
let full_special_split s =
- let l = Aux.split_chars_after '@' ['F';'L';'V';'Y';'T';'`';':';'?'] s in
+ let l = Aux.split_chars_after '@'
+ ['F';'L';'V';'U';'Y';'T';'`';':';'?'] s in
let is_special c = (c = '(') || (c = ')') ||(c = '[') || (c = ']') ||
(c = ',') in
let divide s =
@@ -381,6 +430,8 @@
let rec parse_type = function
| (Aux.Delim "@?") :: (Aux.Text n) :: rest ->
Var (n, 0, top_type_term, [||]), rest
+ | (Aux.Delim "@U") :: rest ->
+ top_type_term, rest
| (Aux.Delim "@F") :: rest ->
(match parse_list rest with
| ([], cont) -> failwith "Function w/o return type."
@@ -410,50 +461,11 @@
let (ty, cont) = parse_type (split_to_list s) in
if cont = [] then ty else failwith "type_of_string: incomplete parse"
+let subst_str subst = String.concat ", "
+ (List.map (fun (s, tp) ->
+ s ^ " <- " ^ (type_to_string tp)) subst)
-(* --- Reconstructing the Type of a Term --- *)
-exception NOT_WELL_TYPED of string
-
-let rec type_sack (i, itys) = function
- | Term (n, _, a) ->
- let ((i, uni_sack, ty_decls), arg_tys) = fold_left type_sack (i ,[]) a in
- (match (suffix i (Hashtbl.find ty_decls n), List.rev arg_tys) with
- | (ty, []) -> ((i+1, uni_sack, ty_decls), ty :: itys)
- | (Term (n, tp, arr), rt) when n = fun_type_name && tp = toplevel_type->
- let l = Array.length arr in
- let (at, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
- (try ((i+1, (List.combine (to_list at) rt) @ uni_sack, ty_decls),
- r :: itys)
- with Invalid_argument _-> raise (NOT_WELL_TYPED "type_sack, term,i.a")
- )
- | _ -> raise (NOT_WELL_TYPED "type_sack, term, end")
- )
- | Var (_, code_degree, var_type, a) ->
- let ((i, uni_sack, ty_decls), arg_tys) = fold_left type_sack (i, []) a in
- (* if code_degree = 0 then var_types.(0) else term_tp in *)
- (match var_type, List.rev arg_tys with
- | (ty, []) -> ((i+1, uni_sack, ty_decls), ty :: itys)
- | (Term (n, tp, arr), rt) when n = fun_type_name && tp = toplevel_type->
- let l = Array.length arr in
- let (at, r) = (Array.sub arr 0 (l-1), arr.(l-1)) in
- (try ((i+1, (List.combine (to_list at) rt) @ uni_sack, ty_decls),
- r :: itys)
- with Invalid_argument _-> raise (NOT_WELL_TYPED "type_sack, var, i.a")
- )
- | _ -> raise (NOT_WELL_TYPED "type_sack, var, end")
- )
-
-let type_of_term type_decls te =
- let ((_, sack, _), type_l) = type_sack ((5, [], type_decls), []) te in
- try
- let subst = mgu [] sack in
- match type_l with
- | [ty] -> apply subst ty
- | _ -> raise (NOT_WELL_TYPED "type_of_term, match")
- with UNIFY -> raise (NOT_WELL_TYPED ("type_of_term, unify "))
-
-
(* --- Hashtables for Terms --- *)
module HashableTerm =
Modified: trunk/Toss/Term/Term.mli
===================================================================
--- trunk/Toss/Term/Term.mli 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/Term.mli 2012-06-25 14:30:21 UTC (rev 1733)
@@ -25,20 +25,42 @@
(** List variables in the given term. *)
val vars_in_term : term -> term list
-
val fn_apply : int -> ('a -> 'a) -> 'a -> 'a
(** {2 Type Unification} *)
-(** Just an alias for term types substitutions. *)
-type substitution = (string * term) list
+(** Substitutions are kept abstract to make it easier to evolve term
+ semantics. *)
+type substitution
(** Exception used in unification algorithm on failure. *)
exception UNIFY
-(** Application of substitutions. *)
-val apply : substitution -> term -> term
+(** Operations on substitutions. *)
+val empty_sb : substitution
+(** Find a term corresponding to the name of a variable or raise
+ [Not_found]. *)
+val assoc_sb : string -> substitution -> term
+val apply_sb : substitution -> term -> term
+(** [compose_sb s1 s2] returns [fun x -> s1 (s2 (x))]; usually the domain
+ of[s1] will be disjoint with the domain of [s2]. Order of
+ substitutions matters. *)
+val compose_sb : substitution -> substitution -> substitution
+(** [combine_mgu_sb s1 s2] first-order-unifies the set of equations
+ induced by both substitutions (i.e. the equations [x = t] for
+ [s1(x)=t] or [s2(x)=t]). The order of substitutions does not
+ matter. *)
+val combine_mgu_sb : substitution -> substitution -> substitution
+(** Check whether equality-based matching or unification would
+ fail. Raises [UNIFY]. *)
+val precheck_eq : term -> term -> unit
+
+(** Returns the matching: [eq_match [] (p,q)] is a well-formed
+ substitution [r] such that [r(p)=q]. *)
+val eq_match : substitution -> (term * term) list -> substitution
+
+
(** Returns the Most General Unifier substitution, throws [UNIFY] if
impossible.
@@ -46,6 +68,10 @@
different types in a (well-formed) term. *)
val mgu : substitution -> (term * term) list -> substitution
+(** Temporary: assuming a single type of a term. *)
+val type_of : term -> term
+(** Return the supertypes of a term or type of a variable. *)
+val types_of : term -> term array
(** {2 Parsing and Printing Types} *)
@@ -61,6 +87,7 @@
(** Parsing types in internal format from string. *)
val type_of_string : string -> term
+val subst_str : substitution -> string
(** {2 Hashtable for Terms} *)
@@ -88,12 +115,3 @@
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
end
-
-
-(** {2 Type of a Term and its Reconstruction} *)
-
-(** Thrown on failure of type reconstruction. *)
-exception NOT_WELL_TYPED of string
-
-(** Reconstruct the type of a term. *)
-val type_of_term : (string, term) Hashtbl.t -> term -> term
Modified: trunk/Toss/Term/TermTest.ml
===================================================================
--- trunk/Toss/Term/TermTest.ml 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/TermTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
@@ -8,10 +8,8 @@
Term("pies", toplevel_type, [||]) |]) in
let s = Term ("ala", toplevel_type, [| Term("kot", toplevel_type, [||]);
Var("y",0,top_type_term,[||]) |]) in
- let subst_str subst = String.concat ", " (List.map (fun (s, tp) ->
- s ^ " <- " ^ (type_to_string tp)) subst) in
assert_equal ~printer:(fun x -> x) "y <- pies, x <- kot"
- (subst_str (mgu [] [t, s]));
+ (subst_str (mgu empty_sb [t, s]));
);
"split_to_list" >::
Modified: trunk/Toss/Term/tests/short_checks.log
===================================================================
--- trunk/Toss/Term/tests/short_checks.log 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/tests/short_checks.log 2012-06-25 14:30:21 UTC (rev 1733)
@@ -106,16 +106,16 @@
// false or x.
Result: {false or x as boolean}
-New function "f" X_1 declared.
+New function "fooo" X_1 declared.
-// (f x) = x.
-Result: {f x = x as boolean}
-// (f x) = f y.
-Result: {f x = f y as boolean}
+// (fooo x) = x.
+Result: {fooo x = x as boolean}
+// (fooo x) = fooo y.
+Result: {fooo x = fooo y as boolean}
// x = x.
Result: {true as boolean}
-// (f x) = f x.
+// (fooo x) = fooo x.
Result: {true as boolean}
// x = y.
Result: {x = y as boolean}
Modified: trunk/Toss/Term/tests/short_checks.trs
===================================================================
--- trunk/Toss/Term/tests/short_checks.trs 2012-06-22 13:58:16 UTC (rev 1732)
+++ trunk/Toss/Term/tests/short_checks.trs 2012-06-25 14:30:21 UTC (rev 1733)
@@ -79,16 +79,16 @@
// false or x.
false or x.
-New function ''f'' boolean as boolean.
+New function ''fooo'' boolean as boolean.
-// (f x) = x.
-(f x) = x.
-// (f x) = f y.
-(f x) = f y.
+// (fooo x) = x.
+(fooo x) = x.
+// (fooo x) = fooo y.
+(fooo x) = fooo y.
// x = x.
x = x.
-// (f x) = f x.
-(f x) = f x.
+// (fooo x) = fooo x.
+(fooo x) = fooo x.
// x = y.
x = y.
// 1 = 1.
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
