From: Stefano Zacchiroli Date: Tue, 7 Jun 2005 15:18:20 +0000 (+0000) Subject: snapshort X-Git-Tag: PRE_INDEX_1~61 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;p=helm.git snapshort - implemented magic instantiation 2 => 1 - implemented DEFAULT pattern matching compilation 2 => 1 --- diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index f6062ad27..133661397 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -1,15 +1,22 @@ + +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 + diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index 749e9148b..f7f11c46d 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -25,8 +25,6 @@ open CicNotationPt -exception Value_not_found of string - type value = | TermValue of term | StringValue of string @@ -41,10 +39,18 @@ type value_type = | 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) @@ -53,19 +59,29 @@ let lookup_value env name = 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)) @@ -103,6 +119,15 @@ let rec well_typed ty value = | _ -> 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 diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli index 7729caef9..be3f6d52d 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.mli +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -23,8 +23,6 @@ * http://helm.cs.unibo.it/ *) -exception Value_not_found of string - (** {2 Types} *) type value = @@ -41,6 +39,13 @@ type value_type = | 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 @@ -51,13 +56,20 @@ val term_of_value: value -> CicNotationPt.term 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 diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index b200de2ef..10bab9e36 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -26,7 +26,9 @@ 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 () @@ -90,7 +92,7 @@ let meta_names_of term = | _ -> assert false in aux term ; - !names + !names *) let unopt_names names env = let rec aux acc = function @@ -188,7 +190,7 @@ let instantiate_level2 env term = | 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 @@ -202,7 +204,8 @@ let instantiate_level2 env term = | 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 *) @@ -222,7 +225,8 @@ let instantiate_level2 env term = | 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 *) diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index f8f73e66b..08a4617f7 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -187,7 +187,9 @@ struct | 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 @@ -226,9 +228,6 @@ struct | _ -> 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 @@ -273,14 +272,13 @@ struct 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 @@ -301,6 +299,15 @@ struct | 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 diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 4f7989516..bc9f33f51 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -136,10 +136,21 @@ and pp_layout = function 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 -> "" diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 2e2d8c9d4..79316319a 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -221,15 +221,10 @@ let get_compiled32 () = 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 = @@ -242,12 +237,56 @@ let instantiate21 env pid = * 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 @@ -265,7 +304,13 @@ let rec pp_ast1 term = 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 diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 18e04640a..52ac0ab67 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -214,3 +214,96 @@ let rec strip_attributes t = 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 + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 92eaf8e8b..760d95ae9 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -41,3 +41,8 @@ val visit_layout: 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 + diff --git a/helm/ocaml/cic_notation/test_parser.conf.xml b/helm/ocaml/cic_notation/test_parser.conf.xml index ea371f06d..ed7b1152e 100644 --- a/helm/ocaml/cic_notation/test_parser.conf.xml +++ b/helm/ocaml/cic_notation/test_parser.conf.xml @@ -1,4 +1,9 @@ +
+ remote + http://mowgli.cs.unibo.it:58081/ +
+ +--> diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 77135a977..98716ad86 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -26,8 +26,8 @@ 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