+
+TODO
+
* implementare trasformazione 1 => 0
* gestione priorita'/associativita'
- annotazioni nel livello 1 generato?
- triplicare livelli nella grammatica?
* implementare type-checker per le trasformazioni
* prestazioni trasformazioni 3 => 2 e 2 => 1
-* implementare istanziazione dei magic a livello 1 (2 => 1)
* problema con pattern overlapping per i magic al livello 2
* magic per gestione degli array?
* gestione speciale dei numeri
-* implementare compilazione dei default in 2 => 1 e
- relativa istanziazione
* gestione greedyness dei magic in 2 => 1
* sintassi concreta / prelexing
- studiare/implementare sintassi con ... per i magic fold
+
+DONE
+
+* implementare istanziazione dei magic a livello 1 (2 => 1)
+* implementare compilazione dei default in 2 => 1
+ -> Tue, 07 Jun 2005 17:17:36 +0200 zack
+
open CicNotationPt
-exception Value_not_found of string
-
type value =
| TermValue of term
| StringValue of string
| OptType of value_type
| ListType of value_type
+exception Value_not_found of string
+exception Type_mismatch of string * value_type
+
type declaration = string * value_type
type binding = string * (value_type * value)
type t = (string * (value_type * value)) list
+let lookup env name =
+ try
+ List.assoc name env
+ with Not_found -> raise (Value_not_found name)
+
let lookup_value env name =
try
snd (List.assoc name env)
let remove env name = List.remove_assoc name env
let lookup_term env name =
- match lookup_value env name with
- | TermValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, TermValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let lookup_num env name =
- match lookup_value env name with
- | NumValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, NumValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let lookup_string env name =
- match lookup_value env name with
- | StringValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, StringValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_opt env name =
+ match lookup env name with
+ | _, OptValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_list env name =
+ match lookup env name with
+ | _, ListValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
| _ -> false
let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
+let declarations_of_term p =
+ List.map declaration_of_var (CicNotationUtil.variables_of_term p)
+
+let rec combine decls values =
+ match decls, values with
+ | [], [] -> []
+ | (name, ty) :: decls, v :: values ->
+ (name, (ty, v)) :: (combine decls values)
+ | _ -> assert false
let coalesce_env declarations env_list =
let env0 = List.map list_binding_of_name declarations in
* http://helm.cs.unibo.it/
*)
-exception Value_not_found of string
-
(** {2 Types} *)
type value =
| OptType of value_type
| ListType of value_type
+ (** looked up value not found in environment *)
+exception Value_not_found of string
+
+ (** looked up value has the wrong type
+ * parameters are value name and value type in environment *)
+exception Type_mismatch of string * value_type
+
type declaration = string * value_type
type binding = string * (value_type * value)
type t = binding list
val well_typed: value_type -> value -> bool
val declarations_of_env: t -> declaration list
+val declarations_of_term: CicNotationPt.term -> declaration list
+val combine: declaration list -> value list -> t (** @raise Invalid_argument *)
(** {2 Environment lookup} *)
-val lookup_value: t -> string -> value
-val lookup_num: t -> string -> string
-val lookup_string: t -> string -> string
+val lookup_value: t -> string -> value (** @raise Value_not_found *)
+
+(** lookup_* functions below may raise Value_not_found and Type_mismatch *)
+
val lookup_term: t -> string -> CicNotationPt.term
+val lookup_string: t -> string -> string
+val lookup_num: t -> string -> string
+val lookup_opt: t -> string -> value option
+val lookup_list: t -> string -> value list
val remove: t -> string -> t
open CicNotationEnv
open CicNotationPt
-let meta_names_of term =
+(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
+ * be removes as soon as we believe implementation are equivalent *)
+(* let meta_names_of term =
let rec names = ref [] in
let add_name n =
if List.mem n !names then ()
| _ -> assert false
in
aux term ;
- !names
+ !names *)
let unopt_names names env =
let rec aux acc = function
| Ascription (term, name) -> assert false
and aux_magic env = function
| Default (some_pattern, none_pattern) ->
- (match meta_names_of some_pattern with
+ (match CicNotationUtil.names_of_term some_pattern with
| [] -> assert false (* some pattern must contain at least 1 name *)
| (name :: _) as names ->
(match lookup_value env name with
| Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ List.filter ((<>) acc_name)
+ (CicNotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
| Fold (`Right, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ List.filter ((<>) acc_name)
+ (CicNotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
| Pt.Variable _ -> Variable
| Pt.Magic _
| Pt.Layout _
- | Pt.Literal _ -> assert false
+ | Pt.Literal _ as t ->
+ prerr_endline (CicNotationPp.pp_term t);
+ assert false
| _ -> Constructor
let tag_of_pattern = CicNotationTag.get_tag
let tag_of_term = CicNotationTag.get_tag
| _ -> assert false)
pl tl
- let decls_of_pattern p =
- List.map Env.declaration_of_var (Util.variables_of_term p)
-
let rec compiler rows =
let rows', magic_maps =
List.split
in
magichooser candidates
in
- M.compiler rows match_cb (fun _ -> None)
+ M.compiler rows' match_cb (fun _ -> None)
and compile_magic = function
| Pt.Fold (kind, p_base, names, p_rec) ->
- let p_rec_decls = decls_of_pattern p_rec in
+ let p_rec_decls = Env.declarations_of_term p_rec in
let acc_name = try List.hd names with Failure _ -> assert false in
- let t_magic = [p_base, 0; p_rec, 1] in
- let compiled = compiler t_magic in
+ let compiled = compiler [p_base, 0; p_rec, 1] in
(fun term env ->
let rec aux term =
match compiled term with
| None -> None
| Some (base_env, rec_envl) ->
Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
+ | Pt.Default (p_some, p_none) -> (* p_none can't bound names *)
+ let p_some_decls = Env.declarations_of_term p_some in
+ let none_env = List.map Env.opt_binding_of_name p_some_decls in
+ let compiled = compiler [p_some, 0] in
+ (fun term env ->
+ match compiled term with
+ | None -> Some none_env
+ | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
+ | _ -> assert false)
| _ -> assert false
end
sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
and pp_magic = function
- | List0 (t, sep_opt) -> sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | List1 (t, sep_opt) -> sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | List0 (t, sep_opt) ->
+ sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | List1 (t, sep_opt) ->
+ sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
| Opt t -> sprintf "\\OPT %s" (pp_term t)
- | _ -> failwith "magic not implemented"
+ | Fold (k, p_base, names, p_rec) ->
+ let acc = match names with acc :: _ -> acc | _ -> assert false in
+ sprintf "\\FOLD %s \\[%s\\] \\LAMBDA %s \\[%s\\]"
+ (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec)
+ | Default (p_some, p_none) ->
+ sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none)
+
+and pp_fold_kind = function
+ | `Left -> "left"
+ | `Right -> "right"
and pp_sep_opt = function
| None -> ""
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
-let instantiate21 env pid =
+let instantiate21 env precedence associativity l1 =
prerr_endline "instantiate21";
- let precedence, associativity, l1 =
- try
- Hashtbl.find level1_patterns21 pid
- with Not_found -> assert false
- in
- let rec subst = function
- | Ast.AttributedTerm (_, t) -> subst t
+ let rec subst last_box env = function
+ | Ast.AttributedTerm (_, t) -> subst last_box env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
let ty, value =
* instantiation fail *)
assert (CicNotationEnv.well_typed expected_ty value);
CicNotationEnv.term_of_value value
- | Ast.Magic _ -> assert false (* TO BE IMPLEMENTED *)
+ | Ast.Magic m -> subst_magic last_box env m
| Ast.Literal _ as t -> t
- | Ast.Layout l -> Ast.Layout (subst_layout l)
- | t -> CicNotationUtil.visit_ast subst t
- and subst_layout l = CicNotationUtil.visit_layout subst l in
- subst l1
+ | Ast.Layout l -> Ast.Layout (subst_layout last_box env l)
+ | t -> CicNotationUtil.visit_ast (subst last_box env) t
+ and subst_magic last_box env = function
+ | Ast.List0 (p, sep_opt)
+ | Ast.List1 (p, sep_opt) ->
+ let rec_decls = CicNotationEnv.declarations_of_term p in
+ let rec_values =
+ List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
+ in
+ let values = CicNotationUtil.ncombine rec_values in
+ let sep =
+ match sep_opt with
+ | None -> []
+ | Some l -> [ CicNotationPt.Literal l ]
+ in
+ let rec instantiate_list acc = function
+ | [] -> List.rev acc
+ | value_set :: tl ->
+ let env = CicNotationEnv.combine rec_decls value_set in
+ instantiate_list ([subst last_box env p] @ sep @ acc) tl
+ in
+ let children = instantiate_list [] values in
+ CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+ | Ast.Opt p ->
+ let opt_decls = CicNotationEnv.declarations_of_term p in
+ let env =
+ let rec build_env = function
+ | [] -> []
+ | (name, ty) :: tl ->
+ (* assumption: if one of the value is None then all are *)
+ (match CicNotationEnv.lookup_opt env name with
+ | None -> raise Exit
+ | Some v -> (name, (ty, v)) :: build_env tl)
+ in
+ try build_env opt_decls with Exit -> []
+ in
+ let children =
+ if env = [] then []
+ else [subst last_box env p]
+ in
+ CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+ | _ -> assert false (* impossible *)
+ and subst_layout last_box env l =
+ CicNotationUtil.visit_layout (subst last_box env) l
+ (* TODO ZACK here we need to remember the last box traversed, but
+ * visit_layout is opaque :-((( *)
+ in
+ subst CicNotationPt.H env l1
let rec pp_ast1 term =
let rec pp_value = function
in
match (get_compiled21 ()) term with
| None -> pp_ast0 term pp_ast1
- | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid
+ | Some (env, pid) ->
+ let precedence, associativity, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ instantiate21 (ast_env_of_env env) precedence associativity l1
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
in
visit_ast ~special_k strip_attributes t
+let meta_names_of_term term =
+ let rec names = ref [] in
+ let add_name n =
+ if List.mem n !names then ()
+ else names := n :: !names
+ in
+ let rec aux = function
+ | AttributedTerm (_, term) -> aux term
+ | Appl terms -> List.iter aux terms
+ | Binder (_, _, body) -> aux body
+ | Case (term, indty, outty_opt, patterns) ->
+ aux term ;
+ aux_opt outty_opt ;
+ List.iter aux_branch patterns
+ | LetIn (_, t1, t2) ->
+ aux t1 ;
+ aux t2
+ | LetRec (_, definitions, body) ->
+ List.iter aux_definition definitions ;
+ aux body
+ | Uri (_, Some substs) -> aux_substs substs
+ | Ident (_, Some substs) -> aux_substs substs
+ | Meta (_, substs) -> aux_meta_substs substs
+
+ | Implicit
+ | Ident _
+ | Num _
+ | Sort _
+ | Symbol _
+ | Uri _
+ | UserInput -> ()
+
+ | Magic magic -> aux_magic magic
+ | Variable var -> aux_variable var
+
+ | _ -> assert false
+ and aux_opt = function
+ | Some term -> aux term
+ | None -> ()
+ and aux_capture_var (_, ty_opt) = aux_opt ty_opt
+ and aux_branch (pattern, term) =
+ aux_pattern pattern ;
+ aux term
+ and aux_pattern (head, vars) =
+ List.iter aux_capture_var vars
+ and aux_definition (var, term, i) =
+ aux_capture_var var ;
+ aux term
+ and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
+ and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
+ and aux_variable = function
+ | NumVar name -> add_name name
+ | IdentVar name -> add_name name
+ | TermVar name -> add_name name
+ | FreshVar _ -> ()
+ | Ascription _ -> assert false
+ and aux_magic = function
+ | Default (t1, t2)
+ | Fold (_, t1, _, t2) ->
+ aux t1 ;
+ aux t2
+ | _ -> assert false
+ in
+ aux term ;
+ !names
+
+let rectangular matrix =
+ let columns = Array.length matrix.(0) in
+ try
+ Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix;
+ true
+ with Exit -> false
+
+let ncombine ll =
+ let matrix = Array.of_list (List.map Array.of_list ll) in
+ assert (rectangular matrix);
+ let rows = Array.length matrix in
+ let columns = Array.length matrix.(0) in
+ let lists = ref [] in
+ for j = 0 to columns - 1 do
+ let l = ref [] in
+ for i = 0 to rows - 1 do
+ l := matrix.(i).(j) :: !l
+ done;
+ lists := List.rev !l :: !lists
+ done;
+ List.rev !lists
+
+let string_of_literal = function
+ | `Symbol s
+ | `Keyword s
+ | `Number s -> s
+
val strip_attributes: CicNotationPt.term -> CicNotationPt.term
+ (** generalization of List.combine to n lists *)
+val ncombine: 'a list list -> 'a list list
+
+val string_of_literal: CicNotationPt.literal -> string
+
<helm_registry>
+ <section name="getter">
+ <key name="mode">remote</key>
+ <key name="url">http://mowgli.cs.unibo.it:58081/</key>
+ </section>
+<!--
<section name="getter">
<key name="prefetch">false</key>
<key name="servers">
<key name="cache_dir">/tmp/zack/cache</key>
<key name="maps_dir">/projects/helm/var</key>
<key name="dtd_dir">/projects/helm/xml/dtd</key>
-<!-- <key name="loglevel">180</key> -->
</section>
+-->
</helm_registry>
open Printf
let _ =
- Helm_registry.load_from "test_parser.conf.xml";
- Http_getter.init ()
+ Helm_registry.load_from "test_parser.conf.xml"
+(* Http_getter.init () *)
let _ =
let module P = CicNotationPt in
projects / helm.git / commitdiff